Completeness Theorem for Hilbert Proof System Instance 2 and Boolean Interpretations
Jump to navigation
Jump to search
![]() | It has been suggested that this page be renamed. To discuss this page in more detail, feel free to use the talk page. |
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 theorem requires a proof. In particular: This is going to be fun You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
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$