INTRODUCTION
************
Here we derive an number of useful propositions from the axioms on lines 1 to 12.
Dan Christensen
Revised: 2014-04-24
This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
Axiom for partial functions of 1 variable giving the sufficient condition for the partial functionality of a set of ordered triples.
1 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[c e a & d e b => [f(c)=d <=> (c,d) e f]]]
Axiom
Define: n, 0, max, s
********************
Here s is a set of ordered pairs of elements of n.
2 Set(n)
Axiom
3 0 e n
Axiom
4 max e n
Axiom
5 Set'(s)
Axiom
s is a subset of n^2
6 ALL(a):ALL(b):[(a,b) e s => a e n & b e n]
Axiom
0 has no predecessor
7 ALL(a):[a e n => ~(a,0) e s]
Axiom
max has no successor
8 ALL(a):[a e n => ~(max,a) e s]
Axiom
All non-max elements have a successor
9 ALL(a):[a e n => [~a=max => EXIST(b):(a,b) e s]]
Axiom
Successors are unique
10 ALL(a):ALL(b):ALL(c):[(a,b) e s & (a,c) e s => b=c]
Axiom
Predecessors are unique
11 ALL(a):ALL(b):ALL(c):[(a,b) e s & (c,b) e s => a=c]
Axiom
Finite Induction
12 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):ALL(c):[b e a & c e n & (b,c) e s => c e a]
=> ALL(b):[b e n => b e a]]]
Axiom
13 ALL(a):ALL(b):[(a,b) e s => a e n & b e n]
& ALL(a):ALL(b):ALL(c):[(a,b) e s & (a,c) e s => b=c]
Join, 6, 10
14 ALL(a):ALL(b):[(a,b) e s => a e n & b e n]
& ALL(a):ALL(b):ALL(c):[(a,b) e s & (a,c) e s => b=c]
Join, 6, 10
15 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e s => c e a & d e b]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e s & (c,d2) e s => d1=d2]
=> ALL(c):ALL(d):[c e a & d e b => [s(c)=d <=> (c,d) e s]]]
U Spec, 1
16 ALL(b):[ALL(c):ALL(d):[(c,d) e s => c e n & d e b]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e s & (c,d2) e s => d1=d2]
=> ALL(c):ALL(d):[c e n & d e b => [s(c)=d <=> (c,d) e s]]]
U Spec, 15
17 ALL(c):ALL(d):[(c,d) e s => c e n & d e n]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e s & (c,d2) e s => d1=d2]
=> ALL(c):ALL(d):[c e n & d e n => [s(c)=d <=> (c,d) e s]]
U Spec, 16
18 ALL(a):ALL(b):[(a,b) e s => a e n & b e n]
& ALL(a):ALL(b):ALL(c):[(a,b) e s & (a,c) e s => b=c]
Join, 6, 10
s is a partial function on n
19 ALL(c):ALL(d):[c e n & d e n => [s(c)=d <=> (c,d) e s]]
Detach, 17, 18
Prove: ALL(a):[a e n => ~s(a)=0]
Suppose...
20 x e n
Premise
21 x e n => ~(x,0) e s
U Spec, 7
22 ~(x,0) e s
Detach, 21, 20
23 ALL(d):[x e n & d e n => [s(x)=d <=> (x,d) e s]]
U Spec, 19
24 x e n & 0 e n => [s(x)=0 <=> (x,0) e s]
U Spec, 23
25 x e n & 0 e n
Join, 20, 3
26 s(x)=0 <=> (x,0) e s
Detach, 24, 25
27 [s(x)=0 => (x,0) e s] & [(x,0) e s => s(x)=0]
Iff-And, 26
28 s(x)=0 => (x,0) e s
Split, 27
29 (x,0) e s => s(x)=0
Split, 27
30 ~(x,0) e s => ~s(x)=0
Contra, 28
31 ~s(x)=0
Detach, 30, 22
As Required:
32 ALL(a):[a e n => ~s(a)=0]
4 Conclusion, 20
Prove: ALL(a):[a e n => ~s(max)=a]
Suppose...
33 x e n
Premise
34 x e n => ~(max,x) e s
U Spec, 8
35 ~(max,x) e s
Detach, 34, 33
36 ALL(d):[max e n & d e n => [s(max)=d <=> (max,d) e s]]
U Spec, 19
37 max e n & x e n => [s(max)=x <=> (max,x) e s]
U Spec, 36
38 max e n & x e n
Join, 4, 33
39 s(max)=x <=> (max,x) e s
Detach, 37, 38
40 [s(max)=x => (max,x) e s] & [(max,x) e s => s(max)=x]
Iff-And, 39
41 s(max)=x => (max,x) e s
Split, 40
42 (max,x) e s => s(max)=x
Split, 40
43 ~(max,x) e s => ~s(max)=x
Contra, 41
44 ~s(max)=x
Detach, 43, 35
As Required:
45 ALL(a):[a e n => ~s(max)=a]
4 Conclusion, 33
Prove: ALL(a):[a e n => [~a=max => EXIST(b):[b e n & s(a)=b]]]
Suppose...
46 x e n
Premise
47 x e n => [~x=max => EXIST(b):(x,b) e s]
U Spec, 9
48 ~x=max => EXIST(b):(x,b) e s
Detach, 47, 46
Prove: ~x=max => EXIST(b):[b e n & s(x)=b]
Suppose...
49 ~x=max
Premise
50 EXIST(b):(x,b) e s
Detach, 48, 49
51 (x,y) e s
E Spec, 50
52 ALL(b):[(x,b) e s => x e n & b e n]
U Spec, 6
53 (x,y) e s => x e n & y e n
U Spec, 52
54 x e n & y e n
Detach, 53, 51
55 x e n
Split, 54
56 y e n
Split, 54
57 ALL(d):[x e n & d e n => [s(x)=d <=> (x,d) e s]]
U Spec, 19
58 x e n & y e n => [s(x)=y <=> (x,y) e s]
U Spec, 57
59 x e n & y e n
Join, 55, 56
60 s(x)=y <=> (x,y) e s
Detach, 58, 59
61 [s(x)=y => (x,y) e s] & [(x,y) e s => s(x)=y]
Iff-And, 60
62 s(x)=y => (x,y) e s
Split, 61
63 (x,y) e s => s(x)=y
Split, 61
64 s(x)=y
Detach, 63, 51
65 y e n & s(x)=y
Join, 56, 64
66 EXIST(b):[b e n & s(x)=b]
E Gen, 65
As Required:
67 ~x=max => EXIST(b):[b e n & s(x)=b]
4 Conclusion, 49
As Required:
68 ALL(a):[a e n => [~a=max => EXIST(b):[b e n & s(a)=b]]]
4 Conclusion, 46
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [s(a)=b & s(c)=b => a=c]]
Suppose...
69 x e n & y e n & z e n
Premise
70 x e n
Split, 69
71 y e n
Split, 69
72 z e n
Split, 69
73 ALL(b):ALL(c):[(x,b) e s & (c,b) e s => x=c]
U Spec, 11
74 ALL(c):[(x,y) e s & (c,y) e s => x=c]
U Spec, 73
75 (x,y) e s & (z,y) e s => x=z
U Spec, 74
76 ALL(d):[x e n & d e n => [s(x)=d <=> (x,d) e s]]
U Spec, 19
77 x e n & y e n => [s(x)=y <=> (x,y) e s]
U Spec, 76
78 x e n & y e n
Join, 70, 71
79 s(x)=y <=> (x,y) e s
Detach, 77, 78
80 [s(x)=y => (x,y) e s] & [(x,y) e s => s(x)=y]
Iff-And, 79
81 s(x)=y => (x,y) e s
Split, 80
82 (x,y) e s => s(x)=y
Split, 80
83 ALL(d):[z e n & d e n => [s(z)=d <=> (z,d) e s]]
U Spec, 19
84 z e n & y e n => [s(z)=y <=> (z,y) e s]
U Spec, 83
85 z e n & y e n
Join, 72, 71
86 s(z)=y <=> (z,y) e s
Detach, 84, 85
87 [s(z)=y => (z,y) e s] & [(z,y) e s => s(z)=y]
Iff-And, 86
88 s(z)=y => (z,y) e s
Split, 87
89 (z,y) e s => s(z)=y
Split, 87
Prove: s(x)=y & s(z)=y => x=z
Suppose...
90 s(x)=y & s(z)=y
Premise
91 s(x)=y
Split, 90
92 s(z)=y
Split, 90
93 (x,y) e s
Detach, 81, 91
94 (z,y) e s
Detach, 88, 92
95 (x,y) e s & (z,y) e s
Join, 93, 94
96 x=z
Detach, 75, 95
As Required:
97 s(x)=y & s(z)=y => x=z
4 Conclusion, 90
As Required:
98 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [s(a)=b & s(c)=b => a=c]]
4 Conclusion, 69
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):ALL(c):[b e a & c e n & s(b)=c => c e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
99 Set(p) & ALL(b):[b e p => b e n]
Premise
100 Set(p)
Split, 99
101 ALL(b):[b e p => b e n]
Split, 99
Prove: 0 e p & ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
=> ALL(b):[b e n => b e p]
Suppose...
102 0 e p & ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
Premise
103 0 e p
Split, 102
104 ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
Split, 102
105 Set(p) & ALL(b):[b e p => b e n]
=> [0 e p & ALL(b):ALL(c):[b e p & c e n & (b,c) e s => c e p]
=> ALL(b):[b e n => b e p]]
U Spec, 12
Sufficient: ALL(b):[b e n => b e p]
106 0 e p & ALL(b):ALL(c):[b e p & c e n & (b,c) e s => c e p]
=> ALL(b):[b e n => b e p]
Detach, 105, 99
Prove: ALL(b):ALL(c):[b e p & c e n & (b,c) e s => c e p]
Suppose...
107 x e p & x' e n & (x,x') e s
Premise
108 x e p
Split, 107
109 x' e n
Split, 107
110 (x,x') e s
Split, 107
111 ALL(c):[x e p & c e n & s(x)=c => c e p]
U Spec, 104
Sufficient: x' e p
112 x e p & x' e n & s(x)=x' => x' e p
U Spec, 111
113 ALL(d):[x e n & d e n => [s(x)=d <=> (x,d) e s]]
U Spec, 19
114 x e n & x' e n => [s(x)=x' <=> (x,x') e s]
U Spec, 113
115 x e p => x e n
U Spec, 101
116 x e n
Detach, 115, 108
117 x e n & x' e n
Join, 116, 109
118 s(x)=x' <=> (x,x') e s
Detach, 114, 117
119 [s(x)=x' => (x,x') e s] & [(x,x') e s => s(x)=x']
Iff-And, 118
120 s(x)=x' => (x,x') e s
Split, 119
121 (x,x') e s => s(x)=x'
Split, 119
122 s(x)=x'
Detach, 121, 110
123 x e p & x' e n
Join, 108, 109
124 x e p & x' e n & s(x)=x'
Join, 123, 122
125 x' e p
Detach, 112, 124
As Required:
126 ALL(b):ALL(c):[b e p & c e n & (b,c) e s => c e p]
4 Conclusion, 107
127 0 e p
& ALL(b):ALL(c):[b e p & c e n & (b,c) e s => c e p]
Join, 103, 126
128 ALL(b):[b e n => b e p]
Detach, 106, 127
As Required:
129 0 e p & ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 102
As Required:
130 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):ALL(c):[b e a & c e n & s(b)=c => c e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 99
Prove: ALL(a):[a e n => [s(a) e n <=> EXIST(b):[b e n & s(a)=b]]]
Suppose...
131 x e n
Premise
'=>'
Prove: s(x) e n => EXIST(b):[b e n & s(x)=b]
Suppose...
132 s(x) e n
Premise
133 s(x)=s(x)
Reflex
134 s(x) e n & s(x)=s(x)
Join, 132, 133
135 EXIST(b):[b e n & s(x)=b]
E Gen, 134
As Required:
136 s(x) e n => EXIST(b):[b e n & s(x)=b]
4 Conclusion, 132
'<='
Prove: EXIST(b):[b e n & s(x)=b] => s(x) e n
Suppose...
137 EXIST(b):[b e n & s(x)=b]
Premise
138 x' e n & s(x)=x'
E Spec, 137
139 x' e n
Split, 138
140 s(x)=x'
Split, 138
141 s(x) e n
Substitute, 140, 139
As Required:
142 EXIST(b):[b e n & s(x)=b] => s(x) e n
4 Conclusion, 137
143 [s(x) e n => EXIST(b):[b e n & s(x)=b]]
& [EXIST(b):[b e n & s(x)=b] => s(x) e n]
Join, 136, 142
144 s(x) e n <=> EXIST(b):[b e n & s(x)=b]
Iff-And, 143
As Required:
145 ALL(a):[a e n => [s(a) e n <=> EXIST(b):[b e n & s(a)=b]]]
4 Conclusion, 131
Prove: ~s(max) e n
146 max e n => [s(max) e n <=> EXIST(b):[b e n & s(max)=b]]
U Spec, 145
147 s(max) e n <=> EXIST(b):[b e n & s(max)=b]
Detach, 146, 4
148 [s(max) e n => EXIST(b):[b e n & s(max)=b]]
& [EXIST(b):[b e n & s(max)=b] => s(max) e n]
Iff-And, 147
149 s(max) e n => EXIST(b):[b e n & s(max)=b]
Split, 148
150 EXIST(b):[b e n & s(max)=b] => s(max) e n
Split, 148
151 ~EXIST(b):[b e n & s(max)=b] => ~s(max) e n
Contra, 149
Prove: ~EXIST(b):[b e n & s(max)=b]
Suppose to the contrary..
152 EXIST(b):[b e n & s(max)=b]
Premise
153 x e n & s(max)=x
E Spec, 152
154 x e n
Split, 153
155 s(max)=x
Split, 153
156 x e n => ~s(max)=x
U Spec, 45
157 ~s(max)=x
Detach, 156, 154
158 s(max)=x & ~s(max)=x
Join, 155, 157
As Required:
159 ~EXIST(b):[b e n & s(max)=b]
4 Conclusion, 152
As Required:
160 ~s(max) e n
Detach, 151, 159
Prove: ALL(a):[a e n => [~a=max => s(a) e n]]
Suppose...
161 x e n
Premise
Prove: ~x=max => s(x) e n
Suppose...
162 ~x=max
Premise
163 x e n => [s(x) e n <=> EXIST(b):[b e n & s(x)=b]]
U Spec, 145
164 s(x) e n <=> EXIST(b):[b e n & s(x)=b]
Detach, 163, 161
165 [s(x) e n => EXIST(b):[b e n & s(x)=b]]
& [EXIST(b):[b e n & s(x)=b] => s(x) e n]
Iff-And, 164
166 s(x) e n => EXIST(b):[b e n & s(x)=b]
Split, 165
Sufficient: s(x) e n
167 EXIST(b):[b e n & s(x)=b] => s(x) e n
Split, 165
168 x e n => [~x=max => EXIST(b):[b e n & s(x)=b]]
U Spec, 68
169 ~x=max => EXIST(b):[b e n & s(x)=b]
Detach, 168, 161
170 EXIST(b):[b e n & s(x)=b]
Detach, 169, 162
171 s(x) e n
Detach, 167, 170
As Required:
172 ~x=max => s(x) e n
4 Conclusion, 162
As Required:
173 ALL(a):[a e n => [~a=max => s(a) e n]]
4 Conclusion, 161
Prove: ALL(a):ALL(b):[a e n & b e n & s(a) e n => [s(a)=s(b) => a=b]]
Suppose...
174 x e n & y e n & s(x) e n
Premise
175 x e n
Split, 174
176 y e n
Split, 174
177 s(x) e n
Split, 174
178 ALL(b):ALL(c):[x e n & b e n & c e n => [s(x)=b & s(c)=b => x=c]]
U Spec, 98
179 ALL(c):[x e n & s(x) e n & c e n => [s(x)=s(x) & s(c)=s(x) => x=c]]
U Spec, 178
180 x e n & s(x) e n & y e n => [s(x)=s(x) & s(y)=s(x) => x=y]
U Spec, 179
181 x e n & s(x) e n
Join, 175, 177
182 x e n & s(x) e n & y e n
Join, 181, 176
183 s(x)=s(x) & s(y)=s(x) => x=y
Detach, 180, 182
Prove: s(x)=s(y) => x=y
Suppose...
184 s(x)=s(y)
Premise
185 s(x)=s(x)
Reflex
186 s(y)=s(x)
Sym, 184
187 s(x)=s(x) & s(y)=s(x)
Join, 185, 186
188 x=y
Detach, 183, 187
As Required:
189 s(x)=s(y) => x=y
4 Conclusion, 184
As Required:
190 ALL(a):ALL(b):[a e n & b e n & s(a) e n => [s(a)=s(b) => a=b]]
4 Conclusion, 174
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a & s(b) e n => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
191 Set(p) & ALL(b):[b e p => b e n]
Premise
192 Set(p)
Split, 191
193 ALL(b):[b e p => b e n]
Split, 191
Prove: 0 e p & ALL(b):[b e p & s(b) e n => s(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
194 0 e p & ALL(b):[b e p & s(b) e n => s(b) e p]
Premise
195 0 e p
Split, 194
196 ALL(b):[b e p & s(b) e n => s(b) e p]
Split, 194
197 Set(p) & ALL(b):[b e p => b e n]
=> [0 e p & ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
=> ALL(b):[b e n => b e p]]
U Spec, 130
Sufficient: ALL(b):[b e n => b e p]
198 0 e p & ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
=> ALL(b):[b e n => b e p]
Detach, 197, 191
Prove: ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
Suppose...
199 x e p & x' e n & s(x)=x'
Premise
200 x e p
Split, 199
201 x' e n
Split, 199
202 s(x)=x'
Split, 199
203 x e p & s(x) e n => s(x) e p
U Spec, 196
Sufficient: x' e p
204 x e p & s(x) e n => x' e p
Substitute, 202, 203
205 x e n => [s(x) e n <=> EXIST(b):[b e n & s(x)=b]]
U Spec, 145
206 x e p => x e n
U Spec, 193
207 x e n
Detach, 206, 200
208 s(x) e n <=> EXIST(b):[b e n & s(x)=b]
Detach, 205, 207
209 [s(x) e n => EXIST(b):[b e n & s(x)=b]]
& [EXIST(b):[b e n & s(x)=b] => s(x) e n]
Iff-And, 208
210 s(x) e n => EXIST(b):[b e n & s(x)=b]
Split, 209
211 EXIST(b):[b e n & s(x)=b] => s(x) e n
Split, 209
212 x' e n & s(x)=x'
Join, 201, 202
213 EXIST(b):[b e n & s(x)=b]
E Gen, 212
214 s(x) e n
Detach, 211, 213
215 x e p & s(x) e n
Join, 200, 214
216 x' e p
Detach, 204, 215
As Required:
217 ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
4 Conclusion, 199
218 0 e p
& ALL(b):ALL(c):[b e p & c e n & s(b)=c => c e p]
Join, 195, 217
219 ALL(b):[b e n => b e p]
Detach, 198, 218
As Required:
220 0 e p & ALL(b):[b e p & s(b) e n => s(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 194
As Required:
221 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a & s(b) e n => s(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 191