Modular Arithmetic (MA) has the same axioms as first order Peano Arithmetic (PA) except $\forall x (Sx \ne 0)$ is replaced with $\exists x(Sx = 0)$.
(http://en.wikipedia.org/wiki/Peano_axioms#First-order_theory_of_arithmetic).
MA has arbitrarily large finite models based on modular arithmetic. All finite models of MA have either an even or odd number of elements. I call a model of MA "even" if it satisfies both of these two sentences:
E1) $\exists x(x \ne 0 \land x+x = 0)$
E2) $\forall x(x+x \ne S0)$
A model of MA is odd if it satisfies both of:
O1) $\forall x(x = 0 \lor x+x \ne 0)$
O2) $\exists x(x+x = S0)$
We can use compactness to prove MA has infinite "even" size models by adding the even definitions above as axioms. We can similarly prove there are infinite "odd" size models of MA. Some infinite sets, like the integers, are neither even nor odd. The integers are not the basis for a model of MA. For example, the four square theorem (every number is the sum of four squares) is a theorem of both MA and PA. The four square theorem is false in the integers. It has been conjectured the complex numbers are a basis for a model of MA. If so, the complex numbers would be an "odd" model of MA.
My question is whether every model of MA must be exclusively even or exclusively odd? Is this statement a theorem of MA?
$$\exists x(x \ne 0 \land x+x = 0) \ \overline{\vee}\ \exists x(x+x = S0)$$
I asked this question on stack exchange and got no answer.
https://math.stackexchange.com/questions/214018/even-xor-odd-infinities
[The following was merged from an answer – ed.]
Ashutosh's proof can be written as:
$\exists x\exists y( (x+x=0 \land y+y=1) \implies (x=0) )$
This answers my question when $\exists x(x+x=1)$ is true but it says nothing about when $\forall x(x+x \ne 1)$ is true. Emil and others have stated any algebraically closed field is a model of MA. Ashutosh's proof shows any algebraically closed field is odd because $\exists x(x+x=1)$ is true.
I want to accept Ben Crowell answer, but I have some reservations. The proof starts by showing how any model of MA can be expanded into a model of PA. I have made similar arguments and always assumed it would be easy to prove. My conjecture is true of all finite models of MA so we only need consider infinite models. MA is omega inconsistent and any infinite model must have non-standard elements. Tennebaum's theorem says addition is not recursive in non-standard models of PA. Can addition actually be recursive in $A$, the model of PA he constructs? It looks like he is assuming we can add non-standard numbers from the model of MA. I also wonder if he is assuming $I$ is a standard model of PA. I don't think it makes any difference, but it might.
Obo's proof is much simpler and similar to a proof I came up with. My proof had the same error as his. I think it is fixable. In the case where we have $S(y+y)=p$ we need to also prove $y \ne p$. $y \ne p$ can be true only in models with three or more elements.
This isn't a discussion group so I won't go into detail why I don't think the complex numbers are a model of MA. I don't think MA has any infinite models. I will point out MA proves a lot of interesting things about odd models. In an odd model the sum of all elements is 0. This can't be stated in first order. I think if we have a successor function defined on the complex numbers we can use it to order the reals. Just ignore numbers with a non-zero imaginary component.
I want to retract my statement that the Lagrange's four square theorem is a theorem of MA. I based my claim on Andrew Boucher's paper on General Arithmetic (GA). Boucher shows GA proves the four square theorem. I thought GA was a weak sub-theory of MA because GA has much weaker successor axioms. Rereading the paper I see Boucher says he is using 2nd order induction. He also says successor is second order.
Best Answer
The answer is no. It is enough to find a model of MA which is an integral domain of characteristic $0$ (whence O1 is true and E1 false) such that $2$ is not invertible (whence E2 is true and O2 false).
One example of such a model is the ring of $2$-adic integers $\mathbb Z_2$. This is clearly a domain, and $2$ is not a unit, hence it suffices to show
Theorem: For any prime $p$, the ring $\mathbb Z_p$ is a model of MA.
Proof: The only problem is to verify that induction holds. Assume $\mathbb Z_p\models\phi(0)\land\forall x\,(\phi(x)\to\phi(x+1))$, where $\phi$ is an arithmetic formula with parameters from $\mathbb Z_p$, and put $\phi(\mathbb Z_p):=\{a\in\mathbb Z_p:\mathbb Z_p\models\phi(a)\}$.
Since $\phi(\mathbb Z_p)$ is definable in $\mathbb Z_p$, it is also definable in the field $\mathbb Q_p$ endowed with a unary predicate for $\mathbb Z_p$. Macintyre [1] proved that such structures admit a form of quantifier elimination, and as a corollary (Thm. 2 on p. 609), every infinite definable set has a nonempty interior. Thus, there is $a_0\in\phi(\mathbb Z_p)$ and $k\ge0$ such that $a_0+p^k\mathbb Z_p\subseteq\phi(\mathbb Z_p)$. Let $a\in\mathbb Z_p$ be arbitrary, and let $b< p^k$ be a natural number such that $b\equiv a-a_0\pmod{p^k}$. Since $\phi(\mathbb Z_p)$ is closed under successor, we have $a\in b+a_0+p^k\mathbb Z_p\subseteq\phi(\mathbb Z_p)$. Thus, $\phi(\mathbb Z_p)=\mathbb Z_p$, i.e., $\mathbb Z_p\models\forall x\,\phi(x)$. QED
I suspect the following may work as additional countermodels (they are domains where $2$ is not a unit, the issue is whether they satisfy induction):
The ring of algebraic integers $\tilde{\mathbb Z}$. A form of quantifier elimination for $\tilde{\mathbb Z}$ was proved by van den Dries [2] and Prestel and Schmid [3], but the basic formulas are somewhat messy, so it is not immediately clear to me whether this implies induction.
The localization of $\tilde{\mathbb Z}$ at a maximal ideal containing $2$. Elimination of quantifiers for this (and similar) rings is reported as Fact 3 in [2], where it is attributed to [4]. It seems it could imply induction by a similar argument as for $\mathbb Z_p$.
[1] Angus Macintyre, On definable subsets of $p$-adic fields, Journal of Symbolic Logic 41 (1976), no. 3, pp. 605–610.
[2] Lou van den Dries, Elimination theory for the ring of algebraic integers, Journal für die reine und angewandte Mathematik 388 (1988), pp. 189–205.
[3] A. Prestel and J. Schmid, Existentially closed domains with radical relations, Journal für die reine und angewandte Mathematik 407 (1990), pp. 178–201.
[4] Angus Macintyre, Kenneth McKenna, Lou van den Dries, Elimination of quantifiers in algebraic structures, Advances in Mathematics 47 (1983), no. 1, pp. 74–87.