Mechanising G\"odel-L\"ob provability logic in HOL Light

TL;DR

This paper presents a formal implementation in HOL Light of the G"odel-L"ob provability logic, including soundness, completeness, and a decision procedure, with applications demonstrated through examples.

Contribution

It introduces a formalised proof of modal completeness for GL and develops a theorem prover as a HOL Light tactic based on labelled sequent calculus.

Findings

Successfully formalised the modal completeness proof for GL.

Developed a decision algorithm for GL provability.

Demonstrated the theorem prover with interactive and automated examples.

Abstract

We introduce our implementation in HOL Light of the metatheory for G\"odel-L\"ob provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- according to the formal language and tools at hand -- of the proof given in George Boolos' 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness and the design of our proof search algorithm. Furthermore, we propose some examples of the latter's interactive and automated use.