Is there any recursive definition, using only addition, of the set of values of $x^2+y^2$?

233 Views Asked by At

There is a recursive definition of the set of squares which uses only addition:

$CS(x,y) := IS(x) \wedge IS(y) \wedge x \lt y \wedge \forall z: (x \lt z) \wedge (z \lt y)⇒\neg IS(z)$

$IS(x)⇔ x=0 \vee x=1 \vee \exists y: \exists z: (CS(z,y) \wedge IS(y) \wedge (\forall z: (y < z \wedge z < x) ⇒ \neg IS(z)) \wedge x + z = y + y + 2)$

($IS$ stands for IsSquare, $CS$ stands for ConsecutiveSquares.)

Expanding $CS$ in terms of $IS$ gives an axiom in the language:

$IS(x) ⇔x=0 \vee x=1 \vee

\exists y: \exists z: (IS(z) \wedge IS(y) \wedge z \lt y \wedge \forall w: (z \lt w) \wedge (w \lt y)⇒\neg IS(w)) \wedge IS(y) \wedge

(\forall z: (y < z \wedge z < x) ⇒ \neg IS(z)) \wedge

x + z = y + y + 2

$

This seems to generalize to a recursive definition, using only addition, of the set of values of any univariate polynomial. Formally I am considering Presburger arithmetic with a unary predicate and associated axioms, yielding an incomplete system in this case.

There are other unary predicates which result in a complete theory. But my question is:

Is there any recursive definition, using only addition, of the set of values of $x^2+y^2$? If so, does it yield an incomplete system? Otherwise, how to prove that such a definition does not exist?

I recently asked "Is there no univariate integer polynomial that takes on the same positive values as the multivariate polynomial $x^2+y^2$? and accepted an answer but I don't understand how to apply it to this situation.