On Thursday, February 27, 2014 1:09:49 PM UTC-5, muec...@rz.fh-augsburg.de wrote: > On Thursday, 27 February 2014 15:44:55 UTC+1, Dan Christensen wrote: > > > > Where does he axiomatize that the difference is always 1? > > > Nowhere. That is just a property of the addition function, which itself can be constructed from Peano's axioms. > > > > Addition cannot be constructed from the axioms.
Yes, it can. The trick is to select the right subset of N^3:
ALL(a):ALL(b):ALL(c):[(a,b,c) in add <=> (a,b,c) in N^3 & ALL(d):[d in Pow(N^3) & ALL(e):[e in N => (e,0,e) in d] & ALL(e):ALL(f):ALL(g):[(e,f,g) in d => (e,next(f),next(g)) in d] => (a,b,c) in d]]
N^3 is the set of ordered triples of natural numbers Pow(N^3) is the power set of N^3