Time and location
Monday, 12-14, room 0.21, Ludwigstraße 31
Tuesday 12-13, room 0.28, Ludwigstraße 31
Basic course material
Lecture notes by Nick Bezhanishvili and Dick de Jongh
Program, exercises, and additional material
(will be updated as the course proceeds)
16 Oct. Course introduction. BHK Interpretation.
Material: pp. 1-7 of the lecture notes.
23 Oct. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Material: Proof system. Kripke semantics.
30 Oct. Completeness of IPC for Kripke semantics. Disjunction property.
Material: pp. 27-31 and 40-41 of the slides.
06 Nov. Finite model property, decidability. p-morphisms.
Material: class notes.
20 Nov. Class canceled due to illness.
27 Nov. Relations between IPC and classical propositional and modal logic.
Material: pp. 26 and 41-52 of these slides.
04 Dec. Topological and algebraic semantics.
Material: pp. 30-34 of the lecture notes.
11 Dec. Lindenbaum-Tarski algebra. Intermediate logics.
Material: class notes.
08 Jan. Rieger-Nishimura lattice and ladder.
Material: class notes.
15 Jan. Intuitionistic first-order logic.
Material: Troelstra-vanDalen, pp. 35-49, 56-59, and 75-84.
22 Jan. Completeness of IQC, Heyting arithmetic.
Material: Troelstra-vanDalen, pp. 87-89.
29 Jan. Curry-Howard correspondence.
Material: Ch. 3 of the book by Sorensen and Urzyczyn (excerpt; notice that some of the relevant notions are defined in Chapter 1).
05 Feb. More on the Curry-Howard correspondence.
Material: Ch. 4 of the book by Sorensen and Urzyczyn.