Completeness Theorem for Hilbert Proof System Instance 2 and Boolean Interpretations
Jump to navigation
Jump to search
This theorem requires a proof.
This is going to be fun
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof.
 It has been suggested that this article or section be renamed.
|
Theorem
Instance 2 of the Hilbert proof systems is a complete proof system for boolean interpretations.
That is, for every WFF $\mathbf A$:
- $\models_{\mathrm{BI}} \mathbf A$ implies $\vdash_{\mathscr H_2} \mathbf A$
Proof
This is going to be fun
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof.
When this page/section has been completed, {{ProofWanted}} should be removed from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Also see
The Soundness Theorem for Hilbert Proof System Instance 2 and Boolean Interpretations in which it is proved that:
- If $\vdash \mathbf A$ then $\models \mathbf A$.
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous): $\S 4.8$: Completeness: Theorem $14$