THEOREM The Knaster Fixed-Point Theorem
*******
Here, we prove:
ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & Subset(a,s)]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
=> EXIST(a):[Set(a) & Subset(a,s) & f(a)=a]]
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
DEFINITIONS/PREVIOUS RESULTS
****************************
Define: Subset
**************
1 ALL(a):ALL(b):[Subset(a,b) <=> ALL(c):[c e a => c e b]]
Axiom
Set equality lemma Proof
******************
2 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> Subset(a,b) & Subset(b,a)]]
Axiom
PROOF
*****
Suppose...
3 Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & Subset(a,s)]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
Premise
4 Set(s)
Split, 3
Define: ps (the power set of s)
**********
5 Set(ps)
Split, 3
6 ALL(a):[a e ps <=> Set(a) & Subset(a,s)]
Split, 3
Define: f (a function mapping ps to itself)
*********
7 ALL(a):[a e ps => f(a) e ps]
Split, 3
f preserves the subset relation
8 ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
Split, 3
9 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e ps & Subset(a,f(a))]]
Subset, 5
10 Set(z) & ALL(a):[a e z <=> a e ps & Subset(a,f(a))]
E Spec, 9
Define: z
*********
z is the family of all subsets A of s that are such that A is a subset of f(A)
11 Set(z)
Split, 10
12 ALL(a):[a e z <=> a e ps & Subset(a,f(a))]
Split, 10
13 ALL(f):[Set(f) & ALL(a):[a e f => Set(a)]
=> EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e f & b e c]]]]
Arb Union
14 Set(z) & ALL(a):[a e z => Set(a)]
=> EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e z & b e c]]]
U Spec, 13
Prove: ALL(a):[a e z => Set(a)]
Suppose...
15 p e z
Premise
Apply definition of z
16 p e z <=> p e ps & Subset(p,f(p))
U Spec, 12
17 [p e z => p e ps & Subset(p,f(p))]
& [p e ps & Subset(p,f(p)) => p e z]
Iff-And, 16
18 p e z => p e ps & Subset(p,f(p))
Split, 17
19 p e ps & Subset(p,f(p)) => p e z
Split, 17
20 p e ps & Subset(p,f(p))
Detach, 18, 15
21 p e ps
Split, 20
22 Subset(p,f(p))
Split, 20
23 p e ps <=> Set(p) & Subset(p,s)
U Spec, 6
24 [p e ps => Set(p) & Subset(p,s)]
& [Set(p) & Subset(p,s) => p e ps]
Iff-And, 23
25 p e ps => Set(p) & Subset(p,s)
Split, 24
26 Set(p) & Subset(p,s) => p e ps
Split, 24
27 Set(p) & Subset(p,s)
Detach, 25, 21
28 Set(p)
Split, 27
As Required:
29 ALL(a):[a e z => Set(a)]
4 Conclusion, 15
30 Set(z) & ALL(a):[a e z => Set(a)]
Join, 11, 29
31 EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e z & b e c]]]
Detach, 14, 30
32 Set(x) & ALL(b):[b e x <=> EXIST(c):[c e z & b e c]]
E Spec, 31
Define: x (the union of z)
*********
33 Set(x)
Split, 32
34 ALL(b):[b e x <=> EXIST(c):[c e z & b e c]]
Split, 32
Prove: ALL(a):[a e z
=> Subset(a,x) & Subset(a,f(a)) & Subset(f(a),f(x))]
Suppose...
35 p e z
Premise
Apply definition of z
36 p e z <=> p e ps & Subset(p,f(p))
U Spec, 12
37 [p e z => p e ps & Subset(p,f(p))]
& [p e ps & Subset(p,f(p)) => p e z]
Iff-And, 36
38 p e z => p e ps & Subset(p,f(p))
Split, 37
39 p e ps & Subset(p,f(p)) => p e z
Split, 37
40 p e ps & Subset(p,f(p))
Detach, 38, 35
41 p e ps
Split, 40
42 Subset(p,f(p))
Split, 40
Apply definition of Subset
43 ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]
U Spec, 1
44 Subset(p,x) <=> ALL(c):[c e p => c e x]
U Spec, 43
45 [Subset(p,x) => ALL(c):[c e p => c e x]]
& [ALL(c):[c e p => c e x] => Subset(p,x)]
Iff-And, 44
46 Subset(p,x) => ALL(c):[c e p => c e x]
Split, 45
47 ALL(c):[c e p => c e x] => Subset(p,x)
Split, 45
Prove: ALL(c):[c e p => c e x]
Suppose...
48 q e p
Premise
Apply definition of x
49 q e x <=> EXIST(c):[c e z & q e c]
U Spec, 34
50 [q e x => EXIST(c):[c e z & q e c]]
& [EXIST(c):[c e z & q e c] => q e x]
Iff-And, 49
51 q e x => EXIST(c):[c e z & q e c]
Split, 50
52 EXIST(c):[c e z & q e c] => q e x
Split, 50
53 p e z & q e p
Join, 35, 48
54 EXIST(c):[c e z & q e c]
E Gen, 53
55 q e x
Detach, 52, 54
As Required:
56 ALL(c):[c e p => c e x]
4 Conclusion, 48
57 Subset(p,x)
Detach, 47, 56
Apply premise
58 ALL(b):[p e ps & b e ps
=> [Subset(p,b) => Subset(f(p),f(b))]]
U Spec, 8
59 p e ps & x e ps
=> [Subset(p,x) => Subset(f(p),f(x))]
U Spec, 58
Apply definition of ps
60 x e ps <=> Set(x) & Subset(x,s)
U Spec, 6
61 [x e ps => Set(x) & Subset(x,s)]
& [Set(x) & Subset(x,s) => x e ps]
Iff-And, 60
62 x e ps => Set(x) & Subset(x,s)
Split, 61
63 Set(x) & Subset(x,s) => x e ps
Split, 61
Apply definition of Subset
64 ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]
U Spec, 1
65 Subset(x,s) <=> ALL(c):[c e x => c e s]
U Spec, 64
66 [Subset(x,s) => ALL(c):[c e x => c e s]]
& [ALL(c):[c e x => c e s] => Subset(x,s)]
Iff-And, 65
67 Subset(x,s) => ALL(c):[c e x => c e s]
Split, 66
68 ALL(c):[c e x => c e s] => Subset(x,s)
Split, 66
Prove: ALL(c):[c e x => c e s]
Suppose...
69 q e x
Premise
Apply definition of x
70 q e x <=> EXIST(c):[c e z & q e c]
U Spec, 34
71 [q e x => EXIST(c):[c e z & q e c]]
& [EXIST(c):[c e z & q e c] => q e x]
Iff-And, 70
72 q e x => EXIST(c):[c e z & q e c]
Split, 71
73 EXIST(c):[c e z & q e c] => q e x
Split, 71
74 EXIST(c):[c e z & q e c]
Detach, 72, 69
75 r e z & q e r
E Spec, 74
76 r e z
Split, 75
77 q e r
Split, 75
Apply definition of z
78 r e z <=> r e ps & Subset(r,f(r))
U Spec, 12
79 [r e z => r e ps & Subset(r,f(r))]
& [r e ps & Subset(r,f(r)) => r e z]
Iff-And, 78
80 r e z => r e ps & Subset(r,f(r))
Split, 79
81 r e ps & Subset(r,f(r)) => r e z
Split, 79
82 r e ps & Subset(r,f(r))
Detach, 80, 76
83 r e ps
Split, 82
84 Subset(r,f(r))
Split, 82
Apply definition of ps
85 r e ps <=> Set(r) & Subset(r,s)
U Spec, 6
86 [r e ps => Set(r) & Subset(r,s)]
& [Set(r) & Subset(r,s) => r e ps]
Iff-And, 85
87 r e ps => Set(r) & Subset(r,s)
Split, 86
88 Set(r) & Subset(r,s) => r e ps
Split, 86
89 Set(r) & Subset(r,s)
Detach, 87, 83
90 Set(r)
Split, 89
91 Subset(r,s)
Split, 89
Apply definition of Subset
92 ALL(b):[Subset(r,b) <=> ALL(c):[c e r => c e b]]
U Spec, 1
93 Subset(r,s) <=> ALL(c):[c e r => c e s]
U Spec, 92
94 [Subset(r,s) => ALL(c):[c e r => c e s]]
& [ALL(c):[c e r => c e s] => Subset(r,s)]
Iff-And, 93
95 Subset(r,s) => ALL(c):[c e r => c e s]
Split, 94
96 ALL(c):[c e r => c e s] => Subset(r,s)
Split, 94
97 ALL(c):[c e r => c e s]
Detach, 95, 91
98 q e r => q e s
U Spec, 97
99 q e s
Detach, 98, 77
As Required:
100 ALL(c):[c e x => c e s]
4 Conclusion, 69
101 Subset(x,s)
Detach, 68, 100
102 Set(x) & Subset(x,s)
Join, 33, 101
103 x e ps
Detach, 63, 102
104 p e ps & x e ps
Join, 41, 103
105 Subset(p,x) => Subset(f(p),f(x))
Detach, 59, 104
106 Subset(f(p),f(x))
Detach, 105, 57
107 Subset(p,x) & Subset(p,f(p))
Join, 57, 42
108 Subset(p,x) & Subset(p,f(p)) & Subset(f(p),f(x))
Join, 107, 106
As Required:
109 ALL(a):[a e z
=> Subset(a,x) & Subset(a,f(a)) & Subset(f(a),f(x))]
4 Conclusion, 35
Apply definition of Subset
110 ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]
U Spec, 1
111 Subset(x,f(x)) <=> ALL(c):[c e x => c e f(x)]
U Spec, 110
112 [Subset(x,f(x)) => ALL(c):[c e x => c e f(x)]]
& [ALL(c):[c e x => c e f(x)] => Subset(x,f(x))]
Iff-And, 111
113 Subset(x,f(x)) => ALL(c):[c e x => c e f(x)]
Split, 112
Sufficient: For Subset(x,f(x))
114 ALL(c):[c e x => c e f(x)] => Subset(x,f(x))
Split, 112
Prove: ALL(c):[c e x => c e f(x)]
Suppose...
115 p e x
Premise
Apply definition of x
116 p e x <=> EXIST(c):[c e z & p e c]
U Spec, 34
117 [p e x => EXIST(c):[c e z & p e c]]
& [EXIST(c):[c e z & p e c] => p e x]
Iff-And, 116
118 p e x => EXIST(c):[c e z & p e c]
Split, 117
119 EXIST(c):[c e z & p e c] => p e x
Split, 117
120 EXIST(c):[c e z & p e c]
Detach, 118, 115
121 q e z & p e q
E Spec, 120
From definition of x, we have q such that...
122 q e z
Split, 121
123 p e q
Split, 121
124 q e z
=> Subset(q,x) & Subset(q,f(q)) & Subset(f(q),f(x))
U Spec, 109
125 Subset(q,x) & Subset(q,f(q)) & Subset(f(q),f(x))
Detach, 124, 122
From previous result...
126 Subset(q,x)
Split, 125
127 Subset(q,f(q))
Split, 125
128 Subset(f(q),f(x))
Split, 125
Apply definition of Subset
129 ALL(b):[Subset(q,b) <=> ALL(c):[c e q => c e b]]
U Spec, 1
130 Subset(q,f(q)) <=> ALL(c):[c e q => c e f(q)]
U Spec, 129
131 [Subset(q,f(q)) => ALL(c):[c e q => c e f(q)]]
& [ALL(c):[c e q => c e f(q)] => Subset(q,f(q))]
Iff-And, 130
132 Subset(q,f(q)) => ALL(c):[c e q => c e f(q)]
Split, 131
133 ALL(c):[c e q => c e f(q)] => Subset(q,f(q))
Split, 131
134 ALL(c):[c e q => c e f(q)]
Detach, 132, 127
135 p e q => p e f(q)
U Spec, 134
136 p e f(q)
Detach, 135, 123
Apply definition of Subset
137 ALL(b):[Subset(f(q),b) <=> ALL(c):[c e f(q) => c e b]]
U Spec, 1
138 Subset(f(q),f(x)) <=> ALL(c):[c e f(q) => c e f(x)]
U Spec, 137
139 [Subset(f(q),f(x)) => ALL(c):[c e f(q) => c e f(x)]]
& [ALL(c):[c e f(q) => c e f(x)] => Subset(f(q),f(x))]
Iff-And, 138
140 Subset(f(q),f(x)) => ALL(c):[c e f(q) => c e f(x)]
Split, 139
141 ALL(c):[c e f(q) => c e f(x)] => Subset(f(q),f(x))
Split, 139
142 ALL(c):[c e f(q) => c e f(x)]
Detach, 140, 128
143 p e f(q) => p e f(x)
U Spec, 142
144 p e f(x)
Detach, 143, 136
As Required:
145 ALL(c):[c e x => c e f(x)]
4 Conclusion, 115
146 Subset(x,f(x))
Detach, 114, 145
Apply premise
147 ALL(b):[x e ps & b e ps
=> [Subset(x,b) => Subset(f(x),f(b))]]
U Spec, 8
148 x e ps & f(x) e ps
=> [Subset(x,f(x)) => Subset(f(x),f(f(x)))]
U Spec, 147
149 x e ps <=> Set(x) & Subset(x,s)
U Spec, 6
150 [x e ps => Set(x) & Subset(x,s)]
& [Set(x) & Subset(x,s) => x e ps]
Iff-And, 149
151 x e ps => Set(x) & Subset(x,s)
Split, 150
152 Set(x) & Subset(x,s) => x e ps
Split, 150
Apply definition of Subset
153 ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]
U Spec, 1
154 Subset(x,s) <=> ALL(c):[c e x => c e s]
U Spec, 153
155 [Subset(x,s) => ALL(c):[c e x => c e s]]
& [ALL(c):[c e x => c e s] => Subset(x,s)]
Iff-And, 154
156 Subset(x,s) => ALL(c):[c e x => c e s]
Split, 155
157 ALL(c):[c e x => c e s] => Subset(x,s)
Split, 155
Prove: ALL(c):[c e x => c e s]
Suppose...
158 p e x
Premise
Apply definition of x
159 p e x <=> EXIST(c):[c e z & p e c]
U Spec, 34
160 [p e x => EXIST(c):[c e z & p e c]]
& [EXIST(c):[c e z & p e c] => p e x]
Iff-And, 159
161 p e x => EXIST(c):[c e z & p e c]
Split, 160
162 EXIST(c):[c e z & p e c] => p e x
Split, 160
163 EXIST(c):[c e z & p e c]
Detach, 161, 158
164 q e z & p e q
E Spec, 163
165 q e z
Split, 164
166 p e q
Split, 164
Apply definition of z
167 q e z <=> q e ps & Subset(q,f(q))
U Spec, 12
168 [q e z => q e ps & Subset(q,f(q))]
& [q e ps & Subset(q,f(q)) => q e z]
Iff-And, 167
169 q e z => q e ps & Subset(q,f(q))
Split, 168
170 q e ps & Subset(q,f(q)) => q e z
Split, 168
171 q e ps & Subset(q,f(q))
Detach, 169, 165
172 q e ps
Split, 171
173 Subset(q,f(q))
Split, 171
Apply definition of ps
174 q e ps <=> Set(q) & Subset(q,s)
U Spec, 6
175 [q e ps => Set(q) & Subset(q,s)]
& [Set(q) & Subset(q,s) => q e ps]
Iff-And, 174
176 q e ps => Set(q) & Subset(q,s)
Split, 175
177 Set(q) & Subset(q,s) => q e ps
Split, 175
178 Set(q) & Subset(q,s)
Detach, 176, 172
179 Set(q)
Split, 178
180 Subset(q,s)
Split, 178
Apply definition of Subset
181 ALL(b):[Subset(q,b) <=> ALL(c):[c e q => c e b]]
U Spec, 1
182 Subset(q,s) <=> ALL(c):[c e q => c e s]
U Spec, 181
183 [Subset(q,s) => ALL(c):[c e q => c e s]]
& [ALL(c):[c e q => c e s] => Subset(q,s)]
Iff-And, 182
184 Subset(q,s) => ALL(c):[c e q => c e s]
Split, 183
185 ALL(c):[c e q => c e s] => Subset(q,s)
Split, 183
186 ALL(c):[c e q => c e s]
Detach, 184, 180
187 p e q => p e s
U Spec, 186
188 p e s
Detach, 187, 166
As Required:
189 ALL(c):[c e x => c e s]
4 Conclusion, 158
190 Subset(x,s)
Detach, 157, 189
191 Set(x) & Subset(x,s)
Join, 33, 190
192 x e ps
Detach, 152, 191
Apply definition of ps
193 f(x) e ps <=> Set(f(x)) & Subset(f(x),s)
U Spec, 6
194 [f(x) e ps => Set(f(x)) & Subset(f(x),s)]
& [Set(f(x)) & Subset(f(x),s) => f(x) e ps]
Iff-And, 193
195 f(x) e ps => Set(f(x)) & Subset(f(x),s)
Split, 194
196 Set(f(x)) & Subset(f(x),s) => f(x) e ps
Split, 194
197 x e ps => f(x) e ps
U Spec, 7
198 f(x) e ps
Detach, 197, 192
199 f(x) e ps <=> Set(f(x)) & Subset(f(x),s)
U Spec, 6
200 [f(x) e ps => Set(f(x)) & Subset(f(x),s)]
& [Set(f(x)) & Subset(f(x),s) => f(x) e ps]
Iff-And, 199
201 f(x) e ps => Set(f(x)) & Subset(f(x),s)
Split, 200
202 Set(f(x)) & Subset(f(x),s) => f(x) e ps
Split, 200
203 Set(f(x)) & Subset(f(x),s)
Detach, 201, 198
204 Set(f(x))
Split, 203
205 Subset(f(x),s)
Split, 203
206 f(x) e ps
Detach, 196, 203
207 x e ps & f(x) e ps
Join, 192, 206
208 Subset(x,f(x)) => Subset(f(x),f(f(x)))
Detach, 148, 207
209 Subset(f(x),f(f(x)))
Detach, 208, 146
210 f(x) e z <=> f(x) e ps & Subset(f(x),f(f(x)))
U Spec, 12
211 [f(x) e z => f(x) e ps & Subset(f(x),f(f(x)))]
& [f(x) e ps & Subset(f(x),f(f(x))) => f(x) e z]
Iff-And, 210
212 f(x) e z => f(x) e ps & Subset(f(x),f(f(x)))
Split, 211
213 f(x) e ps & Subset(f(x),f(f(x))) => f(x) e z
Split, 211
214 f(x) e ps & Subset(f(x),f(f(x)))
Join, 206, 209
215 f(x) e z
Detach, 213, 214
Apply definition of Subset
216 ALL(b):[Subset(f(x),b) <=> ALL(c):[c e f(x) => c e b]]
U Spec, 1
217 Subset(f(x),x) <=> ALL(c):[c e f(x) => c e x]
U Spec, 216
218 [Subset(f(x),x) => ALL(c):[c e f(x) => c e x]]
& [ALL(c):[c e f(x) => c e x] => Subset(f(x),x)]
Iff-And, 217
219 Subset(f(x),x) => ALL(c):[c e f(x) => c e x]
Split, 218
220 ALL(c):[c e f(x) => c e x] => Subset(f(x),x)
Split, 218
Prove: ALL(c):[c e f(x) => c e x]
Suppose...
221 p e f(x)
Premise
Apply definition of x
222 p e x <=> EXIST(c):[c e z & p e c]
U Spec, 34
223 [p e x => EXIST(c):[c e z & p e c]]
& [EXIST(c):[c e z & p e c] => p e x]
Iff-And, 222
224 p e x => EXIST(c):[c e z & p e c]
Split, 223
Sufficient: For p e x
225 EXIST(c):[c e z & p e c] => p e x
Split, 223
226 f(x) e z & p e f(x)
Join, 215, 221
227 EXIST(c):[c e z & p e c]
E Gen, 226
228 p e x
Detach, 225, 227
As Required:
229 ALL(c):[c e f(x) => c e x]
4 Conclusion, 221
230 Subset(f(x),x)
Detach, 220, 229
Apply previous result
231 ALL(b):[Set(f(x)) & Set(b) => [f(x)=b <=> Subset(f(x),b) & Subset(b,f(x))]]
U Spec, 2
232 Set(f(x)) & Set(x) => [f(x)=x <=> Subset(f(x),x) & Subset(x,f(x))]
U Spec, 231
233 Set(f(x)) & Set(x)
Join, 204, 33
234 f(x)=x <=> Subset(f(x),x) & Subset(x,f(x))
Detach, 232, 233
235 [f(x)=x => Subset(f(x),x) & Subset(x,f(x))]
& [Subset(f(x),x) & Subset(x,f(x)) => f(x)=x]
Iff-And, 234
236 f(x)=x => Subset(f(x),x) & Subset(x,f(x))
Split, 235
237 Subset(f(x),x) & Subset(x,f(x)) => f(x)=x
Split, 235
238 Subset(f(x),x) & Subset(x,f(x))
Join, 230, 146
239 f(x)=x
Detach, 237, 238
240 Set(x) & Subset(x,s) & f(x)=x
Join, 191, 239
As Required:
241 ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & Subset(a,s)]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
=> EXIST(a):[Set(a) & Subset(a,s) & f(a)=a]]
4 Conclusion, 3