Unifying Sequent Systems for G\"odel-L\"ob Provability Logic via Syntactic Transformations

TL;DR

This paper establishes comprehensive proof-theoretic correspondences among various sequent systems for G"odel-L"ob provability logic, introducing a new linear nested sequent calculus and constructive proof mappings.

Contribution

It introduces a novel linearization technique and the first cut-free linear nested sequent calculus LNGL, unifying multiple sequent systems for G"odel-L"ob logic.

Findings

Established full proof-theoretic correspondences among six sequent systems.

Developed a new linearization technique transforming tree-hypersequent proofs.

Constructed the first cut-free linear nested sequent calculus LNGL.

Abstract

We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for G\"odel-L\"ob provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic sequent systems GL$\infty$ and GLcirc, Poggiolesi's tree-hypersequent system CSGL, and Negri's labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GLseq, GL$\infty$, and GLcirc, and Gor\'e and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for G\"odel-L\"ob provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GLseq and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GLseq, GL$\infty$, GLcirc, CSGL, G3GL, and LNGL while also giving (to the best of the author's knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.