4 added 134 characters in body

NOTE: The first proof is wrong because it uses second-order induction. The second-proof is wrong as well per Wofsey's comment.

Ashutosh in the comments 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 \ {(p,0)}. Then T induces the normal ordering < on A, with p the maximal element. It can be shown that (1) x < Sy implies x <= y.

Clearly p + p <= p. Let x be the least element such that x + x <= 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 <= x. So v < Sy. By (1) v <= y, contradicting the leastness of x.

ABOVE assumed second-order induction. BELOW works using first-order induction (and is easier to boot...).

I claim: (x)(∃y(y+y=x v S(y+y)=x))

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.

3 added 17 characters in body

Ashutosh in the comments 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 \ {(p,0)}. Then T induces the normal ordering < on A, with p the maximal element. It can be shown that (1) x < Sy implies x <= y.

Clearly p + p <= p. Let x be the least element such that x + x <= 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 <= x. So v < Sy. By (1) v <= y, contradicting the leastness of x.

ABOVE assumed second-order PAinduction. BELOW works in using first-order PA induction (and is easier to boot...).

I claim: (x)(∃y(y+y=x v S(y+y)=x))

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.

2 added 488 characters in body

Ashutosh in the comments 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 \ {(p,0)}. Then T induces the normal ordering < on A, with p the maximal element. It can be shown that (1) x < Sy implies x <= y.

Clearly p + p <= p. Let x be the least element such that x + x <= 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 <= x. So v < Sy. By (1) v <= y, contradicting the leastness of x.

ABOVE assumed second-order PA. BELOW works in first-order PA (and is easier to boot...).

I claim: (x)(∃y(y+y=x v S(y+y)=x))

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.

1