Tableau Extension Lemma/General Statement/Proof 1

Theorem

Let $T$ be a finite propositional tableau.

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

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 $T_{\mathbf H'}$ be the finite propositional tableau obtained by replacing the hypothesis set $\mathbf H$ of $T$ with $\mathbf H \cup \mathbf H'$.

By the Tableau Extension Lemma, $T_{\mathbf H'}$ has a finished extension $T'$.

By definition of extension, $T_{\mathbf H'}$ is a rooted subtree of $T'$.

But $T_{\mathbf H'}$ and $T$ are equal when considered as rooted trees.

The result follows.

$\blacksquare$