Mathematical Logic

(http://www.coli.uni-saarland.de/~saurer/lehre/ml/math-logic.html)


(Diese Seite gibt es auch auf Deutsch.)

Lecture with Exercise Session.
M.Sc. LS&T and LCT
Instructor: Werner Saurer

Lecture: Tue 12:15 - 13:45, Building C 72, Seminar Room 1.12
Exercise Session: Mon 12:15 - 13:45, Building C 72, Seminar Room 1.12

First meeting:  Mon 24 April 2017 (lecture)


Content

Mathematical logic is one of the most important formal tools in computational linguistics, especially - but not only - for semantics. In this intermediate to advanced course in logic we will be largely concerned with metalogical results such as correctness and completeness of logical calculi. We will consider axiom systems for propositional and first order predicate logic and prove that these systems are semantically correct and complete.

Prerequisites

Mathematical Foundations I or good working knowledge of first order predicate logic.

Text book (available in the library)

R. H. Thomason, Symbolic Logic. An Introduction. Macmillan 1970 [T]


  • Position in degree programs

    The course carries 6 credit points (M.Sc.: specialization course in linguistics/computational linguistics). There will be a written exam (90 min) at the end of the semester. (The exact date will be announced in time.) Registration deadline for the exam is Monday, July 24, 2017.

    Exercise session

    There will be a separate exercise session (2h). The beginning will be announced in the first lecture meeting.

  • Course Schedule

  • <>Lecture 1
    Introduction, (uninterpreted) formal systems, an axiom system, informal semantics
    Reading: [T] Chapters I and II

    Lecture 2
    Natural deduction (conditional logic and full propositional logic)
    Reading: [T] Chapters III and IV

    Lecture 3
    Metatheory of propostional logic: syntax; the system Hs, various metatheorems on Hs (M1-M7); significance of  the deduction theorem
    Reading: [T] Chapter V

    Lecture 4
    Proof of the deduction theorem; further metatheorems and definitions; metatheorems and their relation to the rules of natural deduction
    Reading: [T] Chapter V

    Lecture 5
    Replacement and substitution; admissible and derived rules; consistency
    Reading: [T] Chapter V

    Lecture 6
    Semantics for the system Hs. Important semantic definitions and metatheorems. Truth table method, consistency trees, semantic tableaux
    Reading: [T]  Chapter VI

    Lecture 7
    Correctness and completeness of Hs (1)
    Reading: [T] Chapter VII
    <>
    Lecture 8
    Correctness and Completeness of Hs (2); Introduction to predicate logic
    Reading: [T] Chapters VII and VIII

    Lecture 9
    The system Sp= (natural deduction). The axiom system Hp= (proof theory)
    Reading: [T] Chapters IX and X

    Lecture 10
    Semantics of Hp=
    Reading: [T] Chapter XI

    Lecture 11
    Correctness and Completeness of Hp= (1)
    Reading: [T] Chapter XII

    Lecture 12
    Completeness of Hp= (2), adequacy results of Hp=, closing remarks
    Reading: [T] Chapter XII

    Office hours

    Wed 14-15, Building C 72, Room 0.07, Tel. 302-4177
    E-mail Werner Saurer