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 $U \left({t}\right)$ 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 iff $U \left({t}\right)$ 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, $U \left({t'}\right)$ and $U \left({t''}\right)$ 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}} U \left({t}\right)$

for some boolean interpretation $v$, then also:

$v \models_{\mathrm{BI}} U \left({t'}\right)$

which contradicts our hypothesis.

Thus, $U \left({t}\right)$ 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}} U \left({t}\right)$

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

$v \models_{\mathrm{BI}} U \left({t'}\right)$
$v \models_{\mathrm{BI}} U \left({t''}\right)$

which contradicts our hypothesis.

Thus, $U \left({t}\right)$ is unsatisfiable.


This proves our claim:

If all leaves that are descendants of $t$ are marked closed, then $U \left({t}\right)$ is unsatisfiable.

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

$\blacksquare$


Sources