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.
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 has no model.
End of Proof.