Finite Main Lemma

Lemma

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

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

Proof

Let $\mathbf H$ be a finite set of propositional WFFs which does not have a tableau confutation.

By the Tableau Extension Lemma, the tableau which consists only of a root node with hypothesis set $\mathbf H$ can be extended into a finite finished tableau $T$.

The tableau $T$ still has root $\mathbf H$.

Since $T$ is not a confutation, it has a finished branch $\Gamma$.

By the Finished Set Lemma, the set $\Delta$ of all WFFs on $\Gamma$ has a model, $\mathcal M$, say.

In particular, $\mathcal M$ is a model of $\mathbf H$ as required.

$\blacksquare$

Comment

From Tableau Confutation means No Model, we already know that $\mathbf H$ can not have both a tableau confutation and a model.

This result gives us that $\mathbf H$ has a tableau confutation iff $\mathbf H$ does not have a model.

Sources

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