uva.nl
ILLC

Master of Logic / ILLC

Projects

2nd Semester 2022/23: Proof theory for Modal and Non-Classical Logics

Instructors
Marianna Girlando
ECTS
6
Description

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.

 

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, possible-worlds 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): 551-577.

  • Lellmann, Björn, and Francesca Poggiolesi. "Nested Sequents or Tree-hypersequents-A 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): 507-544. 


Back