Lecture 1 - Tuesday 6th June, 11:00 - 13:00, room F1.15, SP107 (notice the room change!)
Labelled calculi for modal logics
Material for Lecture 1 - Slides, Exercises
The following list of references (by no means exaustive) can be used to deeepen the main subjects of the lecture.

• Sequent calculus G3c: Troelstra and Schwichtenberg, Basic proof theory, Cambridge University Press, 2000.
• Modal logics: Blackburn, de Rijke and Venema, Modal Logic, Cambridge University Press, 2001.
• Labelled calculi for the S5-cube: Negri, Proof analysis in modal logic, Journal of Philosophical Logic 34.5, 2005 (pdf)
• Labelled calculi, general method:
  Negri, Contraction-free sequent calculi for geometric theories with an application to Barr's theorem, Arch. Math. Logic 42, 2003 (pdf)
  Negri, Proof analysis beyond geometric theories: from rule systems to systems of rules, Journal of Logic and Computation 26.2, 2014 (pdf)
• Completeness through countermodel construction for labelled sequents: Negri, Proofs and Countermodels in Non-Classical Logics, Log. Univers. 8, 25–60, 2014 (pdf)

Lecture 2 - Thursday 8th June, 13:00 - 15:00, room F1.43, SP107
Nested calculi for modal logics
Material for Lecture 2 - Exercises (there are no slides for lecture 2)
Additional references:

• Overview of various kinds of calculi (including nested sequents): Lellmann, Poggiolesi, Nested Sequents or Tree-hypersequents-A survey Saul Kripke on Modal Logic, 2022 (pdf)
• Nested sequents, as discussed in class: Brünnler, Deep sequent systems for modal logic, Arch. Math. Logic 48, 551–577, 2009 (pdf)
• How to obrain full modularity of nested sequents: Marin, Straßburger, Label-free modular systems for classical and intuitionistic modal logics, Advances in Modal Logic 10, 2014 (pdf)

Lecture 3 - Monday 12th June, 11:00 - 13:00, room F1.15, SP107
Proof systems for intuitionistic logic
Material for Lecture 3 - Slides, Exercises
Additional references:

• Overview of various proof systems for intuitionistic propositional logic: Dyckhoff, Intuitionistic decision procedures since Gentzen, in Advances in Proof Theory. Springer, 2016 (pdf)
• Nested sequents for intuitionistic propositional logic: Fitting, Nested sequents for intuitionistic logics., in Notre Dame Journal of Formal Logic, vol. 55, no 1, 2014.
• Labelled sequent calculus for intuitionistic propositional logic: Dyckhoff, Negri, Proof analysis in intermediate logics, Arch. Math. Logic 51, 71–92, 2012 (pdf)

Lecture 4 - Wednesday 14th June, 11:00 - 13:00, room F1.15, SP107
Proof systems for intuitionistic modal logics
Material for Lecture 4 - Slides, Exercises
Additional references:

• Overview of intuitionistic modal logic IK (and extensions): Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, 1994 (pdf)
• Single-conclusion nested sequents for intuitionistic modal logics: Straßburger, Cut Elimination in Nested Sequents for Intuitionistic Modal Logics, In: Pfenning, (eds) Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol 7794, 2013 (pdf)
• Multi-conclusion nested sequents for intuitionistic modal logics: Kuznets, Straßburger, Maehara-style modal nested calculi, Arch. Math. Logic 58, 359–385, 2019 (pdf)
• Labelled sequents for intuitionistic modal logics: Marin, Morales, Straßburger, A fully labelled proof system for intuitionistic modal logics, Journal of Logic and Computation, Volume 31, Issue 3, 2021, (pdf)

• Termination and countermodel construction for labelled calculi for modal logics. Apply the method described in this paper to some logics in the S5 cube:
  Negri, Proofs and Countermodels in Non-Classical Logics, Log. Univers. 8, 25–60, 2014 (pdf)


• Cut-elimination for nested sequent calculi for modal logics. Give an overview of the proof strategy, fully detailed in this paper:
  Brünnler, Deep sequent systems for modal logic, Arch. Math. Logic 48, 551–577, 2009 (pdf)


• Proof systems for intuitionistic propositional logic. Taking inspiration from the extensive summary below, choose a two or three proof systems and compare them.
  Dyckhoff, Intuitionistic decision procedures since Gentzen, in Advances in Proof Theory. Springer, 2016 (pdf)


• Proof systems for classical and intuitionistic non-normal modal logics. Explore the proof theory of modal logics weaker than modal logic K or their intuitionistic counterpart. Two starting points are:
Dalmonte et al., Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity, Journal of Logic and Computation, Volume 31, Issue 1, 2021 (pdf)
Dalmonte, Grellois, Olivetti, Intuitionistic Non-normal Modal Logics: A General Framework Journal Philosophical Logic 49, 2020 (pdf)

As it is well-known, analytic proof systems for classical and intuitionistic logic can be defined by means of Gentzen-style sequent calculi. However, in the case of modal and non-classical logics, defining a Gentzen-style sequent calculus which is also cut-free complete can be an arduous task. In fact, many logics (e.g. modal logic S5) lack an analytic sequent calculus.

In this project we explore one solution to this problem, which consists in enriching the Gentzen-style formalism. In general, this can be done in two ways: either labels, i.e., variables carrying an explicit semantic information, are added to the language of the calculus, or the structure of the sequent is augmented with new structural connectives. The first approach results in the definition of labelled sequent calculi, while the second approach comprehends a number of "structured" proof systems, including hypersequents and various forms of nested sequents. Other than cut-free completeness, both labelled and structured calculi often offer a high degree of modularity, meaning that proof systems can be uniformly defined for a family of logics (e.g. modal logics) by adding rules to a basic calculus.

The project will mainly focus on labelled and nested sequents. In the first week of the project we will introduce both kinds of calculi, taking the S5-cube of classical modal logics as our case study. In the second week, we will consider intuitionistic logic and intuitionistic modal logics, and we will show how the labelled and nested formalism can be adapted to define cut-free proof systems for these logics. Then, the project consists of a part of individual study, where students can either deepen a subject presented in the lectures (e.g. how does cut-elimination for nested sequents work?) or focus on other kinds of proof systems (e.g., hypersequents, or display calculi). References and a list of possible topics will be provided. Students are also welcome to propose topics depending on their personal interest, as long as they fit the general scope of the project.

An oral presentation or a short written report. Because of participation to a conference, I won't be available in the last week of June and first days of July. Depending on your preferences, you can one of the following options:

• Oral presentation before 23th June
• Oral presentation after 5th July
• Short written report, with deadline on 7th July (tentative)

The oral presentations will be scheduled by the end of the lectures period (first two weeks of the course).

In case of specific constraints or problems with the above schedule, send me and email!

Basic familiarity with modal logic, possible-worlds models, and with sequent calculus for classical propositional logic. If you are interested in the project but do not have the prerequisites, send me an email!