Tableau Confutation implies Unsatisfiable
Theorem
Let $\mathbf H$ be a collection of WFFs of propositional logic.
Suppose there exists a tableau confutation of $\mathbf H$.
Then $\mathbf H$ is unsatisfiable for boolean interpretations.
Proof
Let $\left({T, \mathbf H, \Phi}\right)$ be a tableau confutation of $\mathbf H$.
Suppose that $v$ were a boolean interpretation model for $\mathbf H$, i.e.:
- $v \models_{\mathrm{BI}} \mathbf H$
By Model of Root of Propositional Tableau is Model of Branch, it follows that:
- $v \models_{\mathrm{BI}} \Phi \left[{\Gamma}\right]$
for some branch $\Gamma$ of $T$.
Since $T$ is a tableau confutation, there is some WFF $\mathbf A$ such that:
- $\mathbf A, \neg\mathbf A \in \Phi \left[{\Gamma}\right]$
Hence $v \models_{\mathrm{BI}} \mathbf A$, i.e.:
- $v \left({\mathbf A}\right) = T$
But by the truth table for $\neg$, this means:
- $v \left({\neg\mathbf A}\right) = F$
which contradicts that $v \models_{\mathrm{BI}} \neg\mathbf A$.
Hence, no such boolean interpretation can exist.
That is, $\mathbf H$ is unsatisfiable for boolean interpretations.
$\blacksquare$
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.8$: Soundness: Lemma $1.8.2$