4
$\begingroup$

I am currently helping teach a course about foundations of mathematics, which has thus far focused mostly on propositional and first-order logic. As part of the course, the students are each required to present a lecture about a specific piece of material. We recently had a student "prove" quantifier-elimination in algebraically closed fields, which I will take to mean:

Theorem: Any elementary predicate in the theory of algebraically closed fields is equivalent to a quantifier-free one.

While the student's talk was a reasonable attempt, it was quite inundated with terminology and equivalences they didn't prove, so I don't think the other students got much out of it. Because of this, I am trying to adapt this proof into a more hands-on assignment. Unfortunately, logic is not my area of expertise and I have not been able to find an elementary proof that is also short enough for an assignment. The closest I have been able to come is Swan’s proof of Theorem 3.2 given here; although each step is certainly within my students' reach, it is probably overall too long.

I have heard that Tarski's original proof was quite hands-on, but also that he never published it. Does anyone know of somewhere I could find Tarski's original proof? Barring that, does anyone know of another proof of this theorem that does not require any high-level machinery, but that is also short enough to constitute an undergraduate-level assignment? Any suggestions are much appreciated.

Improve this question
$\endgroup$
2
  • $\begingroup$ This will probably be unhelpful for your purposes, but you can also approach using basic algebraic geometry. The statement is equivalent to the stability of constructible subsets of affine spaces over an algebraically closed field under projections $\mathbb{A}^{n+m}_k\to \mathbb{A}^{n}_k$. This follows from Chevalley's theorem. $\endgroup$
    – Donu Arapura
    Commented Apr 30, 2022 at 14:53
  • $\begingroup$ Chevalley's theorem is essentially the same thing as Tarski's theorem. We should really call both of them "Tarski-Chevalley" or something. $\endgroup$
    – Erik Walsberg
    Commented May 1, 2022 at 2:52

2 Answers 2

Reset to default
5
$\begingroup$

I doubt you’ll find a shorter proof than Swan’s which is equally elementary. In particular:

  • For algebraically closed fields, you can stop in the middle of page 10 of the document, which should make it less overwhelming.
  • Tarski’s published papers on this are longer and more difficult to read (or were for me), and his unpublished papers were probably worse.

But an assignment need not give the whole proof, especially since there is such a nice algorithm. So you might ask:

  • What is the result of eliminating quantifiers in these sentences? $$(\forall x)(ax^2+bx+c=0\implies dx^2+ex+f=0)$$ $$(\forall x)(\exists y)(ax+by=c \wedge dx+ey\neq f)$$
  • Which results in Swan’s paper describe which steps of your eliminations?
  • What are non-trivial examples for each step in Swan’s proof?
Improve this answer
$\endgroup$
3
$\begingroup$

Passmore's PhD thesis has an introductory section developing an elementary quantifier elimination algorithm for algebraically closed fields of characteristic zero "from scratch" with much detail. It is based on Muchnik's method, which is similar in many ways to Cohen's Q.E. method for real closed fields. (In fact, with a few modifications and extensions, it is then developed into a Q.E. procedure for real closed fields in a subsequent section).

Thesis: https://www.cl.cam.ac.uk/~gp351/passmore-phd-thesis.pdf

He also has a separate expository note "Understanding Algebro-Geometric Quantifier Elimination: Part I, Algebraically Closed Fields of Characteristic Zero via Muchnik" on this: https://www.cl.cam.ac.uk/~gp351/acf-qe.pdf

I know many people have implemented the method in code using this as a basis, so it is in a lot of detail!

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .