The Commutativiy of Addition for Natural Numbers by Mark Hurd Prove: ALL(a):ALL(b):[an & bn => b+a=a+b] (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 Define: + 2 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 3 Set(n) Split, 1 4 1n Split, 1 5 ALL(a):[an => next(a)n] Split, 1 6 ALL(a):[an => ~next(a)=1] Split, 1 7 ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b] Split, 1 8 ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a] => ALL(b):[bn => ba]] Split, 1 9 ALL(a):ALL(b):[an & bn => a+bn] Split, 2 10 ALL(a):[an => a+1=next(a)] Split, 2 11 ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)] Split, 2 Prove: ALL(a):[an => ALL(b):[bn => b+a=a+b]] Applying induction shortcut... 12 ALL(b):[bn => b+1=1+b] & ALL(a):[an & ALL(b):[bn => b+a=a+b] => ALL(b):[bn => b+next(a)=next(a)+b]] => ALL(a):[an => ALL(b):[bn => b+a=a+b]] Induction Prove: ALL(b):[bn => b+1=1+b] Applying induction shortcut... 13 1+1=1+1 & ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)] => ALL(b):[bn => b+1=1+b] Induction 14 1+1=1+1 Reflex Prove: bn & b+1=1+b => next(b)+1=1+next(b) Suppose... 15 bn & b+1=1+b Premise 16 bn Split, 15 17 b+1=1+b Split, 15 Applying definition of +... 18 bn => b+1=next(b) U Spec, 10 19 b+1=next(b) Detach, 18, 16 20 next(b)=1+b Substitute, 19, 17 21 ALL(b):[1n & bn => 1+next(b)=next(1+b)] U Spec, 11 22 1n & bn => 1+next(b)=next(1+b) U Spec, 21 23 1n & bn => 1+next(b)=next(next(b)) Substitute, 20, 22 24 next(b)n => next(b)+1=next(next(b)) U Spec, 10 25 1n & bn Join, 4, 16 26 1+next(b)=next(next(b)) Detach, 23, 25 27 next(b)n => next(b)+1=1+next(b) Substitute, 26, 24 28 bn => next(b)n U Spec, 5 29 next(b)n Detach, 28, 16 30 next(b)+1=1+next(b) Detach, 27, 29 As Required: 31 bn & b+1=1+b => next(b)+1=1+next(b) Conclusion, 15 Generalizing... 32 ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)] U Gen, 31 33 1+1=1+1 & ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)] Join, 14, 32 As Required: 34 ALL(b):[bn => b+1=1+b] Detach, 13, 33 35 pn & ALL(b):[bn => b+p=p+b] Premise 36 pn Split, 35 37 ALL(b):[bn => b+p=p+b] Split, 35 38 1+next(p)=next(p)+1 & ALL(b):[bn & b+next(p)=next(p)+b => next(b)+next(p)=next(p)+next(b)] => ALL(b):[bn => b+next(p)=next(p)+b] Induction 39 pn & p+1=1+p => next(p)+1=1+next(p) U Spec, 32 40 1n => 1+p=p+1 U Spec, 37 41 1+p=p+1 Detach, 40, 4 42 p+1=1+p Sym, 41 43 pn & p+1=1+p Join, 36, 42 44 next(p)+1=1+next(p) Detach, 39, 43 45 1+next(p)=next(p)+1 Sym, 44 Prove: qn & q+next(p)=next(p)+q => next(q)+next(p)=next(p)+next(q) Suppose... 46 qn & q+next(p)=next(p)+q Premise 47 qn Split, 46 48 q+next(p)=next(p)+q Split, 46 Applying the definition of +... 49 ALL(b):[next(p)n & bn => next(p)+next(b)=next(next(p)+b)] U Spec, 11 50 next(p)n & qn => next(p)+next(q)=next(next(p)+q) U Spec, 49 51 ALL(b):[next(q)n & bn => next(q)+next(b)=next(next(q)+b)] U Spec, 11 52 next(q)n & pn => next(q)+next(p)=next(next(q)+p) U Spec, 51 53 pn => next(p)n U Spec, 5 54 qn => next(q)n U Spec, 5 55 next(p)n Detach, 53, 36 56 next(q)n Detach, 54, 47 57 next(p)n & qn Join, 55, 47 58 next(q)n & pn Join, 56, 36 59 next(p)+next(q)=next(next(p)+q) Detach, 50, 57 60 next(q)+next(p)=next(next(q)+p) Detach, 52, 58 61 ALL(b):[qn & bn => q+next(b)=next(q+b)] U Spec, 11 62 qn & pn => q+next(p)=next(q+p) U Spec, 61 63 qn & pn Join, 47, 36 64 q+next(p)=next(q+p) Detach, 62, 63 65 next(p)+q=next(q+p) Substitute, 48, 64 66 qn => q+p=p+q U Spec, 37 67 q+p=p+q Detach, 66, 47 68 next(p)+q=next(p+q) Substitute, 67, 65 69 next(q)n => next(q)+p=p+next(q) U Spec, 37 70 next(q)+p=p+next(q) Detach, 69, 56 71 ALL(b):[pn & bn => p+next(b)=next(p+b)] U Spec, 11 72 pn & qn => p+next(q)=next(p+q) U Spec, 71 73 pn & qn Join, 36, 47 74 p+next(q)=next(p+q) Detach, 72, 73 75 next(q)+p=next(p+q) Substitute, 74, 70 76 next(p)+next(q)=next(next(p+q)) Substitute, 68, 59 77 next(q)+next(p)=next(next(p+q)) Substitute, 75, 60 78 next(q)+next(p)=next(p)+next(q) Substitute, 76, 77 As Required: 79 qn & q+next(p)=next(p)+q => next(q)+next(p)=next(p)+next(q) Conclusion, 46 Generalizing... 80 ALL(b):[bn & b+next(p)=next(p)+b => next(b)+next(p)=next(p)+next(b)] U Gen, 79 81 1+next(p)=next(p)+1 & ALL(b):[bn & b+next(p)=next(p)+b => next(b)+next(p)=next(p)+next(b)] Join, 45, 80 82 ALL(b):[bn => b+next(p)=next(p)+b] Detach, 38, 81 As Required: 83 pn & ALL(b):[bn => b+p=p+b] => ALL(b):[bn => b+next(p)=next(p)+b] Conclusion, 35 Generalizing... 84 ALL(a):[an & ALL(b):[bn => b+a=a+b] => ALL(b):[bn => b+next(a)=next(a)+b]] U Gen, 83 85 ALL(b):[bn => b+1=1+b] & ALL(a):[an & ALL(b):[bn => b+a=a+b] => ALL(b):[bn => b+next(a)=next(a)+b]] Join, 34, 84 86 ALL(a):[an => ALL(b):[bn => b+a=a+b]] Detach, 12, 85 Prove: pn & qn => q+p=p+q Suppose... 87 pn & qn Premise 88 pn => ALL(b):[bn => b+p=p+b] U Spec, 86 89 pn Split, 87 90 qn Split, 87 91 ALL(b):[bn => b+p=p+b] Detach, 88, 89 92 qn => q+p=p+q U Spec, 91 93 q+p=p+q Detach, 92, 90 As Required: 94 pn & qn => q+p=p+q Conclusion, 87 Generalizing... 95 ALL(b):[pn & bn => b+p=p+b] U Gen, 94 As Required: 96 ALL(a):ALL(b):[an & bn => b+a=a+b] U Gen, 95