Is there a first order formula $\varphi[x]$ in $(\mathbb Q, +, \cdot, 0)$ such that $x≥0$ iff $\varphi[x]$?

Question

In the first-order language $\mathscr L$ having $(+, \cdot, 0)$ as signature, it is easy to define a formula $\phi[x]$, namely $\exists y \; x = y^2$, satisfying : $$\text{for all } x \in \Bbb R, \quad x \in \Bbb R_+ \;\text{ if and only if} \;\; \phi[x] $$

My question is : what happens if I replace $\Bbb R$ by $\Bbb Q$ ? More precisely :

Is there a first-order formula $\phi[x]$ of $\scr L$, such that $$\text{for all } x \in \Bbb Q, \quad x \in \Bbb Q_+ \;\text{ if and only if} \;\; \phi[x] $$

Said differently, I would like to know if the set of the positive rationals is definable in that language. Related questions are, for instance : (1), (2).

I don't know if the $\scr L$-structure $(\Bbb Q, +, \cdot, 0)$ admits elimination of quantifiers. If this is the case, then this could be helpful ; see this answer.

Thank you for your comments !

Answer 1

Yes. Every rational number $\ge 0$ is the sum of four squares. This is easily derived from Lagrange's Theorem which says that every non-negative integer is the sum of four squares.

Note that the formula we get is existential.

Answer 2

It is a famous result of Julia Robinson that $(\Bbb{Q}, +, \cdot, 0)$ is undecidable. This implies that $(\Bbb{Q}, +, \cdot, 0)$ does not admit elimination of quantifiers. That the rational numbers are not definable in the first-order theory of the reals follows from this, but also follows from well-known facts about O-minimality of the first-order theory of the reals