This webpage contains the slides, handouts and homeowork assignments for the course Proof Theory of Modal Logic, which will take place within the 5th Tsinghua Logic Summer School, organized by the Tsinghua University - University of Amsterdam Joint Research Centre for Logic. The course will take place at the Tsinghua University, from 14th to 18th July 2025.
This course is based on a course taught at ESSLLI2024, prepared in collaboration with Tiziano Dalmonte.
The material will be regularly updated throughout the course.
In this lecture we will introduce Gentzen-style sequent calculus for classical propositional logic, using the proof system G3cpl presented in Section 3.5 of (Troelstra and Schwichtenberg, 2000). We will use the calculus to illustrate the main proof-theoretical properties which we will be focusing on in the course, including invertibility of the rules, cut-admissibility and termination of proof search. We will then (quickly) introduce the classical modal logics in the S5-cube, and discuss the available proof systems for the logics. In particular, we will see that the Gentzen-style formalism is not enough to define cut-free calculi for modal logic. This motivates the introduction to nested and labelled proof systems, which enrich Gentzen-style sequent calculus in different ways.
Slides: Slides Lecture 1, Annotated Slides Lecture 1
Typos: There is a typo in the last slide (exercises), Question 2: the formula is missing a parenthesis. The correct formula is: $ \Box ( p \land (\Box p \rightarrow \bot ) ) \rightarrow \bot $
In this lecture we will focus on nested sequent calculi for modal logics in the S5-cube. Nested sequents enrich the structure of Gentzen-style sequent calculus, by introducing an additional structural connective, intrepreted as Box. Nested sequents encode trees of Gentzen-style sequents and, thanks to their richer structure, constitute a cut-free proof system for modal logic. We will mostly discuss nested sequents for modal logic K and illustrate its main proof-theorerical properties. The presentation of nested seqeunts is based on (Brünnler, 2009).
Slides: Slides Lecture 2, Annotated Slides Lecture 2
Labelled sequent calculi enrich the language of Gentzen-style sequents by introducing labels, which are variables representing worlds of a Kripke model. We will discuss labelled proof systems for modal logics in the S5-cube, and illustrate their main proof-theoretical properties. Following (Negri, 2003), we will see how labelled calculi can be defined for any modal logic whose frame conditions can be expressed by geometric formulas.
Slides: Slides Lecture 3, Annotated Slides Lecture 3
In this lecture, we will consider semantic completeness, that is, the method to prove completeness by constructing a countermodel from a failed proof-search tree. We will illustrate this method for both nested sequents and labelled calculi, which are particularly well-suited to the purpose. As a case study, we will consider the labelled proof system for modal logic K4.
Slides - Slides Lecture 4, Annotated Slides Lecture 4
In this lecture we will show how to define labelled sequent calculi for different kinds of modal logics, demonstrating the flexibility and modularity of the labelled formalism. In particular, we will consider labelled calculi for intuitionistic modal logic, whose semantics is defined in terms of bi-relational models, and and labelled calculi for conditional logic, whose semantics is defined in terms of neighbourood models.
Slides - Slides Lecture 5 (new version)
Each homework will receive a maximum of 10 points, and will amount to 20% of the final grade. Each homework will be published right before the corresponding lecture, and is due right before the next lecture. The take-home exam will amount to 40% of the final grade, and it is due on Sunday 20 June, at 23:59.
Typos: there are two small typos in Homework 3: in Question 1, there is a “\forall x” missing in the frame condition for confluence, and in Question 3, in the statement of the invertibility lemma, “x:A” should be “y:A”. A version of Homework 3 in which both typos have been corrected is here
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. In particular, we will be using versions of G3cpl, the sequent calculus for classical propositional logic presented in Section 3.5 of (Troelstra and Schwichtenberg, 2000).
There are several textbooks and resources that introduce modal logics. You could have a look at one of the following:
For an introduction to proof theory, you can refer to:
On nested sequent calculi:
On labelled sequent calculi: