Adjoin to the negations of all closed-term instances of . If the resulting set had a first-order model , its ground-term substructure from (ii) would still first-order model . The assumed existential consequence therefore supplies a tuple in satisfying . Each is the value of a closed term .
Quantifier-free agreement between a substructure and its ambient first-order structure givescontradicting the adjoined negation of this very ground instance. Thusis unsatisfiable. Compactness theorem gives a finite unsatisfiable subset. Its finitely many ground negations imply that, for some finite list of first-order term tuples,If the finite subset already shows itself inconsistent and supplies no ground negations, choose any one closed-term tuple using the available constant; then any first-order sentence is a consequence of , so suffices. Otherwise the selected list is nonempty. This also explains why the conclusion contains a finite disjunction rather than necessarily one universal choice of a witness first-order term.
Articles by others on the same topic
There are currently no matching articles.