The compactness theorem says that a set of first-order sentences has a first-order model if and only if every finite subset of 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 has none. Semantically , so completeness gives a formal logical derivation . A formal logical derivation is finite and uses only finitely many assumptions, say . Thus . Soundness would make unsatisfiable, contradicting the hypothesis. Here can be any fixed contradictory first-order sentence, such as , if it is not a primitive logical symbol. Therefore finite satisfiability implies satisfiability.
Articles by others on the same topic
There are currently no matching articles.