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](http://www.math.uchicago.edu/%7Eswan/expo/Tarski.pdf); 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.



Tarski's original proof of quantifier elimination in algebraically closed fields
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?


