License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.26
URN: urn:nbn:de:0030-drops-139215
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13921/
Maggesi, Marco ;
Perini Brogi, Cosimo
A Formal Proof of Modal Completeness for Provability Logic
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.
BibTeX - Entry
@InProceedings{maggesi_et_al:LIPIcs.ITP.2021.26,
author = {Maggesi, Marco and Perini Brogi, Cosimo},
title = {{A Formal Proof of Modal Completeness for Provability Logic}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13921},
URN = {urn:nbn:de:0030-drops-139215},
doi = {10.4230/LIPIcs.ITP.2021.26},
annote = {Keywords: Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light Theorem Prover}
}
