Intuitionistic logic 2019


Here is a pdf with a typeset version of the lecture notes. Many thanks to Linda Grohmann, Bendix Kemmann, and Teofilius Virbickas for typing this!!!

The re-sit exam will take place on Friday 14.02, 10-12, at Prof.-Huber-Platz 2(V) Raum Lehrturm-V005 (see LSF for a map).

Time and location

Monday, 16-18room 0.21, Ludwigstraße 31
Final exam: February 3, 16-18, room 0.21, Ludwigstraße 31

Exercise session

Monday, 11-12, room K.001, Amalienstraße 52 (no exercise session on 14 Oct)

Basic course material

Lecture notes by Nick Bezhanishvili and Dick de Jongh

Program, exercises, and additional material
(will be updated as the course proceeds)

14 Oct. Course introduction. BHK Interpretation.
Material: pp. 3-7 of the notes. Exercises.

21 Oct. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Material: Proof systemKripke semanticsExercises.

28 Oct. Completeness of IPC for Kripke semantics. Disjunction property.
Material: Class notesExercises.

04 Nov. Finite model property, decidability. p-morphisms.
Material: Class notesExercises.

11 Nov. Negative translation, modal translation.
Material: Class notesExercises.

18 Nov. Topological semantics.
Material: Class notesExercises.

25 Nov. Algebraic semantics, Lindenbaum-Tarsky algebra. Frame validity.
Material: pp. 30-34 of the lecture notes. Class notesExercises.

02 Dec.  Intermediate logics.
Material: Class notesExercises.

09 Dec. Rieger-Nishimura lattice and ladder.
Material: Class notesExercises.

16 Dec. Intuitionistic first-order logic IQC.
Material: class notesExercises.
Optional: Troelstra-vanDalen pp. 35-49,  56-59, and 75-84.

13 Jan. Simply typed lambda calculus.
Material: class notes + Ch. 3 of Sørensen and Urzyczyn
(notice that some of the relevant notions are defined in Chapter 1).

20 Jan. Curry-Howard correspondence.
Material: class notes + Ch. 4 of Sørensen and Urzyczyn
ExercisesPractice exam.

27 Jan. Discussion of practice exam. 

03 Feb. Final exam.