THEOREM
*******
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))]]]
(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
DEFINITIONS
***********
7 1 e n
Axiom
8 1=next(0)
Axiom
9 2 e n
Axiom
10 2=next(1)
Axiom
PROOF
*****
Suppose...
11 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))]
Premise
12 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
Split, 11
13 ALL(a):ALL(b):[a e n & b e n => add(a,next(b))=next(add(a,b))]
Split, 11
'=>'
Prove: ALL(a):[a e n => add(a,0)=a] => ALL(a):[aen => add(a,2)=next(next(a))]
Suppose...
14 ALL(a):[a e n => add(a,0)=a]
Premise
Prove: ALL(a):[a e n => add(a,2)=next(next(a))]
Suppose...
15 x e n
Premise
16 x e n => add(x,0)=x
U Spec, 14
17 add(x,0)=x
Detach, 16, 15
18 ALL(b):[x e n & b e n => add(x,next(b))=next(add(x,b))]
U Spec, 13
19 x e n & 0 e n => add(x,next(0))=next(add(x,0))
U Spec, 18
20 x e n & 0 e n
Join, 15, 2
21 add(x,next(0))=next(add(x,0))
Detach, 19, 20
22 add(x,1)=next(add(x,0))
Substitute, 8, 21
23 add(x,1)=next(x)
Substitute, 17, 22
24 ALL(b):[x e n & b e n => add(x,next(b))=next(add(x,b))]
U Spec, 13
25 x e n & 1 e n => add(x,next(1))=next(add(x,1))
U Spec, 24
26 x e n & 1 e n
Join, 15, 7
27 add(x,next(1))=next(add(x,1))
Detach, 25, 26
28 add(x,2)=next(add(x,1))
Substitute, 10, 27
29 add(x,2)=next(next(x))
Substitute, 23, 28
As Required:
30 ALL(a):[a e n => add(a,2)=next(next(a))]
4 Conclusion, 15
As Required:
31 ALL(a):[a e n => add(a,0)=a]
=> ALL(a):[a e n => add(a,2)=next(next(a))]
4 Conclusion, 14
'<='
Prove: ALL(a):[a e n => add(a,2)=next(next(a))]
=> ALL(a):[a e n => add(a,0)=a]
Suppose...
32 ALL(a):[a e n => add(a,2)=next(next(a))]
Premise
Prove: ALL(a):[a e n => add(a,0)=a]
Suppose...
33 x e n
Premise
34 x e n => add(x,2)=next(next(x))
U Spec, 32
35 add(x,2)=next(next(x))
Detach, 34, 33
36 ALL(b):[x e n & b e n => add(x,next(b))=next(add(x,b))]
U Spec, 13
37 x e n & 1 e n => add(x,next(1))=next(add(x,1))
U Spec, 36
38 x e n & 1 e n
Join, 33, 7
39 add(x,next(1))=next(add(x,1))
Detach, 37, 38
40 add(x,2)=next(add(x,1))
Substitute, 10, 39
41 next(next(x))=next(add(x,1))
Substitute, 35, 40
42 ALL(b):[next(x) e n & b e n => [next(next(x))=next(b) => next(x)=b]]
U Spec, 4
43 next(x) e n & add(x,1) e n => [next(next(x))=next(add(x,1)) => next(x)=add(x,1)]
U Spec, 42
44 x e n => next(x) e n
U Spec, 3
45 next(x) e n
Detach, 44, 33
46 ALL(b):[x e n & b e n => add(x,b) e n]
U Spec, 12
47 x e n & 1 e n => add(x,1) e n
U Spec, 46
48 add(x,1) e n
Detach, 47, 38
49 next(x) e n & add(x,1) e n
Join, 45, 48
50 next(next(x))=next(add(x,1)) => next(x)=add(x,1)
Detach, 43, 49
51 next(x)=add(x,1)
Detach, 50, 41
52 ALL(b):[x e n & b e n => add(x,next(b))=next(add(x,b))]
U Spec, 13
53 x e n & 0 e n => add(x,next(0))=next(add(x,0))
U Spec, 52
54 x e n & 0 e n
Join, 33, 2
55 add(x,next(0))=next(add(x,0))
Detach, 53, 54
56 add(x,1)=next(add(x,0))
Substitute, 8, 55
57 next(x)=next(add(x,0))
Substitute, 51, 56
58 ALL(b):[x e n & b e n => [next(x)=next(b) => x=b]]
U Spec, 4
59 x e n & add(x,0) e n => [next(x)=next(add(x,0)) => x=add(x,0)]
U Spec, 58
60 ALL(b):[x e n & b e n => add(x,b) e n]
U Spec, 12
61 x e n & 0 e n => add(x,0) e n
U Spec, 60
62 x e n & 0 e n
Join, 33, 2
63 add(x,0) e n
Detach, 61, 62
64 x e n & add(x,0) e n
Join, 33, 63
65 next(x)=next(add(x,0)) => x=add(x,0)
Detach, 59, 64
66 x=add(x,0)
Detach, 65, 57
67 add(x,0)=x
Sym, 66
As Required:
68 ALL(a):[a e n => add(a,0)=a]
4 Conclusion, 33
As Required:
69 ALL(a):[a e n => add(a,2)=next(next(a))]
=> ALL(a):[a e n => add(a,0)=a]
4 Conclusion, 32
70 [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]]
Join, 31, 69
71 ALL(a):[a e n => add(a,0)=a]
<=> ALL(a):[a e n => add(a,2)=next(next(a))]
Iff-And, 70
As Required:
72 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))]]]
4 Conclusion, 11