Compactness Theorem of Propositional Calculus

Theorem

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

Suppose every finite subset of $\mathbf H$ has a model.

Then $\mathbf H$ has a model.

Proof

Suppose $\mathbf H$ does not have a model.

By the Main Lemma of Propositional Calculus, $\mathbf H$ has a tableau confutation $T$.

Since each tableau confutation is a finite tableau, the set $\mathbf H'$ of all propositional WFFs in $\mathbf H$ used somewhere in $T$ is finite.

Now, let $T'$ be the labeled tree which is the same as $T$ but with root $\mathbf H'$ instead of $\mathbf H$.

Then $T'$ is a tableau confutation of $\mathbf H'$.

By the Extended Soundness Theorem of Propositional Calculus, $\mathbf H'$ has no models.

But this contradicts the assumption that all finite subsets of $\mathbf H$ have models.

Hence the result.

$\blacksquare$

Sources

• H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability (1996): $\S 1.11$: Corollary $1.11.5$