Proof Theory of Modal Logic
Webpage for the ESSLLI2024 course Proof Theory of Modal Logic
This webpage contains material and references for the ESSLLI2024 advanced course Proof Theory of Modal Logic. The course will take place in Week 2 (5-9 August 2024) and consists of five 90-minutes lectures. As course material, we use the slides of the lectures and, possibly, some handouts. The slides of each lecture will contain some exercises that you are encouraged to try to solve!
Table of Contents
Course material
The material will be regularly updated throughout the course.
Lecture 1 - Sequent Calculi
Slides
Slides Lecture 1
The exercises for Lecture 1 can be found within the Slides Lecture 1.
References
- Blackburn, de Rijke and Venema, Modal Logic, Cambridge University Press, 2001.
- Troelstra and Schwichtenberg, Basic proof theory, Cambridge University Press, 2000.
Lecture 2 - Labelled Proof Systems
Slides
Annotated Slides Lecture 2
Exercises Lecture 2
References
- Negri, Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem, Arch. Math. Logic 42, 2003 (doi).
- Negri, Proof analysis beyond geometric theories: from rule systems to systems of rules, Journal of Logic and Computation 26.2, 2016 (doi).
- Negri, Proof analysis in modal logic, Journal of Philosophical Logic 34.5, 2005 (doi).
Lecture 3 - Semantic Completeness of Labelled Calculi
Slides part 1: Semantic Completeness of Labelled Calculi
Annotated Slides Lecture 3 - Includes the correct example
Exercises Lecture 3
Slides part 2: Hypersequent Systems
[not covered, will be part of Lecture 4]
References
- Garg, Genovese, Negri, Countermodels from sequent calculi in multi-modal logics, 27th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2012 (pdf).
- Negri, Kripke completeness revisited, Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to Göran Sundholm, 2009 (pdf).
- Negri, Proofs and Countermodels in Non-Classical Logics, Log. Univers. 8, 25–60, 2014 (doi).
Additional references
- Girlando, Kuznets, Marin, Morales, Strassburger, A Simple Loopcheck for Intuitionistic K, International Workshop on Logic, Language, Information, and Computation. Cham: Springer Nature Switzerland, 2024 (pdf)
Lecture 4 - Hypersequent Systems
Slides - Hypersequent Systems
Slides Lecture 4
The exercises for Lecture 4 can be found within the Slides Lecture 4.
References
- Lellmann, Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science, 656, 2016. 76-105 (pdf).
- Poggiolesi, A cut-free simple sequent calculus for modal logic S5, Review of Symbolic Logic, 2008 (pdf).
Lecture 5 - Nested Sequents and Beyond the S5-cube
Slides
Annotated Slides Lecture 5
The exercises for Lecture 5 can be found within the Slides Lecture 5.
References
- Brünnler, Deep sequent systems for modal logic, Arch. Math. Logic 48, 551–577, 2009 (doi).
- Brünnler, Nested sequents, Habilitationsschrift, Institut für Informatik und angewandte Mathematik Universität Bern, 2010 (arXiv).
- Lellmann, Poggiolesi, Nested Sequents or Tree-hypersequents-A survey Saul Kripke on Modal Logic, 2022 (arXiv).
- Marin, Straßburger, Label-free modular systems for classical and intuitionistic modal logics, Advances in Modal Logic 10, 2014 (pdf)).
Prerequisites
We only assume some basic familiarity with sequent calculus and modal logics. We will briefly introduce both topics, recalling the main notions used throughout the course, in Lecture 1. To learn more about sequent calculus and proof theory, you can attend the introductory course Linear Logic, which will also take place in Week 2 of ESSLLI24.
References
There are several textbooks and resources that introduce modal logics. You could have a look at one of the following:
- The Stanford Encyclopedia entry for “Modal logics” (link).
- van Benthem, Modal logic for open minds, Stanford: Center for the Study of Language and Information, 2010.
- Blackburn, de Rijke and Venema, Modal Logic, Cambridge University Press, 2001 (only the first chapters will be relevant for the course).
For an introduction to proof theory, you can refer to:
- Mancosu, Galvan and Zach, An introduction to proof theory, Oxford University Press, 2021.
- Troelstra and Schwichtenberg, Basic proof theory, Cambridge University Press, 2000 (only chapters 3 and 4 are relevant for the course).
For any question or comment, you can use the ESSLLI discord server, or reach out to us at “tiziano.dalmonte at unibz dot it” and “m.girlando at uva dot nl”.