Compactness for First-Order Logic

Theorem (Compactness for First-Order Logic): If every finite subset of a set $S_0$ of first-order formulas has a model, then $S_0$ has a model.

Proof:

Let $S_0$ be a set of first-order formulas. We show contrapositive.

Suppose $S_0$ has no model.

Then $expandProp(clauses(S_0))$ has no model.

Then by Compactness Theorem for propositional logic, some finite subset $S_1 \subseteq expandProp(clauses(S_0))$ of it has no model.

There is then finite subset of clauses $S_2 \subseteq clauses(S_0)$ that generate $S_1$ , i.e. such that $S_1 \subseteq expandProp(S_2)$ . Therefore, $S_2$ has no model.

These clauses are generated by a finite subset $S_3 \subseteq S_0$ , i.e. $S_2 \subseteq clauses(S_3)$ .

Therefore the finite subset $S_3$ of $S_0$ has no model.

End of Proof.