DC Proof 1_"Uniqueness of even number function n 1 next n 1 next )6=+/5)# n 1 next n 1 next :AH: n  n  1 n  1 n  n next  n next  '+2 n next 1 n next 1 79TX_ n next  n next df 1 n next 1 n next   n  n AEL  n 1 next n 1 next QTpt{  n next  n next  # n  n $  n  n )AI?  n  n  n  n  sw} n  n D x n y  x n y   x n  x n "* y n  y n /37<D x y  x y IMSX` x n y  x n y eiuz  x n  x n  x n y  x n y  x y n  x y n   x n  x n   3 8 A  x n y  x n y F J a f o  x y  x y t x ~ ! z n  z n  z n  z n   z n  z n   z n  z n   * 0 9  z n  z n > C I O \  z n  n  z a e t y !! n  n "" x n  x n #" y n  y n  $# x n  x n    # %$ y n  y n ( , 2 7 D & x n  x n I M '' x n y  x n y K P Y (%& x n y  x n y ^ b r w )() x y  x y  ** x y  x y  $ ) 1 +* x y  x y 6 : M R Z ,C x y  x y _ d f l r - x n  x n w | .. x n y  x n y // x n y  x n y 6<E0/ x n y  x n y JOtz1 x n y  x n y 2 x n y  x n y 32- x n y  x n y  43- x n y  x n y  :@K504 x y  x y PU[an615 x y  x y sx~76 x y  x y 8  x n  x n 99 x n y  x n y TZc:: x n y  x n y hm;% x n y  x n y <<& x n y  x n y  ==8 x n y  x n y CIT>>7 x n y  x n y Y^?;? x y  x y @@ x y  x y A,A x y  x y $/B- x y  x y 48;@OC x n y  n  x y TWuyDD x n  n  x :EE n  n uF] x n y  x n y $)/GDG x y  x y 48;@MHG x n  x n RVZ_gIG y n  y n lptyJG x y  x y KK y x  y x LJI y n x  y n x MML y n x  y n x  NF y n  y n ;@IOO y n x  y n x NRpu~PPN y x  y x Q x n  x n  RR x n y  x n y gluSIJ x n y  x n y z~TST x y  x y UU x y  x y  V"V x y  x y "49DW"W x y  x y IMafqXX y x  y x vzY Y y x  y x ZZQ x y  x y [[H x y  x y  \G x n y  n  x y 26E] x n  n  x JMsw^ n  n From email: From: "Thomas Heye" <1910-131@onlinehome.de> To: Sent: Saturday, September 16, 2006 3:41 AM Subject: [DC Proof] Ideas for uniqueness of even number function > Hi folks, > I'd like to prove for all natural numbers a,b that a +a=b+b implies > a=b. > > My ideas so far: Having shown that a exclusive, it should be possible to deduce from a+a=b+b that a resp. is impossible, so equality must hold. > > Or is there an easier way? > > Thanks, > > Thomas Peano's Axioms 1 Set(n) & 1 @ n & ALL(a):[a @ n => next(a) @ n] & ALL(a):[a @ n => ~next(a)=1] & ALL(a):ALL(b):[a @ n & b @ n & next(a)=next(b) => a=b] & ALL(a):[Set(a) & 1 @ a & ALL(b):[b @ n & b @ a => next(b) @ a] => ALL(b):[b @ n => b @ a]] Premise Define + 2 ALL(a):ALL(b):[a @ n & b @ n => a+b @ n] & ALL(a):[a @ n => a+1=next(a)] & ALL(a):ALL(b):[a @ n & b @ n => a+next(b)=next(a+b)] Definition 3 Set(n) Split, 1 4 1 @ n Split, 1 5 ALL(a):[a @ n => next(a) @ n] Split, 1 6 ALL(a):[a @ n => ~next(a)=1] Split, 1 7 ALL(a):ALL(b):[a @ n & b @ n & next(a)=next(b) => a=b] Split, 1 8 ALL(a):[Set(a) & 1 @ a & ALL(b):[b @ n & b @ a => next(b) @ a] => ALL(b):[b @ n => b @ a]] Split, 1 9 ALL(a):ALL(b):[a @ n & b @ n => a+b @ n] Split, 2 10 ALL(a):[a @ n => a+1=next(a)] Split, 2 11 ALL(a):ALL(b):[a @ n & b @ n => a+next(b)=next(a+b)] Split, 2 Define < 12 ALL(a):ALL(b):[a @ n & b @ n => [a EXIST(c):[c @ n & a+c=b]]] Definition Assumed: a a a a+b=b+a] Premise Assumed: Exclusivity of a [a a+c a+c x+b @ n] U Spec, 9 23 x @ n & y @ n => x+y @ n U Spec, 22 24 x+y @ n Detach, 23, 21 25 ALL(b):[x @ n & b @ n => x+b=b+x] U Spec, 14 26 x @ n & y @ n => x+y=y+x U Spec, 25 27 x+y=y+x Detach, 26, 21 28 z @ n Premise 29 z @ n & z @ n Join, 28, 28 30 ALL(b):[z @ n & b @ n => z+b @ n] U Spec, 9 31 z @ n & z @ n => z+z @ n U Spec, 30 32 z+z @ n Detach, 31, 29 33 z @ n => z+z @ n 4 Conclusion, 28 34 ALL(c):[c @ n => c+c @ n] U Gen, 33 35 x @ n => x+x @ n U Spec, 34 36 y @ n => y+y @ n U Spec, 34 37 x+x @ n Detach, 35, 18 38 y+y @ n Detach, 36, 19 39 ALL(b):[x+x @ n & b @ n => [x+x [x+x x+c x+c x+x x+y x+x x+x x+x ~x ~x ~a ~y ~y [x [x x=y] | y x=y] => y ~~[~x x=y] Contra, 88 90 ~y [~x x=y] Rem DNeg, 89 91 ~x x=y Detach, 90, 81 92 x=y Detach, 91, 72 93 x @ n & y @ n & x+x=y+y => x=y 4 Conclusion, 71 94 ALL(b):[x @ n & b @ n & x+x=b+b => x=b] U Gen, 93 95 ALL(a):ALL(b):[a @ n & b @ n & a+a=b+b => a=b] U Gen, 94 Join, 76, 18 78 y @ n & x @ n & y @ n Join, 76, 19 79 y @ n & x @ n & x @ n & y y+y y+y y+y [x [x x=y] | y x=y] => y ~~[~x x=y] Contra, 102 104 ~y [~x x=y] Rem DNeg, 103 105 ~x x=y Detach, 104, 93 106 x=y Detach, 105, 69 107 x @ n & y @ n & x+x=y+y => x=y 4 Conclusion, 17 108 ALL(b):[x @ n & b @ n & x+x=b+b => x=b] U Gen, 107 109 ALL(a):ALL(b):[a @ n & b @ n & a+a=b+b => a=b] U Gen, 108