THEOREM
*******
The add function on n 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,s(b))=s(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,s(b))=s(add'(a,b))]
=> ALL(a):ALL(b):[a
e n & b e n => add(a,b)=add'(a,b)]]
This formal proof was written
and machine-verified using the author's DC Proof 2.0 freeware available at http://www.dcproof.com
Dan Christensen
2021-6-7
Peano's Axioms
**************
1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=0]
Axiom
6 ALL(a):[Set(a) &
ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
Axiom
Let add and add' be addition functions on n
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,s(b))=s(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,s(b))=s(add'(a,b))]
Premise
Define: add on n
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,s(b))=s(add(a,b))]
Split, 7
Define: add' on n
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,s(b))=s(add'(a,b))]
Split, 7
Prove: ALL(a):[a e n => ALL(b):[b e n => add(a,b)=add'(a,b)]]
Suppose...
14 t e n
Premise
15 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & add(t,b)=add'(t,b)]]
Subset, 1
16 Set(p) & ALL(b):[b e p <=> b e n & add(t,b)=add'(t,b)]
E Spec, 15
Define: p
17 Set(p)
Split, 16
18 ALL(b):[b e p <=> b e n & add(t,b)=add'(t,b)]
Split, 16
Apply Induction Axiom
19 Set(p) & ALL(b):[b e p => b e n]
=>
[0 e p & ALL(b):[b e p => s(b) e p]
=>
ALL(b):[b e n => b e p]]
U Spec, 6
Prove: ALL(b):[b e p => b e n]
Suppose...
20 u e p
Premise
21 u e p <=> u e n & add(t,u)=add'(t,u)
U Spec, 18
22 [u e p => u e n & add(t,u)=add'(t,u)]
&
[u e n & add(t,u)=add'(t,u) => u e p]
Iff-And, 21
23 u e p => u e n & add(t,u)=add'(t,u)
Split, 22
24 u e n & add(t,u)=add'(t,u)
Detach, 23, 20
25 u e n
Split, 24
As Required:
26 ALL(b):[b e p => b e n]
4 Conclusion, 20
27 Set(p) & ALL(b):[b e p => b e n]
Join, 17, 26
Base Case
*********
Sufficient: For ALL(b):[b e n => b e p]
28 0 e p & ALL(b):[b e p => s(b) e p]
=>
ALL(b):[b e n => b e p]
Detach, 19, 27
29 0 e p <=> 0 e n & add(t,0)=add'(t,0)
U Spec, 18
30 [0 e p => 0 e n & add(t,0)=add'(t,0)]
&
[0 e n & add(t,0)=add'(t,0) => 0 e p]
Iff-And, 29
Sufficient: For 0 e p
31 0 e n & add(t,0)=add'(t,0) => 0 e p
Split, 30
32 t e n => add(t,0)=t
U Spec, 9
33 add(t,0)=t
Detach, 32, 14
34 t e n => add'(t,0)=t
U Spec, 12
35 add'(t,0)=t
Detach, 34, 14
36 add(t,0)=add'(t,0)
Substitute, 35,
33
37 0 e n & add(t,0)=add'(t,0)
Join, 2, 36
As Required:
38 0 e p
Detach, 31, 37
Inductive Step
**************
Prove: ALL(b):[b e p => s(b) e p]
Suppose...
39 u e p
Premise
40 u e p <=> u e n & add(t,u)=add'(t,u)
U Spec, 18
41 [u e p => u e n & add(t,u)=add'(t,u)]
&
[u e n & add(t,u)=add'(t,u) => u e p]
Iff-And, 40
42 u e p => u e n & add(t,u)=add'(t,u)
Split, 41
43 u e n & add(t,u)=add'(t,u)
Detach, 42, 39
44 u e n
Split, 43
45 add(t,u)=add'(t,u)
Split, 43
46 u e n => s(u) e n
U Spec, 3
47 s(u) e n
Detach, 46, 44
48 s(u) e p <=> s(u) e n & add(t,s(u))=add'(t,s(u))
U Spec, 18, 47
49 [s(u) e p => s(u) e n & add(t,s(u))=add'(t,s(u))]
&
[s(u) e n & add(t,s(u))=add'(t,s(u)) => s(u) e p]
Iff-And, 48
Sufficient: For s(u) e p
50 s(u) e n & add(t,s(u))=add'(t,s(u)) => s(u) e p
Split, 49
51 ALL(b):[t e n & b e n => add(t,s(b))=s(add(t,b))]
U Spec, 10
52 t e n & u e n => add(t,s(u))=s(add(t,u))
U Spec, 51
53 t e n & u e n
Join, 14, 44
54 add(t,s(u))=s(add(t,u))
Detach, 52, 53
55 ALL(b):[t e n & b e n => add'(t,s(b))=s(add'(t,b))]
U Spec, 13
56 t e n & u e n => add'(t,s(u))=s(add'(t,u))
U Spec, 55
57 add'(t,s(u))=s(add'(t,u))
Detach, 56, 53
58 add'(t,s(u))=s(add(t,u))
Substitute, 45,
57
59 add(t,s(u))=add'(t,s(u))
Substitute, 58,
54
60 s(u) e n & add(t,s(u))=add'(t,s(u))
Join, 47, 59
61 s(u) e p
Detach, 50, 60
As Required:
62 ALL(b):[b e p => s(b) e p]
4 Conclusion, 39
63 0 e p & ALL(b):[b e p => s(b) e p]
Join, 38, 62
As Required:
64 ALL(b):[b e n => b e p]
Detach, 28, 63
Prove: ALL(b):[b e n => add(t,b)=add'(t,b)]
Suppose...
65 u e n
Premise
66 u e n => u e p
U Spec, 64
67 u e p
Detach, 66, 65
68 u e p <=> u e n & add(t,u)=add'(t,u)
U Spec, 18
69 [u e p => u e n & add(t,u)=add'(t,u)]
&
[u e n & add(t,u)=add'(t,u) => u e p]
Iff-And, 68
70 u e p => u e n & add(t,u)=add'(t,u)
Split, 69
71 u e n & add(t,u)=add'(t,u)
Detach, 70, 67
72 u e n
Split, 71
73 add(t,u)=add'(t,u)
Split, 71
As Required:
74 ALL(b):[b e n => add(t,b)=add'(t,b)]
4 Conclusion, 65
As Required:
75 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...
76 t e n & u e n
Premise
77 t e n
Split, 76
78 u e n
Split, 76
79 t e n => ALL(b):[b e n => add(t,b)=add'(t,b)]
U Spec, 75
80 ALL(b):[b e n => add(t,b)=add'(t,b)]
Detach, 79, 77
81 u e n => add(t,u)=add'(t,u)
U Spec, 80
82 add(t,u)=add'(t,u)
Detach, 81, 78
As Required:
83 ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]
4 Conclusion, 76
As Required:
84 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,s(b))=s(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,s(b))=s(add'(a,b))]
=>
ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]]
4 Conclusion, 7