Quantifier elimination in ACF from an example

Question

The (first order) theory of algebraically closed field (ACF) admits quantifier elimination.

That means that for each (possibly) quantified statement $\phi$ in the theory, we can construct a statement $\psi$ without quantifiers such that it is a theorem of ACF that $\phi \iff \psi$.

I would like to understand how this works, on a particular example and in the general case.

I have seen I don't understand how the theory of algebraically closed fields admits quantifier elimination and it is interesting but the example described is quite basic.

First, an example: Suppose $P$ and $Q$ are polynomials in $\mathbb{Z}[X]$ (so that if $x$ is a bound variable, the formula $P(x)$ is in the language of $ACF$ when, for instance, we identify an integer $n$ with $1 + 1 + \ldots + 1$ (repeated $n$ times)).

Question 1: How do we eliminate quantifiers in the case of the statement $\exists x, (P(x) = 0) \land (Q(x) \neq 0)$?

Now, the general case: we can assume that $\phi$ is normalized so as to start with a finite sequence of $\forall$, $\exists$ with associated quantified variables — we can also restrict to the $\exists$ symbol (possibly negated). We can also normalize the formula that follows so that it is expressed in disjunctive normal form (e.g. $(A \land \lnot B \land C) \lor (D \land \lnot E) \lor F$ where $A,B,C,D,E,F$ are expressed as polynomial equalities involving integers and the bound variables. So we should show that these statements admit quantifier elimination.

Question 2: Is this a correct formulation of the problem of quantifier elimination for ACF?

When reading this MO question, it appears though that showing ACF admits quantifier elimination is not a trivial task. Reading proofs here and there I was not able to grasp the idea (mainly because most of the proofs I found are presented in a more general context).

Question 3: In the context of ACF, as formulated above, what are the main steps to show that it admits quantifier elimination? (in particular, what is the non-trivial part?)

Answer 1

For question 1 in the general case ($P$ and $Q$ may have coefficients involving other variables), we're looking to determine if $P$ has a root that $Q$ does not have. This is equivalent to $\neg (P | Q^{\text{deg } P})$ (this is clear if one imagines $P$ and $Q$ written in fully factored form).

The algorithm for determining this is as follows:

First, calculate $Q^{\text{deg } P}$ using the algorithm for multiplying polynomials together.

Next, perform polynomial long division (https://en.wikipedia.org/wiki/Polynomial_long_division). As the coefficients of $P$ and $Q^{\text{deg } P}$ may involve other variables, every term showing up in the polynomial long division may involve other variables.

The polynomial long division algorithm involves checking if various terms are $0$, so at every such point we must branch into ($t(y_1,\ldots,y_n) = 0$ AND the result of continuing the division algorithm assuming the term is $0$) OR ($t(y_1,\ldots,y_n) \neq 0$ AND the result of continuing the division algorithm assuming the term is not $0$)

At the end, you will obtain an algebraic expression for the remainder: a polynomial whose coefficients are terms in the other variables. For divisibility, this remainder must be $0$, so all of its coefficients (which are terms in the other variables) must be $0$.

To really understand this, it helps to manually carry out one of these polynomial long divisions. Let's try to determine if $x^2+ax+b$ divides into $x^3+cx^2+dx+e$. First, we know that the quotient starts with $x$, so we multiply $x$ by $x^2+ax+b$ and subtract from $x^3+cx^2+dx+e$ to get $(c-a)x^2 + (d-b)x + e$. At this point, we should branch based on whether $c-a = 0$ or not, but we handle these similarly enough: the resulting quotient is $x + (c-a)$ with a remainder of $$(c-a)x^2+(d-b)x+e $$$$- ((c-a)x^2+ (c-a)ax + (c-a)b)$$ $$= (d-b-ca+a^2)x + (e-cb+ab)$$ So we have divisibility if $d-b-ca+a^2 = 0$ and $e-cb+ab=0$.

Answer 2

I'm not sure this is a complete answer to your question (in particular, I don't work out any examples), but I have a number of comments to make, which I hope will be helpful. Let me first point out that whenever we want to eliminate quantifiers, we can focus our attention on a very special case.

A primitive existential formula is one of the form $\exists x\, \bigwedge_{i<n} \varphi_i(x,\overline{y})$, where $x$ is a single variable, $\overline{y}$ is a tuple of variables (possibly empty), and each $\varphi_i$ is an atomic or negated atomic formula.

Claim: Suppose that every primitive existential formula is $T$-equivalent to a quantifier-free formula. Then $T$ has quantifier elimination.

Proof: By induction on the structure of formulas. It suffices to handle inductive steps for the boolean connectives $\land$, $\lor$, and $\lnot$, and the existential quantifier $\exists x$, since we can rewrite $\forall x$ as $\lnot \exists x \lnot$. In the base case, every atomic formula is already quantifier-free, and the induction steps for the boolean connectives are trivial. So suppose we have $\exists x\, \varphi(x,\overline{y})$. By induction, we can assume $\varphi$ is quantifier-free. Writing $\varphi$ is disjunctive normal form, we have $\exists x\, \bigvee_{j<m}\bigwedge_{i<n_j} \psi_{i,j}(x,\overline{y})$, where each $\psi_{i,j}$ is atomic or negated atomic. Since $\exists$ distributes over $\vee$, this is equivalent to $\bigvee_{j<m}\exists x\, \bigwedge_{i<n_j}\psi_{i,j}(x,\overline{y})$, and by hypothesis each primitive existential formula $\exists x\, \bigwedge_{i<n_j}\psi_{i,j}(x,\overline{y})$ is equivalent to a quantifier-free formula, so we're done.

---

Now when $T$ is $\mathsf{ACF}$, an atomic formula is equivalent to $p = 0$, where $p$ is some polynomial with coefficients in $\mathbb{Z}$, and a conjunction $\bigwedge_{i<n} p_i \neq 0$ is equivalent to the single negated atomic formula $\prod_{i<n}p_i \neq 0$. So every primitive existential formula is equivalent to $\exists x\, (p(x,\overline{y}) \neq 0\land \bigwedge_{i<n} q_i(x,\overline{y})= 0)$. The upshot is that on very general grounds, eliminating quantifiers for $\mathsf{ACF}$ reduces to something very close to the special case you ask about in your Question 1.

In both Question 1 and Question 2, you seem to only be thinking about sentences, i.e., formulas with no free variables. E.g., in Question 2, you say that you're working with "polynomial equalities involving integers and the bound variables". But quantifier elimination is much stronger than this: it applies to formulas with free variables as well (and in fact we need this for the induction argument above, to handle formulas with multiple quantifiers). That is, we are trying to come up with quantifier-free conditions on the variable coefficients of our polynomials to ensure that there is some solution to our system of polynomial equations and inequations. Other than omitting the free variables, your understanding in Question 2 is correct.

---

Now for Question 3: There are two ways to go to show that ACF eliminates quantifiers from primitive existential formulas.

The hard route is to give an explicit algorithm - this will inevitably involve some clever uses of the division algorithm in multivariate polynomial rings. It has been a while since I've been through a proof, but I don't recall any particular step standing out as the non-trivial one. It's just good old-fashioned hard work, you might say. Maybe others can say something more helpful. The Math Overflow question you linked to has a number of references to this approach.

The easy route is to use model-theoretic compactness. This approach is given almost any introductory model theory textbook. It reduces the problem to showing that if $F$ and $F'$ are sufficiently saturated algebraically closed fields (i.e., of uncountable transcendence degree over the prime field) and $k$ is a countable common subfield of $F$ and $F'$, then for any $a\in F$, there exists $b\in F'$ such that $k(a)$ is isomorphic to $k(b)$ by an isomorphism fixing $k$. And this is essentially obvious, breaking into two cases depending on whether $a$ is algebraic or transcendental over $k$, and using the fact that $F'$ is algebraically closed and contains elements transcendental over $k$.

The drawback of the compactness approach is that it is non-constructive, i.e., it proves that every formula has a quantifier-free equivalent, but it doesn't tell you how to actually find the quantifier-free formula. Henry Towsner has a very nice recent preprint in which he explains how to extract algorithms from proofs of quantifier elimination using the compactness theorem.

Answer 3

Let me give a simple example of what one step of a quantifier elimination algorithm could look like. The basic idea is that in a generic case, an ideal of $\mathbb{F}[x_1, \ldots, x_{n-1}, x_n]$ will reduce to an ideal of $\mathbb{F}(x_1, \ldots, x_{n-1})[x_n]$ which must be a principal ideal $\langle p \rangle$. Then, the fact that $\mathbb{F}$ is algebraically complete will allow us to eliminate $(\exists x_n) (p(x_1, \ldots, x_{n-1}, x_n) = 0)$ to true if $p$ is nonconstant or $p=0$, or to false if $p$ is nonzero constant. And we will see that also in the exceptional cases, we can make progress on eliminating $x_n$.

So, the example I will have in mind will be the first step in using quantifier elimination to "prove" the formula $(\forall x)(\forall y)(\forall z) (xz = y^2 \leftrightarrow (\exists t)(\exists u) (x=t^2 \land y=tu \land z=u^2))$. Here, the lowest level quantifier to eliminate will clearly be $(\exists u) (x=t^2 \land y=tu \land z=u^2)$. This is already in a disjunctive normal form (in general, the first step will be to rewrite to such a form), so let us proceed.

Since the $x=t^2$ term does not involve $u$, let us move that out and concentrate on trying to make $\langle tu - y, u^2 - z \rangle$ into a principal ideal. Now, in the generic case, we could consider dividing the first generator by $t$ and then doing a polynomial division of $u^2 - z$ by $u - t^{-1} y$. To simplify the notation a bit and avoid needing to introduce an inverse, I'll instead observe that if $t \ne 0$, then multiplying the second generator by $t$ does not change the ideal, so $\langle tu - y, u^2 - z \rangle = \langle tu - y, tu^2 - tz \rangle = \langle tu - y, yu - tz \rangle = \langle tu-y, tyu - t^2 z \rangle = \langle tu-y, y^2 - t^2 z \rangle$. At this point, a more automated algorithm might break into cases depending on whether $y^2 - t^2 z$ is zero or nonzero. However, since $y^2 - t^2 z$ no longer dependent on $u$, I'll stop here and declare that in the case $t \ne 0$, the existence quantifier is equivalent to $x - t^2 = 0 \land y^2 - t^2 z = 0$.

On the other hand, in the case $t = 0$, the ideal generators reduce to $\langle -y, u^2 - z \rangle$. At this point, we are again close enough to a principal ideal that in this case, the existence quantifier is equivalent to $x-t^2 = 0 \land -y = 0$.

So in summary, we have that $(\exists u)(x=t^2 \land y=tu \land z=u^2)$ is equivalent to $(t\ne 0 \land x-t^2 = 0 \land y^2 - t^2 z = 0) \lor (t=0 \land x-t^2=0 \land -y=0)$.

---

Hopefully, this will give a fairly good idea of how the algorithm might work in general. As for why the algorithm should run in finite time in general: each time you do a division algorithm step, or you reduce one of the leading terms of a generator to zero, you will decrease the sum of the $x_n$-degrees of the generators.

---

I do see that having an inequality part of one of the conjunctions could complicate things a bit: for example $(\exists t) (t \ne 2 \land t^2 - 4t + 4 = 0)$ should eliminate to $\bot$. In this case, you can still run the above elimination algorithm on the ideal corresponding to the equality parts, and eventually in each branched case you will get to a conjunction of an inequality, and some number of equalities out of which at most one will involve $x_n$. At this point, you can move out the equalities not involving $x_n$, and proceed to use the algorithm described in the answer by TomKern.