Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic

doi:None

Title	Authors

Home

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.

Create an Account Learn More Hide this message

Main content

Home

Menu

Start managing your projects on the OSF today.

Main content

Links to this project

Home

Menu

Add new wiki page

Page permissions have changed

Wiki page deleted

Connected to the collaborative wiki

Connecting to the collaborative wiki

Collaborative wiki is unavailable

Browser unsupported

Start managing your projects on the OSF today.