[FOM] Further comment on commutativity in a weak arithmetic
Andrew Boucher
Helene.Boucher at wanadoo.fr
Sun Sep 23 05:11:05 EDT 2007
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''.
More information about the FOM
mailing list