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

Tim LyonTim Lyon

Tim Lyon
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
In Jörg Endrullis, Sylvain Schmitz, eds., Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025, volume 326 of LIPIcs, to appear. Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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∞ and GLcirc, Poggiolesi's tree-hypersequent system CSGL, and Negri's labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GLseq, GL∞, 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∞, 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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{L2025,
  author    = {Tim Lyon},
  title     = {Unifying Sequent Systems for G{\"{o}}del-L{\"{o}}b Provability
               Logic via Syntactic Transformations},
  editor    = {J{\"{o}}rg Endrullis and Sylvain Schmitz},
  booktitle = {Proceedings of the 33rd {EACSL} Annual Conference on Computer
               Science Logic 2025},
  series    = {LIPIcs},
  volume    = {326},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2025}
}