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.