Given the structure $(\mathbb Z,+,-,\times,0,1)$, what's the easiest way to write "$x\ge0$" in that structure?
I know that this works: $$\exists a\exists b\exists c\exists d,a^2+b^2+c^2+d^2=x$$ because of Lagrange's four-square theorem, but this seems like an unnecessarily complicated way to do it (because the theorem is such a nontrivial result). Is there an easier way?
On
I don't know of any more elementary definition of $x\geq 0$.
You can think of this definition as a generalization of the obvious definition of $x\geq 0$ in $(\mathbb{R},+,-,\times,0,1)$: $$\exists y\, y^2 = x.$$
The problem, of course, is that not every positive element in $\mathbb{Z}$ has a square root. $\mathbb{Z}$ is a much more complicated structure than $\mathbb{R}$, and it's not surprising that nontrivial number theory gets involved when you start writing down formulas with quantifiers in $\mathbb{Z}$.
An integer $d$ is $\ge 0$ if it is a perfect square or there exist integers $x$ and $y$ such that $xy\ne 0$ and $x^2-dy^2=1$. Here we are appealing to the theory of the Pell equation instead of the Lagrange four squares theorem. Arguably more complicated!