Compactness for First-Order Logic
Theorem (Compactness for First-Order Logic): If every finite subset of a set of first-order formulas has a model, then has a model.
Let be a set of first-order formulas. We show contrapositive.
Suppose has no model.
Then has no model.
Then by Compactness Theorem for propositional logic, some finite subset of it has no model.
There is then finite subset of clauses that generate , i.e. such that . Therefore, has no model.
These clauses are generated by a finite subset , i.e. .
Therefore the finite subset of has no model.
End of Proof.