THEOREM
*******
The successor function defined on the set of natural N connects every number to another one. The induction axiom rules out the possibility that any non-empty, proper subset of N can be completely disconnected from the remainder of N.
Given Peano's Axioms, we have:
~EXIST(a):[Set(a)
& ALL(b):[b e a => b e n]
& EXIST(b):b e a
& EXIST(b):[b e n & ~b e a]
& ALL(b):ALL(c):[b e a & c e n & ~c e a => ~s(b)=c & ~s(c)=b]]
We begin by assuming to the contrary that such a subset exists in the natural numbers. We then show that this will falsify the principle of induction, leading to a contradiction.
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
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]] (Not used here)
Axiom
5 ALL(a):[a e n => ~s(a)=0] (Not used here)
Axiom
Induction principle:
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
Suppose to the contrary...
7 Set(x)
& ALL(b):[b e x => b e n]
& EXIST(b):b e x
& EXIST(b):[b e n & ~b e x]
& ALL(b):ALL(c):[b e x & c e n & ~c e x => ~s(b)=c & ~s(c)=b]
Premise
x is a non-empty, proper subset of n
8 Set(x)
Split, 7
9 ALL(b):[b e x => b e n]
Split, 7
10 EXIST(b):b e x
Split, 7
11 EXIST(b):[b e n & ~b e x]
Split, 7
x is completely disconnected from those elements of n not in x
12 ALL(b):ALL(c):[b e x & c e n & ~c e x => ~s(b)=c & ~s(c)=b]
Split, 7
Define: y (an element of x)
13 y e x
E Spec, 10
14 y e x => y e n
U Spec, 9
15 y e n
Detach, 14, 13
16 z e n & ~z e x
E Spec, 11
Define: z (an element of n not in x)
17 z e n
Split, 16
18 ~z e x
Split, 16
Construct the complement of x wrt n
Apply the Subset Axiom
19 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~a e x]]
Subset, 1
20 Set(x') & ALL(a):[a e x' <=> a e n & ~a e x]
E Spec, 19
Define: x' (the complement of x wrt n)
21 Set(x')
Split, 20
22 ALL(a):[a e x' <=> a e n & ~a e x]
Split, 20
Two cases to consider:
23 0 e x | ~0 e x
Or Not
Case 1
Prove: ~0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n] (negation of induction axiom)
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Suppose...
24 ~0 e x
Premise
Prove: 0 e x'
Apply definition of x'
25 0 e x' <=> 0 e n & ~0 e x
U Spec, 22
26 [0 e x' => 0 e n & ~0 e x] & [0 e n & ~0 e x => 0 e x']
Iff-And, 25
27 0 e x' => 0 e n & ~0 e x
Split, 26
28 0 e n & ~0 e x => 0 e x'
Split, 26
29 0 e n & ~0 e x
Join, 2, 24
As Required:
30 0 e x'
Detach, 28, 29
Prove: ALL(b):[b e x' => s(b) e x']
Suppose...
31 t e x'
Premise
Prove: ~tex
Apply definition of x'
32 t e x' <=> t e n & ~t e x
U Spec, 22
33 [t e x' => t e n & ~t e x] & [t e n & ~t e x => t e x']
Iff-And, 32
34 t e x' => t e n & ~t e x
Split, 33
35 t e n & ~t e x => t e x'
Split, 33
36 t e n & ~t e x
Detach, 34, 31
37 t e n
Split, 36
As Required:
38 ~t e x
Split, 36
Prove: ~s(t) e x
Suppose to contrary...
39 s(t) e x
Premise
Apply initial premise
40 ALL(c):[s(t) e x & c e n & ~c e x => ~s(s(t))=c & ~s(c)=s(t)]
U Spec, 12
41 s(t) e x & t e n & ~t e x => ~s(s(t))=t & ~s(t)=s(t)
U Spec, 40
42 s(t) e x & t e n
Join, 39, 37
43 s(t) e x & t e n & ~t e x
Join, 42, 38
44 ~s(s(t))=t & ~s(t)=s(t)
Detach, 41, 43
45 ~s(s(t))=t
Split, 44
46 ~s(t)=s(t)
Split, 44
47 s(t)=s(t)
Reflex
Obtain contradiction...
48 s(t)=s(t) & ~s(t)=s(t)
Join, 47, 46
As Required:
49 ~s(t) e x
4 Conclusion, 39
Prove: s(t)ex'
Apply defintion of x'
50 s(t) e x' <=> s(t) e n & ~s(t) e x
U Spec, 22
51 [s(t) e x' => s(t) e n & ~s(t) e x]
& [s(t) e n & ~s(t) e x => s(t) e x']
Iff-And, 50
52 s(t) e x' => s(t) e n & ~s(t) e x
Split, 51
53 s(t) e n & ~s(t) e x => s(t) e x'
Split, 51
Apply axiom
54 t e n => s(t) e n
U Spec, 3
55 s(t) e n
Detach, 54, 37
56 s(t) e n & ~s(t) e x
Join, 55, 49
As Required:
57 s(t) e x'
Detach, 53, 56
As Required:
58 ALL(b):[b e x' => s(b) e x']
4 Conclusion, 31
Prove: y e x'
Apply definition of x'
59 y e x' <=> y e n & ~y e x
U Spec, 22
60 [y e x' => y e n & ~y e x] & [y e n & ~y e x => y e x']
Iff-And, 59
61 y e x' => y e n & ~y e x
Split, 60
62 y e n & ~y e x => y e x'
Split, 60
63 ~[y e n & ~y e x] => ~y e x'
Contra, 61
64 ~~[~y e n | ~~y e x] => ~y e x'
DeMorgan, 63
65 ~y e n | ~~y e x => ~y e x'
Rem DNeg, 64
66 ~y e n | y e x => ~y e x'
Rem DNeg, 65
67 ~y e n | y e x
Arb Or, 13
As Required:
68 ~y e x'
Detach, 66, 67
69 y e n & ~y e x'
Join, 15, 68
As Required:
70 EXIST(b):[b e n & ~b e x']
E Gen, 69
Prove: ALL(b):[b e x' => b e n]
Suppose...
71 t e x'
Premise
Prove: ten
Apply definition of x'
72 t e x' <=> t e n & ~t e x
U Spec, 22
73 [t e x' => t e n & ~t e x] & [t e n & ~t e x => t e x']
Iff-And, 72
74 t e x' => t e n & ~t e x
Split, 73
75 t e n & ~t e x => t e x'
Split, 73
76 t e n & ~t e x
Detach, 74, 71
As Required:
77 t e n
Split, 76
As Required:
78 ALL(b):[b e x' => b e n]
4 Conclusion, 71
79 Set(x') & ALL(b):[b e x' => b e n]
Join, 21, 78
80 0 e x' & ALL(b):[b e x' => s(b) e x']
Join, 30, 58
81 0 e x' & ALL(b):[b e x' => s(b) e x']
& EXIST(b):[b e n & ~b e x']
Join, 80, 70
82 Set(x') & ALL(b):[b e x' => b e n]
& [0 e x' & ALL(b):[b e x' => s(b) e x']
& EXIST(b):[b e n & ~b e x']]
Join, 79, 81
83 EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
E Gen, 82
Case 1
As Required:
84 ~0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
4 Conclusion, 24
Case 2
Prove: 0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n] (negation of induction axiom)
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Suppose...
85 0 e x
Premise
Prove: ALL(b):[b e x => s(b) e x]
Suppose...
86 t e x
Premise
Prove: ~t e x'
Apply definition of x'
87 t e x' <=> t e n & ~t e x
U Spec, 22
88 [t e x' => t e n & ~t e x] & [t e n & ~t e x => t e x']
Iff-And, 87
89 t e x' => t e n & ~t e x
Split, 88
90 t e n & ~t e x => t e x'
Split, 88
91 ~[t e n & ~t e x] => ~t e x'
Contra, 89
92 ~~[~t e n | ~~t e x] => ~t e x'
DeMorgan, 91
93 ~t e n | ~~t e x => ~t e x'
Rem DNeg, 92
94 ~t e n | t e x => ~t e x'
Rem DNeg, 93
95 ~t e n | t e x
Arb Or, 86
As Required:
96 ~t e x'
Detach, 94, 95
Prove: ~s(t) e x'
Suppose to the contrary...
97 s(t) e x'
Premise
Apply intitial premise
98 ALL(c):[t e x & c e n & ~c e x => ~s(t)=c & ~s(c)=t]
U Spec, 12
99 t e x & s(t) e n & ~s(t) e x => ~s(t)=s(t) & ~s(s(t))=t
U Spec, 98
100 s(t) e x' <=> s(t) e n & ~s(t) e x
U Spec, 22
101 [s(t) e x' => s(t) e n & ~s(t) e x]
& [s(t) e n & ~s(t) e x => s(t) e x']
Iff-And, 100
102 s(t) e x' => s(t) e n & ~s(t) e x
Split, 101
103 s(t) e n & ~s(t) e x => s(t) e x'
Split, 101
104 s(t) e n & ~s(t) e x
Detach, 102, 97
105 s(t) e n
Split, 104
106 ~s(t) e x
Split, 104
107 t e x & s(t) e n
Join, 86, 105
108 t e x & s(t) e n & ~s(t) e x
Join, 107, 106
109 ~s(t)=s(t) & ~s(s(t))=t
Detach, 99, 108
110 ~s(t)=s(t)
Split, 109
111 ~s(s(t))=t
Split, 109
112 s(t)=s(t)
Reflex
Obtain contradiction...
113 s(t)=s(t) & ~s(t)=s(t)
Join, 112, 110
As Required:
114 ~s(t) e x'
4 Conclusion, 97
115 s(t) e x' <=> s(t) e n & ~s(t) e x
U Spec, 22
116 [s(t) e x' => s(t) e n & ~s(t) e x]
& [s(t) e n & ~s(t) e x => s(t) e x']
Iff-And, 115
117 s(t) e x' => s(t) e n & ~s(t) e x
Split, 116
118 s(t) e n & ~s(t) e x => s(t) e x'
Split, 116
119 ~s(t) e x' => ~[s(t) e n & ~s(t) e x]
Contra, 118
120 ~[s(t) e n & ~s(t) e x]
Detach, 119, 114
121 ~~[s(t) e n => ~~s(t) e x]
Imply-And, 120
122 s(t) e n => ~~s(t) e x
Rem DNeg, 121
123 s(t) e n => s(t) e x
Rem DNeg, 122
Apply initial premise
124 t e x => t e n
U Spec, 9
125 t e n
Detach, 124, 86
126 t e n => s(t) e n
U Spec, 3
127 s(t) e n
Detach, 126, 125
128 s(t) e x
Detach, 123, 127
As Required:
129 ALL(b):[b e x => s(b) e x]
4 Conclusion, 86
130 Set(x) & ALL(b):[b e x => b e n]
Join, 8, 9
131 0 e x & ALL(b):[b e x => s(b) e x]
Join, 85, 129
132 0 e x & ALL(b):[b e x => s(b) e x]
& EXIST(b):[b e n & ~b e x]
Join, 131, 11
133 Set(x) & ALL(b):[b e x => b e n]
& [0 e x & ALL(b):[b e x => s(b) e x]
& EXIST(b):[b e n & ~b e x]]
Join, 130, 132
134 EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
E Gen, 133
Case 2
As Required:
135 0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
4 Conclusion, 85
Joining results for Cases Rule
136 [0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]]
& [~0 e x
=> EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]]
Join, 135, 84
Apply Cases Rule
In both cases, we have...
137 EXIST(a):[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Cases, 23, 136
138 ~ALL(a):~[Set(a) & ALL(b):[b e a => b e n]
& [0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Quant, 137
139 ~ALL(a):~~[Set(a) & ALL(b):[b e a => b e n] => ~[0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Imply-And, 138
140 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] => ~[0 e a & ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]]
Rem DNeg, 139
141 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] => ~~[0 e a & ALL(b):[b e a => s(b) e a] => ~EXIST(b):[b e n & ~b e a]]]
Imply-And, 140
142 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [0 e a & ALL(b):[b e a => s(b) e a] => ~EXIST(b):[b e n & ~b e a]]]
Rem DNeg, 141
143 ~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]]]
Quant, 142
144 ~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]]]
Rem DNeg, 143
145 ~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]]]
Imply-And, 144
146 ~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]]]
Rem DNeg, 145
147 ~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]]]
Rem DNeg, 146
Obtain the contradiction...
148 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]]]
& ~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]]]
Join, 6, 147
As Required:
149 ~EXIST(a):[Set(a)
& ALL(b):[b e a => b e n]
& EXIST(b):b e a
& EXIST(b):[b e n & ~b e a]
& ALL(b):ALL(c):[b e a & c e n & ~c e a => ~s(b)=c & ~s(c)=b]]
4 Conclusion, 7