Tableau Extension Lemma/General Statement/Proof 2

== Theorem ==
Let $T$ be a finite propositional tableau.
Let its hypothesis set $\mathbf H$ be finite.
== Proof ==
The proof uses induction on the number $n$ of elements of $\mathbf H$.
Suppose we are given the result for the case $n = 1$, that is, when $\mathbf H$ is a singleton.
Suppose also that we are given the result for all sets $\mathbf H'$ with $n$ elements.
Now, given a set $\mathbf H' = \set {\mathbf A_1, \ldots, \mathbf A_{n+1} }$ with $n + 1$ elements.
Let $T$ be a finite propositional tableau.
By induction hypothesis, there is a finished finite propositional tableau $T'$ containing $T$ as a subgraph, and with root $\mathbf H \cup \set {\mathbf A_1, \ldots, \mathbf A_n}$.
Now apply the case $n = 1$ to this resulting propositional tableau $T'$ and the set $set {\mathbf A_{n + 1} }$.
This yields a finished finite propositional tableau $T$ which:
$(1):\quad$ has root $\mathbf H \cup \set {\mathbf A_1, \ldots, \mathbf A_n} \cup \set {\mathbf A_{n + 1} } = \mathbf H \cup \mathbf H'$;
$(2):\quad$ contains $T'$ as a subgraph.
But then $T$ also contains $T$ as a subgraph, proving the result for $\mathbf H'$.
It thus only remains to take care of the base cases $n = 0$ and $n = 1$.
First, the case $n = 0$.
Let $T$ be a finite propositional tableau.
To find the finite propositional tableau $T'$ with the desired properties, we use some of the tableau construction rules, starting with $T$.
Let $t$ be any leaf node of $T$, and let $\Gamma_t$ be the branch from Leaf of Rooted Tree is on One Branch.
Let $\map n {\Gamma_t}$ be the number of non-basic WFFs that were not used to add any of the nodes of $\Gamma_t$ to $T$.
It is seen that for any application of the tableau construction rules on $t$:
:If $s$ is added by the rule, then $\map n {\Gamma_s} \le \map n {\Gamma_t}$.
Moreover, it is seen that any rule reduces the total count $\map m {\Gamma_t}$ of logical connectives occurring in these non-basic, unused WFFs along $\Gamma_t$.
In conclusion:
:If $s$ is added by a rule, then $\map m {\Gamma_s} < \map m {\Gamma_t}$
By the Method of Infinite Descent applied to $\map m {\Gamma_t}$, only finitely many rules can be applied, starting from $t$.
Since $T$ has only finitely many leaves and corresponding branches, only finitely many rules can be applied to $T$ in total.
Let $T'$ be the finite propositional tableau resulting from applying all these possible rules.
By construction of $T'$, it follows that every branch of $\Gamma$ is either contradictory or finished.
That is, $T'$ is finished.
Finally, the last case, $n = 1$.
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a finite propositional tableau.
First, using the case $n = 0$, extend $T$ to a finished finite propositional tableau $T'$.
Again using the case $n = 0$, let $T_{\mathbf A}$ be a finished finite propositional tableau with root $\set {\mathbf A}$.
Now add $\mathbf A$ to the root of $T'$.
Then at every leaf $t$ of $T'$, $\mathbf A$ is the only WFF that is not used yet.
As far as the rules for propositional tableaus are concerned, there is no difference between:
:$t$ as a leaf of $T'$, and 
:the tableau consisting only of a root and with hypothesis set $\mathbf A$.
Therefore, the rules allow to "paste", as it were, the finished tableau $T_{\mathbf A}$ under every leaf $t$ of $T'$.
Denote the resulting tableau with $T'_{\mathbf A}$.
Then for any branch $\Gamma$ of $T'_{\mathbf A}$ and every non-basic WFF $\mathbf B$ along it:
:$\mathbf B$ is on $T'$, or:
:$\mathbf B$ is on a copy of $T_{\mathbf A}$.
In either case, the finished nature of these tableaus implies that:
:$\mathbf B$ is used at some node of $\Gamma$
Hence $\Gamma$ is contradictory or finished.
In conclusion, $T'_{\mathbf A}$ is finished, and contains $T$ as a subgraph.
The result follows from the Principle of Mathematical Induction.
Category:Tableau Extension Lemma