1st Semester 2005/06: Intuitionistic Logic

Instructors

Nick Bezhanishvili

If you are interested in this project, please contact the instructor by e-mail.

ECTS

6

Description

Goal. Become familiar with Kripke and algebraic semantics of intuitionistic logic and the connections between intuitionistic logic and modal logic. Learn the construction of universal models and the technique of frame-based formulas.

This project is intended to give an overview of the intuitionistic propositional calculus IPC. The following topics will be covered in the course:

• The BHK (Brouwer-Heyting-Kolmogorov) interpretation
• Proof systems (Hilbert type systems, natural deduction, sequent systems)
• Kripke semantics, completeness and the finite model property
• Translations of the classical propositional calculus CPC into IPC and of IPC into S4 and other modal logics (i.e., Glivenko's theorem)
• algebraic semantics: Heyting algebras
• Henkin models and universal models of IPC
• Jankov-de Jongh formulas and intermediate logics

Assessment

Grades are based on weekly homework (25%) and a final paper (75%).

References

Nick Bezhanishvili and Dick de Jongh, Intuitionistic Logic, ESSLLI'05 course notes.
A. Chagrov and M. Zakharyaschev, Modal Logic, Oxford University Press, 1997.