Time

Class: Mondays 12-14 and Thursdays 10-12
Exercise sessions: Thursdays and Fridays 9-10
Classes start on 12.04 and end on 27.05

---

Location

The course takes place via Zoom. Login details will be sent via LFS.
If you have not received them by Friday 09.04, please contact me.
Note that in order to log in you need a Zoom account based on an LMU address.

---

Teaching assistant

Ben Kemmann
Email: [email protected]

---

Basic course material

Lecture notes based on the present course (updated as the course proceeds)
Lecture notes by Nick Bezhanishvili and Dick de Jongh
Further materials given below.

---

Assignments

Every week, an exercise sheet will be posted on Thursdays.
We ask you to submit solutions by the following Monday here.
We will then discuss the solutions in class, and Ben will also give you feedback.
NB Your solutions will not be graded. Grade is based on final exam.

---

Assessment

Final exam: Friday 04.06, 14:00-16:30.

---

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

---

12.04. Course introduction. BHK Interpretation.
Material: pp. 6-9 of Troelstra 03 (for more on intuitionism, see here and here)

---

15.04. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Material: Proof system, Kripke semantics.
First exercise sheet. Model solutions.

---

19.04. Completeness of IPC for Kripke semantics. Disjunction property.
Material: Class notes.

---

22.04. Finite model property, decidability. p-morphisms.
Material: Class notes.
Second exercise sheet. Model solutions.

---

26.04. Negative translation, modal translation.
Material: Class notes.

---

29.04. Topological semantics.
Material: Class notes.
Third exercise sheet. Model solutions.

---

03.05. Algebraic semantics.
Material: pp. 30-34 of the Bezhanishvili-de Jongh lecture notes. Class notes.

---

06.05.  Frame validity. Intermediate logics.
Material: Class notes.
Fourth exercise sheet. Model solutions.

---

10.05. Rieger-Nishimura lattice and ladder.
Material: Class notes.
Fifth exercise sheet. Model solutions.

---

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

---

20.05. 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).
Sixth exercise sheet. Model solutions.

---

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