THEOREM
*******
Add0(x,y) = Add2(x,y)
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,2)=next(next(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
PREVIOUS RESULTS
****************
Add0 is unique Add0Unique.htm
7 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)]]
Axiom
Add0, Add2 equivalence Add2Equivalence.htm
8 ALL(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
=> [ALL(a):[a e n => add(a,0)=a]
<=> ALL(a):[a e n => add(a,2)=next(next(a))]]]
Axiom
DEFINITIONS
***********
9 1 e n
Axiom
10 1=next(0)
Axiom
11 2 e n
Axiom
12 2=next(1)
Axiom
PROOF
*****
Prove: 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,2)=next(next(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)]]
Suppose...
13 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,2)=next(next(a))]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
Premise
14 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
Split, 13
15 ALL(a):[a e n => add(a,0)=a]
Split, 13
16 ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
Split, 13
17 ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
Split, 13
18 ALL(a):[a e n => add'(a,2)=next(next(a))]
Split, 13
19 ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
Split, 13
Apply previous result
20 ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
=> [ALL(a):[a e n => add'(a,0)=a]
<=> ALL(a):[a e n => add'(a,2)=next(next(a))]]
U Spec, 8
21 ALL(a):ALL(b):[a e n & b e n => add'(a,b) e n]
& ALL(a):ALL(b):[a e n & b e n => add'(a,next(b))=next(add'(a,b))]
Join, 17, 19
22 ALL(a):[a e n => add'(a,0)=a]
<=> ALL(a):[a e n => add'(a,2)=next(next(a))]
Detach, 20, 21
23 [ALL(a):[a e n => add'(a,0)=a] => ALL(a):[a e n => add'(a,2)=next(next(a))]]
& [ALL(a):[a e n => add'(a,2)=next(next(a))] => ALL(a):[a e n => add'(a,0)=a]]
Iff-And, 22
24 ALL(a):[a e n => add'(a,0)=a] => ALL(a):[a e n => add'(a,2)=next(next(a))]
Split, 23
25 ALL(a):[a e n => add'(a,2)=next(next(a))] => ALL(a):[a e n => add'(a,0)=a]
Split, 23
26 ALL(a):[a e n => add'(a,0)=a]
Detach, 25, 18
Apply previous result
27 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)]]
U Spec, 7
28 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)]
U Spec, 27
29 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
Join, 14, 15
30 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))]
Join, 29, 16
31 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]
Join, 30, 17
32 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]
Join, 31, 26
33 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))]
Join, 32, 19
34 ALL(a):ALL(b):[a e n & b e n => add(a,b)=add'(a,b)]
Detach, 28, 33
As Required:
35 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,2)=next(next(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, 13