Modular arithmetic (MA) has the same axioms as first order Peano arithmetic (PA) except $\forall x(Sx \neq 0)$ is replaced with $\exists x(Sx=0)$. In Even XOR Odd Infinities? 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. One counter-example was the 2-adic integers, $Z_2$. There is no 2-adic integer, $m \neq 0$, such that $2m=0 \lor 2m=1$. Notice both sides of statement (1) are false in $Z_2$. Statement (1) is not a theorem of MA even if I weaken the $\overline{\vee}$ to $\lor$. Consider this second statement:
2) $\forall x(\exists y(y+y=x) \lor \exists y(y+y+1=x))$
There are numerous inductive proofs in PA of statement (2) on the internet. I have always assumed the universe of any model of MA is an initial segment of some model of PA. Let $M_2$ be a model of PA that has $Z_2$ as an initial segment. I don't see how statement (2) can be true in $M_2$. Let $m \in M_2$ be the non-standard natural number that corresponds to -1 in a $Z_2$ model of MA. We know $\forall x((x=0 \lor x+x \neq Sm) \land (x+x \neq SSm))$. This means $SSm$ is not even and, since $Sm$ is not even, $SSm$ can't be odd.
My question is whether $Z_2$ is an initial segment of some model of PA? If so, is statement (2) true in this model?
I previously asked this question on Stack Exchange.