A first-order theory is model-complete if every structure embedding between models of is an elementary embedding. Equivalently, whenever and both satisfy , one has :for every first-order formula and every finite tuple . This is preservation of all formulas with parameters, rather than merely all first-order sentences.
Assume has quantifier elimination, and let be a structure embedding between its models. For any first-order formula , choose a quantifier-free formula equivalent to it modulo . A structure embedding preserves and reflects atomic formulas; induction through the Boolean connectives therefore preserves every quantifier-free formula. ThusThe embedding is elementary. Every theory with quantifier elimination is model-complete.
A model companion of a first-order theory , in the same first-order language, is a model-complete theory with the same universal consequences of a theory as :Equivalently, every model of embeds into a model of , and every model of embeds into a model of . The equivalence follows from the diagram embedding criterion for universal theories, which is an application of the compactness theorem. A model companion need not be a syntactic extension of , and uniqueness is understood up to logical equivalence of theories.
Suppose and are model companions of . Their universal consequences of a theory agree, so the diagram embedding criterion for universal theories permits embeddings in both directions between their model classes.
Starting from any , alternately take such extensions, identifying each model with its image under the embedding:Since is model-complete, ; since is model-complete, . The two subsequences have the same union . The elementary chain theorem givesEvery axiom of , as a sentence true in , is therefore true in . Thus every model of is a model of . Reversing their roles proves the converse. The model companion is unique up to logical equivalence. If is inconsistent, its only possible companion is likewise inconsistent, so the same uniqueness conclusion holds.
A formally real field is a field in which is not a finite sum of squares. The theory of formally real fields consists of the field axioms and, for each , the sentenceA real closed field is a formally real field with no proper formally real algebraic extension. An equivalent first-order axiomatization of the Theory of real closed fields adds: every or its negative is a square, and every odd-degree polynomial has a root. Explicitly the square axiom isand the polynomial axioms say that every monic polynomial of degree has a root, for each .
The Artin-Schreier ordering criterion says that every formally real field can be ordered, and the real closure theorem embeds each ordered field into an algebraic real closed field extension. Consequently every FRF model embeds into an RCF model. Conversely every RCF model is itself an FRF model, so the reverse embedding requirement is automatic.
It remains to establish model completeness. A real closed field has a unique order, definable in the field language byAny field embedding between real closed fields preserves this order: positive elements are nonzero squares, and negative elements have positive negatives. The quantifier elimination for ordered real closed fields theorem makes every such ordered embedding elementary, by the preceding part. Restricting to formulas of the field language makes the original embedding elementary as well. Thus RCF is model-complete in the field language.
The embedding conditions and model completeness proveThe quantifier elimination invoked here is in the ordered language. In the unordered field language, model completeness still holds, but full quantifier elimination does not follow from forgetting the order.
Articles by others on the same topic
There are currently no matching articles.