I would like some predicates in the language of first order Peano arithemetic (PA) that are true for the standard natural numbers and false for other types of numbers like negative numbers, fractions, irrational numbers, etc. An example would be Lagrange's four square theorem.
$P(x) = \exists a \exists b \exists c \exists d(x=a\cdot a + b\cdot b + c \cdot c + d \cdot d)$
This predicate is true for non-negative integers but false for negative integers.
I actually want to work in Modular arithmetic (MA). MA has the same axioms as PA except $\forall x(Sx \neq 0)$ is replaced with $\exists x(Sx=0)$. MA has the same language as PA, $(0, S, +, \cdot)$. Order, $\leq$, is not defined in MA so I don't what predicates that use it.
These predicates can be used to prove certain sets are not models of MA. The four square theorem can be used to prove $\mathbb{Z}$ is not a model of MA. We can prove $\forall x (P(x))$ using induction which is clearly false for $\mathbb{Z}$. I am looking for other theorems like the four square theorem. Maybe something based on the binomial theorem. Some of the rings thought to be models of MA include $\mathbb{Z} /n \mathbb{Z}$, any algebraically closed field, and $Z_2$.
Response to Asaf Karagila
I am working in the first order theory Modular arithmetic (MA). I think of MA as an alternate definition of the natural numbers. I am interested in MA as a tool for proving PA is inconsistent. It is well suited for this task. MA has finite models so it is hard to argue it is inconsistent. MA has the same signature as PA and almost all of the same axioms. MA is $\omega$-inconsistent and every infinite model has non-standard elements. MA is not well ordered or well founded.
MA is basically commutative ring theory with first order induction. Induction is valid in surprisingly few commutative rings. Induction fails in $\mathbb{Z}, \mathbb{Q}$, and the Gaussian integers.
I would be interested in a predicate that identified $\mathbb{Z}$ inside $Z_2$. I could combine such a predicate with the four square theorem to indentify the non-negative integers. Such a combined predicate would prove $Z_2$ is not a model of MA.
Because MA has finite models, I only need a predicate that allows me to prove the model is not finite. For example, if $P(x)$ is only true if $x$ is a particular irrational number, I could use $P(x)$ to prove $\mathbb{C}$ is not a finite model of MA.
This is another example of what I am looking for. This statement can only be true in an infinite model of MA:
$\forall x \exists y(S0 \neq 0 \land SS0 \neq 0 \land x = y \cdot y)$.
I have to eliminate the trivial ring and $\mathbb{Z} /2 \mathbb{Z}$. Any statement which is true in only a finite number of finite rings but true in an algebraically closed field or $Z_2$ would be acceptable.