Compactness Theorem for Boolean Interpretations/Proof 1
Theorem
Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Suppose $\mathbf H$ is finitely satisfiable for boolean interpretations.
That is, suppose that every finite subset $\mathbf H' \subseteq \mathbf H$ is satisfiable for boolean interpretations.
Then $\mathbf H$ has a model.
Proof
Suppose $\mathbf H$ does not have a model.
By the Main Lemma of Propositional Tableaus, $\mathbf H$ has a tableau confutation $T$.
By Tableau Confutation contains Finite Tableau Confutation, $T$ may be assumed to be finite.
Hence the set $\mathbf H'$ of all 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 Tableau Confutation implies Unsatisfiable, $\mathbf H'$ has no models.
But this contradicts the assumption that all finite subsets of $\mathbf H$ have models.
Hence the result.
$\blacksquare$
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.11$: Compactness: Theorem $1.11.5$