“Comparing Modal Sequent Systems,” in progress.
Labelled systems and display systems are very different generalisations of the pure sequent calculus, giving what appear to be quite different accounts of modal deduction. Display sequents are equipped with a rich “structural” vocabulary, allowing us to directly express modal facts in the punctuation of a sequent. Labelled sequents encode into the proof theory the structure of a Kripke model. Formulas are equipped with labels (effectively replacing formulas by predicates of worlds) and the accessibility relation from the model makes its appearance in the syntax of the sequent. In this paper, I show how derivations in display logic may be converted into derivations in a labelled sequent system, lending some support to the claim that a labelled sequent system need be no more expressive than a display system. Using this result, we may we may simplify a labelled proof theory further, so that the labels disappear and we are left with a different, structural sequent system for modal logics.