This is an old revision of the document!
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.
Proof:
Let be a set of first-order formulas. We show contrapositive.
Suppose has no model.
Then has no model.
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.