§ Quantifier Elimination For Algebraically Closed Fields

• (C, +, ., 0, 1).
• First reduction, see what we only need to eliminate existentials, since we can convert ∀x,P(x) into !(∃x, !P(x)).
• Next, we write P(x) is disjunctive normal form, so we get ∃x, P1(x) \/ P2(x) \/ ... Pn(x), where each Pi is CNF.
• Now, this can be rewritten as (∃ x1, P1(x1)) \/ (∃x2, P2(x2)) \/ ....
• So, we really just need to solve ∃ xi, Pi(xi) where Pi is a conjunction of atomic predicates.
• Now, we have an equation like p(x, y) = q(x, y), but this is ofc the same as p(x, y) - q(x, y) = 0.
• In general, we can convert stuff into f = 0 or f != 0.
• If we have many polynomials f1(x, y0, ... yn) = 0, f2 (x, y0, ... yn) = 0, ... fi (x, y0, ... yn) = 0, then we can find the greatest common factor of these, where we treat them as polynomials in x with coefficients in C[y0, ... yn].
• Call this as p for the greatest common factor of f1, ... fi. So we now write this as p = 0.
• To combine f(x, y0, ... yn) != 0 with f2(x, y0, ... yn) != 0, we just say that their product is not equal to zero. Call the combined polynomial q.
• So, after the redn, we are trying to solve, ∃ x, P(x) = 0 /\ Q(x) != 0.
• That is, is there a root of P that is not a root of Q.
• Let's suppose we can factorize these, so then we are checking:

∃ x, a(x - r0)^e0 (x - ri)^ei /\ b(x - s0)^f0 (x - sj)^fj

• If p divides q^(deg p), where p is considered a polynomial in x, then every root of q is a root of p ?
• Of course, the question is, why does this suffice?

§ References

• Thomas Kern