Quantifier elimination is a staple of model theory. Suppose that is a quantifier-free formula in some language . Then one says a quantifier-free formula is equivalent modulo a -theory to the (quantified ) formula , if in every model of , .
Geometrically speaking, eliminating existential quantifiers corresponds to taking image under coordinate projection. The statement “” is equivalent to “”, where is the projection map to the “-coordinates”, and we have used the standard model-thoretic notation to denote , and .
All the above is clear from the logical perspective. The trouble arises when one works at the boundary of model theory and algebraic geometry, and would like to interpret the above definitions in the language of algebraic geometry.
Schematic image, constructible sets and Chevalley’s theorem
Suppose is a field. Denote by , the -dimensional affine space over , and let the scheme-theoretic morphism, corresponding to the inclusion
One calls a subset of the underlying topological space (Zariski topology) of the scheme to be constructible, if it is a finite union of subsets of the form where are the underlying topological spaces of closed subschemes of .
Now if is a subscheme, then its schematic image, , is a well defined subset of the underlying topological space of . What does one mean by the schematic image ? Suppose is a point of .
Let denote the restriction to of the morphism , i.e. corresponds to the composition
Then, belongs to the schematic image if and only if for some . (The schematic image of only depends on the underlying topological space of , and thus we can replace by the corresponding reduced scheme ( is the smallest closed subscheme of whose underlying space is equal to that of ) in the above description without changing .)
If are closed subschemes of , then so is . We define the schematic image, of the constructible set to be , and more generally we define the schematic image of by .
The following standard example is helpful. Let be the affine subscheme of defined by the single polynomial i.e. . Let be the projection (see picture).
Then each closed point , other than the point is contained in the schematic image of . For example, is in the image since . However, there is no prime ideal of whose inverse image under the composition is equal to . Note that the ideal generated by in contains (i.e. corresponds to the generic element of ), and its inverse image in is itself, which corresponds to the generic element of (confirming the intuition that the generic element of maps to the generic element of ). But the schematic map is not surjective, since the closed point corresponding to the ideal is not in the image.
Chevalley’s theorem states that the schematic image of a constructible set (as defined previously) is again constructible.
What’s the connection with model theory ?
There is the obvious temptation to identify constructible subsets of with definable subsets of , for a model of some theory which extends the theory of fields. If is the theory of algebraically closed fields, then is algebraically closed, and each definable subset of can be identified with the set of closed points of some constructible subset of . In this case the closed points also correspond to the -rational points — and so the each definable subset of is of the form, , for closed subschemes of . Chevalley’s theorem then immediately implies in particular that the theory of algebraically closed fields admits quantifier elimination.
1. What about non-algebraically closed fields ?
What if one considers some theory (still in the language of fields) of fields (for example, the theory of real closed fields, or the theory of ) which are not algebraically closed. Chevalley’s theorem still holds. But what breaks down now is that the definable subsets of are no longer just the sets of the form , for closed subschemes . The class of the former can be strictly bigger. Moreover, even if one restricts to definable subsets of of the form , for closed subschemes , the -points of the schematic image can be strictly larger than the image under the set-theoretic projection of the definable subset under consideration.
Take for example the definable subset of defined by the one equation . The image of the set theoretic projection to the -axis of the -points of the affine subscheme defined by is obviously the real interval (which note is not a definable subset of ). But if one takes the schematic image , and then considers the -points of contained in , then we get all of .
Thus, taking the -points “upstairs” and then the set theoretic image, can produce a strictly smaller set, than first taking the schematic image and then the -points of the image “downstairs”.
The above example shows that the theory of real closed fields does not admit quantifier elimination. The image under projection of a definable subset need not be definable. One can recover quantifier elimination by expanding the language (and thus also the definable subsets). For example, clearly one must include the subset which occurs in the example above. One way is to expand the language and include the predicate (often, abbreviated to (!)). The resulting theory in the expanded language does have quantifier elimination. This is the Tarski-Seidenberg theorem — while being still elementary — is harder to prove than Chevalley’s theorem. In the case of the theory of , in order to get quantifier elimination one has to go further and include all the predicates (Macintyre predicates).
The property of having quantifier-elimination in theories of non-alegebraically closed fields always involve some special property of the models of the theory in question (for example, the fact that real closed fields admit a unique ordering in the case of the reals).
This post is a prelude to a longer post that I have been thinking about making on the connections between quantifier elimination, cohomology and complexity theory. A glimpse of this is available here:
Connectivity of joins, cohomological quantifier elimination, and an algebraic Toda’s theorem, Saugata Basu, Deepam Patel, Selecta Mathematica, volume 26, (2020).
All background material can be found in the two books shown below.
It goes without saying that the views expressed are mine and may not reflect those of my co-authors/co-conspirators. The LaTeX to WordPress conversion was done using the latex2wp package written by Luca Trevisan.