I don't understand how the theory of algebraically closed fields admits quantifier elimination

Question

I was reading the wiki page about quantifier elimination and it says that the theory of algebraically closed fields is decidable using quantifier elimination, what I understand by this is that all the formulae about that theory has an equivalent formula without quantifiers, but I don't really understand how this is possible, could someone explain to me what this concept really means, and how it can be applied to some theory?

Answer 1

Here is an example of quantifier elimination in action in the case of algebraically closed fields. Consider the question of whether a polynomial (of degree $3$, say) has a root. We can express this as a formula in the first-order language of rings (which is usually taken to consist of binary operations $+$ and $\cdot$, a unary operation $-$, and constants $0$ and $1$) as $$\exists x (ax^3+bx^2+cx+d=0).$$ Here $a$, $b$, $c$, and $d$ are all free variables. Quantifier elimination says that the condition on $a$, $b$, $c$, and $d$, that a root exists can be expressed in the language of rings without using any quantifiers. How do we do this? Well, because we are in an algebraically closed field, we just need to know that the polynomial is not a nonzero constant, that is: $$\neg (a=0)\vee \neg (b=0)\vee\neg(c=0)\vee (d=0).$$

Or for a slightly more complicated example, consider the formula $$\exists x\exists y (ax^2+bx+c=0)\wedge (ay^2+by+c=0)\wedge\neg(x=y)$$ with free variables $a$, $b$, and $c$. This says that a quadratic polynomial has two distinct roots. In this case, we know that this is equivalent to the discriminant being nonzero (and also $a$ being nonzero, or else all the coefficients being zero), i.e. $$(\neg(a=0)\wedge\neg(b^2-4ac=0))\vee((a=0)\wedge(b=0)\wedge(c=0)).$$

In general, a quantifier-free formula must just be a Boolean combination of equations between polynomials in the free variables. Quantifier elimination says that any first-order formula in some free variables is equivalent to such a quantifier-free formula. This is a very strong and not at all obvious statement! For the examples above it was easy, but if I give you some really complicated statement with 12 nested quantifiers, it's quite impressive to know that it is equivalent to some equalities and inequalities between polynomials in the free variables!