Completeness Theorem for Propositional Tableaus and Boolean Interpretations

From ProofWiki
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