Soundness Theorem for Semantic Tableaus

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf A$ be a WFF of propositional logic.

Let $T$ be a completed tableau for $\mathbf A$.

Suppose that $T$ is closed.


Then $\mathbf A$ is unsatisfiable for boolean interpretations.


Proof

We will prove inductively the following claim for every node $t$ of $T$:

If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.


By the Semantic Tableau Algorithm, we know this statement to hold for the leaf nodes themselves.

For, a leaf $t$ is marked closed if and only if $\map U t$ contains a complementary pair.

The assertion follows from Set of Literals Satisfiable iff No Complementary Pairs.


Inductively, suppose that all children of a node $t$ satisfy the mentioned condition.

If all descendant leaf nodes of $t$ are marked closed, this evidently holds for the children $t', t''$ of $t$ as well.

Hence by hypothesis, $\map U {t'}$ and $\map U {t''}$ are unsatisfiable.

Let $\mathbf B$ be the WFF used by the Semantic Tableau Algorithm at $t$.

Let $\mathbf B_1, \mathbf B_2$ be the formulas added to $t'$ and $t''$.


First, the case that $\mathbf B$ is an $\alpha$-formula.

Then $t' = t''$, and $\mathbf B$ is semantically equivalent to $\mathbf B_1 \land \mathbf B_2$.

It follows that if:

$v \models_{\mathrm{BI}} \map U t$

for some boolean interpretation $v$, then also:

$v \models_{\mathrm{BI}} \map U {t'}$

which contradicts our hypothesis.

Thus, $\map U t$ is unsatisfiable.


Next, the case that $\mathbf B$ is a $\beta$-formula.

Then $\mathbf B$ is semantically equivalent to $\mathbf B_1 \lor \mathbf B_2$.

It follows that if:

$v \models_{\mathrm{BI}} \map U t$

for some boolean interpretation $v$, then also one of the following must hold:

$v \models_{\mathrm{BI}} \map U {t'}$
$v \models_{\mathrm{BI}} \map U {t''}$

which contradicts our hypothesis.

Thus, $\map U t$ is unsatisfiable.




This proves our claim:

If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.

Applying this claim to the root node of $T$, we obtain the desired result.

$\blacksquare$


Sources