Intuitionistic logic (MCMP)

Updates:

notice the change of location for the Monday session.

We will meet in the larger seminar room, 012. Class starts at 12.05.


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.


30 Oct. Completeness of IPC for Kripke semantics. Finite model property, decidability. Unraveling models into trees.


06 Nov. Relations between IPC and classical propositional and modal logic.


20 Nov. Topological and algebraic semantics.


27 Nov. Rieger-Nishimura lattice and ladder. n-universal models.


04 Dec. n-universal models, Diego’s theorem.


11 Dec. Intermediate logics.


08 Jan. Intuitionistic first-order logic.


15 Jan. Heyting arithmetic.


22 Jan. Heyting arithmetic.


29 Jan. Curry-Howard correspondence.


05 Feb. Curry-Howard correspondence.


Catch-up class (date to be fixed). Intuitionistic logic and inquisitive logic.