Inducing Syntactic Cut-Elimination for Indexed Nested Sequents

摘要

The key to the proof-theoretical study of a logic is a cutfree proof calculus. Unfortunately there are many logics of interest lacking suitable proof calculi. The proof formalism of nested sequents was recently generalised to indexed nested sequents in order to yield cutfree proof calculi for extensions of the modal logic K by Geach (Lemmon-Scott) axioms. The proofs of completeness and cut-elimination therein were semantical and intricate. Here we identify a subclass of the labelled sequent formalism and show that it corresponds to the indexed nested sequent formalism. This correspondence is then exploited to induce syntactic proofs for indexed nested sequents using the elegant existing proofs in the labelled sequent formalism. A larger goal of this work is to demonstrate how specialising existing proof-theoretical transformations (adapting these as required to remain within the subclass) is an alternative proof method which can alleviate the need for independent proofs from'scratch' in each formalism. Moreover, such coercion can be used to induce new cutfree calculi. We demonstrate by presenting the first indexed nested sequent calculi for intermediate logics.