THEOREM
*******
ALL(a):[a e n => ~s(a)=a]
Where n = the set of natural
numbers, s() is the successor function on n as defined
below.
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
PROOF BY INDUCTION
******************
Construct p
Apply the Subset Axiom
7 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~s(a)=a]]
Subset, 1
8 Set(p) & ALL(a):[a e p <=> a e n & ~s(a)=a]
E Spec, 7
Define: p
9 Set(p)
Split, 8
10 ALL(a):[a e p <=> a e n & ~s(a)=a]
Split, 8
Apply Induction Axiom
11 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...
12 x e p
Premise
Apply definition of p
13 x e p <=> x e n & ~s(x)=x
U Spec, 10
14 [x e p => x e n & ~s(x)=x] & [x e n & ~s(x)=x => x e p]
Iff-And, 13
15 x e p => x e n & ~s(x)=x
Split, 14
16 x e n & ~s(x)=x => x e p
Split, 14
17 x e n & ~s(x)=x
Detach, 15, 12
18 x e n
Split, 17
As Required:
19 ALL(b):[b e p => b e n]
4 Conclusion, 12
Joining results...
20 Set(p) & ALL(b):[b e p => b e n]
Join, 9, 19
Sufficient: For ALL(b):[b e n => b e p]
21 0 e p & ALL(b):[b e p => s(b) e p]
=>
ALL(b):[b e n => b e p]
Detach, 11, 20
BASE CASE
*********
Prove: 0 e p
Apply definition of p
22 0 e p <=> 0 e n & ~s(0)=0
U Spec, 10
23 [0 e p => 0 e n & ~s(0)=0] & [0 e n & ~s(0)=0 => 0 e p]
Iff-And, 22
24 0 e p => 0 e n & ~s(0)=0
Split, 23
Sufficient: For 0 e p
25 0 e n & ~s(0)=0 => 0 e p
Split, 23
Apply axiom
26 0 e n => ~s(0)=0
U Spec, 5
27 ~s(0)=0
Detach, 26, 2
28 0 e n & ~s(0)=0
Join, 2, 27
As Required:
29 0 e p
Detach, 25, 28
INDUCTIVE STEP
**************
Prove: ALL(b):[b e p => s(b) e p]
Suppose...
30 y e p
Premise
Apply definition of p
31 y e p <=> y e n & ~s(y)=y
U Spec, 10
32 [y e p => y e n & ~s(y)=y] & [y e n & ~s(y)=y => y e p]
Iff-And, 31
33 y e p => y e n & ~s(y)=y
Split, 32
34 y e n & ~s(y)=y => y e p
Split, 32
35 y e n & ~s(y)=y
Detach, 33, 30
36 y e n
Split, 35
37 ~s(y)=y
Split, 35
Prove: ~~s(y) e p
Suppose to the contrary...
38 ~s(y) e p
Premise
Apply axiom
39 y e n => s(y) e n
U Spec, 3
40 s(y) e n
Detach, 39, 36
Apply definition of p
41 s(y) e p <=> s(y) e n & ~s(s(y))=s(y)
U Spec, 10, 40
42 [s(y) e p => s(y) e n & ~s(s(y))=s(y)]
&
[s(y) e n & ~s(s(y))=s(y) => s(y) e p]
Iff-And, 41
43 s(y) e p => s(y) e n & ~s(s(y))=s(y)
Split, 42
44 s(y) e n & ~s(s(y))=s(y) => s(y) e p
Split, 42
45 ~s(y) e p => ~[s(y) e n & ~s(s(y))=s(y)]
Contra, 44
46 ~[s(y) e n & ~s(s(y))=s(y)]
Detach, 45, 38
47 ~~[s(y) e n => ~~s(s(y))=s(y)]
Imply-And, 46
48 s(y) e n => ~~s(s(y))=s(y)
Rem DNeg, 47
49 s(y) e n => s(s(y))=s(y)
Rem DNeg, 48
50 s(s(y))=s(y)
Detach, 49, 40
Apply axiom
51 ALL(b):[y e n & b e n => [s(y)=s(b) => y=b]]
U Spec, 4
52 ALL(b):[y e n & b e n => [s(y)=s(b) => y=b]]
U Spec, 4
53 y e n & s(y) e n => [s(y)=s(s(y)) => y=s(y)]
U Spec, 52, 40
54 y e n & s(y) e n
Join, 36, 40
55 s(y)=s(s(y)) => y=s(y)
Detach, 53, 54
56 s(y)=s(s(y))
Sym, 50
57 y=s(y)
Detach, 55, 56
58 s(y)=y
Sym, 57
Obtain the contradiction...
59 s(y)=y & ~s(y)=y
Join, 58, 37
As Required:
60 ~~s(y) e p
4 Conclusion, 38
As Required:
61 s(y) e p
Rem DNeg, 60
As Required:
62 ALL(b):[b e p => s(b) e p]
4 Conclusion, 30
Joining results...
63 0 e p & ALL(b):[b e p => s(b) e p]
Join, 29, 62
As Required:
64 ALL(b):[b e n => b e p]
Detach, 21, 63
Prove: ALL(a):[a e n => ~s(a)=a]
Suppose...
65 z e n
Premise
66 z e n => z e p
U Spec, 64
67 z e p
Detach, 66, 65
Apply definition of p
68 z e p <=> z e n & ~s(z)=z
U Spec, 10
69 [z e p => z e n & ~s(z)=z] & [z e n & ~s(z)=z => z e p]
Iff-And, 68
70 z e p => z e n & ~s(z)=z
Split, 69
71 z e n & ~s(z)=z => z e p
Split, 69
72 z e n & ~s(z)=z
Detach, 70, 67
73 z e n
Split, 72
74 ~s(z)=z
Split, 72
As Required:
75 ALL(a):[a e n => ~s(a)=a]
4 Conclusion, 65