Intuitionistic logic (MCMP)

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

(this will be updated as the course proceeds)


16 Oct. Course introduction. BHK Interpretation.
Material: pp. 1-7 of the lecture notes. Exercise sheet 1.


23 Oct. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Material: Proof systemKripke semanticsExercise sheet 2.


30 Oct. Completeness of IPC for Kripke semantics. Disjunction property.
Material: pp. 27-31 and 40-41 of the slides. Exercise sheet 3.


06 Nov. Finite model property, decidability. p-morphisms.
Material: class notes. Exercise sheet 4.


20 Nov. Class canceled due to illness.
Exercise sheet 5.


27 Nov. Relations between IPC and classical propositional and modal logic.
Material: pp. 26 and 41-52 of these slidesExercise sheet 6


04 Dec. Topological and algebraic semantics.
Material: pp. 30-34 of the lecture notesExercise sheet 7.


11 Dec. Lindenbaum-Tarski algebra. Intermediate logics.
Material: class notes. Exercise sheet 8.


08 Jan. Rieger-Nishimura lattice and ladder.
Material: class notes. Exercise sheet 9.


15 Jan. Intuitionistic first-order logic.
Material: Troelstra-vanDalenpp. 35-49,  56-59, and 75-84.
Exercise sheet 10


22 Jan. Completeness of IQC, Heyting arithmetic.
Material: Troelstra-vanDalen, pp. 87-89.
Exercise sheet 11


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).
Exercise sheet 12


05 Feb. More on the Curry-Howard correspondence.
Material: Ch. 4 of the book by Sorensen and Urzyczyn.


26 Feb, 11-13. Final exam.