Announcements
Here is a pdf with a typeset version of the lecture notes. Many thanks to Linda Grohmann, Bendix Kemmann, and Teofilius Virbickas for typing this!!!
The re-sit exam will take place on Friday 14.02, 10-12, at Prof.-Huber-Platz 2(V) Raum Lehrturm-V005 (see LSF for a map).
Time and location
Monday, 16-18, room 0.21, Ludwigstraße 31
Final exam: February 3, 16-18, room 0.21, Ludwigstraße 31
Exercise session
Monday, 11-12, room K.001, Amalienstraße 52 (no exercise session on 14 Oct)
Basic course material
Lecture notes by Nick Bezhanishvili and Dick de Jongh
Program, exercises, and additional material
(will be updated as the course proceeds)
14 Oct. Course introduction. BHK Interpretation.
Material: pp. 3-7 of the notes. Exercises.
21 Oct. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Material: Proof system, Kripke semantics. Exercises.
28 Oct. Completeness of IPC for Kripke semantics. Disjunction property.
Material: Class notes. Exercises.
04 Nov. Finite model property, decidability. p-morphisms.
Material: Class notes. Exercises.
11 Nov. Negative translation, modal translation.
Material: Class notes. Exercises.
18 Nov. Topological semantics.
Material: Class notes. Exercises.
25 Nov. Algebraic semantics, Lindenbaum-Tarski algebra. Frame validity.
Material: pp. 30-34 of the lecture notes. Class notes. Exercises.
02 Dec. Intermediate logics.
Material: Class notes. Exercises.
09 Dec. Rieger-Nishimura lattice and ladder.
Material: Class notes. Exercises.
16 Dec. Intuitionistic first-order logic IQC.
Material: class notes. Exercises.
Optional: Troelstra-vanDalen pp. 35-49, 56-59, and 75-84.
13 Jan. Simply typed lambda calculus.
Material: class notes + Ch. 3 of Sørensen and Urzyczyn
(notice that some of the relevant notions are defined in Chapter 1).
Exercises.
20 Jan. Curry-Howard correspondence.
Material: class notes + Ch. 4 of Sørensen and Urzyczyn
Exercises.
27 Jan. Discussion of practice exam.
03 Feb. Final exam.