Introduction
------------
Here is described a set n with a successor function s defined on it. 1 is an element of n, and for all but a single element x, this successor function s behaves like the normal successor on the set of natural numbers. The element x, however, is the successor of itself. No natural number can be a successor of itself. (See Example 13 of DC Proof Tutorial)
Despite this anomaly, n, 1 and s can be shown to conform to all of the Peano Axioms but the axiom of mathematical induction -- which is shown not to hold here. This shows the induction axiom on not dependent on the other Peano axioms.
PA1: 1 e n
PA2: ALL(a):[a e n => s(a) e n]
PA3: ALL(a):[a e n => ~s(a)=1]
PA4: ALL(a):ALL(b):[a e n & b e n & s(a)=s(b) => a=b]
PA5: ALL(a):[Set(a) (Shown not to hold here)
& ALL(b):[b e a => b e n]
& 1 e a
& ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]
Note: This proof was written with the aid of DC Proof 2.0.
Download at http://www.dcproof.com
Axioms
------
Properties of n, 1, x and s
n is a set
1 Set(n)
Axiom
PA1:
---
2 1 e n
Axiom
3 x e n
Axiom
4 ~x=1
Axiom
5 ALL(a):[a e n & ~a=x => s(a) e n & ~s(a)=x]
Axiom
6 ALL(a):[a e n & ~a=x => ~s(a)=1]
Axiom
7 ALL(a):ALL(b):[a e n & ~a=x & b e n & ~b=x & s(a)=s(b) => a=b]
Axiom
8 s(x)=x
Axiom
Proof
-----
PA2
---
Prove: ALL(a):[a e n => s(a) e n]
Suppose...
9 y e n
Premise
2 cases:
10 y=x | ~y=x
Or Not
Case 1
Prove: y=x => s(y) e n
Suppose...
11 y=x
Premise
12 s(y)=x
Substitute, 11, 8
13 s(y) e n
Substitute, 12, 3
Case 1
As Required:
14 y=x => s(y) e n
4 Conclusion, 11
Case 2
Prove: ~y=x => s(y) e n
Suppose...
15 ~y=x
Premise
Apply axiom
16 y e n & ~y=x => s(y) e n & ~s(y)=x
U Spec, 5
17 y e n & ~y=x
Join, 9, 15
18 s(y) e n & ~s(y)=x
Detach, 16, 17
19 s(y) e n
Split, 18
Case 2
As Required:
20 ~y=x => s(y) e n
4 Conclusion, 15
21 [y=x => s(y) e n] & [~y=x => s(y) e n]
Join, 14, 20
22 s(y) e n
Cases, 10, 21
PA2:
---
23 ALL(a):[a e n => s(a) e n]
4 Conclusion, 9
PA3
---
Prove: ALL(a):[a e n => ~s(a)=1]
Suppose...
24 y e n
Premise
2 cases:
25 y=x | ~y=x
Or Not
Case 1
Prove: y=x => ~s(y)=1
Suppose...
26 y=x
Premise
Prove: ~s(y)=1
Suppose to the contrary...
27 s(y)=1
Premise
28 s(x)=1
Substitute, 26, 27
29 x=1
Substitute, 8, 28
30 x=1 & ~x=1
Join, 29, 4
As Required:
31 ~s(y)=1
4 Conclusion, 27
Case 1
As Required:
32 y=x => ~s(y)=1
4 Conclusion, 26
Case 2
Prove: ~y=x => ~s(y)=1
Suppose...
33 ~y=x
Premise
Apply axiom
34 y e n & ~y=x => ~s(y)=1
U Spec, 6
35 y e n & ~y=x
Join, 24, 33
36 ~s(y)=1
Detach, 34, 35
Case 2
As Required:
37 ~y=x => ~s(y)=1
4 Conclusion, 33
38 [y=x => ~s(y)=1] & [~y=x => ~s(y)=1]
Join, 32, 37
39 ~s(y)=1
Cases, 25, 38
PA3:
---
40 ALL(a):[a e n => ~s(a)=1]
4 Conclusion, 24
PA4
---
Prove: ALL(a):[a e n => [s(a)=x => a=x]]
Suppose...
41 y e n
Premise
Prove: s(y)=x => y=x
Suppose...
42 s(y)=x
Premise
Prove: y=x
Suppose to the contrary...
43 ~y=x
Premise
Apply axiom
44 y e n & ~y=x => s(y) e n & ~s(y)=x
U Spec, 5
45 y e n & ~y=x
Join, 41, 43
46 s(y) e n & ~s(y)=x
Detach, 44, 45
47 s(y) e n
Split, 46
48 ~s(y)=x
Split, 46
49 s(y)=x & ~s(y)=x
Join, 42, 48
50 ~~y=x
4 Conclusion, 43
As Required:
51 y=x
Rem DNeg, 50
As Required:
52 s(y)=x => y=x
4 Conclusion, 42
As Required:
53 ALL(a):[a e n => [s(a)=x => a=x]]
4 Conclusion, 41
Prove: ALL(a):[a e n => [~s(a)=x => ~a=x]]
Suppose...
54 y e n
Premise
Prove: ~s(y)=x => ~y=x
Suppose...
55 ~s(y)=x
Premise
Prove: ~y=x
Suppose to the contrary...
56 y=x
Premise
57 ~s(x)=x
Substitute, 56, 55
58 s(x)=x & ~s(x)=x
Join, 8, 57
As Required:
59 ~y=x
4 Conclusion, 56
As Required:
60 ~s(y)=x => ~y=x
4 Conclusion, 55
As Required:
61 ALL(a):[a e n => [~s(a)=x => ~a=x]]
4 Conclusion, 54
Prove: ALL(a):[a e n
=> ALL(b):[b e n & s(b)=a => ALL(c):[c e n & s(c)=a => b=c]]]
Suppose...
62 y e n
Premise
2 cases:
63 y=x | ~y=x
Or Not
Case 1
Prove: y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
Suppose...
64 y=x
Premise
Prove: ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
Suppose...
65 p e n & s(p)=y
Premise
66 p e n
Split, 65
67 s(p)=y
Split, 65
Prove: ALL(c):[c e n & s(c)=y => p=c]
Suppose...
68 q e n & s(q)=y
Premise
69 q e n
Split, 68
70 s(q)=y
Split, 68
71 s(p)=x
Substitute, 64, 67
72 s(q)=x
Substitute, 64, 70
Apply previous result for p
73 p e n => [s(p)=x => p=x]
U Spec, 53
74 s(p)=x => p=x
Detach, 73, 66
75 p=x
Detach, 74, 71
Apply previous result for q
76 q e n => [s(q)=x => q=x]
U Spec, 53
77 s(q)=x => q=x
Detach, 76, 69
78 q=x
Detach, 77, 72
79 p=q
Substitute, 78, 75
As Required:
80 ALL(c):[c e n & s(c)=y => p=c]
4 Conclusion, 68
As Required:
81 ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
4 Conclusion, 65
Case 1
As Required:
82 y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
4 Conclusion, 64
Case 2
Prove: ~y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
Suppose...
83 ~y=x
Premise
84 p e n & s(p)=y
Premise
85 p e n
Split, 84
86 s(p)=y
Split, 84
Sufficient: ALL(c):[c e n & s(c)=y => p=c]
Suppose...
87 q e n & s(q)=y
Premise
88 q e n
Split, 87
89 s(q)=y
Split, 87
Apply axiom
90 ALL(b):[p e n & ~p=x & b e n & ~b=x & s(p)=s(b) => p=b]
U Spec, 7
91 p e n & ~p=x & q e n & ~q=x & s(p)=s(q) => p=q
U Spec, 90
92 ~s(p)=x
Substitute, 86, 83
93 ~s(q)=x
Substitute, 89, 83
94 p e n => [~s(p)=x => ~p=x]
U Spec, 61
95 ~s(p)=x => ~p=x
Detach, 94, 85
96 ~p=x
Detach, 95, 92
Apply previous result
97 q e n => [~s(q)=x => ~q=x]
U Spec, 61
98 ~s(q)=x => ~q=x
Detach, 97, 88
99 ~q=x
Detach, 98, 93
100 s(p)=s(q)
Substitute, 89, 86
101 p e n & ~p=x
Join, 85, 96
102 p e n & ~p=x & q e n
Join, 101, 88
103 p e n & ~p=x & q e n & ~q=x
Join, 102, 99
104 p e n & ~p=x & q e n & ~q=x & s(p)=s(q)
Join, 103, 100
105 p=q
Detach, 91, 104
As Required:
106 ALL(c):[c e n & s(c)=y => p=c]
4 Conclusion, 87
As Required:
107 ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
4 Conclusion, 84
Case 2
As Required:
108 ~y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
4 Conclusion, 83
109 [y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]]
& [~y=x
=> ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]]
Join, 82, 108
110 ALL(b):[b e n & s(b)=y => ALL(c):[c e n & s(c)=y => b=c]]
Cases, 63, 109
As Required:
111 ALL(a):[a e n
=> ALL(b):[b e n & s(b)=a => ALL(c):[c e n & s(c)=a => b=c]]]
4 Conclusion, 62
Prove: ALL(a):ALL(b):[a e n & b e n & s(a)=s(b) => a=b]
Suppose...
112 y e n & z e n & s(y)=s(z)
Premise
113 y e n
Split, 112
114 z e n
Split, 112
115 s(y)=s(z)
Split, 112
Apply previous result
116 s(y) e n
=> ALL(b):[b e n & s(b)=s(y) => ALL(c):[c e n & s(c)=s(y) => b=c]]
U Spec, 111
117 y e n => s(y) e n
U Spec, 23
118 s(y) e n
Detach, 117, 113
119 ALL(b):[b e n & s(b)=s(y) => ALL(c):[c e n & s(c)=s(y) => b=c]]
Detach, 116, 118
120 z e n & s(z)=s(y) => ALL(c):[c e n & s(c)=s(y) => z=c]
U Spec, 119
121 s(z)=s(y)
Sym, 115
122 z e n & s(z)=s(y)
Join, 114, 121
123 ALL(c):[c e n & s(c)=s(y) => z=c]
Detach, 120, 122
124 y e n & s(y)=s(y) => z=y
U Spec, 123
125 s(y)=s(y)
Reflex
126 y e n & s(y)=s(y)
Join, 113, 125
127 z=y
Detach, 124, 126
128 y=z
Sym, 127
PA4:
---
129 ALL(a):ALL(b):[a e n & b e n & s(a)=s(b) => a=b]
4 Conclusion, 112
PA5
---
Prove: ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ALL(b):[b e n => b e a]]
Apply subset axiom
130 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~a=x]]
Subset, 1
131 Set(n') & ALL(a):[a e n' <=> a e n & ~a=x]
E Spec, 130
Define: n', n without element x
132 Set(n')
Split, 131
133 ALL(a):[a e n' <=> a e n & ~a=x]
Split, 131
Prove: ALL(b):[b e n' => b e n]
Suppose...
134 y e n'
Premise
Apply definiton of n'
135 y e n' <=> y e n & ~y=x
U Spec, 133
136 [y e n' => y e n & ~y=x] & [y e n & ~y=x => y e n']
Iff-And, 135
137 y e n' => y e n & ~y=x
Split, 136
138 y e n & ~y=x => y e n'
Split, 136
139 y e n & ~y=x
Detach, 137, 134
140 y e n
Split, 139
As Required:
141 ALL(b):[b e n' => b e n]
4 Conclusion, 134
Prove: 1 e n'
Apply definition of n'
142 1 e n' <=> 1 e n & ~1=x
U Spec, 133
143 [1 e n' => 1 e n & ~1=x] & [1 e n & ~1=x => 1 e n']
Iff-And, 142
144 1 e n' => 1 e n & ~1=x
Split, 143
145 1 e n & ~1=x => 1 e n'
Split, 143
146 ~1=x
Sym, 4
147 1 e n & ~1=x
Join, 2, 146
As Required:
148 1 e n'
Detach, 145, 147
Prove: ALL(b):[ben' => s(b)en']
Suppose...
149 y e n'
Premise
Apply definition of n'
150 y e n' <=> y e n & ~y=x
U Spec, 133
151 [y e n' => y e n & ~y=x] & [y e n & ~y=x => y e n']
Iff-And, 150
152 y e n' => y e n & ~y=x
Split, 151
153 y e n & ~y=x => y e n'
Split, 151
154 y e n & ~y=x
Detach, 152, 149
155 y e n
Split, 154
156 ~y=x
Split, 154
Apply axiom
157 y e n & ~y=x => s(y) e n & ~s(y)=x
U Spec, 5
158 s(y) e n & ~s(y)=x
Detach, 157, 154
Apply definiton of n'
159 s(y) e n' <=> s(y) e n & ~s(y)=x
U Spec, 133
160 [s(y) e n' => s(y) e n & ~s(y)=x]
& [s(y) e n & ~s(y)=x => s(y) e n']
Iff-And, 159
161 s(y) e n' => s(y) e n & ~s(y)=x
Split, 160
Sufficient: s(y) e n'
162 s(y) e n & ~s(y)=x => s(y) e n'
Split, 160
163 s(y) e n'
Detach, 162, 158
As Required:
164 ALL(b):[b e n' => s(b) e n']
4 Conclusion, 149
Prove: EXIST(b):[b e n & ~b e n'] (namely x)
Apply definition of n'
165 x e n' <=> x e n & ~x=x
U Spec, 133
166 [x e n' => x e n & ~x=x] & [x e n & ~x=x => x e n']
Iff-And, 165
167 [x e n' => x e n & ~x=x] & [x e n & ~x=x => x e n']
Iff-And, 165
168 x e n' => x e n & ~x=x
Split, 167
169 x e n & ~x=x => x e n'
Split, 167
170 ~[x e n & ~x=x] => ~x e n'
Contra, 168
171 ~~[~x e n | ~~x=x] => ~x e n'
DeMorgan, 170
172 ~x e n | ~~x=x => ~x e n'
Rem DNeg, 171
173 ~x e n | x=x => ~x e n'
Rem DNeg, 172
174 x=x
Reflex
175 ~x e n | x=x
Arb Or, 174
176 ~x e n'
Detach, 173, 175
177 x e n & ~x e n'
Join, 3, 176
As Required:
178 EXIST(b):[b e n & ~b e n']
E Gen, 177
Joining results...
179 Set(n') & ALL(b):[b e n' => b e n]
Join, 132, 141
180 Set(n') & ALL(b):[b e n' => b e n] & 1 e n'
Join, 179, 148
181 Set(n') & ALL(b):[b e n' => b e n] & 1 e n'
& ALL(b):[b e n' => s(b) e n']
Join, 180, 164
182 Set(n') & ALL(b):[b e n' => b e n] & 1 e n'
& ALL(b):[b e n' => s(b) e n']
& EXIST(b):[b e n & ~b e n']
Join, 181, 178
183 EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]
E Gen, 182
184 ~ALL(a):~[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a]
& EXIST(b):[b e n & ~b e a]]
Quant, 183
185 ~ALL(a):~~[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ~EXIST(b):[b e n & ~b e a]]
Imply-And, 184
186 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ~EXIST(b):[b e n & ~b e a]]
Rem DNeg, 185
187 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ~~ALL(b):~[b e n & ~b e a]]
Quant, 186
188 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ALL(b):~[b e n & ~b e a]]
Rem DNeg, 187
189 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ALL(b):~~[b e n => ~~b e a]]
Imply-And, 188
190 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ALL(b):[b e n => ~~b e a]]
Rem DNeg, 189
PA5: Does not hold
---
191 ~ALL(a):[Set(a) & ALL(b):[b e a => b e n] & 1 e a
& ALL(b):[b e a => s(b) e a] => ALL(b):[b e n => b e a]]
Rem DNeg, 190