I would like to know if the following statement is true in the 2-adic integers.
$\forall n( n=0 \lor Ex( (x \neq 0 \land x+x=0 \bmod n) \lor (x+x=1 \bmod n) ))$
I will define a modulo predicate as:
$M(x,n,r) := (n=0 \lor Ey(x=yn+r))$
$\forall n( (n=0 \lor Ex( x \neq 0 \land M(x,n,0)) \lor M(x,n,1) ))$
Would my expression be false for some n = an irrational 2-adic integer?
Edit: The second statement should be
$\forall n( n=0 \lor Ex( (x \neq 0 \land M(x+x,n,0)) \lor M(x+x,n,1) ))$
In response to anon.
I may be totally confused, but I think part of your argument implicitly assumes $Z_2$ has an "odd" number of elements. The number of elements in $Z_2$ is neither even nor odd. $\exists x(x \neq 0 \land x+x = 0) \overline{\vee} \exists x(x+x = 1)$ is false in $Z_2$.
You state "If $n$ is even with $n=2m$ then $x=m$ is a solution to $2x \equiv 0$." This statement is false in rings with an odd number of elements because every element is both even and odd "inside" the ring. Even numbers in an even size ring have two solutions to $n=2m$ and only one of these solutions satisfy my expression (in rings with more than 2 elements). Consider the ring $\mathbb{Z} /10 \mathbb{Z}$ and let $n = 8$. There are two solutions to $8=2m$ inside the ring.
$9 + 9 = -1 + -1 = 8 = -2 \bmod 10$ and $4 + 4 = -6 + -6 = 8 = -2 \bmod 10$ However, only $4+4 = 0 \bmod 8$. $9+9 = 2 \bmod 8$ is not a solution to my expression.
Now consider the ring $\mathbb{Z} /11 \mathbb{Z}$ and let $n=9$. There is one solution to $9 = 2m$.
$10 + 10 = -1 + -1 = 9 = -2 \bmod 11$ Clearly, $10 + 10 \neq 0 \bmod 9$.
Let $n = -2 \in Z_2$. $-2$ is even "inside" $Z_2$ because the $2^0$ bit is $0$. Your argument says because $-2 = -1 + -1$ then $x = -1$ is a solution to $2x \equiv 0$. I think $-1 \equiv 1 \bmod -2$ is a theorem. $-1 + -1 \equiv 2 \bmod -2$. Would this mean $Z_2 \bmod -2 \in Z_2 \equiv \mathbb{Z} /2 \mathbb{Z}$?
I have to apologise. I've realized I need to make one of my assumptions more explicit.
$\forall n( n=0 \lor Ex( (x \neq 0 \bmod n \land x+x=0 \bmod n) \lor (x+x=1 \bmod n) ))$
I am sorry for any confusion my omission may have caused. $x \neq 0 \bmod n$ is an important part of my definition of even because it removes solutions of the form $0=0+0$. anon's post helped me figure out where the mis-communication occurred and I hope he will respond to this new constraint on the problem.