We investigate Henkin-style completeness proofs by considering a simple example: an axiomatic proof system with one rule and three axioms for propositional logic. We carry out this task by formalizing the completeness proof in the Isabelle/HOL proof assistant, i.e. by working in the formal language of higher-order logic, with machine support, rather than in natural language. As such, we define everything rigorously: syntax and semantics, the proof system, maximal consistent sets and how to synthesize them, Hintikka sets, model existence and completeness. Our formalization is only one in a long line of formalized completeness results, but one that is particularly simple and exposes the central ideas without much distraction.
OSF does not support the use of Internet Explorer. For optimal performance, please switch to another browser.