= Solution
The <compactness theorem> says that a <set> $T$ of <first-order sentences> has a <first-order model> if and only if every finite <subset> of $T$ has a <first-order model>. One direction follows by using the same <first-order model> for each <subset>.
For the nontrivial direction suppose every finite <subset> has a <first-order model>, but $T$ has none. Semantically $T\models\bot$, so completeness gives a formal <logical derivation> $T\vdash\bot$. A formal <logical derivation> is finite and uses only finitely many assumptions, say $T_0\subseteq T$. Thus $T_0\vdash\bot$. <Soundness> would make $T_0$ unsatisfiable, contradicting the hypothesis. Here $\bot$ can be any fixed contradictory <first-order sentence>, such as $\exists x\,(x\ne x)$, if it is not a primitive logical symbol. Therefore \b[finite satisfiability implies satisfiability].
Back to article page
