Intuitionistic Logic @ MCMP 18

Time and location

Wednesday, 12-14room 0.21, Ludwigstraße 31
Thursday 11-12, 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)

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

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

31 Oct. Completeness of IPC for Kripke semantics. Disjunction property.
Material: p. 18 of the lecture notes (excluding the final remarks on finite model property and IQC) and p. 20 (only the first part on the disjunction property)

07 Nov. Finite model property, decidability. p-morphisms.
Material: notes

14 Nov. Tree model property. Negative translation.
Material: notes (up to and excluding the modal translation)

21 Nov. Modal translation. Topological semantics.
Material: second part of the notes for previous class + class notes

28 Nov. Algebraic semantics, Lindenbaum-Tarski algebra.
Material: pp. 30-34 of the lecture notes + class notes

05 Dec. Intermediate logics.
Material: class notes. (Optionally, for the existence of a continuum of intermediate logic, see Section 5 of the lecture notes, in particular 5.3 and 5.4.)

12 Dec. Rieger-Nishimura lattice and ladder.
Material: class notes

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

09 Jan. Negative translation for IQC. 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).

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

23 Jan. Inquisitive logic.
Material: questions as information types

30 Jan. Inquisitive logic and intermediate logics.
Material: inquisitive logic

6 Feb. Final exam.