THEOREM
*******
EXIST(add):[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))]]
(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
****************
Existence of an add function such that:
1. add(a,0)=a
2. add(a,next(b))= next(add(a,b)) ConstructAdd0.htm
7 EXIST(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))]]
Axiom
Equivalence: ALL(a):[a e n => add(a,0)=a] <=> ALL(a):[a e n => add(a,2)=next(next(a))] 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
*****
Apply previous result
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))]
E Spec, 7
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
Apply previous result
17 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
18 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, 14, 16
19 ALL(a):[a e n => add(a,0)=a]
<=> ALL(a):[a e n => add(a,2)=next(next(a))]
Detach, 17, 18
20 [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, 19
21 ALL(a):[a e n => add(a,0)=a] => ALL(a):[a e n => add(a,2)=next(next(a))]
Split, 20
22 ALL(a):[a e n => add(a,2)=next(next(a))] => ALL(a):[a e n => add(a,0)=a]
Split, 20
23 ALL(a):[a e n => add(a,2)=next(next(a))]
Detach, 21, 15
24 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))]
Join, 14, 23
25 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))]
Join, 24, 16
As Required:
26 EXIST(add):[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))]]
E Gen, 25