Stalnaker's Epistemic Logic in Isabelle/HOL

TL;DR

This paper formalizes the soundness and completeness of Stalnaker's epistemic logic S4.2 for multiple agents within Isabelle/HOL, bridging different semantics and strengthening foundational results.

Contribution

It provides a formal proof of soundness and completeness for S4.2 in Isabelle/HOL, including equivalence of two axiomatizations under different semantics.

Findings

Formalized soundness and completeness of S4.2 in Isabelle/HOL

Proved equivalence of two S4 axiomatizations under different semantics

Strengthened foundational understanding of epistemic logic in proof assistants.

Abstract

The foundations of formal models for epistemic and doxastic logics often rely on certain logical aspects of modal logics such as S4 and S4.2 and their semantics; however, the corresponding mathematical results are often stated in papers or books without including a detailed proof, or a reference to it, that allows the reader to convince themselves about them. We reinforce the foundations of the epistemic logic S4.2 for countably many agents by formalizing its soundness and completeness results for the class of all weakly-directed pre-orders in the proof assistant Isabelle/HOL. This logic corresponds to the knowledge fragment, i.e., the logic for formulas that may only include knowledge modalities in Stalnaker's system for knowledge and belief. Additionally, we formalize the equivalence between two axiomatizations for S4, which are used depending on the type of semantics given to the modal operators, as one is commonly used for the relational semantics, and the other one arises naturally from the topological semantics.