Semantic Tableau Algorithm Terminates

From ProofWiki
Jump to: navigation, search

Theorem

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


Then the Semantic Tableau Algorithm for $\mathbf A$ terminates.

Each leaf node of the resulting semantic tableau is marked.


Proof

Let $t$ be an unmarked leaf of the semantic tableau $T$ being constructed.

Let $b \left({t}\right)$ be the number of binary logical connectives occurring in its label $U \left({t}\right)$.

Let $n \left({t}\right)$ be the number of negations occurring in $U \left({t}\right)$.

Let $i \left({t}\right)$ be the number of biconditionals and exclusive ors occurring in $U \left({t}\right)$.

Define $W \left({t}\right)$ as:

$W \left({t}\right) = 3 b \left({t}\right) + n \left({t}\right) + 4 i \left({t}\right)$[1]


Next, we aim to prove that:

$W \left({t'}\right) < W \left({t}\right)$

for every leaf $t'$ that could be added to $t$ in following the Semantic Tableau Algorithm.


First, presume an $\alpha$-formula $\mathbf A$ from $U \left({t}\right)$ is picked.

Looking at the mutations from $U \left({t}\right)$ to $U \left({t'}\right)$, it follows that the claim is reduced to:

$W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) < W \left({\mathbf A}\right)$

This claim can be verified by looking up the appropriate row in the following extension of the table of $\alpha$-formulas:

$\begin{array}{ccc||ccc} \hline \mathbf A & \mathbf A_1 & \mathbf A_2 & W \left({\mathbf A}\right) & W \left({\mathbf A_1}\right) & W \left({\mathbf A_2}\right) \\ \hline \neg\neg \mathbf A_1 & \mathbf A_1 & & W \left({\mathbf A_1}\right) + 2 & W \left({\mathbf A_1}\right) & 0\\ \mathbf A_1 \land \mathbf A_2 & \mathbf A_1 & \mathbf A_2 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 3 & W \left({\mathbf A_1}\right) & W \left({\mathbf A_2}\right) \\ \neg \left({\mathbf A_1 \lor \mathbf A_2}\right) & \neg \mathbf A_1 & \neg \mathbf A_2 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 4 & W \left({\mathbf A_1}\right) + 1 & W \left({\mathbf A_2}\right) + 1 \\ \neg \left({\mathbf A_1 \implies \mathbf A_2}\right) & \mathbf A_1 & \neg \mathbf A_2 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 4 & W \left({\mathbf A_1}\right) & W \left({\mathbf A_2}\right) + 1 \\ \neg \left({\mathbf A_1 \mathbin \uparrow \mathbf A_2}\right) & \mathbf A_1 & \mathbf A_2 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 4 & W \left({\mathbf A_1}\right) & W \left({\mathbf A_2}\right) \\ \mathbf A_1 \mathbin \downarrow \mathbf A_2 & \neg \mathbf A_1 & \neg \mathbf A_2 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 3 & W \left({\mathbf A_1}\right) + 1 & W \left({\mathbf A_2}\right) + 1 \\ \mathbf A_1 \iff \mathbf A_2 & \mathbf A_1 \implies \mathbf A_2 & \mathbf A_2 \implies \mathbf A_1 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 7 & W \left({\mathbf A_1}\right) + 3 & W \left({\mathbf A_2}\right) + 3\\ \neg \left({\mathbf A_1 \oplus \mathbf A_2}\right) & \mathbf A_1 \implies \mathbf A_2 & \mathbf A_2 \implies \mathbf A_1 & W \left({\mathbf A_1}\right) + W \left({\mathbf A_2}\right) + 8 & W \left({\mathbf A_1}\right) + 3 & W \left({\mathbf A_2}\right) + 3\\ \hline \end{array}$


Now presume a $\beta$-formula $\mathbf B$ from $U \left({t}\right)$ is picked.

Looking at the mutations from $U \left({t}\right)$ to $U \left({t'}\right)$, it follows that the claim is reduced to:

$W \left({\mathbf B_1}\right), W \left({\mathbf B_2}\right) < W \left({\mathbf B}\right)$

This claim can be verified by looking up the appropriate row in the following extension of the table of $\beta$-formulas:

$\begin{array}{ccc||ccc} \hline \mathbf B & \mathbf B_1 & \mathbf B_2 & W \left({\mathbf B}\right) & W \left({\mathbf B_1}\right) & W \left({\mathbf B_2}\right)\\ \hline \neg \left({\mathbf B_1 \land \mathbf B_2}\right) & \neg \mathbf B_1 & \neg \mathbf B_2 & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 4 & W \left({\mathbf B_1}\right) + 1 & W \left({\mathbf B_2}\right) + 1\\ \mathbf B_1 \lor \mathbf B_2 & \mathbf B_1 & \mathbf B_2 & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 3 & W \left({\mathbf B_1}\right) & W \left({\mathbf B_2}\right)\\ \mathbf B_1 \implies \mathbf B_2 & \neg \mathbf B_1 & \mathbf B_2 & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 3 & W \left({\mathbf B_1}\right) + 1 & W \left({\mathbf B_2}\right)\\ \mathbf B_1 \mathbin \uparrow \mathbf B_2 & \neg \mathbf B_1 & \neg \mathbf B_2 & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 3 & W \left({\mathbf B_1}\right) + 1 & W \left({\mathbf B_2}\right) + 1\\ \neg \left({\mathbf B_1 \mathbin \downarrow \mathbf B_2}\right) & \mathbf B_1 & \mathbf B_2 & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 4 & W \left({\mathbf B_1}\right) & W \left({\mathbf B_2}\right)\\ \neg \left({\mathbf B_1 \iff \mathbf B_2}\right) & \neg \left({\mathbf B_1 \implies \mathbf B_2}\right) & \neg \left({\mathbf B_2 \implies \mathbf B_1}\right) & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 8 & W \left({\mathbf B_1}\right) + 4 & W \left({\mathbf B_2}\right) + 4 \\ \mathbf B_1 \oplus \mathbf B_2 & \neg \left({\mathbf B_1 \implies \mathbf B_2}\right) & \neg \left({\mathbf B_2 \implies \mathbf B_1}\right) & W \left({\mathbf B_1}\right) + W \left({\mathbf B_2}\right) + 7 & W \left({\mathbf B_1}\right) + 4 & W \left({\mathbf B_2}\right) + 4\\ \hline \end{array}$


Because of the strictly decreasing nature of $W \left({t}\right)$, it must be that eventually, all leaves of $T$ cannot be extended further.

A leaf $t$ cannot be extended if and only if $U \left({t}\right)$ comprises only literals.

These finitely many leaves will be marked by Step 3 of the Semantic Tableau Algorithm.


In conclusion, the Semantic Tableau Algorithm terminates, yielding a semantic tableau with only marked leaves.

$\blacksquare$


References

  1. In Mathematical Logic for Computer Science (3rd ed., 2012), M. Ben-Ari omits the $4 i \left({t}\right)$ term.
    However, as one can verify, this compromises the $\iff$ and $\neg \oplus$ cases for $\alpha$-formulas.


Sources