Is the formula $\exists x : x^2-a=0$ not downward absolute over the theory of field of rational numbers?

Question

The ordered field $(\mathbb{R},+,\cdot,<,0,1)$ and the field $(\mathbb{C},+,\cdot,0,1)$ have quantifier-free criteria to determine the existence of the square root of a given number. However, the field of rational numbers seems not to be the case.

I tried to prove it really does, that is the field of rational numbers (with ordering) really does not have a quantifier-free criteria to determine the existence of a square root. My attempt is as follows: if there is a quantifier-free criteria, then the formula $\exists x :x^2-a=0$ would be downward absolute among models of the theory of the field of rational numbers $(\mathbb{Q},+,\times, 0,1,<)$. My first idea is to construct two models $\mathfrak{A}$ and $\mathfrak{B}$ such that

1. $\mathfrak{A}\subseteq \mathfrak{B}$ are models of $\operatorname{Th}(\mathbb{Q},+,\cdot,0,1,<)$ and
2. there is $\epsilon \in \mathfrak{A}$ such that $\epsilon$ has a square root over $\mathfrak{B}$, but not over $\mathfrak{A}$.

However I failed to construct these models. I have tried to realize my idea by showing $\mathbb{Q}(\epsilon)$, an ordered field with "infinitesimal" is elementarily equivalent to $\mathbb{Q}$, but it seems not to work well. I would appreciate any help, thanks.

Answer 1

Your idea about $\mathbb{Q}(\epsilon)$ is a good one, and we can make it work with a bit of compactness.

First, by compactness we have that the theory $$T=Th(\mathbb{Q})\cup\{\epsilon>0\}\cup\{\epsilon<{1\over n}:n\in\mathbb{N}\}\cup\{\forall x: x^2\not=\epsilon\}$$ is consistent. Let $M\models T$.

Now we want to "give $\epsilon^M$ a square root." This is going to be another compactness argument: we need $$T'=Th(\mathbb{Q})\cup QF(M)\cup\{\exists x(x^2=\epsilon^M)\}$$ to be consistent, where $QF(M)$ is the quantifier-free diagram of $M$. The key point here is that for every finite set of quantifier-free sentence about $\epsilon^M$, there is a rational satisfying that same set of sentences which has a square root. (Basically, to rule that out in a quantifier-free way we'd have to declare that $\epsilon^M$ is one of finitely many actual rationals.) So by compactness $T'$ also has a model.