Intuitionistic logic (MCMP)

Updates: in order to recover the two classes we missed,
since next week the Monday class will last until 14.30.

Time and location

Monday, 12-14.30, 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.


08 Jan. Rieger-Nishimura lattice and ladder. n-universal models.


15 Jan. Intuitionistic first-order logic.


22 Jan. Heyting arithmetic.


29 Feb. Curry-Howard correspondence.


05 Feb. More on the Curry-Howard correspondence.