Nested Sequents

TL;DR

This paper develops a systematic proof theory for modal logics using nested sequents, enabling properties like cut-elimination and proof search termination, and extends this to the logic of common knowledge with a new nested sequent system.

Contribution

It introduces nested sequent systems for all normal modal logics and the logic of common knowledge, achieving syntactic cut-elimination and proof-theoretic properties.

Findings

Nested sequents stay within the modal language and have the subformula property.

Soundness, completeness, and cut-elimination are established for the systems.

Nested sequents enable proof search termination and ordinal bounds for proofs.

Abstract

We see how nested sequents, a natural generalisation of hypersequents, allow us to develop a systematic proof theory for modal logics. As opposed to other prominent formalisms, such as the display calculus and labelled sequents, nested sequents stay inside the modal language and allow for proof systems which enjoy the subformula property in the literal sense. In the first part we study a systematic set of nested sequent systems for all normal modal logics formed by some combination of the axioms for seriality, reflexivity, symmetry, transitivity and euclideanness. We establish soundness and completeness and some of their good properties, such as invertibility of all rules, admissibility of the structural rules, termination of proof-search, as well as syntactic cut-elimination. In the second part we study the logic of common knowledge, a modal logic with a fixpoint modality. We look at two infinitary proof systems for this logic: an existing one based on ordinary sequents, for which no syntactic cut-elimination procedure is known, and a new one based on nested sequents. We see how nested sequents, in contrast to ordinary sequents, allow for syntactic cut-elimination and thus allow us to obtain an ordinal upper bound on the length of proofs.