Quantifier elimination of valued fields.

Question

I have been reading the quantifier elimination theorem for valued fields, Theorem 3.26 on page 35 of these lecture notes by Lou van den Dries: http://homepages.math.uic.edu/~freitag/valfields.pdf

I do not quite understand why we need the $|E|^+$-saturation in the proof.

I mean I know that we need it to use the QE-test but I do not understand why it does not reduce the generality of our proof. And how we can prove that the ACVF is saturated? Is it because the types are in the form of polynomials?

Answer 1

Let me try to address your questions one by one.

I do not quite understand why we need the $|E|^+$-saturation in the proof.

There are several places in the proof where saturation is explicitly used. For example, in Case 1, van den Dries writes "By the saturation assumption on $(F,B)$, we can find $y\in B$ such that $\bar{y}\notin k_{B\cap iK}$." Here, this amounts to writing down a partial type in the variable $y$ which expresses the condition "$y\in B$ and $\bar{y}\notin k_{B\cap iK}$" and checking that it is consistent (by compactness) and uses at most $|E|$-many parameters. Then $|E|^+$-saturation of $(F,B)$ implies that the partial type is realized in $(F,B)$.

I know that we need it to use the QE-test but I do not understand why it does not reduce the generality of our proof.

Why would it reduce the generality? The QE test says that if we check some semantic condition on models of $T$, then we can conclude that $T$ has QE. The semantic condition involves an arbitrary model $M\models T$ and an $|M|^+$-saturated model $N\models T$. To understand why we may assume that $N$ is $|M|^+$-saturated, you need to read the proof of the QE test! For example, see Theorem 7.14 in these lecture notes on model theory by van den Dries and Henson.

And how we can prove that the ACVF is saturated?

ACVF is a theory. Saturation is a property of a model. So "ACVF is saturated" makes no sense.

It is a standard theorem that sufficiently saturated models exist: For any cardinal $\kappa$, any first-order theory $T$, and any model $M\models T$, $M$ has an elementary extension which is $\kappa$-saturated. In particular, every algebraically closed valued field embeds (elementarily) in an algebraically closed valued field which is as saturated as you need it to be.

But note that in the statement of the QE test, you are handed an arbitrary model $M$ and an $|M|^+$-saturated model $N$. You don't need to construct $N$ or prove that it is $|M|^+$-saturated. You just need to extend homomorphisms from substructures of $M$ to $N$.

Is it because the types are in the form of polynomials?

It's not clear what it would mean to "types to be in the form of polynomials". But whatever you mean by that, it's not true in ACVF - formulas also include information about the valuation, not just polynomial equations. Quantifier elimination will allow you to reduce understanding the type of a tuple to understanding equations and valuation relations between polynomials in the tuple (since QE says every formula is equivalent to Boolean combination of atomic formulas, and every atomic formula is equivalent to an equality or a valuation relation between polynomials), but you can't assume this in the proof of QE.