Proof Theory of Modal Logic

While proof systems for classical and intuitionistic logic can be defined using sequent calculus, the Gentzen-style formalism does not readily extend to the case of modal logic. And indeed, Gentzen-style sequents fail to meet basic requirements in the case of several modal logics: for instance, no cut-free sequent calculus is known for logic S5. In order to overcome these difficulties, various proof systems extending Gentzen’s sequent calculus have been introduced. Namely, labelled calculi extend the language of the calculi with semantic information, while structured calculi, such as hypersequents or nested sequents, employ additional structural connectives.

In this course we will introduce labelled and structured proof systems and illustrate their main properties, including cut-freeness and modularity. Other than normal modal logics, we will discuss logics with neighbourhood semantics, such as conditional logics, and intuitionistic modal logics. We will showcase how labelled and structured calculi are suitable to obtain decision procedures for these logics. To conclude, we will compare the various proof systems by defining formal translations allowing to convert proofs from one formalism to another.