THEOREM
*******
Add0 is unique
ALL(add):ALL(add'):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
& ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
& ALL(a):[a e n => add'(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
=> ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]]
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com)
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
2 0 e n
Axiom
next is a function on n
3 ALL(a):[a e n => next(a) e n]
Axiom
next is an injective (1-to-1) function
4 ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Axiom
0 has no predecessor
5 ALL(a):[a e n => ~next(a)=0]
Axiom
Principle of mathematical induction (PMI)
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Suppose we have add and add' such that...
7 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
& ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
& ALL(a):[a e n => add'(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
Premise
8 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
Split, 7
9 ALL(a):[a e n => add(a,0)=a]
Split, 7
10 ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
Split, 7
11 ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
Split, 7
12 ALL(a):[a e n => add'(a,0)=a]
Split, 7
13 ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
Split, 7
Prove: ALL(a):[a e n => ALL(b):[b e n => add(a,b)=add'(a,b)]]
Suppose...
14 x e n
Premise
15 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & add(x,b)=add'(x,b)]]
Subset, 1
16 Set(p1) & ALL(b):[b e p1 <=> b e n & add(x,b)=add'(x,b)]
E Spec, 15
Define: p1
17 Set(p1)
Split, 16
18 ALL(b):[b e p1 <=> b e n & add(x,b)=add'(x,b)]
Split, 16
19 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 6
Prove: ALL(b):[b e p1 => b e n]
Suppose...
20 y e p1
Premise
21 y e p1 <=> y e n & add(x,y)=add'(x,y)
U Spec, 18
22 [y e p1 => y e n & add(x,y)=add'(x,y)]
& [y e n & add(x,y)=add'(x,y) => y e p1]
Iff-And, 21
23 y e p1 => y e n & add(x,y)=add'(x,y)
Split, 22
24 y e n & add(x,y)=add'(x,y) => y e p1
Split, 22
25 y e n & add(x,y)=add'(x,y)
Detach, 23, 20
26 y e n
Split, 25
As Required:
27 ALL(b):[b e p1 => b e n]
4 Conclusion, 20
28 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 17, 27
Sufficient: ALL(b):[b e n => b e p1]
29 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]
Detach, 19, 28
30 0 e p1 <=> 0 e n & add(x,0)=add'(x,0)
U Spec, 18
31 [0 e p1 => 0 e n & add(x,0)=add'(x,0)]
& [0 e n & add(x,0)=add'(x,0) => 0 e p1]
Iff-And, 30
32 0 e p1 => 0 e n & add(x,0)=add'(x,0)
Split, 31
Sufficient: 0 e p1
33 0 e n & add(x,0)=add'(x,0) => 0 e p1
Split, 31
34 x e n => add(x,0)=x
U Spec, 9
35 add(x,0)=x
Detach, 34, 14
36 x e n => add'(x,0)=x
U Spec, 12
37 add'(x,0)=x
Detach, 36, 14
38 add(x,0)=add'(x,0)
Substitute, 37, 35
39 0 e n & add(x,0)=add'(x,0)
Join, 2, 38
As Required:
40 0 e p1
Detach, 33, 39
Prove: ALL(b):[b e p1 => next(b) e p1]
Suppose...
41 y e p1
Premise
42 y e p1 <=> y e n & add(x,y)=add'(x,y)
U Spec, 18
43 [y e p1 => y e n & add(x,y)=add'(x,y)]
& [y e n & add(x,y)=add'(x,y) => y e p1]
Iff-And, 42
44 y e p1 => y e n & add(x,y)=add'(x,y)
Split, 43
45 y e n & add(x,y)=add'(x,y) => y e p1
Split, 43
46 y e n & add(x,y)=add'(x,y)
Detach, 44, 41
47 y e n
Split, 46
48 add(x,y)=add'(x,y)
Split, 46
49 next(y) e p1 <=> next(y) e n & add(x,next(y))=add'(x,next(y))
U Spec, 18
50 [next(y) e p1 => next(y) e n & add(x,next(y))=add'(x,next(y))]
& [next(y) e n & add(x,next(y))=add'(x,next(y)) => next(y) e p1]
Iff-And, 49
51 next(y) e p1 => next(y) e n & add(x,next(y))=add'(x,next(y))
Split, 50
Sufficient: next(y) e p1
52 next(y) e n & add(x,next(y))=add'(x,next(y)) => next(y) e p1
Split, 50
53 y e n => next(y) e n
U Spec, 3
54 next(y) e n
Detach, 53, 47
55 ALL(b):[x e n & b e n => add(x,next(b))=next(add(x,b))]
U Spec, 10
56 x e n & y e n => add(x,next(y))=next(add(x,y))
U Spec, 55
57 x e n & y e n
Join, 14, 47
58 add(x,next(y))=next(add(x,y))
Detach, 56, 57
59 ALL(b):[x e n & b e n => add'(x,next(b))=next(add'(x,b))]
U Spec, 13
60 x e n & y e n => add'(x,next(y))=next(add'(x,y))
U Spec, 59
61 add'(x,next(y))=next(add'(x,y))
Detach, 60, 57
62 add'(x,next(y))=next(add(x,y))
Substitute, 48, 61
63 add(x,next(y))=add'(x,next(y))
Substitute, 62, 58
64 next(y) e n & add(x,next(y))=add'(x,next(y))
Join, 54, 63
65 next(y) e p1
Detach, 52, 64
As Required:
66 ALL(b):[b e p1 => next(b) e p1]
4 Conclusion, 41
67 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
Join, 40, 66
68 ALL(b):[b e n => b e p1]
Detach, 29, 67
Prove: ALL(b):[b e n => add(x,b)=add'(x,b)]
Suppose...
69 y e n
Premise
70 y e n => y e p1
U Spec, 68
71 y e p1
Detach, 70, 69
72 y e p1 <=> y e n & add(x,y)=add'(x,y)
U Spec, 18
73 [y e p1 => y e n & add(x,y)=add'(x,y)]
& [y e n & add(x,y)=add'(x,y) => y e p1]
Iff-And, 72
74 y e p1 => y e n & add(x,y)=add'(x,y)
Split, 73
75 y e n & add(x,y)=add'(x,y) => y e p1
Split, 73
76 y e n & add(x,y)=add'(x,y)
Detach, 74, 71
77 y e n
Split, 76
78 add(x,y)=add'(x,y)
Split, 76
As Required:
79 ALL(b):[b e n => add(x,b)=add'(x,b)]
4 Conclusion, 69
As Required:
80 ALL(a):[a e n => ALL(b):[b e n => add(a,b)=add'(a,b)]]
4 Conclusion, 14
Prove: ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]
Suppose...
81 x e n & y e n
Premise
82 x e n
Split, 81
83 y e n
Split, 81
84 x e n => ALL(b):[b e n => add(x,b)=add'(x,b)]
U Spec, 80
85 ALL(b):[b e n => add(x,b)=add'(x,b)]
Detach, 84, 82
86 y e n => add(x,y)=add'(x,y)
U Spec, 85
87 add(x,y)=add'(x,y)
Detach, 86, 83
As Required:
88 ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]
4 Conclusion, 81
As Required:
89 ALL(add):ALL(add'):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
& ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
& ALL(a):[a e n => add'(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
=> ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]]
4 Conclusion, 7