Modular arithmetic (MA) has the same axioms as first order Peano arithmetic except $\forall x(Sx \neq 0)$ is replaced with $\exists x(Sx = 0)$. MA has finite models and every infinite model of MA must have non-standard elements. In Even XOR Odd Infinities? I asked if every model of MA is exclusively even or exclusively odd. I asked if this statement is a theorem of MA:
1) $\exists x(x \neq 0 \land x+x = 0) \overline{\vee} \exists x(x+x = 1)$
The answer was no. Emil Jeřábek showed the 2-adic integers, $Z_2$, are a model of MA and the above statement is false in $Z_2$. Now, I am interested in whether the following statement is a theorem of first order PA:
2) $\forall x(x = 0 \lor (\exists y(y \neq 0 \land (x = y+y \lor Sx = y+y))))$
Is statement (2) a theorem of first order PA? If so, does this mean any proof of (2) in first order PA must use the axiom $\forall x(Sx\neq 0)$? Notice that statement (2) is false for $-1$ in $Z_2$ and (2) is not a theorem of MA. Is it possible there are non-standard models of PA with elements that are neither even nor odd?
I am accepting the answer that (2) is provable using induction. I want to show why.
Let $P(x) = (x = 0 \lor (\exists y(y \neq 0 \land (x = y+y \lor sx = y+y)))$.
Obviously, $P(0)$ is true. The induction schema also requires we prove $\forall x(P(x) \rightarrow P(S(x)))$. Notice I have defined two successor functions. $sx$ is in the definition of $P(x)$ and $S(x)$ is used in the induction axiom. It is easier to break the proof into parts.
Consider the case where $\exists y(sx = y+y)$. Then we have $(sx=y+y) \rightarrow (S(x)=y+y)$. Since the two successor functions are equal this part of the proof only requires the axiom of equality. This part of the proof works in both PA and MA.
Next, consider the case $\exists y(y \neq 0 \land x=y+y)$. Now:
$(y \neq 0 \land x=y+y) \rightarrow (sy \neq 0 \land sS(x)=sy+sy)$.
This can be proven in PA, but not in MA because of the $sy \neq 0$ in the induction step. We can prove $sy \neq 0$ in PA using the axiom $\forall x(sx \neq 0)$. The rest of the statement can be proven using the axiom $\forall x \forall y(x+S(y) = S(x+y))$. Combining the cases we have a proof of $\forall x(P(x) \rightarrow P(S(x)))$ in PA.
I find it interesting we need the axiom $\forall x(sx \neq 0)$ to prove every natural number is even or odd.
Statement 2 is a theorem of first order PA. It is true for $x=0$ and $x=S0$ by inspection. Then if it is true for $k$, there is a witness $y$ and either $y$ or $y+1$ is a witness for $k+1$. Given that it is a theorem of PA, it is true for all nonstandard elements as well. Since we have a hard time describing a nonstandard element, we have a hard time deciding whether it is even or odd, but it is one of those.