Tableau Confutation contains Finite Tableau Confutation
Theorem
Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Let $T$ be a tableau confutation of $\mathbf H$.
Then there exists a finite rooted subtree of $T'$ that is also a tableau confutation of $\mathbf H'$.
Proof
For each node $v \in T$, let $\map p v$ be the path from $v$ to $r_T$, the root of $T$.
This path is unique by Path in Tree is Unique.
Let $\VV$ be the subtree of $T$ consisting those nodes $v$ of $T$ such that $\map p v$ is not contradictory.
Aiming for a contradiction, suppose that $\VV$ were infinite.
Then by König's Tree Lemma, $\VV$ has an infinite branch $\Gamma$.
Since $\VV \subseteq T$, it follows that $\Gamma$ is also a branch of $T$.
However, by construction, it is impossible that $\Gamma$ is contradictory.
This contradicts that $T$ is a tableau confutation.
Hence $\VV$ is finite.
Next, define a finite propositional tableau $T'$ by:
- $v \in T' \iff \map \pi v \in \VV$
that is, the rooted tree formed by $\VV$ and all its children.
Then by construction, for each leaf node $v$ of $T'$, we have that $v \notin \VV$.
That is, that $\map p v$ is a contradictory branch of $T'$.
By Leaf of Rooted Tree is on One Branch, every branch of $T'$ is contradictory.
Hence $T'$ is a tableau confutation of $\mathbf H'$, as desired.
$\blacksquare$
Comment
Some sources define a tableau confutation to be a finite propositional tableau.
This result establishes that this distinction is not of material importance.