THEOREM
*******
Assume the existence of an
infinite set m. We can select a subset n of m such that: n = {n0, s(n0), s(s(n0))...}, and each of the Peano
Axioms can be shown to hold n on (n,s,n0).
PA1 n0 e n (Lines 20-30)
PA2 s: n --> n (Lines 31-59)
PA3 s is injective (Lines 60-71)
PA4 s(x)=/=n0 (Lines 72-77)
PA5 Induction (Lines 78-105)
Only direct proof is used. An
axiom of set theory is used only once (on line 8, the Subset Axiom, equivalent
to Specification in ZFC).
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 software available
at http://www.dcproof.com
PROOF
*****
Assume the existence of an
infinite set m (after Dedekind)
1 Set(m)
Axiom
Define: s
s: m --> m
2 ALL(a):[a e m => s(a) e m]
Axiom
s is injective
3 ALL(a):ALL(b):[a e m & b e m => [s(a)=s(b) => a=b]]
Axiom
s is not surjective
4 EXIST(a):[a e m & ALL(b):[b e m => ~s(b)=a]]
Axiom
Define: n0
5 n0 e m & ALL(b):[b e m => ~s(b)=n0]
E Spec, 4
6 n0 e m
Split, 5
7 ALL(b):[b e m => ~s(b)=n0]
Split, 5
Construct n
Apply the Subset Axiom
8 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]]
Subset, 1
9 Set(n) & ALL(a):[a e n <=> a e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]
E Spec, 8
Define: n
Informally, n = {n0, s(n0),
s(s(n0))...}
10 Set(n)
Split, 9
11 ALL(a):[a e n <=> a e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]
Split, 9
Prove: ALL(a):[a e n => a e m]
Suppose...
12 x e n
Premise
13 x e n <=> x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
U Spec, 11
14 [x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]]
&
[x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n]
Iff-And, 13
15 x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 14
16 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n
Split, 14
17 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Detach, 15, 12
18 x e m
Split, 17
As Required:
19 ALL(a):[a e n => a e m]
4 Conclusion, 12
PA1
Prove: n0 e n
20 n0 e n <=> n0 e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b]
U Spec, 11
21 [n0 e n => n0 e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b]]
&
[n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b] => n0 e n]
Iff-And, 20
22 n0 e n => n0 e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b]
Split, 21
Sufficient: For n0 e n
23 n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b] => n0 e n
Split, 21
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e m]
Suppose...
24 Set(y) & ALL(c):[c e y => c e m]
&
n0 e y
&
ALL(c):[c e y => s(c) e y]
Premise
25 Set(y)
Split, 24
26 ALL(c):[c e y => c e m]
Split, 24
27 n0 e y
Split, 24
As Required:
28 ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b]
4 Conclusion, 24
29 n0 e m
&
ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
n0 e b]
Join, 6, 28
PA1
30 n0 e n
Detach, 23, 29
PA2
Prove: ALL(a):[a e n => s(a) e n]
Suppose...
31 x e n
Premise
32 s(x) e n <=> s(x) e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b]
U Spec, 11
33 [s(x) e n => s(x) e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b]]
&
[s(x) e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b] => s(x) e n]
Iff-And, 32
34 s(x) e n => s(x) e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b]
Split, 33
Sufficient: For s(x) e n
35 s(x) e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b] => s(x) e n
Split, 33
36 x e m => s(x) e m
U Spec, 2
37 x e n => x e m
U Spec, 19
38 x e m
Detach, 37, 31
As Required:
39 s(x) e m
Detach, 36, 38
Prove: ALL(b):[Set(b) &
ALL(c):[c e b => c e m]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
Suppose...
40 Set(y) & ALL(c):[c e y => c e m]
&
n0 e y
&
ALL(c):[c e y => s(c) e y]
Premise
41 Set(y)
Split, 40
42 ALL(c):[c e y => c e m]
Split, 40
43 n0 e y
Split, 40
44 ALL(c):[c e y => s(c) e y]
Split, 40
45 x e n <=> x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
U Spec, 11
46 [x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]]
&
[x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n]
Iff-And, 45
47 x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 46
48 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n
Split, 46
49 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Detach, 47, 31
50 x e m
Split, 49
51 ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
& ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 49
52 Set(y) & ALL(c):[c e y => c e m]
&
n0 e y
&
ALL(c):[c e y => s(c) e y]
=>
x e y
U Spec, 51
53 x e y
Detach, 52, 40
54 x e y => s(x) e y
U Spec, 44
55 s(x) e y
Detach, 54, 53
As Required:
56 ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b]
4 Conclusion, 40
57 s(x) e m
&
ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
s(x) e b]
Join, 39, 56
58 s(x) e n
Detach, 35, 57
PA2
59 ALL(a):[a e n => s(a) e n]
4 Conclusion, 31
PA3
Prove: ALL(a):ALL(b):[a e n & b e n =>
[s(a)=s(b) => a=b]]
Suppose...
60 x e n & y e n
Premise
61 x e n
Split, 60
62 y e n
Split, 60
63 ALL(b):[x e m & b e m => [s(x)=s(b) => x=b]]
U Spec, 3
64 x e m & y e m => [s(x)=s(y) => x=y]
U Spec, 63
65 x e n => x e m
U Spec, 19
66 x e m
Detach, 65, 61
67 y e n => y e m
U Spec, 19
68 y e m
Detach, 67, 62
69 x e m & y e m
Join, 66, 68
70 s(x)=s(y) => x=y
Detach, 64, 69
PA3
71 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
4 Conclusion, 60
PA4
Prove: ALL(a):[a e n => ~s(a)=n0]
Suppose...
72 x e n
Premise
73 x e m => ~s(x)=n0
U Spec, 7
74 x e n => x e m
U Spec, 19
75 x e m
Detach, 74, 72
76 ~s(x)=n0
Detach, 73, 75
PA4
77 ALL(a):[a e n => ~s(a)=n0]
4 Conclusion, 72
PA5 (Induction)
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
78 Set(p) & ALL(b):[b e p => b e n]
Premise
79 Set(p)
Split, 78
80 ALL(b):[b e p => b e n]
Split, 78
Prove: n0 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
81 n0 e p & ALL(b):[b e p => s(b) e p]
Premise
82 n0 e p
Split, 81
83 ALL(b):[b e p => s(b) e p]
Split, 81
Prove: ALL(b):[b e n => b e p]
Suppose...
84 x e n
Premise
85 x e n <=> x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
U Spec, 11
86 [x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=> x e b]]
&
[x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n]
Iff-And, 85
87 x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 86
88 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e n
Split, 86
89 x e m & ALL(b):[Set(b)
& ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Detach, 87, 84
90 x e m
Split, 89
91 ALL(b):[Set(b) & ALL(c):[c e b => c e m]
&
n0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 89
Sufficient: For x e p
92 Set(p) & ALL(c):[c e p => c e m]
&
n0 e p
&
ALL(c):[c e p => s(c) e p]
=>
x e p
U Spec, 91
93 y e p
Premise
94 y e p => y e n
U Spec, 80
95 y e n
Detach, 94, 93
96 y e n => y e m
U Spec, 19
97 y e m
Detach, 96, 95
As Required:
98 ALL(c):[c e p => c e m]
4 Conclusion, 93
99 Set(p) & ALL(c):[c e p => c e m]
Join, 79, 98
100 Set(p) & ALL(c):[c e p => c e m] & n0 e p
Join, 99, 82
101 Set(p) & ALL(c):[c e p => c e m] & n0 e p
&
ALL(b):[b e p => s(b) e p]
Join, 100, 83
102 x e p
Detach, 92, 101
As Required:
103 ALL(b):[b e n => b e p]
4 Conclusion, 84
As Required:
104 n0 e p & ALL(b):[b e p => s(b) e p]
=>
ALL(b):[b e n => b e p]
4 Conclusion, 81
PA5 (Induction axiom)
105 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=>
[n0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
4 Conclusion, 78