A Henkin-style completeness proof for the modal logic S5

TL;DR

This paper formalizes a Henkin-style completeness proof for the modal logic S5 using the Lean theorem prover, providing a rigorous computer-verified demonstration of the logic's completeness.

Contribution

It offers a formalized, machine-checked proof of S5 completeness in Lean, based on a Mendelson system with specific axioms and inference rules, enhancing rigor and reproducibility.

Findings

Proof formalized in Lean theorem prover

Source code is publicly available and typechecked

Provides a rigorous, machine-verified completeness proof

Abstract

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical connectives and necessity as the only primitive modal operator. The full source code is available online at https://github.com/bbentzen/mpl/ and has been typechecked with Lean 3.4.2.