Tableau Extension Lemma

Lemma

Let $T$ be a finite propositional tableau.

Let its hypothesis set $\mathbf H$ be finite.

Then $T$ can be extended to a finished finite propositional tableau $T'$ which also has hypothesis set $\mathbf H$.

General Statement

Let $\mathbf H'$ be another finite set of WFFs.

Then there exists a finished finite propositional tableau $T'$ such that:

$(1):\quad$ the root of $T'$ is $\mathbf H \cup \mathbf H'$;

$(2):\quad$ $T$ is a rooted subtree of $T'$.

Proof

Let $\mathbf A$ be a WFF of propositional logic at a node $t$ such that:

• $\mathbf A$ is not a basic WFF;

• There is a non-contradictory branch through $t$ on which $\mathbf A$ is not used.

Such a WFF $\mathbf A$ will be called unused.

Note that a tableau is finished iff there are no unused WFFs in the tableau.

Let $u \left({T}\right)$ be the length of the longest unused WFF in $T$.

If $T$ is finished, we set $u \left({T}\right) = 0$.

Since there are only finitely many WFFs in $T$, the number $u \left({T}\right)$ must exist.

Let $R \left({n}\right)$ be the proposition that every finite propositional tableau with hypothesis set $\mathbf H$ and with $u \left({T}\right) < n$ can be extended to a finite finished tableau.

That is, $R \left({n}\right)$ is an assertion that this lemma is true whenever $u \left({T}\right) < n$.

The statement $R \left({1}\right)$ is true, because a tableau $T$ such that $u \left({T}\right) < 1$ is already finished.

So, let us assume the truth of $R \left({k}\right)$.

Suppose that $u \left({T}\right) < k+1$.

We extend $T$ to a new tableau $T'$ by using every unused WFF $\mathbf A$ in $T$ once on every non-contradictory branch through $\mathbf A$.

Each of the unused WFFs in $T$ is used in the new tableau $T'$.

Also, each new WFF which was added when forming $T'$ has a length less than $u \left({T}\right)$, because the added WFFs are always shorter than the used WFFs.

So $u \left({T'}\right) < u \left({T}\right) < k + 1$, so $u \left({T'}\right) < k$.

So, by the induction hypothesis $R \left({k}\right)$, there is a finite finished extension $T$ of $T'$.

$T$ is also a finished extension of $T$.

Hence $R \left({k+1}\right)$, and the result follows by strong induction.

$\blacksquare$

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.10$: Completeness: Lemma $1.10.2$