Completeness Theorem for Propositional Tableaus and Boolean Interpretations
Jump to navigation
Jump to search
Theorem
Tableau proofs (in terms of propositional tableaus) are a complete proof system for boolean interpretations.
That is, for every WFF $\mathbf A$:
- $\models_{\mathrm{BI} } \mathbf A$ implies $\vdash_{\mathrm{PT} } \mathbf A$
Proof
This is a corollary of the Extended Completeness Theorem for Propositional Tableaus and Boolean Interpretations.
Namely, it is the special case $\mathbf H = \O$.
Hence the result.
$\blacksquare$
Also see
The Soundness Theorem for Propositional Tableaus and Boolean Interpretations in which it is proved that:
- If $\vdash \mathbf A$ then $\models \mathbf A$.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.10$: Completeness