# Elimination of quantifiers for $\exists x\ x^2=y$

Consider the formula $\exists x\ x^2=y$ with free variable $y$. We know that it is equivalent in $Th(\mathbb R,+,0,\cdot,1, \geq)$ (the complete theory of the ordered field $\mathbb R$) to $y\geq 0$. Now I have been told that such elimination of quantifiers cannot be performed in $Th(\mathbb R, 0,1,+,\cdot)$, i.e. without using order.

I have tried to convince myself of this, and, intuitively, I sort of understand it. But can someone give me a precise proof of this fact?

• (what is $Th$?) Commented Sep 5, 2017 at 15:05
• The complete theory of the ordered field $\mathbb R$: edited. Commented Sep 5, 2017 at 15:08
A quantifier-free assertion about $y$ in the language of $\{0,1,+,\cdot\}$ is a Boolean combination of polynomial equations in $y$ with natural number coefficients. Since every such equation has either at most finitely many solutions or every number as a solution, it follows that every set definable by such a Boolean combination of polynomial equations in $y$ is either finite or cofinite in the reals. Thus, we cannot define the positive numbers in this way, and in particular, there is no quantifier-free way to express the assertion $\exists x\ x^2=y$ of your title.