Document Open Access Logo

Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics

Authors Anupam Das, Iris van der Giessen, Sonia Marin

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.22.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Anupam Das
  • University of Birmingham, UK
Iris van der Giessen
  • University of Birmingham, UK
Sonia Marin
  • University of Birmingham, UK

Funding

This work was partially supported by a UKRI Future Leaders Fellowship, "Structure vs Invariants in Proofs", project reference MR/S035540/1.

Acknowledgements

We would like to thank Marianna Girlando and Jan Rooduijn for several valuable discussions on the topic. We particularly thank Marianna for her input during our reading group on intuitionistic modal logic which led to the preliminary ideas on which part of this paper is built.

Cite AsGet BibTex

Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.22

Abstract

We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that ℓIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • provability logic
  • proof theory
  • intuitionistic modal logic
  • cyclic proofs
  • non-wellfounded proofs
  • proof search
  • cut-elimination
  • labelled sequents

Metrics

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

Related Versions

References

  1. Mohammad Ardeshir and Motjaba Mojtahedi. The Σ₁-provability logic of HA. Annals of Pure and Applied Logic, 169(10):997-1043, 2018. Google Scholar
  2. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, volume 62 of LIPIcs, pages 42:1-17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  3. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  4. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8, 2012. Google Scholar
  5. Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal logic, volume 53. Cambridge University Press, 2001. Google Scholar
  6. Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. North-Holland, 2007. Google Scholar
  7. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  8. Ranald Clouston and Rajeev Goré. Sequent calculus in the topos of trees. In Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, pages 133-147. Springer, 2015. Google Scholar
  9. Anupam Das. On the logical complexity of cyclic arithmetic. Logical Methods in Computer Science, 16, 2020. Google Scholar
  10. Anupam Das and Sonia Marin. Brouwer meets Kripke: constructivising modal logic, 2022. Post on The Proof Theory Blog (accessed 2 August 2023). URL: https://prooftheory.blog/2022/08/19/brouwer-meets-kripke-constructivising-modal-logic/.
  11. Anupam Das and Sonia Marin. On intuitionistic diamonds (and lack thereof). In Automated Reasoning with Analytic Tableaux and Related Methods, volume 14278 of Lecture Notes in Computer Science, pages 283-301. Springer, 2023. Google Scholar
  12. Anupam Das and Damien Pous. Non-wellfounded proof theory for (Kleene+Action) (Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, volume 119 of LIPIcs, pages 19:1-19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  13. Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic gödel-löb logic, à la simpson: labelled systems and birelational semantics, 2023. URL: https://arxiv.org/abs/2309.00532.
  14. Gisèle Fischer Servi. On modal logic with an intuitionistic base. Studia Logica, 36:141-149, 1977. Google Scholar
  15. Iris van der Giessen. Uniform Interpolation and Admissible Rules: Proof-theoretic investigations into (intuitionistic) modal logics. PhD thesis, Utrecht University, 2022. Google Scholar
  16. Iris van der Giessen and Rosalie Iemhoff. Sequent calculi for intuitionistic Gödel–Löb logic. Notre Dame Journal of Formal Logic, 62(2):221-246, 2021. Google Scholar
  17. Rajeev Goré and Revantha Ramanayake. Valentini’s cut-elimination for provability logic resolved. In Carlos Areces and Robert Goldblatt, editors, Proceedings of the 7th conference on Advances in Modal Logic, pages 67-86. College Publications, 2008. Google Scholar
  18. Rajeev Goré and Ian Shillito. Direct elimination of additive-cuts in GL4ip: verified and extracted. In Advances in Modal Logic 14, 2022. Google Scholar
  19. Leo Harrington. Analytic determinacy and 0^#. The Journal of Symbolic Logic, 43(4):685-693, 1978. URL: https://doi.org/10.2307/2273508.
  20. Rosalie Iemhoff. Reasoning in circles. In Jan van Eijck, Joost J. Joosten, and Rosalie Iemhoff, editors, Liber Amicorum Alberti. A Tribute to Albert Visser, pages 165-178. College Publications, 2016. Google Scholar
  21. G. Alex Kavvos. Intensionality, intensional recursion and the Gödel-Löb axiom. FLAP, 8(8):2287-2312, 2021. Google Scholar
  22. Daniel Leivant. On the proof theory of the modal logic for arithmetic provability. The Journal of Symbolic Logic, 46(3):531-538, 1981. Google Scholar
  23. Tadeusz Litak. Constructive modalities with provability smack. In Guram Bezhanishvili, editor, Leo Esakia on Duality in Modal and Intuitionistic Logics, volume 4 of Outstanding Contributions to Logic, pages 187-216. Springer Netherlands, 2014. Google Scholar
  24. Anders Moen. The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate. In The 13th Nordic Workshop in Programming Theory, 2001. Google Scholar
  25. Mojtaba Mojtahedi. On provability logic of HA, 2022. URL: https://doi.org/10.48550/arXiv.2206.00445.
  26. Hiroshi Nakano. A modality for recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), pages 255-266. IEEE, 2000. Google Scholar
  27. Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34:507-544, 2005. Google Scholar
  28. Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1-2):99-116, 1996. Google Scholar
  29. Gordon Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pages 399-406, 1986. Google Scholar
  30. 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. Google Scholar
  31. Katsumi Sasaki. Löb’s axiom and cut-elimination theorem. Academia Mathematical Sciences and Information Engineering Nanzan University, 1:91-98, 2001. Google Scholar
  32. Krister Segerberg. Results in non-classical propositional logic. Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet., 1971. Google Scholar
  33. Daniyar S. Shamkanov. Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96:575-585, 2014. Google Scholar
  34. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994. Google Scholar
  35. Alex K. Simpson. Cyclic arithmetic is equivalent to Peano arithmetic. In Foundations of Software Science and Computation Structures Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. Google Scholar
  36. Robert M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25:287-304, 1976. Google Scholar
  37. Gaisi Takeuti. Proof Theory. New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co., 1975. Google Scholar
  38. Silvio Valentini. The modal logic of provability: cut-elimination. Journal of Philosophical logic, pages 471-476, 1983. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact