Document Open Access Logo

A Formal Proof of Modal Completeness for Provability Logic

Authors Marco Maggesi , Cosimo Perini Brogi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.26.pdf
  • Filesize: 0.69 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Automated reasoning
Keywords
  • Provability Logic
  • Higher-Order Logic
  • Mechanized Mathematics
  • HOL Light Theorem Prover

Metrics

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

Abstract

This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation. In particular, we show how we adapted the proof in the Boolos' monograph according to the formal language and tools at hand. The strategy we develop here overcomes the technical difficulty due to the non-compactness of GL, and simplify the implementation. Moreover, it can be applied to other normal modal systems with minimal changes.

Cite As Get BibTex

Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.26

Author Details

Marco Maggesi
  • University of Florence, Italy
Cosimo Perini Brogi
  • University of Genoa, Italy

Funding

  • Maggesi, Marco: Supported by the Italian Ministry of University and Research and by INdAM-GNSAGA.

Supplementary Materials

References

  1. Juan Aguilera and David Fernández-Duque. Strong completeness of provability logic for ordinal spaces. The Journal of Symbolic Logic, 82:608–628, November 2017. URL: https://doi.org/10.1017/jsl.2017.3.
  2. Miëtek Bak. Introspective Kripke models and normalisation by evaluation for the λ^Box-calculus. 7th Workshop on Intuitionistic Modal Logic and Applications (IMLA 2017). https://github.com/mietek/imla2017/blob/master/doc/imla2017.pdf, 2017.
  3. Lev Beklemishev and Albert Visser. Problems in the logic of provability. In Mathematical Problems from Applied Logic I, pages 77-136. Springer, 2006. Google Scholar
  4. Bruno Bentzen. A Henkin-style completeness proof for the modal logic S5. CoRR, abs/1910.01697, 2019. URL: http://arxiv.org/abs/1910.01697.
  5. Patrick Blackburn and Johan Van Benthem. Modal logic: a semantic perspective. In Handbook of modal logic, volume 3, pages 1-84. Elsevier, 2007. Google Scholar
  6. Jasmin Christian Blanchette. Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk). In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, page 1–13, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294087.
  7. George Boolos. The logic of provability. Cambridge university press, 1995. Google Scholar
  8. Alonzo Church. Introduction to Mathematical Logic. Princeton: Princeton University Press, 1956. Google Scholar
  9. B. Jack Copeland. The genesis of possible worlds semantics. Journal of Philosophical logic, 31(2):99-137, 2002. Google Scholar
  10. Melvin Fitting and Richard L Mendelsohn. First-order modal logic, volume 277. Springer Science & Business Media, 2012. Google Scholar
  11. Kurt Gödel. Eine Interpretation des Intuitionistischen Aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums, 4: 39-40, 1933. english translation, with an introductory note by A.S. Troelstra. Kurt Gödel, Collected Works, 1:296-303, 1986. Google Scholar
  12. Robert Goldblatt. Mathematical modal logic: A view of its evolution. In Handbook of the History of Logic, volume 7, pages 1-98. Elsevier, 2006. Google Scholar
  13. Raul Hakli and Sara Negri. Does the deduction theorem fail for modal logic? Synthese, 187(3):849-867, 2012. Google Scholar
  14. John Harrison. The HOL Light Theorem Prover. Web site: URL: https://github.com/jrh13/hol-light.
  15. John Harrison. HOL Light tutorial. http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf, 2017.
  16. David Hilbert and Paul Bernays. Grundlagen der Mathematik, Vol. I (1934), Vol II (1939). Berlin: Springer, 1939. Google Scholar
  17. Joachim Lambek and Philip J. Scott. Introduction to higher-order categorical logic, volume 7. Cambridge University Press, 1988. Google Scholar
  18. Julius Michaelis and Tobias Nipkow. Formalized proof systems for propositional logic. In A. Abel, F. Nordvall Forsberg, and A. Kaposi, editors, 23rd Int. Conf. Types for Proofs and Programs (TYPES 2017), volume 104 of LIPIcs, pages 6:1-6:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  19. Sally Popkorn. First steps in modal logic. Cambridge University Press, 1994. Google Scholar
  20. Natarajan Shankar. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407-434, 1985. Google Scholar
  21. Robert M. Solovay. Provability interpretations of modal logic. Israel journal of mathematics, 25(3-4):287-304, 1976. Google Scholar
  22. Yiming Xu and Michael Norrish. Mechanised modal model theory. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 518-533, Cham, 2020. Springer International Publishing. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact