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 system. Kripke 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-vanDalen, pp. 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.