2026-07-23T14:20:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13921 2024-03-06T10:53:08Z ddc:004 open_access

A Formal Proof of Modal Completeness for Provability Logic Maggesi, Marco Perini Brogi, Cosimo Provability Logic Higher-Order Logic Mechanized Mathematics HOL Light Theorem Prover 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marco Maggesi and Cosimo Perini Brogi 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.26 urn:nbn:de:0030-drops-139215 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26 eng https://creativecommons.org/licenses/by/4.0/legalcode