indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
One thinks of existential quantification as projection. A theory eliminates quantifiers when “the projection of a primitive (quantifier-free) definable set is still primitive (quantifier-free).”
For example, suppose we’re working in the theory of a vector space over a fixed field . Let be a linear transformation . Let be an -tuple, a variable, and an -tuple of variables. Then the solution set for
is the projection of the solution set for
to the -hyperplane. Since the projection of a (translated) hyperplane is again a (translated) hyperplane, there exists some such that
This is an instance of the fact that the theories of vector spaces over division rings admits quantifier elimination. It’s nice when this happens, and when it doesn’t, one asks for minimal ways to expand the language to make it happen. That ACF eliminates quantifiers is a special case of Chevalley's theorem on constructible sets (“the image of a constructible set is constructible”).
Often, in order to prove quantifier-elimination, one develops an effective procedure for reducing an arbitrary sentence to a quantifier-free one, which shows that the theory is decidable; this is how Tarski proved that the theory RCF? of real closed fields is decidable.
An -theory eliminates quantifiers if every -formula is equivalent to a quantifier-free -formula , i.e.
Any theory is bi-interpretable with an expanded theory where every definable set is named with a predicate, called its Morleyization, which eliminates quantifiers.
Therefore, whether or not a structure has quantifier elimination depends on the language being used to describe the structure.
Quantifier elimination implies model completeness: all submodels are elementary submodels and all models are existentially closed.
It is an informative exercise to try to prove QE syntactically (a “tractable” case like DLO suffices) to appreciate the usefulness of the semantic/model-theoretic characterization of QE below.
The characterizations below (and in general important tools in model theory like the compactness theorem, the Lowenheim-Skolem theorem, etc.) only work for infinite models.
Since quantifier elimination is equivalent to substructure completeness and elementarily equivalent finite structures are isomorphic, (the theory of a) finite first-order structure eliminates quantifiers if and only if it is ultrahomogeneous.
A first-order theory eliminates quantifiers if and only if it is substructure-complete: plus the quantifier-free diagram of any substructure of any model of form a complete theory.
Let be a theory. The following are equivalent:
eliminates quantifiers.
For every and models of such that is -saturated and every proper substructure such that there is an embedding , there exists a proper intermediate substructure , and an extension of to .
(1. 2.) Suppose eliminates quantifiers. Since this is equivalent to substructure-completeness, choose , and let be the substructure of generated by Then, since quantifier-free statements are transferred by embeddings, the type (in model theory) of over in is finitely realized in and therefore realized via -saturation by some .
A standard back-and-forth argument starting at lets us build our required extension.
(2. 1.) By possibly transfinitely iterating 2., we obtain an embedding As we can always embed a -model inside a larger, arbitrarily saturated -model, we therefore have amalgamation.
This gives model completeness: since model completeness is equivalent to every -submodel being an elementary submodel, it suffices by the Tarski-Vaught test (and an induction on complexity of formulas) to test that whenever is a tuple from , is a quantifier-free formula, and , then (i.e. that is existentially closed.)
Embed into a sufficiently saturated elementary extension (by taking a large enough ultrapower, if you like). Then by (2.), the elementary embedding extends along the embedding to an embedding . If , then there is a witness such that . Since was quantifier-free, this transfers along the embedding , so that , and therefore This then transfers down the elementary embedding , so Since and were arbitrary, is model complete.
Since model completeness + amalgamation implies substructure completeness and substructure completeness is equivalent to quantifier elimination, the theorem is proved.
ACF admits quantifier elimination. Furthermore, the theories (where is specification of the characteristic) are complete.
We put ourselves into the situation of the above theorem. Let and be algebraically closed fields such that is -saturated. Let be a subring of with an embedding. As is a field, is an integral domain, and thus contains the fraction field of . The embedding extends uniquely to . By a back-and-forth argument, extends uniquely to . Therefore, we can assume that is algebraically closed. Let . Then is transcendental over , and by saturation its type is realized by some which is transcendental over the image of under . Then induces an embedding , which extends . Thus the hypotheses of the theorem are satisfied and ACF admits QE.
That becomes complete after specifying a characteristic follows from the fact that in any theory with quantifier elimination, naming a substructure (thus passing to the theory of all models which contain a copy of that substructure) makes the theory complete, and every field of characteristic contains the prime field of characteristic .
Let eliminate quantifiers. Let be a substructure (not necessarily a submodel) of some model of . Then the theory of models of interpreting a copy of also has quantifier elimination.
In particular, if we specialize to ACF, this tells us that not only do all algebraically closed fields admit quantifier elimination in the language of rings, but so do all algebraically closed fields containing a fixed ring (i.e. the geometric points of ), in the language of rings with constants for the elements of .
Last revised on August 3, 2017 at 22:57:00. See the history of this page for a list of all contributions to it.