2nd Semester 2022/23: Proof theory for Modal and NonClassical Logics
 Instructors
 Marianna Girlando
 ECTS
 6
 Description
As it is wellknown, analytic proof systems for classical and intuitionistic logic can be defined by means of Gentzenstyle sequent calculi. However, in the case of modal and nonclassical logics, defining a Gentzenstyle sequent calculus which is also cutfree 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 Gentzenstyle 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 cutfree 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 S5cube 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 cutfree 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 cutelimination 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.
 Organisation
The Project consists of 4 lectures (in presence, with possibility for hybrid attendance if requested), followed by individual study.
Tentative schedule:
Week 1
2 lectures: Labelled calculi for classical modal logics, Nested calculi for classical modal logics
Week 2
2 lectures: Proof systems for intuitionistic logic, Proof systems for intuitionistic modal logics
Week 3
Consultations for individual study / presentations (see Assessment below)
Week 4 / Week 4+1
Individual study / presentations / deadline for short report (see Assessment below)
 Prerequisites
Basic familiarity with modal logic, possibleworlds models, and with sequent calculus for classical propositional logic.
 Assessment
Two homework assignments and, in addition, an oral presentation or a short written report. Because of a conference, the lecturer is away from 23th June to 4th/5th July. Thus, depending on their preferences, students can choose one of the following options:

Oral presentation in Week 3 (before 23th June)

Oral presentation in Week 4+1 (after 4th or 5th July, to be confirmed)

Short written report, with deadline at the end of Week 4+1 (tentative deadline: 7th July)
The oral presentations will be scheduled at the end of Week 2.

 References

Brünnler, Kai. "Deep sequent systems for modal logic." Archive for Mathematical Logic 48.6 (2009): 551577.

Lellmann, Björn, and Francesca Poggiolesi. "Nested Sequents or TreehypersequentsA survey." R. Padro and Yale Weiss eds, Saul Kripke on Modal Logic. Springer (2022).

Negri, Sara. "Proof analysis in modal logic." Journal of Philosophical Logic 34 (2005): 507544.
