Addition is Associative Prove: + is associative on the natural numbers (F5 to view highlights only) Peano's Axioms 1 Set(n) & 1n & ALL(a):[an => next(a)n] & ALL(a):[an => ~next(a)=1] & ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b] & ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a] => ALL(b):[bn => ba]] Premise 2 Set(n) Split, 1 3 1n Split, 1 4 ALL(a):[an => next(a)n] Split, 1 5 ALL(a):[an => ~next(a)=1] Split, 1 6 ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b] Split, 1 7 ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a] => ALL(b):[bn => ba]] Split, 1 Define + on the natural numbers 8 ALL(a):ALL(b):[an & bn => a+bn] & ALL(a):[an => a+1=next(a)] & ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)] Definition 9 ALL(a):ALL(b):[an & bn => a+bn] Split, 8 10 ALL(a):[an => a+1=next(a)] Split, 8 11 ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)] Split, 8 Prove: xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]] Suppose... 12 xn Premise Prove: yn => ALL(z):[zn => x+y+z=x+(y+z)] Suppose... 13 yn Premise Sufficient: For ALL(z):[zn => x+y+z=x+(y+z)] Applying the induction rule... 14 x+y+1=x+(y+1) & ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))] => ALL(z):[zn => x+y+z=x+(y+z)] Induction Prove: x+y+1=x+(y+1) (the case for z=1) Applying the definition of +... 15 ALL(b):[xn & bn => x+next(b)=next(x+b)] U Spec, 11 16 xn & yn => x+next(y)=next(x+y) U Spec, 15 17 xn & yn Join, 12, 13 18 x+next(y)=next(x+y) Detach, 16, 17 19 yn => y+1=next(y) U Spec, 10 20 y+1=next(y) Detach, 19, 13 21 x+(y+1)=next(x+y) Substitute, 20, 18 Applying the definition of +... 22 x+yn => x+y+1=next(x+y) U Spec, 10 23 ALL(b):[xn & bn => x+bn] U Spec, 9 24 xn & yn => x+yn U Spec, 23 25 x+yn Detach, 24, 17 26 x+y+1=next(x+y) Detach, 22, 25 As Required: Case for z=1 Subsituting... 27 x+y+1=x+(y+1) Substitute, 21, 26 Prove: zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z)) Suppose... 28 zn & x+y+z=x+(y+z) Premise 29 zn Split, 28 30 x+y+z=x+(y+z) Split, 28 Applying definition of +... 31 ALL(b):[x+yn & bn => x+y+next(b)=next(x+y+b)] U Spec, 11 32 x+yn & zn => x+y+next(z)=next(x+y+z) U Spec, 31 33 ALL(b):[xn & bn => x+bn] U Spec, 9 34 xn & yn => x+yn U Spec, 33 35 x+yn Detach, 34, 17 36 x+yn & zn Join, 35, 29 37 x+y+next(z)=next(x+y+z) Detach, 32, 36 Applying definition of +... 38 x+y+zn => x+y+z+1=next(x+y+z) U Spec, 10 39 ALL(b):[x+yn & bn => x+y+bn] U Spec, 9 40 x+yn & zn => x+y+zn U Spec, 39 41 x+y+zn Detach, 40, 36 42 x+y+z+1=next(x+y+z) Detach, 38, 41 43 x+y+next(z)=x+y+z+1 Substitute, 42, 37 44 x+(y+next(z))=x+(y+next(z)) Reflex Applying definition of +... 45 ALL(b):[yn & bn => y+next(b)=next(y+b)] U Spec, 11 46 yn & zn => y+next(z)=next(y+z) U Spec, 45 47 yn & zn Join, 13, 29 48 y+next(z)=next(y+z) Detach, 46, 47 49 x+(y+next(z))=x+next(y+z) Substitute, 48, 44 Applying definition of +... 50 ALL(b):[xn & bn => x+next(b)=next(x+b)] U Spec, 11 51 xn & y+zn => x+next(y+z)=next(x+(y+z)) U Spec, 50 52 ALL(b):[yn & bn => y+bn] U Spec, 9 53 yn & zn => y+zn U Spec, 52 54 yn & zn Join, 13, 29 55 y+zn Detach, 53, 54 56 xn & y+zn Join, 12, 55 57 x+next(y+z)=next(x+(y+z)) Detach, 51, 56 58 x+(y+next(z))=next(x+(y+z)) Substitute, 57, 49 Applying definition of +... 59 x+(y+z)n => x+(y+z)+1=next(x+(y+z)) U Spec, 10 60 ALL(b):[xn & bn => x+bn] U Spec, 9 61 xn & y+zn => x+(y+z)n U Spec, 60 62 x+(y+z)n Detach, 61, 56 63 x+(y+z)+1=next(x+(y+z)) Detach, 59, 62 64 x+(y+next(z))=x+(y+z)+1 Substitute, 63, 58 From premise, substituting... 65 x+(y+next(z))=x+y+z+1 Substitute, 30, 64 66 x+y+next(z)=x+(y+next(z)) Substitute, 65, 43 As Required: 67 zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z)) Conclusion, 28 Generalizing... 68 ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))] U Gen, 67 69 x+y+1=x+(y+1) & ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))] Join, 27, 68 By induction... 70 ALL(z):[zn => x+y+z=x+(y+z)] Detach, 14, 69 As Required: 71 yn => ALL(z):[zn => x+y+z=x+(y+z)] Conclusion, 13 Generalizing... 72 ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]] U Gen, 71 As Required: 73 xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]] Conclusion, 12 Generalizing... 74 ALL(x):[xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]] U Gen, 73 Prove: xn & yn & zn => x+y+z=x+(y+z) Suppose... 75 xn & yn & zn Premise 76 xn Split, 75 77 yn Split, 75 78 zn Split, 75 79 xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]] U Spec, 74 80 ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]] Detach, 79, 76 81 yn => ALL(z):[zn => x+y+z=x+(y+z)] U Spec, 80 82 ALL(z):[zn => x+y+z=x+(y+z)] Detach, 81, 77 83 zn => x+y+z=x+(y+z) U Spec, 82 84 x+y+z=x+(y+z) Detach, 83, 78 As Required: 85 xn & yn & zn => x+y+z=x+(y+z) Conclusion, 75 Generalizing... 86 ALL(c):[xn & yn & cn => x+y+c=x+(y+c)] U Gen, 85 87 ALL(b):ALL(c):[xn & bn & cn => x+b+c=x+(b+c)] U Gen, 86 As Required: + is associative 88 ALL(a):ALL(b):ALL(c):[an & bn & cn => a+b+c=a+(b+c)] U Gen, 87