Main Lemma of Propositional Tableaus

Lemma

Let $\mathbf H$ be a countable set of WFFs of propositional logic.

Either $\mathbf H$ has a tableau confutation or $\mathbf H$ has a model.

Proof

If $\mathbf H$ is finite, then the Finite Main Lemma of Propositional Tableaus applies.

So, assume that $\mathbf H$ is countably infinite.

Suppose $\mathbf H$ does not have a tableau confutation.

By Countable Hypothesis Set has Finished Tableau, there is a finished tableau $T$ with hypothesis set $\mathbf H$.

By Finished Propositional Tableau has Finished Branch or is Confutation‎, as $T$ is (by hypothesis) not a confutation, it must have a finished branch; call it $\Gamma$.

By Finished Set Lemma, the set of WFFs of propositional logic on $\Gamma$ has a model $\MM$.

Finally, because all the WFFs in the hypothesis set occur on $\Gamma$, $\MM \models \mathbf H$.

$\blacksquare$

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.11$: Compactness: Lemma $1.11.1$