NOTE: The first proof is wrong because it uses second-order induction. The second-proof is wrong as well per [Wofsey's comment](https://mathoverflow.net/questions/119375/even-xor-odd-infinities/119428#comment306806_119428). In [his comment](https://mathoverflow.net/questions/119375/even-xor-odd-infinities/119428#comment306655_119375) Ashutosh has shown that exclusion holds. Here is a proof of existence. Let $A$ be the elements of the model. Let $p$ be the predecessor of $0$ in $A$. Let $T = S \setminus \{(p,0)\}$. Then $T$ induces the normal ordering $<$ on $A$, with $p$ the maximal element. It can be shown that $$x < Sy \text{ implies } x \le y .\tag1\label1$$ Clearly $p + p \le p$. Let $x$ be the least element such that $x + x \le x$. We claim $x + x = 0$ or $x + x = 1$. Suppose not. Then there exists $y$ such that $Sy = x$ and $v$ such that $SSv = x + x$ and $y < x$ and $v < x + x$. ($y < x$ because otherwise $x = 0$, so $x + x = 0$, a contradiction.) But $v = y + y$, and $v < x + x \le x$. So $v < Sy$. By \eqref{1}, $v \le y$, contradicting the leastness of $x$. ABOVE assumed second-order induction. BELOW works using first-order induction (and is easier to boot...). I claim: $\forall x \exists y \bigl(y+y=x \lor S(y+y)=x \bigr)$ For this is true when $x = 0$ (take $y = 0$). Suppose true for $k$. If $y+y=k$, then $S(y+y)=Sk$. And if $S(y+y)=k$, then $Sy+Sy =Sk$. So if true for $k$, then true for $Sk$. By induction (first-order!!), the claim is true. Let $p$ be the predecessor of $0$. Then by the claim $y+y=p$ or $S(y+y) = p$ for some $y$. In the first case $Sy+Sy = 1$, in the second $Sy+Sy = 0$.