Regular Languages and Model Theory 21: Quantifier Elimination on Fields

In this video, I introduce the concept of quantifier elimination, and show that the complex numbers with + and * has quantifier elimination. I also demonstrate Sturm's Theorem, which plays a critical role in the quantifier elimination procedure for the real numbers.

The literature will very often talk about quantifier elimination on algebraically closed fields (of characteristic 0) or real closed fields. These are the classes of structures that are first-order equivalent to the complex or real numbers respectively, so one is essentially just studying the first-order logic of the complex or real numbers.

The lecture notes below discuss some of the geometric applications of the decision procedure for the real numbers, and a proof of Sturm's theorem and quantifier elimination on the reals:

Note that there are also applications of the decision procedure for the real numbers to analysis: the epsilon-delta definition of a limit (of polynomials) can be expressed in this first order logic.

00:00 Quantifier Elimination
12:38 Complex Numbers
31:16 Real Numbers
35:38 Sturm's Theorem

[shift_reset]

The first time I heard about Quantifier Elimination over C, I didn't really quite understand the point of it, but now I'm seeing a connection with all the neat Grobner basis stuff I learned about during the summer after my undergrad

[TheKivifreak]

So the formula boils down to saying that p and q share no common root:
/\ /\
/ i \ / j \ r_i (y0, .., yn) ≠ s_j(y0, ..., yn)
which is equivalent to saying:
not p divides q^(deg(p))

I can see that we can implement polynomial divisibility on a turing machine if we have the factors of the polynomial a_m x^m + ... + a_1 x + a_0. I think it's also possible to create a boolean circuit for this given a bounded size of factors.
We then need to find a symbolic expression of the factors a_i of the polynomials p and q with free variables y0, .., yn and +, *. This symbolic equation can then be turned into a boolean circuit I believe.
With this, I think I understood the proof.
But it's not as simple as implementing long division on a turing machine, since Gödels beta is not quantifier free and we relied on Gödels beta to (run/check the halting property) of a turing machine.
Thanks again for communicating such a mind-blowing fact!

[tuongnguyen]

Oh damn can you do something about cylindrical algebraic decomposition ?