[FOM] Further comment on commutativity in a weak arithmetic

[Andrew Boucher]

As a follow-up to the questions on commutativity and Q, it may be  
interesting to note that in the presence of induction, commutativity  
of addition is equivalent to the functionality of the Successor  
function.

To be precise, working in first-order logic augmented by a 2-ary  
relationship S and a 3-ary relationship +, suppose induction:

(Induction Schema)  Suppose phi(0) and (x)(y)(phi(x) & Sx,y => phi 
(y)).  Then (x)phi(x).

Suppose addition satisfies the following axioms:

AX1/  (x) +(x,0,x)
AX2/  (x)(y) (+(x,0,y) => x = y)
AX3/ (x)(y)(z)(y')(z') (+(x,y,z) & Sy,y' & Sz,z' => +(x,y',z'))
AX4/ (x)(y)(y')(z') (+(x,y',z') & Sy,y' => (there exists z) +(x,y,z))

Consider:
(S-FUNC) (x)(y)(z)(Sx,y & Sx,z => y = z)
(+-COM)  (x)(y)(z)(+(x,y,z) => +(y,x,z))

Then:
Prop.  S-FUNC <=> +-COM.
Pf (! is used for "not"):
	Let ! S-FUNC.  Then Sx,y & Sx,z for some x,y,z where ! y = z.   +(x, 
0,x) by AX1.  If ! +(0,x,x) then ! +-COM and we are done.   So  
suppose +(0,x,x).  Then by AX3 +(0,y,z).  By AX2, ! +(y,0,z).   
Hence ! +-COM.
	For the other direction, it's the usual proof; ithe details are in  
the Appendix.

In general the system Induction plus S-functionality (i.e. one-to- 
oneness of S, totality of S, and 0 not being in image of S are not  
assumed) is an interesting and reasonably strong system.  I've called  
it "General Arithmetic", but perhaps someone knows of a prior name?


**********  Appendix **********

Prop 1.  (x) +(0,x,x)
Pf:
Induction on x.

Prop 2.  Let S0,y & +(x,y,z).  Then Sx,z.
Pf:
+(x,0,c) for some c where Sc,z, by AX4.  But x = c by AX2.

Prop 3.  Let +(x,y',z) & Sy,y'.  Then there exists x' such that Sx,x'  
& +(x',y,z).
Pf:
By induction on y.
Suppose +(x,y',z) & S0,y'.  Then Sx,z by Prop 2.  But +(z,0,z) by AX 1.
Now assume the proposition holds for y and let Sy,y'.  And let + 
(x,y'',z) & Sy',y''.  Then there exists z' such that +(x,y',z') &  
Sz',z, by AX 4. By induction hypothesis, there exists x' such that  
Sx,x' & +(x',y,z').  By AX 3, +(x',y',z).

Prop 4.  Assume S-FUNC.  Let +(x,y,z).  Then +(y,x,z).
Pf:
By induction on y.  If +(x,0,z), then x = z by AX 2, and +(0,x,z) by  
Prop 1.
Now assume the proposition holds for y and let Sy,y'.  Let + 
(x,y',z).  By Prop 3, there exists x' such that Sx,x' & +(x',y,z).   
By induction hypothesis, +(y,x',z).  By Prop 3, there exists y'' such  
that Sy,y'' & +(y'',x,z).  By S-Functionality, y' = y''.