Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

TL;DR

This work addresses the problem of establishing full, constructive correspondences among the main sequent formalisms for Gödel-Löb provability logic, including $GL_{seq}$, $GL_{\infty}$, $GL_{circ}$, $CSGL$, and $G3GL$. It develops a two-stage approach: first restructure tree-hypersequent proofs into end-active form and apply a novel linearization to derive a cut-free linear nested sequent calculus, $LNGL$; then show that LNGL proofs can be normalized into a stage-based form that translates into $GL_{seq}$ and then into $G3GL$, yielding six-way correspondences among the systems. This provides the first constructive mappings between structural (labeled, tree-hypersequent, linear nested) and cyclic sequent systems, enabling cross-formalism transfer of results and potential automation across these formalisms. The framework paves the way for generalizing the linear nested sequent approach to other modal and provability logics by deriving linear nested sequent systems from tree-hypersequent representations.

Abstract

We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb 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é 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ödel-Löb 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.

Figures (3)

• Figure 1: Proof transformations and correspondences between sequent systems for $\mathsf{GL}$.
• Figure 2: Labeled Sequent Calculus $\mathsf{G3GL}$ for $\mathsf{GL}$. The $\Box\mathsf{R}$ rule is subject to a side condition $\dag$, namely, the rule is applicable only if the label $y$ is fresh.
• Figure 3: Admissible rules.

Theorems & Definitions (6)

• Definition 1: Model
• Definition 2: Semantic Clauses
• Definition 3: Labeled Sequent Semantics
• Remark 4
• Remark 5
• Theorem 6: $\mathsf{G3GL}$ Properties Neg05