Soundness Theorem for Semantic Tableaus
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 article contains statements that are justified by handwavery. In particular: "It follows", is obvious, and is tedious to write down You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding precise reasons why such statements hold. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Handwaving}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
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
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.7.1$