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

Author Tim S. Lyon



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.42.pdf
  • Filesize: 0.82 MB
  • 23 pages

Document Identifiers

Author Details

Tim S. Lyon
  • Technische Universität Dresden, Germany

Cite As Get BibTex

Tim S. Lyon. Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.42

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 GL_{seq}, Shamkanov’s non-wellfounded and cyclic sequent systems GL_∞ and GL_{circ}, Poggiolesi’s tree-hypersequent system CSGL, and Negri’s labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GL_{seq}, GL_∞, and GL_{circ}, 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 GL_{seq} and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GL_{seq}, GL_∞, GL_{circ}, 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Constructive mathematics
Keywords
  • Cyclic proof
  • Gödel-Löb logic
  • Labeled sequent
  • Linear nested sequent
  • Modal logic
  • Non-wellfounded proof
  • Proof theory
  • Proof transformation
  • Tree-hypersequent

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  2. Arnon Avron. On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3):935-942, 1984. URL: https://doi.org/10.2307/2274147.
  3. James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 78-92, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11554554_8.
  4. James Brotherston. Formalised inductive reasoning in the logic of bunched implications. In Hanne Riis Nielson and Gilberto Filé, editors, Static Analysis, pages 87-103, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74061-2_6.
  5. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, October 2010. URL: https://doi.org/10.1093/logcom/exq052.
  6. Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551-577, 2009. URL: https://doi.org/10.1007/s00153-009-0137-3.
  7. Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85-100, 1992. URL: https://doi.org/10.1002/MALQ.19920380107.
  8. Marcos A Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281-297, 1997. URL: https://doi.org/10.3233/FI-1997-323404.
  9. Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1-31, 2021. URL: https://doi.org/10.1145/3460492.
  10. Anupam Das and Marianna Girlando. Cyclic hypersequent system for transitive closure logic. Journal of Automated Reasoning, 67(3):27, 2023. URL: https://doi.org/10.1007/s10817-023-09675-1.
  11. Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.22.
  12. Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237-247, 1972. URL: https://doi.org/10.1305/NDJFL/1093894722.
  13. Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41-61, 2014. URL: https://doi.org/10.1215/00294527-2377869.
  14. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43-66. College Publications, 2008. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
  15. Rajeev Goré and Revantha Ramanayake. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 279-299. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Gore-Ramanayake.pdf.
  16. Rajeev Goré and Revantha Ramanayake. Valentini’s cut-elimination for provability logic resolved. The Review of Symbolic Logic, 5(2):212-238, 2012. URL: https://doi.org/10.1017/S1755020311000323.
  17. Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149-164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-73099-6_13.
  18. Stig Kanger. Provability in logic. Almqvist & Wiksell, 1957. Google Scholar
  19. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-135, 1994. URL: https://doi.org/10.1007/BF01053026.
  20. Roman Kuznets and Björn Lellmann. Interpolation for intermediate logics via hyper- and linear nested sequents. In Guram Bezhanishvili, Giovanna D'Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, pages 473-492. College Publications, 2018. URL: http://www.aiml.net/volumes/volume12/Kuznets-Lellmann.pdf.
  21. Björn Lellmann. Linear nested sequents, 2-sequents and hypersequents. In Hans De Nivelle, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 9323 of Lecture Notes in Computer Science, pages 135-150, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-24312-2_10.
  22. Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213-265, December 2020. URL: https://doi.org/10.1093/logcom/exaa078.
  23. Tim Lyon. Refining labelled systems for modal and constructive logics with applications. PhD thesis, TU Wien, 2021. URL: https://arxiv.org/abs/2107.14487,
  24. Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.28.
  25. Tim S. Lyon. Nested sequents for intuitionistic modal logics via structural refinement. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 409-427, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-86059-2_24.
  26. Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, and Revantha Ramanayake. Internal and external calculi: Ordering the jungle without being lost in translations. Found on arXiv, 2023. URL: https://arxiv.org/abs/2312.03426, URL: https://doi.org/10.48550/arXiv.2312.03426.
  27. Tim S. Lyon and Eugenio Orlandelli. Nested sequents for quantified modal logics. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 449-467, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-43513-3_24.
  28. Tim S. Lyon and Piotr Ostropolski-Nalewaja. Foundations for an abstract proof theory in the context of horn rules. Found on arXiv, 2024. URL: https://arxiv.org/abs/2304.05697, URL: https://doi.org/10.48550/arXiv.2304.05697.
  29. Andrea Masini. 2-sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58(3):229-246, 1992. URL: https://doi.org/10.1016/0168-0072(92)90029-Y.
  30. Andrea Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of Logic and Computation, 3(5):533-562, 1993. URL: https://doi.org/10.1093/LOGCOM/3.5.533.
  31. Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5):507-544, 2005. URL: https://doi.org/10.1007/s10992-005-2267-3.
  32. Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  33. Elaine Pimentel, Revantha Ramanayake, and Björn Lellmann. Sequentialising nested systems. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of Lecture Notes in Computer Science, pages 147-165, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-29026-9_9.
  34. Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors, Towards Mathematical Philosophy, volume 28 of Trends in logic, pages 31-51. Springer, 2009. URL: https://doi.org/10.1007/978-1-4020-9084-4_3.
  35. Francesca Poggiolesi. A purely syntactic and cut-free sequent calculus for the modal logic of provability. The Review of Symbolic Logic, 2(4):593-611, 2009. URL: https://doi.org/10.1017/S1755020309990244.
  36. G. Sambin and S. Valentini. A modal sequent calculus for a fragment of arithmetic. Studia Logica: An International Journal for Symbolic Logic, 39(2/3):245-256, 1980. URL: http://www.jstor.org/stable/20014984.
  37. Giovanni Sambin and Silvio Valentini. The modal logic of provability. the sequential approach. Journal of Philosophical Logic, 11(3):311-342, 1982. URL: http://www.jstor.org/stable/30226252, URL: https://doi.org/10.1007/BF00293433.
  38. Krister Segerberg. An Essay in Classical Modal Logic. Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet, 1971. Google Scholar
  39. D. S. Shamkanov. Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96(3):575-585, 2014. URL: https://doi.org/10.1134/S0001434614090326.
  40. Alex K Simpson. The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994. Google Scholar
  41. Robert M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25(3):287-304, 1976. URL: https://doi.org/10.1007/BF02757006.
  42. Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, volume 7794 of Lecture Notes in Computer Science, pages 209-224, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-37075-5_14.
  43. Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail