Tableau Confutation implies Unsatisfiable

From ProofWiki
Jump to navigation Jump to search

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