A neat trick to distinguish integers

Something neat from Hector Pasten’s talk at the CYMS seminar: suppose that we want to give a formula for the statement “$x \neq y$” where $x$ and $y$ are integers, but we want to do so in a positive existential system, i.e., using only the defined arithmetical operations $(+,\times,=)$ and the existential quantifier $\exists$. In particular, we can’t use negation or the universal quantifier $\forall$.

At first glance, this might seem difficult – how do we express the concept of “not equal” without using “not”? However, there is a very nice trick. First, observe that $$ x \neq y \iff x-y-1 \ge 0 \vee x-y-1 \le 0. $$ We’ve changed the problem from defining $x \neq y$ to the problem of defining “$x \ge 0$” (in a positive existential way). Recall Lagrange’s Four Square Theorem:

Theorem (Lagrange’s Four Square Theorem)

Every nonnegative integer $n \in \mathbb{N}$ may be written as a sum of four squares: $$ n = x_1^2 + x_2^2 + x_3^2 + x_4^2 \quad x_i \in \mathbb{N}. $$

So, we can write: $$ x \ge 0 \iff \exists x_1,\ldots,x_4 ( x = x_1^2 + x_2^2 + x_3^2 + x_4^2) $$ which, in turn, gives us our desired positive existential formula for $x \neq y$.