Mathematical Logic


(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 16 April 2018 (lecture)


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.


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 (to be determined).

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
Werner Saurer