A formal proof of modal completeness for provability logic

TL;DR

This paper provides a formalized proof of modal completeness for G"odel-L"ob provability logic (GL) using the HOL Light theorem prover, detailing the implementation, proof strategies, and insights gained from the formalization process.

Contribution

It presents the first formal proof of modal completeness for GL in HOL Light, including the development of specialized proof code and an analysis of formal reasoning techniques.

Findings

Successful formalization of GL completeness in HOL Light

Insights into proof structuring and tool use in theorem proving

Evaluation of the advantages and challenges of formal proof methods

Abstract

This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the topic in an informal setting. Moreover, we propose a reflection on our own experience in using this specific theorem prover for this formalization task, with an analysis of pros and cons of reasoning within and about the formal system for GL we implemented in our code.