The Commutativiy of Addition for Natural Numbers
by Mark Hurd
Prove: ALL(a):ALL(b):[a
n & 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