§ Quantifier Elimination for Real Closed Fields

§ Why do we need <=?

• For a quick intution, suppose we want to know if ∃ x, ax^2 + bx + c = 0.
• We know that this is true only when b^2 - 4ac >= 0.
• Bu this needs us to have the >= symbol.
• If we try to define it, then we can do x >= y := ∃ s, x = y + s^2, but this now costs us a quantifier! So we cannot do quantifier elimination for this.

§ Why do we need <=, example 2

• Consider the question ∃ x, x^2 = y.
• The answer is literally y >= 0, which needs a >=.

§ Real Closed Fields

• (R, +, -, 0, 1, <=)
• By the usual reduction, we need to be able to eliminate ∃ x, p(x, y0, ... yn) = 0 /\ q(x, y0, ..., yn) != 0 /\ r(x, y0, ... yn) >= 0 /\ s(x, y0, ... yn) <= 0.

§ Sturm's Theorem / Sturm Sequences

• Let p0 = p.
• Let p1 = p'.
• Let p2 = - (p0 % p1). (It can't be p1 % p0 since deg(p1) < deg(p0)).
• Let V(x) be the number of sign alternations when we plug in X.
• Then V(a) - V(b) is the number of distinct real roots of p between a and b.