Cut-elimination for provability logics and some results in display logic

Abstract

A syntactic proof of cut-elimination yields a procedure to eliminate every instance the cut-rule from a derivation in the sequent calculus thus leading to a cut-free derivation. This is a central result in the proof-theory of a logic. In 1983, Valentini [71] presented a syntactic proof of cut-elimination for the provability logic GL for a traditional Gentzen sequent calculus built from sets, as opposed to multisets, thus avoiding an explicit rule of contraction. From a syntactic point of view it is more satisfying and formal to explicitly identify the applications of the contraction rule that are hidden in such calculi. Recently it has been claimed the cut-elimination procedure does not terminate when applied to the corresponding sequent calculus built from multisets. Here we show how to resolve this issue in order to obtain a syntactic proof of cut-elimination for GL. The logics Grz and Go have a syntactically similar axiomatisation to GL which suggests that it might be possible to extend the proof to these logics. This is borne out by an existing proof for Grz. However, no proof has been presented for Go. We fill this gap in the literature by presenting a proof of syntactic cut-elimination for this logic. The transformations for Go require a deeper analysis of the derivation structures than the proofs for the other logics. Next we examine Kracht's syntactic characterisation for the class of logics that can be presented via cutfree modal and tense display calculi. Recently it has been shown that the characterisation for modal display calculi is incorrect. In this work we significantly extend the class of modal logics that can be presented using cutfree modal display calculi. We utilise this result to give a proof theory for a syntactically-specified class of superintuitionistic logics. Then we take a semantic approach and show how to construct display calculi for superintuitionistic logics specified by suitable frame conditions. Finally, we introduce the natural maps between tree-hypersequent and nested sequent calculi, and a proper subclass of labelled sequent calculi that we call labelled tree sequent calculi. Then we show how to embed certain labelled sequent calculi into the corresponding labelled tree sequent systems. Using the existing soundness and completeness and cut-admissibility results for the labelled sequent calculus G3GL we then obtain the corresponding results for Poggiolesi's [58] tree-hypersequent calculus CSGL, thus alleviating the need for independent proofs and answering a question posed in that paper. Next, we generalise a scheme for obtaining labelled tree sequent rules corresponding to modal axioms and investigate the possibility of using this method to obtain modular cutfree nested sequent systems for a large class of modal logics. Although the general result remains to be proved, we consider some concrete cases and show that the scheme leads to cutfree systems.