Main content



Loading wiki pages...

Wiki Version:
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.
This website relies on cookies to help provide a better user experience. By clicking Accept or continuing to use the site, you agree. For more information, see our Privacy Policy and information on cookie use.

Start managing your projects on the OSF today.

Free and easy to use, the Open Science Framework supports the entire research lifecycle: planning, execution, reporting, archiving, and discovery.