Intuitionistic logic 2017

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 systemKripke 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-vanDalenpp. 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.