Time and location
Wednesdays, 15-17, room B0.203
Thursdays, 15-17, room G0.18A
Basic course material
Lecture notes by Nick Bezhanishvili and Dick de Jongh
Slides by Dick de Jongh
Teaching assistant
Assessment
Weekly assignments and a final exam. Exercises are assigned on Thursdays, and solutions should be handed in before the following class on Wednesday, either in person or by email to Gianluca. Deadlines are strict.
Program, assignments, and additional material
(this will be updated as the course proceeds)
8 Feb. Course introduction. BHK Interpretation.
Teacher: Ivano and Dick
Material: pp. 1-7 of the lecture notes + note on constructive proofs.
9 Feb. Intuitionistic propositional logic IPC: proof system and Kripke semantics.
Teacher: Ivano
Material
15 Feb. Completeness of IPC for Kripke semantics. Finite model property, decidability. Unraveling models into trees.
Teacher: Ivano
Material: pp. 27-33 of the slides.
Supplementary material: some useful intuitionistic equivalences
16 Feb. Relations between IPC and classical propositional and modal logic.
Teacher: Dick
Material: pp. 41-52 of the slides
22 Feb. Topological and algebraic semantics.
Teacher: Ivano
Material: pp. 30-34 + 38-39 (up to Cor. 74) of the lecture notes.
23 Feb. Diego’s theorem. Rieger-Nishimura lattice and ladder.
Teacher: Dick
Material: note on Diego’s theorem + pp. 24-25 and 42-43 of the lecture notes
1 Mar. Intermediate logics.
Teacher: Ivano
Material: class notes.
2 Mar. n-universal models, Jankov formulas.
Teacher: Dick
Material: pp. 92-117 of the slides, pp. 1-7 of paper by deJongh-Yang on n-universal models.
8 Mar. Intuitionistic predicate logic IQC.
Teacher: Ivano
Material: Troelstra-vanDalen, pp. 35-49, 56-59, 75-84 and 87-89
9 Mar. more on n-universal models, Heyting arithmetic
Teacher: Dick
Material: pp. 7-9 + 16-17 of the deJongh-Yang paper, pp. 115-126 of the slides.
P. 10 of the lecture notes.
15 Mar. Completeness of HA for IPC
Teacher: Dick
Material: pp 339-354 of Troelstra, Metamathematical investigations of Intuitionistic Arithmetic and Analysis
16 Mar. Curry-Howard correspondence
Teacher: Ivano
Material: Ch. 3 and 4 of the book by Sorensen and Urzyczyn (excerpt; notice that some of the relevant notions are defined in Chapter 1).
Extra material (optional): Wadler-propositions-as-types
22 Mar. Inquisitive logic, part 1
Teacher: Ivano
Material: sections 1-4 of Questions as Information Types.
23 Mar. Inquisitive logic, part 2
Teacher: Ivano
Material: sections 2-6 of Inquisitive Logic.
29 Mar. Practice and Q&A session.
Teacher: Gianluca
Usual time and room.
30 Mar. Final exam.
Usual time, room SP B0.203
(the room where we usually are on Wednesdays)