|
273
|
1 <html>
|
|
|
2 <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8">
|
|
|
3 <head>
|
|
|
4 <STYLE type="text/css">
|
|
|
5 .main { width:100%; }
|
|
|
6 .side { top:0px; width:0%; position:fixed; left:80%; display:none}
|
|
|
7 </STYLE>
|
|
|
8 <script type="text/javascript">
|
|
|
9 function showElement(layer){
|
|
|
10 var myLayer = document.getElementById(layer);
|
|
|
11 var main = document.getElementById('mmm');
|
|
|
12 if(myLayer.style.display=="none"){
|
|
|
13 myLayer.style.width="20%";
|
|
|
14 main.style.width="80%";
|
|
|
15 myLayer.style.display="block";
|
|
|
16 myLayer.backgroundPosition="top";
|
|
|
17 } else {
|
|
|
18 myLayer.style.width="0%";
|
|
|
19 main.style.width="100%";
|
|
|
20 myLayer.style.display="none";
|
|
|
21 }
|
|
|
22 }
|
|
|
23 </script>
|
|
|
24 <title>Constructing ZF Set Theory in Agda </title>
|
|
|
25 </head>
|
|
|
26 <body>
|
|
|
27 <div class="main" id="mmm">
|
|
|
28 <h1>Constructing ZF Set Theory in Agda </h1>
|
|
|
29 <a href="#" right="0px" onclick="javascript:showElement('menu')">
|
|
|
30 <span>Menu</span>
|
|
|
31 </a>
|
|
|
32 <a href="#" left="0px" onclick="javascript:showElement('menu')">
|
|
|
33 <span>Menu</span>
|
|
|
34 </a>
|
|
|
35
|
|
|
36 <p>
|
|
|
37
|
|
|
38 <author> Shinji KONO</author>
|
|
|
39
|
|
|
40 <hr/>
|
|
279
|
41 <h2><a name="content000">ZF in Agda</a></h2>
|
|
|
42
|
|
|
43 <pre>
|
|
|
44 zf.agda axiom of ZF
|
|
|
45 zfc.agda axiom of choice
|
|
|
46 Ordinals.agda axiom of Ordinals
|
|
|
47 ordinal.agda countable model of Ordinals
|
|
|
48 OD.agda model of ZF based on Ordinal Definable Set with assumptions
|
|
|
49 ODC.agda Law of exclude middle from axiom of choice assumptions
|
|
|
50 LEMC.agda model of choice with assumption of the Law of exclude middle
|
|
|
51 OPair.agda ordered pair on OD
|
|
|
52 BAlgbra.agda Boolean algebra on OD (not yet done)
|
|
|
53 filter.agda Filter on OD (not yet done)
|
|
|
54 cardinal.agda Caedinal number on OD (not yet done)
|
|
|
55 logic.agda some basics on logic
|
|
|
56 nat.agda some basics on Nat
|
|
|
57
|
|
|
58 </pre>
|
|
|
59
|
|
|
60 <hr/>
|
|
|
61 <h2><a name="content001">Programming Mathematics</a></h2>
|
|
|
62
|
|
|
63 <p>
|
|
273
|
64 Programming is processing data structure with λ terms.
|
|
|
65 <p>
|
|
|
66 We are going to handle Mathematics in intuitionistic logic with λ terms.
|
|
|
67 <p>
|
|
|
68 Mathematics is a functional programming which values are proofs.
|
|
|
69 <p>
|
|
|
70 Programming ZF Set Theory in Agda
|
|
|
71 <p>
|
|
|
72
|
|
|
73 <hr/>
|
|
279
|
74 <h2><a name="content002">Target</a></h2>
|
|
273
|
75
|
|
|
76 <pre>
|
|
|
77 Describe ZF axioms in Agda
|
|
|
78 Construction a Model of ZF Set Theory in Agda
|
|
|
79 Show necessary assumptions for the model
|
|
|
80 Show validities of ZF axioms on the model
|
|
|
81
|
|
|
82 </pre>
|
|
|
83 This shows consistency of Set Theory (with some assumptions),
|
|
|
84 without circulating ZF Theory assumption.
|
|
|
85 <p>
|
|
|
86 <a href="https://github.com/shinji-kono/zf-in-agda">
|
|
|
87 ZF in Agda https://github.com/shinji-kono/zf-in-agda
|
|
|
88 </a>
|
|
|
89 <p>
|
|
|
90
|
|
|
91 <hr/>
|
|
279
|
92 <h2><a name="content003">Why Set Theory</a></h2>
|
|
273
|
93 If we can formulate Set theory, it suppose to work on any mathematical theory.
|
|
|
94 <p>
|
|
|
95 Set Theory is a difficult point for beginners especially axiom of choice.
|
|
|
96 <p>
|
|
|
97 It has some amount of difficulty and self circulating discussion.
|
|
|
98 <p>
|
|
|
99 I'm planning to do it in my old age, but I'm enough age now.
|
|
|
100 <p>
|
|
338
|
101 if you familier with Agda, you can skip to <a href="#set-theory">
|
|
|
102 there
|
|
|
103 </a>
|
|
273
|
104 <p>
|
|
|
105
|
|
|
106 <hr/>
|
|
279
|
107 <h2><a name="content004">Agda and Intuitionistic Logic </a></h2>
|
|
273
|
108 Curry Howard Isomorphism
|
|
|
109 <p>
|
|
|
110
|
|
|
111 <pre>
|
|
|
112 Proposition : Proof ⇔ Type : Value
|
|
|
113
|
|
|
114 </pre>
|
|
|
115 which means
|
|
|
116 <p>
|
|
|
117 constructing a typed lambda calculus which corresponds a logic
|
|
|
118 <p>
|
|
|
119 Typed lambda calculus which allows complex type as a value of a variable (System FC)
|
|
|
120 <p>
|
|
|
121 First class Type / Dependent Type
|
|
|
122 <p>
|
|
|
123 Agda is a such a programming language which has similar syntax of Haskell
|
|
|
124 <p>
|
|
|
125 Coq is specialized in proof assistance such as command and tactics .
|
|
|
126 <p>
|
|
|
127
|
|
|
128 <hr/>
|
|
279
|
129 <h2><a name="content005">Introduction of Agda </a></h2>
|
|
273
|
130 A length of a list of type A.
|
|
|
131 <p>
|
|
|
132
|
|
|
133 <pre>
|
|
|
134 length : {A : Set } → List A → Nat
|
|
|
135 length [] = zero
|
|
|
136 length (_ ∷ t) = suc ( length t )
|
|
|
137
|
|
|
138 </pre>
|
|
|
139 Simple functional programming language. Type declaration is mandatory.
|
|
|
140 A colon means type, an equal means value. Indentation based.
|
|
|
141 <p>
|
|
|
142 Set is a base type (which may have a level ).
|
|
|
143 <p>
|
|
|
144 {} means implicit variable which can be omitted if Agda infers its value.
|
|
|
145 <p>
|
|
|
146
|
|
|
147 <hr/>
|
|
279
|
148 <h2><a name="content006">data ( Sum type )</a></h2>
|
|
273
|
149 A data type which as exclusive multiple constructors. A similar one as
|
|
|
150 union in C or case class in Scala.
|
|
|
151 <p>
|
|
|
152 It has a similar syntax as Haskell but it has a slight difference.
|
|
|
153 <p>
|
|
|
154
|
|
|
155 <pre>
|
|
|
156 data List (A : Set ) : Set where
|
|
|
157 [] : List A
|
|
|
158 _∷_ : A → List A → List A
|
|
|
159
|
|
|
160 </pre>
|
|
|
161 _∷_ means infix operator. If use explicit _, it can be used in a normal function
|
|
|
162 syntax.
|
|
|
163 <p>
|
|
|
164 Natural number can be defined as a usual way.
|
|
|
165 <p>
|
|
|
166
|
|
|
167 <pre>
|
|
|
168 data Nat : Set where
|
|
|
169 zero : Nat
|
|
|
170 suc : Nat → Nat
|
|
|
171
|
|
|
172 </pre>
|
|
|
173
|
|
|
174 <hr/>
|
|
279
|
175 <h2><a name="content007"> A → B means "A implies B"</a></h2>
|
|
273
|
176
|
|
|
177 <p>
|
|
|
178 In Agda, a type can be a value of a variable, which is usually called dependent type.
|
|
|
179 Type has a name Set in Agda.
|
|
|
180 <p>
|
|
|
181
|
|
|
182 <pre>
|
|
|
183 ex3 : {A B : Set} → Set
|
|
|
184 ex3 {A}{B} = A → B
|
|
|
185
|
|
|
186 </pre>
|
|
|
187 ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
|
|
|
188 <p>
|
|
|
189
|
|
|
190 <pre>
|
|
|
191 A type is a formula, the value is the proof
|
|
|
192
|
|
|
193 </pre>
|
|
|
194 A value of A → B can be interpreted as an inference from the formula A to the formula B, which
|
|
|
195 can be a function from a proof of A to a proof of B.
|
|
|
196 <p>
|
|
|
197
|
|
|
198 <hr/>
|
|
279
|
199 <h2><a name="content008">introduction と elimination</a></h2>
|
|
273
|
200 For a logical operator, there are two types of inference, an introduction and an elimination.
|
|
|
201 <p>
|
|
|
202
|
|
|
203 <pre>
|
|
|
204 intro creating symbol / constructor / introduction
|
|
|
205 elim using symbolic / accessors / elimination
|
|
|
206
|
|
|
207 </pre>
|
|
|
208 In Natural deduction, this can be written in proof schema.
|
|
|
209 <p>
|
|
|
210
|
|
|
211 <pre>
|
|
|
212 A
|
|
|
213 :
|
|
|
214 B A A → B
|
|
|
215 ------------- →intro ------------------ →elim
|
|
|
216 A → B B
|
|
|
217
|
|
|
218 </pre>
|
|
|
219 In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
|
|
|
220 <p>
|
|
|
221
|
|
|
222 <pre>
|
|
|
223 →intro : {A B : Set } → A → B → ( A → B )
|
|
|
224 →intro _ b = λ x → b
|
|
|
225 →elim : {A B : Set } → A → ( A → B ) → B
|
|
|
226 →elim a f = f a
|
|
|
227
|
|
|
228 </pre>
|
|
|
229 Important
|
|
|
230 <p>
|
|
|
231
|
|
|
232 <pre>
|
|
|
233 {A B : Set } → A → B → ( A → B )
|
|
|
234
|
|
|
235 </pre>
|
|
|
236 is
|
|
|
237 <p>
|
|
|
238
|
|
|
239 <pre>
|
|
|
240 {A B : Set } → ( A → ( B → ( A → B ) ))
|
|
|
241
|
|
|
242 </pre>
|
|
|
243 This makes currying of function easy.
|
|
|
244 <p>
|
|
|
245
|
|
|
246 <hr/>
|
|
279
|
247 <h2><a name="content009"> To prove A → B </a></h2>
|
|
273
|
248 Make a left type as an argument. (intros in Coq)
|
|
|
249 <p>
|
|
|
250
|
|
|
251 <pre>
|
|
|
252 ex5 : {A B C : Set } → A → B → C → ?
|
|
|
253 ex5 a b c = ?
|
|
|
254
|
|
|
255 </pre>
|
|
|
256 ? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
|
|
|
257 <p>
|
|
|
258 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
|
|
|
259 insufficient proof or instance (Yellow), Non-termination, the proof is completed.
|
|
|
260 <p>
|
|
|
261
|
|
|
262 <hr/>
|
|
279
|
263 <h2><a name="content010"> A ∧ B</a></h2>
|
|
273
|
264 Well known conjunction's introduction and elimination is as follow.
|
|
|
265 <p>
|
|
|
266
|
|
|
267 <pre>
|
|
|
268 A B A ∧ B A ∧ B
|
|
|
269 ------------- ----------- proj1 ---------- proj2
|
|
|
270 A ∧ B A B
|
|
|
271
|
|
|
272 </pre>
|
|
|
273 We can introduce a corresponding structure in our functional programming language.
|
|
|
274 <p>
|
|
|
275
|
|
|
276 <hr/>
|
|
279
|
277 <h2><a name="content011"> record</a></h2>
|
|
273
|
278
|
|
|
279 <pre>
|
|
|
280 record _∧_ A B : Set
|
|
|
281 field
|
|
|
282 proj1 : A
|
|
|
283 proj2 : B
|
|
|
284
|
|
|
285 </pre>
|
|
|
286 _∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) )
|
|
|
287 <p>
|
|
|
288 This a type which constructed from type A and type B. You may think this as an object
|
|
|
289 or struct.
|
|
|
290 <p>
|
|
|
291
|
|
|
292 <pre>
|
|
|
293 record { proj1 = x ; proj2 = y }
|
|
|
294
|
|
|
295 </pre>
|
|
|
296 is a constructor of _∧_.
|
|
|
297 <p>
|
|
|
298
|
|
|
299 <pre>
|
|
|
300 ex3 : {A B : Set} → A → B → ( A ∧ B )
|
|
|
301 ex3 a b = record { proj1 = a ; proj2 = b }
|
|
|
302 ex1 : {A B : Set} → ( A ∧ B ) → A
|
|
|
303 ex1 a∧b = proj1 a∧b
|
|
|
304
|
|
|
305 </pre>
|
|
|
306 a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
|
|
|
307 except parenthesis or colons. A symbol requires space separation such as a type defining colon.
|
|
|
308 <p>
|
|
|
309 Defining record can be recursively, but we don't use the recursion here.
|
|
|
310 <p>
|
|
|
311
|
|
|
312 <hr/>
|
|
279
|
313 <h2><a name="content012"> Mathematical structure</a></h2>
|
|
273
|
314 We have types of elements and the relationship in a mathematical structure.
|
|
|
315 <p>
|
|
|
316
|
|
|
317 <pre>
|
|
|
318 logical relation has no ordering
|
|
|
319 there is a natural ordering in arguments and a value in a function
|
|
|
320
|
|
|
321 </pre>
|
|
|
322 So we have typical definition style of mathematical structure with records.
|
|
|
323 <p>
|
|
|
324
|
|
|
325 <pre>
|
|
|
326 record IsOrdinals {n : Level} (ord : Set n)
|
|
|
327 (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
|
|
|
328 field
|
|
|
329 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
|
|
|
330 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
331 field
|
|
|
332 ord : Set n
|
|
|
333 _o<_ : ord → ord → Set n
|
|
|
334 isOrdinal : IsOrdinals ord _o<_
|
|
|
335
|
|
|
336 </pre>
|
|
|
337 In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
|
|
|
338 inputs and outputs are put in the field including IsOrdinal.
|
|
|
339 <p>
|
|
|
340 Fields of Ordinal is existential objects in the mathematical structure.
|
|
|
341 <p>
|
|
|
342
|
|
|
343 <hr/>
|
|
359
|
344 <h2><a name="content013"> Limit Ordinal</a></h2>
|
|
|
345 If an ordinal is not a succesor of other, it is called limit ordinal. We need predicate to decide it.
|
|
|
346 <p>
|
|
|
347
|
|
|
348 <pre>
|
|
|
349 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
|
|
|
350
|
|
|
351 </pre>
|
|
|
352 An ordinal may have an imeditate limit ordinal, we call it next x. Axiom of nrext is this.
|
|
|
353 <p>
|
|
|
354
|
|
|
355 <pre>
|
|
|
356 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord )
|
|
|
357 (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
|
|
|
358 field
|
|
|
359 x<nx : { y : ord } → (y o< next y )
|
|
|
360 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
|
|
|
361 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
|
|
|
362
|
|
|
363 </pre>
|
|
|
364 We show some intresting lemma.
|
|
|
365 <p>
|
|
|
366
|
|
|
367 <pre>
|
|
|
368 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
|
|
|
369 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y
|
|
|
370 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
|
|
|
371 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
|
|
|
372
|
|
|
373 </pre>
|
|
|
374 These are proved from the axiom. Our countable ordinal satisfies these.
|
|
|
375 <p>
|
|
|
376
|
|
|
377 <hr/>
|
|
|
378 <h2><a name="content014"> A Model and a theory</a></h2>
|
|
273
|
379 Agda record is a type, so we can write it in the argument, but is it really exists?
|
|
|
380 <p>
|
|
|
381 If we have a value of the record, it simply exists, that is, we need to create all the existence
|
|
|
382 in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
|
|
|
383 <p>
|
|
|
384
|
|
|
385 <pre>
|
|
|
386 type of record = theory
|
|
|
387 value of record = model
|
|
|
388
|
|
|
389 </pre>
|
|
|
390 We call the value of the record as a model. If mathematical structure has a
|
|
|
391 model, it exists. Pretty Obvious.
|
|
|
392 <p>
|
|
|
393
|
|
|
394 <hr/>
|
|
359
|
395 <h2><a name="content015"> postulate と module</a></h2>
|
|
273
|
396 Agda proofs are separated by modules, which are large records.
|
|
|
397 <p>
|
|
|
398 postulates are assumptions. We can assume a type without proofs.
|
|
|
399 <p>
|
|
|
400
|
|
|
401 <pre>
|
|
|
402 postulate
|
|
|
403 sup-o : ( Ordinal → Ordinal ) → Ordinal
|
|
|
404 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
|
|
|
405
|
|
|
406 </pre>
|
|
|
407 sup-o is an example of upper bound of a function and sup-o< assumes it actually satisfies all the value is less than upper bound.
|
|
|
408 <p>
|
|
|
409 Writing some type in a module argument is the same as postulating a type, but
|
|
|
410 postulate can be written the middle of a proof.
|
|
|
411 <p>
|
|
|
412 postulate can be constructive.
|
|
|
413 <p>
|
|
338
|
414 postulate can be inconsistent, which result everything has a proof. Actualy this assumption
|
|
|
415 doesnot work for Ordinals, we discuss this later.
|
|
273
|
416 <p>
|
|
|
417
|
|
|
418 <hr/>
|
|
359
|
419 <h2><a name="content016"> A ∨ B</a></h2>
|
|
273
|
420
|
|
|
421 <pre>
|
|
|
422 data _∨_ (A B : Set) : Set where
|
|
|
423 case1 : A → A ∨ B
|
|
|
424 case2 : B → A ∨ B
|
|
|
425
|
|
|
426 </pre>
|
|
|
427 As Haskell, case1/case2 are patterns.
|
|
|
428 <p>
|
|
|
429
|
|
|
430 <pre>
|
|
|
431 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
432 ex3 = ?
|
|
|
433
|
|
|
434 </pre>
|
|
|
435 In a case statement, Agda command C-C C-C generates possible cases in the head.
|
|
|
436 <p>
|
|
|
437
|
|
|
438 <pre>
|
|
|
439 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
440 ex3 (case1 x) = ?
|
|
|
441 ex3 (case2 x) = ?
|
|
|
442
|
|
|
443 </pre>
|
|
|
444 Proof schema of ∨ is omit due to the complexity.
|
|
|
445 <p>
|
|
|
446
|
|
|
447 <hr/>
|
|
359
|
448 <h2><a name="content017"> Negation</a></h2>
|
|
273
|
449
|
|
|
450 <pre>
|
|
|
451 ⊥
|
|
|
452 ------------- ⊥-elim
|
|
|
453 A
|
|
|
454
|
|
|
455 </pre>
|
|
|
456 Anything can be derived from bottom, in this case a Set A. There is no introduction rule
|
|
|
457 in ⊥, which can be implemented as data which has no constructor.
|
|
|
458 <p>
|
|
|
459
|
|
|
460 <pre>
|
|
|
461 data ⊥ : Set where
|
|
|
462
|
|
|
463 </pre>
|
|
|
464 ⊥-elim can be proved like this.
|
|
|
465 <p>
|
|
|
466
|
|
|
467 <pre>
|
|
|
468 ⊥-elim : {A : Set } -> ⊥ -> A
|
|
|
469 ⊥-elim ()
|
|
|
470
|
|
|
471 </pre>
|
|
|
472 () means no match argument nor value.
|
|
|
473 <p>
|
|
|
474 A negation can be defined using ⊥ like this.
|
|
|
475 <p>
|
|
|
476
|
|
|
477 <pre>
|
|
|
478 ¬_ : Set → Set
|
|
|
479 ¬ A = A → ⊥
|
|
|
480
|
|
|
481 </pre>
|
|
|
482
|
|
|
483 <hr/>
|
|
359
|
484 <h2><a name="content018">Equality </a></h2>
|
|
273
|
485
|
|
|
486 <p>
|
|
|
487 All the value in Agda are terms. If we have the same normalized form, two terms are equal.
|
|
|
488 If we have variables in the terms, we will perform an unification. unifiable terms are equal.
|
|
|
489 We don't go further on the unification.
|
|
|
490 <p>
|
|
|
491
|
|
|
492 <pre>
|
|
|
493 { x : A } x ≡ y f x y
|
|
|
494 --------------- ≡-intro --------------------- ≡-elim
|
|
|
495 x ≡ x f x x
|
|
|
496
|
|
|
497 </pre>
|
|
|
498 equality _≡_ can be defined as a data.
|
|
|
499 <p>
|
|
|
500
|
|
|
501 <pre>
|
|
|
502 data _≡_ {A : Set } : A → A → Set where
|
|
|
503 refl : {x : A} → x ≡ x
|
|
|
504
|
|
|
505 </pre>
|
|
|
506 The elimination of equality is a substitution in a term.
|
|
|
507 <p>
|
|
|
508
|
|
|
509 <pre>
|
|
|
510 subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
|
|
|
511 subst {A} {x} {y} f refl fx = fx
|
|
|
512 ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
|
513 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
|
|
|
514
|
|
|
515 </pre>
|
|
|
516
|
|
|
517 <hr/>
|
|
359
|
518 <h2><a name="content019">Equivalence relation</a></h2>
|
|
273
|
519
|
|
|
520 <p>
|
|
|
521
|
|
|
522 <pre>
|
|
|
523 refl' : {A : Set} {x : A } → x ≡ x
|
|
|
524 refl' = ?
|
|
|
525 sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
|
|
|
526 sym = ?
|
|
|
527 trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
|
|
|
528 trans = ?
|
|
|
529 cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
|
|
|
530 cong = ?
|
|
|
531
|
|
|
532 </pre>
|
|
|
533
|
|
|
534 <hr/>
|
|
359
|
535 <h2><a name="content020">Ordering</a></h2>
|
|
273
|
536
|
|
|
537 <p>
|
|
|
538 Relation is a predicate on two value which has a same type.
|
|
|
539 <p>
|
|
|
540
|
|
|
541 <pre>
|
|
|
542 A → A → Set
|
|
|
543
|
|
|
544 </pre>
|
|
|
545 Defining order is the definition of this type with predicate or a data.
|
|
|
546 <p>
|
|
|
547
|
|
|
548 <pre>
|
|
|
549 data _≤_ : Rel ℕ 0ℓ where
|
|
|
550 z≤n : ∀ {n} → zero ≤ n
|
|
|
551 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
|
|
|
552
|
|
|
553 </pre>
|
|
|
554
|
|
|
555 <hr/>
|
|
359
|
556 <h2><a name="content021">Quantifier</a></h2>
|
|
273
|
557
|
|
|
558 <p>
|
|
|
559 Handling quantifier in an intuitionistic logic requires special cares.
|
|
|
560 <p>
|
|
|
561 In the input of a function, there are no restriction on it, that is, it has
|
|
|
562 a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
|
|
|
563 <p>
|
|
|
564 There is no ∃ in agda, the one way is using negation like this.
|
|
|
565 <p>
|
|
|
566 ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
|
|
|
567 <p>
|
|
|
568 On the another way, f : A can be used like this.
|
|
|
569 <p>
|
|
|
570
|
|
|
571 <pre>
|
|
|
572 p f
|
|
|
573
|
|
|
574 </pre>
|
|
|
575 If we use a function which can be defined globally which has stronger meaning the
|
|
|
576 usage of ∃ x in a logical expression.
|
|
|
577 <p>
|
|
|
578
|
|
|
579 <hr/>
|
|
359
|
580 <h2><a name="content022">Can we do math in this way?</a></h2>
|
|
273
|
581 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
|
|
|
582 <p>
|
|
|
583 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
|
|
|
584 <p>
|
|
|
585
|
|
|
586 <pre>
|
|
|
587 define mathematical structure as a record
|
|
|
588 program inferences as if we have proofs in variables
|
|
|
589
|
|
|
590 </pre>
|
|
|
591
|
|
|
592 <hr/>
|
|
359
|
593 <h2><a name="content023">Things which Agda cannot prove</a></h2>
|
|
273
|
594
|
|
|
595 <p>
|
|
|
596 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
|
|
|
597 leads uniqueness of a functor in Category Theory.
|
|
|
598 <p>
|
|
|
599 Functional extensionality cannot be proved.
|
|
|
600 <pre>
|
|
|
601 (∀ x → f x ≡ g x) → f ≡ g
|
|
|
602
|
|
|
603 </pre>
|
|
|
604 Agda has no law of exclude middle.
|
|
|
605 <p>
|
|
|
606
|
|
|
607 <pre>
|
|
|
608 a ∨ ( ¬ a )
|
|
|
609
|
|
|
610 </pre>
|
|
|
611 For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
|
|
|
612 <p>
|
|
|
613 It also other problems such as termination, type inference or unification which we may overcome with
|
|
|
614 efforts or devices or may not.
|
|
|
615 <p>
|
|
|
616 If we cannot prove something, we can safely postulate it unless it leads a contradiction.
|
|
|
617 <pre>
|
|
|
618
|
|
|
619
|
|
|
620 </pre>
|
|
|
621
|
|
|
622 <hr/>
|
|
359
|
623 <h2><a name="content024">Classical story of ZF Set Theory</a></h2>
|
|
273
|
624
|
|
|
625 <p>
|
|
338
|
626 <a name="set-theory">
|
|
273
|
627 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
|
|
|
628 a relative consistency proof of the Set Theory.
|
|
|
629 Ordinal number is used in the flow.
|
|
|
630 <p>
|
|
|
631 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
|
|
|
632 We need some non constructive assumptions in the construction. A model of Set theory is
|
|
|
633 constructed based on these assumptions.
|
|
|
634 <p>
|
|
|
635 <img src="fig/set-theory.svg">
|
|
|
636
|
|
|
637 <p>
|
|
|
638
|
|
|
639 <hr/>
|
|
359
|
640 <h2><a name="content025">Ordinals</a></h2>
|
|
273
|
641 Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
|
|
|
642 It also has a successor osuc.
|
|
|
643 <p>
|
|
|
644
|
|
|
645 <pre>
|
|
|
646 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
647 field
|
|
|
648 ord : Set n
|
|
|
649 o∅ : ord
|
|
|
650 osuc : ord → ord
|
|
|
651 _o<_ : ord → ord → Set n
|
|
|
652 isOrdinal : IsOrdinals ord o∅ osuc _o<_
|
|
|
653
|
|
|
654 </pre>
|
|
|
655 It is different from natural numbers in way. The order of Ordinals is not defined in terms
|
|
|
656 of successor. It is given from outside, which make it possible to have higher order infinity.
|
|
|
657 <p>
|
|
|
658
|
|
|
659 <hr/>
|
|
359
|
660 <h2><a name="content026">Axiom of Ordinals</a></h2>
|
|
273
|
661 Properties of infinite things. We request a transfinite induction, which states that if
|
|
|
662 some properties are satisfied below all possible ordinals, the properties are true on all
|
|
|
663 ordinals.
|
|
|
664 <p>
|
|
|
665 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
|
|
|
666 which is not a successor of any ordinals. It is called limit ordinal.
|
|
|
667 <p>
|
|
|
668 Any two ordinal can be compared, that is less, equal or more, that is total order.
|
|
|
669 <p>
|
|
|
670
|
|
|
671 <pre>
|
|
|
672 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
|
|
|
673 (osuc : ord → ord )
|
|
|
674 (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
|
|
|
675 field
|
|
|
676 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
|
|
|
677 OTri : Trichotomous {n} _≡_ _o<_
|
|
|
678 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
|
|
|
679 <-osuc : { x : ord } → x o< osuc x
|
|
|
680 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
|
|
|
681 TransFinite : { ψ : ord → Set (suc n) }
|
|
|
682 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
|
|
|
683 → ∀ (x : ord) → ψ x
|
|
|
684
|
|
|
685 </pre>
|
|
|
686
|
|
|
687 <hr/>
|
|
359
|
688 <h2><a name="content027">Concrete Ordinals or Countable Ordinals</a></h2>
|
|
273
|
689
|
|
|
690 <p>
|
|
|
691 We can define a list like structure with level, which is a kind of two dimensional infinite array.
|
|
|
692 <p>
|
|
|
693
|
|
|
694 <pre>
|
|
|
695 data OrdinalD {n : Level} : (lv : Nat) → Set n where
|
|
|
696 Φ : (lv : Nat) → OrdinalD lv
|
|
|
697 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
|
|
|
698
|
|
|
699 </pre>
|
|
|
700 The order of the OrdinalD can be defined in this way.
|
|
|
701 <p>
|
|
|
702
|
|
|
703 <pre>
|
|
|
704 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
|
|
|
705 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
|
|
|
706 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
|
|
|
707
|
|
|
708 </pre>
|
|
|
709 This is a simple data structure, it has no abstract assumptions, and it is countable many data
|
|
|
710 structure.
|
|
|
711 <p>
|
|
|
712
|
|
|
713 <pre>
|
|
|
714 Φ 0
|
|
|
715 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
|
|
|
716 Osuc 0 (Φ 0) d< Φ 1
|
|
|
717
|
|
|
718 </pre>
|
|
|
719
|
|
|
720 <hr/>
|
|
359
|
721 <h2><a name="content028">Model of Ordinals</a></h2>
|
|
273
|
722
|
|
|
723 <p>
|
|
|
724 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
|
|
|
725 <p>
|
|
|
726 So our Ordinals has a mode. This means axiom of Ordinals are consistent.
|
|
|
727 <p>
|
|
|
728
|
|
|
729 <hr/>
|
|
359
|
730 <h2><a name="content029">Debugging axioms using Model</a></h2>
|
|
273
|
731 Whether axiom is correct or not can be checked by a validity on a mode.
|
|
|
732 <p>
|
|
|
733 If not, we may fix the axioms or the model, such as the definitions of the order.
|
|
|
734 <p>
|
|
|
735 We can also ask whether the inputs exist.
|
|
|
736 <p>
|
|
|
737
|
|
|
738 <hr/>
|
|
359
|
739 <h2><a name="content030">Countable Ordinals can contains uncountable set?</a></h2>
|
|
273
|
740 Yes, the ordinals contains any level of infinite Set in the axioms.
|
|
|
741 <p>
|
|
|
742 If we handle real-number in the model, only countable number of real-number is used.
|
|
|
743 <p>
|
|
|
744
|
|
|
745 <pre>
|
|
|
746 from the outside view point, it is countable
|
|
|
747 from the internal view point, it is uncountable
|
|
|
748
|
|
|
749 </pre>
|
|
|
750 The definition of countable/uncountable is the same, but the properties are different
|
|
|
751 depending on the context.
|
|
|
752 <p>
|
|
|
753 We don't show the definition of cardinal number here.
|
|
|
754 <p>
|
|
|
755
|
|
|
756 <hr/>
|
|
359
|
757 <h2><a name="content031">What is Set</a></h2>
|
|
273
|
758 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
|
|
|
759 <p>
|
|
|
760 From naive point view, a set i a list, but in Agda, elements have all the same type.
|
|
|
761 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
|
|
|
762 <p>
|
|
|
763 Finite set may be written in finite series of ∨, but ...
|
|
|
764 <p>
|
|
|
765
|
|
|
766 <hr/>
|
|
359
|
767 <h2><a name="content032">We don't ask the contents of Set. It can be anything.</a></h2>
|
|
273
|
768 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
|
|
|
769 and all of them, and again we repeat this.
|
|
|
770 <p>
|
|
|
771
|
|
|
772 <pre>
|
|
|
773 φ {φ} {φ,{φ}}, {φ,{φ},...}
|
|
|
774
|
|
|
775 </pre>
|
|
|
776 It is called V.
|
|
|
777 <p>
|
|
|
778 This operation can be performed within a ZF Set theory. Classical Set Theory assumes
|
|
|
779 ZF, so this kind of thing is allowed.
|
|
|
780 <p>
|
|
|
781 But in our case, we have no ZF theory, so we are going to use Ordinals.
|
|
|
782 <p>
|
|
338
|
783 The idea is to use an ordinal as a pointer to a record which defines a Set.
|
|
|
784 If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set.
|
|
|
785 <p>
|
|
273
|
786
|
|
|
787 <hr/>
|
|
359
|
788 <h2><a name="content033">Ordinal Definable Set</a></h2>
|
|
273
|
789 We can define a sbuset of Ordinals using predicates. What is a subset?
|
|
|
790 <p>
|
|
|
791
|
|
|
792 <pre>
|
|
|
793 a predicate has an Ordinal argument
|
|
|
794
|
|
|
795 </pre>
|
|
|
796 is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
|
|
|
797 <p>
|
|
|
798
|
|
|
799 <pre>
|
|
|
800 record OD : Set (suc n ) where
|
|
|
801 field
|
|
|
802 def : (x : Ordinal ) → Set n
|
|
|
803
|
|
|
804 </pre>
|
|
|
805 Ordinals itself is not a set in a ZF Set theory but a class. In OD,
|
|
|
806 <p>
|
|
|
807
|
|
|
808 <pre>
|
|
338
|
809 data One : Set n where
|
|
|
810 OneObj : One
|
|
|
811 record { def = λ x → One }
|
|
273
|
812
|
|
|
813 </pre>
|
|
338
|
814 means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
|
|
|
815 You can say OD is a class in ZF Set Theory term.
|
|
|
816 <p>
|
|
|
817
|
|
|
818 <hr/>
|
|
359
|
819 <h2><a name="content034">OD is not ZF Set</a></h2>
|
|
338
|
820 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
|
|
|
821 a Set. The idea is to use an ordinal as a pointer to OD.
|
|
|
822 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
|
|
|
823 <p>
|
|
|
824
|
|
|
825 <pre>
|
|
425
|
826 ¬OD-order : ( & : OD → Ordinal )
|
|
|
827 → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥
|
|
|
828 ¬OD-order & * c<→o< = ?
|
|
338
|
829
|
|
|
830 </pre>
|
|
|
831 Actualy we can prove this contrdction, so we need some restrctions on OD.
|
|
|
832 <p>
|
|
|
833 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
|
|
273
|
834 <p>
|
|
|
835
|
|
|
836 <hr/>
|
|
359
|
837 <h2><a name="content035"> HOD : Hereditarily Ordinal Definable</a></h2>
|
|
338
|
838 What we need is a bounded OD, the containment is limited by an ordinal.
|
|
|
839 <p>
|
|
|
840
|
|
|
841 <pre>
|
|
|
842 record HOD : Set (suc n) where
|
|
|
843 field
|
|
|
844 od : OD
|
|
|
845 odmax : Ordinal
|
|
|
846 <odmax : {y : Ordinal} → def od y → y o< odmax
|
|
|
847
|
|
|
848 </pre>
|
|
|
849 In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
|
|
273
|
850 <p>
|
|
|
851
|
|
|
852 <pre>
|
|
338
|
853 HOD = { x | TC x ⊆ OD }
|
|
273
|
854
|
|
|
855 </pre>
|
|
338
|
856 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD.
|
|
|
857 <p>
|
|
|
858
|
|
|
859 <hr/>
|
|
359
|
860 <h2><a name="content036">1 to 1 mapping between an HOD and an Ordinal</a></h2>
|
|
338
|
861 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
|
|
|
862 <p>
|
|
|
863
|
|
|
864 <pre>
|
|
425
|
865 & : HOD → Ordinal
|
|
|
866 * : Ordinal → HOD
|
|
|
867 oiso : {x : HOD } → * ( & x ) ≡ x
|
|
|
868 diso : {x : Ordinal } → & ( * x ) ≡ x
|
|
338
|
869
|
|
|
870 </pre>
|
|
|
871 we can check an HOD is an element of the OD using def.
|
|
273
|
872 <p>
|
|
|
873 A ∋ x can be define as follows.
|
|
|
874 <p>
|
|
|
875
|
|
|
876 <pre>
|
|
338
|
877 _∋_ : ( A x : HOD ) → Set n
|
|
425
|
878 _∋_ A x = def (od A) ( & x )
|
|
273
|
879
|
|
|
880 </pre>
|
|
|
881 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
|
|
|
882 <p>
|
|
|
883
|
|
|
884 <pre>
|
|
425
|
885 A x = def A ( & x ) = ψ (& x)
|
|
273
|
886
|
|
|
887 </pre>
|
|
|
888 They say the existing of the mappings can be proved in Classical Set Theory, but we
|
|
|
889 simply assumes these non constructively.
|
|
|
890 <p>
|
|
|
891 <img src="fig/ord-od-mapping.svg">
|
|
|
892
|
|
|
893 <p>
|
|
|
894
|
|
|
895 <hr/>
|
|
359
|
896 <h2><a name="content037">Order preserving in the mapping of OD and Ordinal</a></h2>
|
|
338
|
897 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
|
|
273
|
898 <p>
|
|
|
899
|
|
|
900 <pre>
|
|
425
|
901 def (od y) ( & x )
|
|
273
|
902
|
|
|
903 </pre>
|
|
338
|
904 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
|
|
273
|
905 have to be smaller than the corresponding ordinal of the containing OD.
|
|
338
|
906 We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
|
|
273
|
907 <p>
|
|
|
908
|
|
|
909 <pre>
|
|
425
|
910 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
|
|
|
911 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
|
|
273
|
912
|
|
|
913 </pre>
|
|
338
|
914 If wa assumes reverse order preservation,
|
|
273
|
915 <p>
|
|
|
916
|
|
|
917 <pre>
|
|
425
|
918 o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (* y) x
|
|
273
|
919
|
|
|
920 </pre>
|
|
338
|
921 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
|
|
273
|
922 <p>
|
|
|
923 <img src="fig/ODandOrdinals.svg">
|
|
|
924
|
|
|
925 <p>
|
|
|
926
|
|
|
927 <hr/>
|
|
359
|
928 <h2><a name="content038">Various Sets</a></h2>
|
|
273
|
929 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
|
|
|
930 <p>
|
|
|
931
|
|
|
932 <pre>
|
|
|
933 Ordinal / things satisfies axiom of Ordinal / extension of natural number
|
|
|
934 V / hierarchical construction of Set from φ
|
|
|
935 L / hierarchical predicate definable construction of Set from φ
|
|
338
|
936 HOD / Hereditarily Ordinal Definable
|
|
273
|
937 OD / equational formula on Ordinals
|
|
|
938 Agda Set / Type / it also has a level
|
|
|
939
|
|
|
940 </pre>
|
|
|
941
|
|
|
942 <hr/>
|
|
361
|
943 <h2><a name="content039">Fixing ZF axom to fit intuitionistic logic</a></h2>
|
|
273
|
944
|
|
|
945 <p>
|
|
|
946 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
|
|
|
947 ZF axioms in Agda.
|
|
|
948 <p>
|
|
|
949 It may not valid in our model. We have to debug it.
|
|
|
950 <p>
|
|
|
951 Fixes are depends on axioms.
|
|
|
952 <p>
|
|
|
953 <img src="fig/axiom-type.svg">
|
|
|
954
|
|
|
955 <p>
|
|
|
956 <a href="fig/zf-record.html">
|
|
|
957 ZFのrecord </a>
|
|
|
958 <p>
|
|
|
959
|
|
|
960 <hr/>
|
|
359
|
961 <h2><a name="content040">Pure logical axioms</a></h2>
|
|
273
|
962
|
|
|
963 <pre>
|
|
279
|
964 empty, pair, select, ε-induction??infinity
|
|
273
|
965
|
|
|
966 </pre>
|
|
|
967 These are logical relations among OD.
|
|
|
968 <p>
|
|
|
969
|
|
|
970 <pre>
|
|
|
971 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
|
|
|
972 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
|
|
|
973 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
|
|
|
974 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
|
|
|
975 infinity∅ : ∅ ∈ infinite
|
|
|
976 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
|
|
|
977 ε-induction : { ψ : OD → Set (suc n)}
|
|
|
978 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
|
|
|
979 → (x : OD ) → ψ x
|
|
|
980
|
|
|
981 </pre>
|
|
|
982 finitely can be define by Agda data.
|
|
|
983 <p>
|
|
|
984
|
|
|
985 <pre>
|
|
|
986 data infinite-d : ( x : Ordinal ) → Set n where
|
|
|
987 iφ : infinite-d o∅
|
|
|
988 isuc : {x : Ordinal } → infinite-d x →
|
|
425
|
989 infinite-d (& ( Union (* x , (* x , * x ) ) ))
|
|
273
|
990
|
|
|
991 </pre>
|
|
|
992 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
|
|
|
993 <p>
|
|
|
994
|
|
|
995 <hr/>
|
|
359
|
996 <h2><a name="content041">Axiom of Pair</a></h2>
|
|
273
|
997 In the Tanaka's book, axiom of pair is as follows.
|
|
|
998 <p>
|
|
|
999
|
|
|
1000 <pre>
|
|
|
1001 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
|
|
|
1002
|
|
|
1003 </pre>
|
|
|
1004 We have fix ∃ z, a function (x , y) is defined, which is _,_ .
|
|
|
1005 <p>
|
|
|
1006
|
|
|
1007 <pre>
|
|
|
1008 _,_ : ( A B : ZFSet ) → ZFSet
|
|
|
1009
|
|
|
1010 </pre>
|
|
|
1011 using this, we can define two directions in separates axioms, like this.
|
|
|
1012 <p>
|
|
|
1013
|
|
|
1014 <pre>
|
|
|
1015 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
|
|
|
1016 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
|
|
|
1017
|
|
|
1018 </pre>
|
|
|
1019 This is already written in Agda, so we use these as axioms. All inputs have ∀.
|
|
|
1020 <p>
|
|
|
1021
|
|
|
1022 <hr/>
|
|
359
|
1023 <h2><a name="content042">pair in OD</a></h2>
|
|
273
|
1024 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
|
|
|
1025 <p>
|
|
|
1026
|
|
|
1027 <pre>
|
|
338
|
1028 _,_ : HOD → HOD → HOD
|
|
425
|
1029 x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = ? ; <odmax = ? }
|
|
273
|
1030
|
|
|
1031 </pre>
|
|
338
|
1032 It is easy to find out odmax from odmax of x and y.
|
|
|
1033 <p>
|
|
273
|
1034 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
|
|
|
1035 <p>
|
|
|
1036
|
|
|
1037 <hr/>
|
|
359
|
1038 <h2><a name="content043">Validity of Axiom of Pair</a></h2>
|
|
273
|
1039 Assuming ZFSet is OD, we are going to prove pair→ .
|
|
|
1040 <p>
|
|
|
1041
|
|
|
1042 <pre>
|
|
|
1043 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
|
|
|
1044 pair→ x y t p = ?
|
|
|
1045
|
|
|
1046 </pre>
|
|
425
|
1047 In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ & x ) ∨ ( t ≡ & y ) .
|
|
273
|
1048 <p>
|
|
|
1049 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
|
|
|
1050 <p>
|
|
|
1051
|
|
|
1052 <pre>
|
|
|
1053 pair→ x y t (case1 t≡x ) = ?
|
|
|
1054 pair→ x y t (case2 t≡y ) = ?
|
|
|
1055
|
|
|
1056 </pre>
|
|
|
1057 The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ .
|
|
|
1058 <p>
|
|
|
1059
|
|
|
1060 <pre>
|
|
|
1061 pair→ x y t (case1 t≡x ) = case1 ?
|
|
|
1062 pair→ x y t (case2 t≡y ) = case2 ?
|
|
|
1063
|
|
|
1064 </pre>
|
|
|
1065 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
|
|
|
1066 which type is
|
|
|
1067 <p>
|
|
|
1068
|
|
|
1069 <pre>
|
|
425
|
1070 t≡x : & t ≡ & x
|
|
273
|
1071
|
|
|
1072 </pre>
|
|
|
1073 which is shown by an Agda command (C-C C-E : agda2-show-context ).
|
|
|
1074 <p>
|
|
|
1075 But we haven't defined == yet.
|
|
|
1076 <p>
|
|
|
1077
|
|
|
1078 <hr/>
|
|
359
|
1079 <h2><a name="content044">Equality of OD and Axiom of Extensionality </a></h2>
|
|
273
|
1080 OD is defined by a predicates, if we compares normal form of the predicates, even if
|
|
|
1081 it contains the same elements, it may be different, which is no good as an equality of
|
|
|
1082 Sets.
|
|
|
1083 <p>
|
|
|
1084 Axiom of Extensionality requires sets having the same elements are handled in the same way
|
|
|
1085 each other.
|
|
|
1086 <p>
|
|
|
1087
|
|
|
1088 <pre>
|
|
|
1089 ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
|
|
|
1090
|
|
|
1091 </pre>
|
|
|
1092 We can write this axiom in Agda as follows.
|
|
|
1093 <p>
|
|
|
1094
|
|
|
1095 <pre>
|
|
|
1096 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
|
|
|
1097
|
|
|
1098 </pre>
|
|
|
1099 So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
|
|
|
1100 A ∈ w ⇔ B ∈ w from A == B.
|
|
|
1101 <p>
|
|
|
1102 x == y can be defined in this way.
|
|
|
1103 <p>
|
|
|
1104
|
|
|
1105 <pre>
|
|
|
1106 record _==_ ( a b : OD ) : Set n where
|
|
|
1107 field
|
|
|
1108 eq→ : ∀ { x : Ordinal } → def a x → def b x
|
|
|
1109 eq← : ∀ { x : Ordinal } → def b x → def a x
|
|
|
1110
|
|
|
1111 </pre>
|
|
338
|
1112 Actually, (z : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B.
|
|
273
|
1113 <p>
|
|
|
1114
|
|
|
1115 <pre>
|
|
338
|
1116 extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od B
|
|
273
|
1117 eq→ (extensionality0 {A} {B} eq ) {x} d = ?
|
|
|
1118 eq← (extensionality0 {A} {B} eq ) {x} d = ?
|
|
|
1119
|
|
|
1120 </pre>
|
|
|
1121 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
|
|
|
1122 <p>
|
|
|
1123 Actual proof is rather complicated.
|
|
|
1124 <p>
|
|
|
1125
|
|
|
1126 <pre>
|
|
425
|
1127 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (* x))) d
|
|
|
1128 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (* x))) d
|
|
273
|
1129
|
|
|
1130 </pre>
|
|
|
1131 where
|
|
|
1132 <p>
|
|
|
1133
|
|
|
1134 <pre>
|
|
338
|
1135 odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x
|
|
|
1136 odef-iso refl t = t
|
|
273
|
1137
|
|
|
1138 </pre>
|
|
|
1139
|
|
|
1140 <hr/>
|
|
425
|
1141 <h2><a name="content045">The uniqueness of HOD</a></h2>
|
|
273
|
1142
|
|
|
1143 <p>
|
|
425
|
1144 To prove extensionality or other we need ==→o≡.
|
|
|
1145 <p>
|
|
|
1146 Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
|
|
|
1147 We can calculate the minimum using sup if we have bound but it is tedius.
|
|
|
1148 Only Select has non minimum odmax. We have the same problem on 'def' itself, but we leave it, that is we assume the
|
|
|
1149 assumption of predicates of Agda have a unique form, it is something like the
|
|
|
1150 functional extensionality assumption.
|
|
|
1151 <p>
|
|
|
1152
|
|
|
1153 <hr/>
|
|
|
1154 <h2><a name="content046">Validity of Axiom of Extensionality</a></h2>
|
|
338
|
1155 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes
|
|
273
|
1156 <p>
|
|
|
1157
|
|
|
1158 <pre>
|
|
338
|
1159 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
|
|
273
|
1160
|
|
|
1161 </pre>
|
|
|
1162 Using this, we have
|
|
|
1163 <p>
|
|
|
1164
|
|
|
1165 <pre>
|
|
338
|
1166 extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
|
|
273
|
1167 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
|
|
338
|
1168 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
|
|
273
|
1169
|
|
|
1170 </pre>
|
|
|
1171
|
|
|
1172 <hr/>
|
|
425
|
1173 <h2><a name="content047">Axiom of infinity</a></h2>
|
|
359
|
1174
|
|
|
1175 <p>
|
|
|
1176 It means it has ω as a ZF Set. It is ususally written like this.
|
|
|
1177 <p>
|
|
|
1178
|
|
|
1179 <pre>
|
|
|
1180 ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
|
|
|
1181
|
|
|
1182 </pre>
|
|
|
1183 x ∪ { x } is Union (x , (x , x)) in our notation. It contains existential quantifier, so we introduce a function
|
|
|
1184 <p>
|
|
|
1185
|
|
|
1186 <pre>
|
|
|
1187 infinite : ZFSet
|
|
|
1188 infinity∅ : ∅ ∈ infinite
|
|
|
1189 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
|
|
|
1190
|
|
|
1191 </pre>
|
|
|
1192
|
|
|
1193 <hr/>
|
|
425
|
1194 <h2><a name="content048">ω in HOD</a></h2>
|
|
359
|
1195
|
|
|
1196 <p>
|
|
425
|
1197 To define an OD which arrows & (Union (x , (x , x))) as a predicate, we can use Agda data structure.
|
|
359
|
1198 <p>
|
|
|
1199
|
|
|
1200 <pre>
|
|
|
1201 data infinite-d : ( x : Ordinal ) → Set n where
|
|
|
1202 iφ : infinite-d o∅
|
|
|
1203 isuc : {x : Ordinal } → infinite-d x →
|
|
425
|
1204 infinite-d (& ( Union (* x , (* x , * x ) ) ))
|
|
359
|
1205
|
|
|
1206 </pre>
|
|
|
1207 It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now
|
|
|
1208 we can define HOD like this.
|
|
|
1209 <p>
|
|
|
1210
|
|
|
1211 <pre>
|
|
|
1212 infinite : HOD
|
|
|
1213 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? }
|
|
|
1214
|
|
|
1215 </pre>
|
|
425
|
1216 So what is the bound of ω? Analyzing the definition, it depends on the value of & (x , x), which
|
|
|
1217 cannot know the aboslute value. This is because we don't have constructive definition of & : HOD → Ordinal.
|
|
359
|
1218 <p>
|
|
361
|
1219
|
|
|
1220 <hr/>
|
|
425
|
1221 <h2><a name="content049">HOD and Agda data structure</a></h2>
|
|
|
1222 We may have
|
|
|
1223 <p>
|
|
|
1224
|
|
|
1225 <pre>
|
|
|
1226 a HOD <=> Agda Data Strucure
|
|
|
1227
|
|
|
1228 </pre>
|
|
|
1229 as a data in Agda. Ex.
|
|
|
1230 <p>
|
|
|
1231
|
|
|
1232 <pre>
|
|
|
1233 data ord-pair : (p : Ordinal) → Set n where
|
|
|
1234 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
|
|
|
1235 ZFProduct : OD
|
|
|
1236 ZFProduct = record { def = λ x → ord-pair x }
|
|
|
1237 pi1 : { p : Ordinal } → ord-pair p → Ordinal
|
|
|
1238 pi1 ( pair x y) = x
|
|
|
1239 π1 : { p : HOD } → def ZFProduct (& p) → HOD
|
|
|
1240 π1 lt = * (pi1 lt )
|
|
|
1241 p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x
|
|
|
1242 p-iso {x} p = ord≡→≡ (op-iso p)
|
|
|
1243
|
|
|
1244 </pre>
|
|
|
1245
|
|
|
1246 <hr/>
|
|
|
1247 <h2><a name="content050">HOD Ordrinal mapping</a></h2>
|
|
|
1248
|
|
|
1249 <p>
|
|
361
|
1250 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger.
|
|
|
1251 The address of HOD can be larger at least it have to be larger than the content's address.
|
|
|
1252 We only have a relative ordering such as
|
|
|
1253 <p>
|
|
|
1254
|
|
|
1255 <pre>
|
|
425
|
1256 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
|
|
|
1257 pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y)
|
|
361
|
1258
|
|
|
1259 </pre>
|
|
|
1260 Basicaly, we cannot know the concrete address of HOD other than empty set.
|
|
|
1261 <p>
|
|
|
1262 <img src="fig/address-of-HOD.svg">
|
|
|
1263
|
|
|
1264 <p>
|
|
|
1265
|
|
|
1266 <hr/>
|
|
425
|
1267 <h2><a name="content051">Possible restriction on HOD</a></h2>
|
|
359
|
1268 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
|
|
|
1269 <p>
|
|
|
1270
|
|
|
1271 <pre>
|
|
|
1272 ωmax : Ordinal
|
|
|
1273 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
|
|
|
1274
|
|
|
1275 </pre>
|
|
|
1276 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be
|
|
|
1277 <p>
|
|
|
1278
|
|
|
1279 <pre>
|
|
|
1280 hod-ord< : {x : HOD } → Set n
|
|
425
|
1281 hod-ord< {x} = & x o< next (odmax x)
|
|
359
|
1282
|
|
|
1283 </pre>
|
|
|
1284 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and
|
|
|
1285 its bound.
|
|
|
1286 <p>
|
|
|
1287 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound.
|
|
|
1288 This is the reason of necessity of Axiom of infinite.
|
|
|
1289 <p>
|
|
|
1290
|
|
|
1291 <hr/>
|
|
425
|
1292 <h2><a name="content052">increment pase of address of HOD</a></h2>
|
|
361
|
1293 Assuming, hod-ord< , we have
|
|
359
|
1294 <p>
|
|
|
1295
|
|
|
1296 <pre>
|
|
425
|
1297 pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
|
|
|
1298 pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where
|
|
|
1299 lemmab0 : next (odmax (x , x)) ≡ next (& x)
|
|
359
|
1300
|
|
|
1301 </pre>
|
|
361
|
1302 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
|
|
359
|
1303 <p>
|
|
361
|
1304
|
|
|
1305 <pre>
|
|
425
|
1306 infinite-bound : ({x : HOD} → & x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
|
|
361
|
1307
|
|
|
1308 </pre>
|
|
425
|
1309 We also notice that if we have & (x , x) ≡ osuc (& x), c<→o< can be drived from ⊆→o≤ .
|
|
359
|
1310 <p>
|
|
|
1311
|
|
|
1312 <pre>
|
|
425
|
1313 ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
|
|
|
1314 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
|
|
|
1315 → {x y : HOD } → def (od y) ( & x ) → & x o< & y
|
|
359
|
1316
|
|
|
1317 </pre>
|
|
|
1318
|
|
|
1319 <hr/>
|
|
425
|
1320 <h2><a name="content053">Non constructive assumptions so far</a></h2>
|
|
338
|
1321
|
|
273
|
1322 <p>
|
|
|
1323
|
|
|
1324 <pre>
|
|
425
|
1325 & : HOD → Ordinal
|
|
|
1326 * : Ordinal → HOD
|
|
|
1327 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
|
|
|
1328 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
|
|
|
1329 oiso : {x : HOD } → * ( & x ) ≡ x
|
|
|
1330 diso : {x : Ordinal } → & ( * x ) ≡ x
|
|
338
|
1331 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
|
|
|
1332 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
|
|
|
1333 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
|
|
273
|
1334
|
|
|
1335 </pre>
|
|
|
1336
|
|
|
1337 <hr/>
|
|
425
|
1338 <h2><a name="content054">Axiom which have negation form</a></h2>
|
|
273
|
1339
|
|
|
1340 <p>
|
|
|
1341
|
|
|
1342 <pre>
|
|
|
1343 Union, Selection
|
|
|
1344
|
|
|
1345 </pre>
|
|
|
1346 These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
|
|
|
1347 <p>
|
|
|
1348 Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
|
|
|
1349 <p>
|
|
|
1350 Power Set axiom requires double negation,
|
|
|
1351 <p>
|
|
|
1352
|
|
|
1353 <pre>
|
|
|
1354 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
|
|
|
1355 power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
|
|
|
1356
|
|
|
1357 </pre>
|
|
|
1358 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
|
|
|
1359 <p>
|
|
|
1360
|
|
|
1361 <hr/>
|
|
425
|
1362 <h2><a name="content055">Union </a></h2>
|
|
273
|
1363 The original form of the Axiom of Union is
|
|
|
1364 <p>
|
|
|
1365
|
|
|
1366 <pre>
|
|
|
1367 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
|
|
|
1368
|
|
|
1369 </pre>
|
|
|
1370 Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃.
|
|
|
1371 <p>
|
|
|
1372
|
|
|
1373 <pre>
|
|
|
1374 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
|
|
|
1375 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
|
|
|
1376
|
|
|
1377 </pre>
|
|
359
|
1378 The definition of Union in HOD is like this.
|
|
273
|
1379 <p>
|
|
|
1380
|
|
|
1381 <pre>
|
|
359
|
1382 Union : HOD → HOD
|
|
425
|
1383 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) }
|
|
|
1384 ; odmax = osuc (& U) ; <odmax = ? }
|
|
273
|
1385
|
|
|
1386 </pre>
|
|
359
|
1387 The bound of Union is evident, but its proof is rather complicated.
|
|
|
1388 <p>
|
|
273
|
1389 Proof of validity is straight forward.
|
|
|
1390 <p>
|
|
|
1391
|
|
|
1392 <pre>
|
|
359
|
1393 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
|
|
425
|
1394 union→ X z u xx not = ⊥-elim ( not (& u) ( record { proj1 = proj1 xx
|
|
|
1395 ; proj2 = subst ( λ k → odef k (& z)) (sym oiso) (proj2 xx) } ))
|
|
359
|
1396 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
|
|
273
|
1397 union← X z UX∋z = FExists _ lemma UX∋z where
|
|
425
|
1398 lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
|
|
|
1399 lemma {y} xx not = not (* y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
|
|
273
|
1400
|
|
|
1401 </pre>
|
|
|
1402 where
|
|
|
1403 <p>
|
|
|
1404
|
|
|
1405 <pre>
|
|
|
1406 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
|
|
|
1407 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
|
|
|
1408 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
|
|
|
1409 → ¬ p
|
|
|
1410 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
|
|
|
1411
|
|
|
1412 </pre>
|
|
|
1413 which checks existence using contra-position.
|
|
|
1414 <p>
|
|
|
1415
|
|
|
1416 <hr/>
|
|
425
|
1417 <h2><a name="content056">Axiom of replacement</a></h2>
|
|
273
|
1418 We can replace the elements of a set by a function and it becomes a set. From the book,
|
|
|
1419 <p>
|
|
|
1420
|
|
|
1421 <pre>
|
|
|
1422 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
|
|
|
1423
|
|
|
1424 </pre>
|
|
|
1425 The existential quantifier can be related by a function,
|
|
|
1426 <p>
|
|
|
1427
|
|
|
1428 <pre>
|
|
359
|
1429 Replace : HOD → (HOD → HOD ) → HOD
|
|
273
|
1430
|
|
|
1431 </pre>
|
|
|
1432 The axioms becomes as follows.
|
|
|
1433 <p>
|
|
|
1434
|
|
|
1435 <pre>
|
|
|
1436 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
|
|
|
1437 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
|
|
|
1438
|
|
|
1439 </pre>
|
|
|
1440 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
|
|
|
1441 negation form of existential quantifier in the definition.
|
|
|
1442 <p>
|
|
|
1443
|
|
|
1444 <pre>
|
|
|
1445 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
|
|
425
|
1446 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ & (ψ (* y ))))) }
|
|
273
|
1447
|
|
|
1448 </pre>
|
|
359
|
1449 in-codomain is a logical relation-ship, and it is written in OD.
|
|
273
|
1450 <p>
|
|
|
1451
|
|
|
1452 <pre>
|
|
359
|
1453 Replace : HOD → (HOD → HOD) → HOD
|
|
425
|
1454 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
|
|
359
|
1455 ; odmax = rmax ; <odmax = rmax<} where
|
|
|
1456 rmax : Ordinal
|
|
425
|
1457 rmax = sup-o X (λ y X∋y → & (ψ (* y)))
|
|
359
|
1458 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
|
|
|
1459 rmax< lt = proj1 lt
|
|
273
|
1460
|
|
|
1461 </pre>
|
|
359
|
1462 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set.
|
|
|
1463 <p>
|
|
|
1464 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship.
|
|
273
|
1465 <p>
|
|
|
1466
|
|
|
1467 <hr/>
|
|
425
|
1468 <h2><a name="content057">Validity of Power Set Axiom</a></h2>
|
|
273
|
1469 The original Power Set Axiom is this.
|
|
|
1470 <p>
|
|
|
1471
|
|
|
1472 <pre>
|
|
|
1473 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
|
|
|
1474
|
|
|
1475 </pre>
|
|
|
1476 The existential quantifier is replaced by a function
|
|
|
1477 <p>
|
|
|
1478
|
|
|
1479 <pre>
|
|
|
1480 Power : ( A : OD ) → OD
|
|
|
1481
|
|
|
1482 </pre>
|
|
|
1483 t ⊆ X is a record like this.
|
|
|
1484 <p>
|
|
|
1485
|
|
|
1486 <pre>
|
|
|
1487 record _⊆_ ( A B : OD ) : Set (suc n) where
|
|
|
1488 field
|
|
|
1489 incl : { x : OD } → A ∋ x → B ∋ x
|
|
|
1490
|
|
|
1491 </pre>
|
|
|
1492 Axiom becomes likes this.
|
|
|
1493 <p>
|
|
|
1494
|
|
|
1495 <pre>
|
|
|
1496 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
1497 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
|
|
|
1498
|
|
|
1499 </pre>
|
|
|
1500 The validity of the axioms are slight complicated, we have to define set of all subset. We define
|
|
|
1501 subset in a different form.
|
|
|
1502 <p>
|
|
|
1503
|
|
|
1504 <pre>
|
|
359
|
1505 ZFSubset : (A x : HOD ) → HOD
|
|
|
1506 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where
|
|
|
1507 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
|
|
|
1508 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
|
|
273
|
1509
|
|
|
1510 </pre>
|
|
|
1511 We can prove,
|
|
|
1512 <p>
|
|
|
1513
|
|
|
1514 <pre>
|
|
359
|
1515 ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
|
|
273
|
1516
|
|
|
1517 </pre>
|
|
|
1518 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
|
|
|
1519 which is an Ordinals with our Model.
|
|
|
1520 <p>
|
|
|
1521
|
|
|
1522 <pre>
|
|
|
1523 Ord : ( a : Ordinal ) → OD
|
|
|
1524 Ord a = record { def = λ y → y o< a }
|
|
|
1525 Def : (A : OD ) → OD
|
|
425
|
1526 Def A = Ord ( sup-o ( λ x → & ( ZFSubset A (* x )) ) )
|
|
273
|
1527
|
|
|
1528 </pre>
|
|
|
1529 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
|
|
|
1530 <p>
|
|
|
1531
|
|
|
1532 <pre>
|
|
|
1533 Power : OD → OD
|
|
425
|
1534 Power A = Replace (Def (Ord (& A))) ( λ x → A ∩ x )
|
|
273
|
1535
|
|
|
1536 </pre>
|
|
|
1537 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
|
|
|
1538 <p>
|
|
|
1539
|
|
|
1540 <pre>
|
|
359
|
1541 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a )
|
|
273
|
1542
|
|
|
1543 </pre>
|
|
|
1544 In case of Ord a intro of Power Set axiom becomes valid.
|
|
|
1545 <p>
|
|
|
1546
|
|
|
1547 <pre>
|
|
359
|
1548 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
|
|
273
|
1549
|
|
|
1550 </pre>
|
|
|
1551 Using this, we can prove,
|
|
|
1552 <p>
|
|
|
1553
|
|
|
1554 <pre>
|
|
359
|
1555 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
1556 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
|
|
273
|
1557
|
|
|
1558 </pre>
|
|
|
1559
|
|
|
1560 <hr/>
|
|
425
|
1561 <h2><a name="content058">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
|
|
273
|
1562
|
|
|
1563 <p>
|
|
|
1564 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
|
|
|
1565 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
|
|
|
1566 <p>
|
|
|
1567 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
|
|
|
1568 choice also becomes valid.
|
|
|
1569 <p>
|
|
|
1570
|
|
|
1571 <pre>
|
|
359
|
1572 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD
|
|
425
|
1573 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( & ( minimal x ne ) )
|
|
|
1574 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (& y)) ∧ (def x (& y) )
|
|
273
|
1575
|
|
|
1576 </pre>
|
|
|
1577 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
|
|
|
1578 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
|
|
|
1579 <p>
|
|
|
1580
|
|
|
1581 <pre>
|
|
359
|
1582 ε-induction : { ψ : HOD → Set (suc n)}
|
|
|
1583 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
|
|
|
1584 → (x : HOD ) → ψ x
|
|
273
|
1585
|
|
|
1586 </pre>
|
|
|
1587 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
|
|
|
1588 <p>
|
|
|
1589 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
|
|
|
1590 <p>
|
|
|
1591
|
|
|
1592 <pre>
|
|
|
1593 ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
1594
|
|
|
1595 </pre>
|
|
|
1596 We can formulate like this.
|
|
|
1597 <p>
|
|
|
1598
|
|
|
1599 <pre>
|
|
|
1600 choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
|
|
|
1601 choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
|
|
|
1602
|
|
|
1603 </pre>
|
|
|
1604 It does not requires ∅ ∉ X .
|
|
|
1605 <p>
|
|
|
1606
|
|
|
1607 <hr/>
|
|
425
|
1608 <h2><a name="content059">Axiom of choice and Law of Excluded Middle</a></h2>
|
|
359
|
1609 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
|
|
273
|
1610 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
|
|
|
1611 but it requires law of the exclude middle.
|
|
|
1612 <p>
|
|
|
1613 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
|
|
|
1614 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
|
|
|
1615 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) .
|
|
|
1616 <p>
|
|
|
1617
|
|
|
1618 <pre>
|
|
359
|
1619 ppp : { p : Set n } { a : HOD } → record { def = λ x → p } ∋ a → p
|
|
273
|
1620 ppp {p} {a} d = d
|
|
|
1621
|
|
|
1622 </pre>
|
|
|
1623 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
|
|
|
1624 and Law of Excluded Middle is equivalent in our mode.
|
|
|
1625 <p>
|
|
|
1626
|
|
|
1627 <hr/>
|
|
425
|
1628 <h2><a name="content060">Relation-ship among ZF axiom</a></h2>
|
|
273
|
1629 <img src="fig/axiom-dependency.svg">
|
|
|
1630
|
|
|
1631 <p>
|
|
|
1632
|
|
|
1633 <hr/>
|
|
425
|
1634 <h2><a name="content061">Non constructive assumption in our model</a></h2>
|
|
359
|
1635 mapping between HOD and Ordinals
|
|
273
|
1636 <p>
|
|
|
1637
|
|
|
1638 <pre>
|
|
425
|
1639 & : HOD → Ordinal
|
|
|
1640 * : Ordinal → OD
|
|
|
1641 oiso : {x : HOD } → * ( & x ) ≡ x
|
|
|
1642 diso : {x : Ordinal } → & ( * x ) ≡ x
|
|
|
1643 c<→o< : {x y : HOD } → def y ( & x ) → & x o< & y
|
|
|
1644 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
|
|
273
|
1645
|
|
|
1646 </pre>
|
|
|
1647 Equivalence on OD
|
|
|
1648 <p>
|
|
|
1649
|
|
|
1650 <pre>
|
|
359
|
1651 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
|
|
273
|
1652
|
|
|
1653 </pre>
|
|
|
1654 Upper bound
|
|
|
1655 <p>
|
|
|
1656
|
|
|
1657 <pre>
|
|
359
|
1658 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
|
|
|
1659 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
|
|
|
1660
|
|
|
1661 </pre>
|
|
|
1662 In order to have bounded ω,
|
|
|
1663 <p>
|
|
|
1664
|
|
|
1665 <pre>
|
|
425
|
1666 hod-ord< : {x : HOD} → & x o< next (odmax x)
|
|
273
|
1667
|
|
|
1668 </pre>
|
|
|
1669 Axiom of choice and strong axiom of regularity.
|
|
|
1670 <p>
|
|
|
1671
|
|
|
1672 <pre>
|
|
359
|
1673 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
|
|
425
|
1674 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
|
|
|
1675 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
|
|
273
|
1676
|
|
|
1677 </pre>
|
|
|
1678
|
|
|
1679 <hr/>
|
|
425
|
1680 <h2><a name="content062">V </a></h2>
|
|
273
|
1681
|
|
|
1682 <p>
|
|
425
|
1683 The cumulative hierarchy
|
|
|
1684 <pre>
|
|
|
1685 V 0 := ∅
|
|
|
1686 V α + 1 := P ( V α )
|
|
|
1687 V α := ⋃ { V β | β < α }
|
|
|
1688
|
|
|
1689 </pre>
|
|
|
1690 Using TransFinite induction
|
|
|
1691 <p>
|
|
|
1692
|
|
|
1693 <pre>
|
|
|
1694 V : ( β : Ordinal ) → HOD
|
|
|
1695 V β = TransFinite V1 β where
|
|
|
1696 V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
1697 V1 x V0 with trio< x o∅
|
|
|
1698 V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
1699 V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
1700 V1 x V0 | tri> ¬a ¬b c with Oprev-p x
|
|
|
1701 V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
1702 V1 x V0 | tri> ¬a ¬b c | no ¬p =
|
|
|
1703 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ;
|
|
|
1704 odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
1705
|
|
|
1706 </pre>
|
|
|
1707 In our system, clearly V ⊆ HOD。
|
|
|
1708 <p>
|
|
|
1709
|
|
|
1710 <hr/>
|
|
|
1711 <h2><a name="content063">L</a></h2>
|
|
|
1712 The constructible Sets
|
|
|
1713 <pre>
|
|
|
1714 L 0 := ∅
|
|
|
1715 L α + 1 := Df (L α) -- Definable Power Set
|
|
|
1716 V α := ⋃ { L β | β < α }
|
|
|
1717
|
|
|
1718 </pre>
|
|
|
1719 What is Df? In our system, Power x is definable by Sup.
|
|
|
1720 <p>
|
|
|
1721
|
|
|
1722 <pre>
|
|
|
1723 record Definitions : Set (suc n) where
|
|
|
1724 field
|
|
|
1725 Definition : HOD → HOD
|
|
|
1726 open Definitions
|
|
|
1727 Df : Definitions → (x : HOD) → HOD
|
|
|
1728 Df D x = Power x ∩ Definition D x
|
|
|
1729
|
|
|
1730 </pre>
|
|
|
1731
|
|
|
1732 <hr/>
|
|
|
1733 <h2><a name="content064">L</a></h2>
|
|
|
1734
|
|
|
1735 <p>
|
|
|
1736
|
|
|
1737 <pre>
|
|
|
1738 L : ( β : Ordinal ) → Definitions → HOD
|
|
|
1739 L β D = TransFinite L1 β where
|
|
|
1740 L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
1741 L1 x L0 with trio< x o∅
|
|
|
1742 L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
1743 L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
1744 L1 x L0 | tri> ¬a ¬b c with Oprev-p x
|
|
|
1745 L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
1746 L1 x L0 | tri> ¬a ¬b c | no ¬p =
|
|
|
1747 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ;
|
|
|
1748 odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
1749
|
|
|
1750 </pre>
|
|
|
1751
|
|
|
1752 <hr/>
|
|
|
1753 <h2><a name="content065">V=L</a></h2>
|
|
|
1754
|
|
|
1755 <p>
|
|
|
1756
|
|
|
1757 <pre>
|
|
|
1758 V=L0 : Set (suc n)
|
|
|
1759 V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
|
|
|
1760
|
|
|
1761 </pre>
|
|
|
1762 is obvious. Definitions should have some restrictions, such as it includes Nat.
|
|
|
1763 <p>
|
|
|
1764
|
|
|
1765 <hr/>
|
|
|
1766 <h2><a name="content066">Some other ...</a></h2>
|
|
|
1767
|
|
|
1768 <hr/>
|
|
|
1769 <h2><a name="content067">So it this correct?</a></h2>
|
|
273
|
1770 Our axiom are syntactically the same in the text book, but negations are slightly different.
|
|
|
1771 <p>
|
|
|
1772 If we assumes excluded middle, these are exactly same.
|
|
|
1773 <p>
|
|
|
1774 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
|
|
|
1775 <p>
|
|
|
1776 Except the upper bound, axioms are simple logical relation.
|
|
|
1777 <p>
|
|
359
|
1778 Proof of existence of mapping between HOD and Ordinals are not obvious. We don't know we prove it or not.
|
|
273
|
1779 <p>
|
|
|
1780 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
|
|
|
1781 but we don't have explicit upper limit on Ordinals.
|
|
|
1782 <p>
|
|
|
1783 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
|
|
|
1784 <p>
|
|
|
1785
|
|
|
1786 <hr/>
|
|
425
|
1787 <h2><a name="content068">How to use Agda Set Theory</a></h2>
|
|
273
|
1788 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
|
|
|
1789 postulated or assuming law of excluded middle.
|
|
|
1790 <p>
|
|
|
1791 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
|
|
|
1792 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
|
|
|
1793 <p>
|
|
|
1794 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
|
|
|
1795 <p>
|
|
|
1796
|
|
|
1797 <hr/>
|
|
425
|
1798 <h2><a name="content069">Topos and Set Theory</a></h2>
|
|
273
|
1799 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
|
|
|
1800 sub-object classifier.
|
|
|
1801 <p>
|
|
|
1802 Topos itself is model of intuitionistic logic.
|
|
|
1803 <p>
|
|
|
1804 Transitive Sets are objects of Cartesian closed category.
|
|
|
1805 It is possible to introduce Power Set Functor on it
|
|
|
1806 <p>
|
|
|
1807 We can use replacement A ∩ x for each element in Transitive Set,
|
|
|
1808 in the similar way of our power set axiom. I
|
|
|
1809 <p>
|
|
|
1810 A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus.
|
|
|
1811 <p>
|
|
|
1812 Our Agda model is a proof theoretic version of it.
|
|
|
1813 <p>
|
|
|
1814
|
|
|
1815 <hr/>
|
|
425
|
1816 <h2><a name="content070">Cardinal number and Continuum hypothesis</a></h2>
|
|
273
|
1817 Axiom of choice is required to define cardinal number
|
|
|
1818 <p>
|
|
|
1819 definition of cardinal number is not yet done
|
|
|
1820 <p>
|
|
|
1821 definition of filter is not yet done
|
|
|
1822 <p>
|
|
|
1823 we may have a model without axiom of choice or without continuum hypothesis
|
|
|
1824 <p>
|
|
|
1825 Possible representation of continuum hypothesis is this.
|
|
|
1826 <p>
|
|
|
1827
|
|
|
1828 <pre>
|
|
|
1829 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
|
|
|
1830
|
|
|
1831 </pre>
|
|
|
1832
|
|
|
1833 <hr/>
|
|
425
|
1834 <h2><a name="content071">Filter</a></h2>
|
|
273
|
1835
|
|
|
1836 <p>
|
|
|
1837 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
|
|
|
1838 is depends on axiom of choice.
|
|
|
1839 <p>
|
|
|
1840
|
|
|
1841 <pre>
|
|
359
|
1842 record Filter ( L : HOD ) : Set (suc n) where
|
|
273
|
1843 field
|
|
|
1844 filter : OD
|
|
|
1845 proper : ¬ ( filter ∋ od∅ )
|
|
|
1846 inL : filter ⊆ L
|
|
359
|
1847 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
|
|
|
1848 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
|
|
273
|
1849
|
|
|
1850 </pre>
|
|
|
1851 We may construct a model of non standard analysis or set theory.
|
|
|
1852 <p>
|
|
|
1853 This may be simpler than classical forcing theory ( not yet done).
|
|
|
1854 <p>
|
|
|
1855
|
|
|
1856 <hr/>
|
|
425
|
1857 <h2><a name="content072">Programming Mathematics</a></h2>
|
|
273
|
1858 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
|
|
|
1859 structure are
|
|
|
1860 <p>
|
|
|
1861
|
|
|
1862 <pre>
|
|
|
1863 record and data
|
|
|
1864
|
|
|
1865 </pre>
|
|
|
1866 Proof is check by type consistency not by the computation, but it may include some normalization.
|
|
|
1867 <p>
|
|
|
1868 Type inference and termination is not so clear in multi recursions.
|
|
|
1869 <p>
|
|
|
1870 Defining Agda record is a good way to understand mathematical theory, for examples,
|
|
|
1871 <p>
|
|
|
1872
|
|
|
1873 <pre>
|
|
|
1874 Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
|
|
|
1875 Automaton ( Subset construction、Language containment)
|
|
|
1876
|
|
|
1877 </pre>
|
|
|
1878 are proved in Agda.
|
|
|
1879 <p>
|
|
|
1880
|
|
|
1881 <hr/>
|
|
425
|
1882 <h2><a name="content073">link</a></h2>
|
|
273
|
1883 Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a>
|
|
|
1884 <p>
|
|
|
1885 Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
|
|
|
1886 </a>
|
|
|
1887 <p>
|
|
|
1888 Agda
|
|
|
1889 <br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a>
|
|
|
1890 <p>
|
|
|
1891 ZF-in-Agda source
|
|
|
1892 <br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git
|
|
|
1893 </a>
|
|
|
1894 <p>
|
|
|
1895 Category theory in Agda source
|
|
|
1896 <br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda
|
|
|
1897 </a>
|
|
|
1898 <p>
|
|
|
1899 </div>
|
|
|
1900 <ol class="side" id="menu">
|
|
|
1901 Constructing ZF Set Theory in Agda
|
|
279
|
1902 <li><a href="#content000"> ZF in Agda</a>
|
|
|
1903 <li><a href="#content001"> Programming Mathematics</a>
|
|
|
1904 <li><a href="#content002"> Target</a>
|
|
|
1905 <li><a href="#content003"> Why Set Theory</a>
|
|
|
1906 <li><a href="#content004"> Agda and Intuitionistic Logic </a>
|
|
|
1907 <li><a href="#content005"> Introduction of Agda </a>
|
|
|
1908 <li><a href="#content006"> data ( Sum type )</a>
|
|
|
1909 <li><a href="#content007"> A → B means "A implies B"</a>
|
|
|
1910 <li><a href="#content008"> introduction と elimination</a>
|
|
|
1911 <li><a href="#content009"> To prove A → B </a>
|
|
|
1912 <li><a href="#content010"> A ∧ B</a>
|
|
|
1913 <li><a href="#content011"> record</a>
|
|
|
1914 <li><a href="#content012"> Mathematical structure</a>
|
|
359
|
1915 <li><a href="#content013"> Limit Ordinal</a>
|
|
|
1916 <li><a href="#content014"> A Model and a theory</a>
|
|
|
1917 <li><a href="#content015"> postulate と module</a>
|
|
|
1918 <li><a href="#content016"> A ∨ B</a>
|
|
|
1919 <li><a href="#content017"> Negation</a>
|
|
|
1920 <li><a href="#content018"> Equality </a>
|
|
|
1921 <li><a href="#content019"> Equivalence relation</a>
|
|
|
1922 <li><a href="#content020"> Ordering</a>
|
|
|
1923 <li><a href="#content021"> Quantifier</a>
|
|
|
1924 <li><a href="#content022"> Can we do math in this way?</a>
|
|
|
1925 <li><a href="#content023"> Things which Agda cannot prove</a>
|
|
|
1926 <li><a href="#content024"> Classical story of ZF Set Theory</a>
|
|
|
1927 <li><a href="#content025"> Ordinals</a>
|
|
|
1928 <li><a href="#content026"> Axiom of Ordinals</a>
|
|
|
1929 <li><a href="#content027"> Concrete Ordinals or Countable Ordinals</a>
|
|
|
1930 <li><a href="#content028"> Model of Ordinals</a>
|
|
|
1931 <li><a href="#content029"> Debugging axioms using Model</a>
|
|
|
1932 <li><a href="#content030"> Countable Ordinals can contains uncountable set?</a>
|
|
|
1933 <li><a href="#content031"> What is Set</a>
|
|
|
1934 <li><a href="#content032"> We don't ask the contents of Set. It can be anything.</a>
|
|
|
1935 <li><a href="#content033"> Ordinal Definable Set</a>
|
|
|
1936 <li><a href="#content034"> OD is not ZF Set</a>
|
|
|
1937 <li><a href="#content035"> HOD : Hereditarily Ordinal Definable</a>
|
|
|
1938 <li><a href="#content036"> 1 to 1 mapping between an HOD and an Ordinal</a>
|
|
|
1939 <li><a href="#content037"> Order preserving in the mapping of OD and Ordinal</a>
|
|
|
1940 <li><a href="#content038"> Various Sets</a>
|
|
361
|
1941 <li><a href="#content039"> Fixing ZF axom to fit intuitionistic logic</a>
|
|
359
|
1942 <li><a href="#content040"> Pure logical axioms</a>
|
|
|
1943 <li><a href="#content041"> Axiom of Pair</a>
|
|
|
1944 <li><a href="#content042"> pair in OD</a>
|
|
|
1945 <li><a href="#content043"> Validity of Axiom of Pair</a>
|
|
|
1946 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a>
|
|
425
|
1947 <li><a href="#content045"> The uniqueness of HOD</a>
|
|
|
1948 <li><a href="#content046"> Validity of Axiom of Extensionality</a>
|
|
|
1949 <li><a href="#content047"> Axiom of infinity</a>
|
|
|
1950 <li><a href="#content048"> ω in HOD</a>
|
|
|
1951 <li><a href="#content049"> HOD and Agda data structure</a>
|
|
|
1952 <li><a href="#content050"> HOD Ordrinal mapping</a>
|
|
|
1953 <li><a href="#content051"> Possible restriction on HOD</a>
|
|
|
1954 <li><a href="#content052"> increment pase of address of HOD</a>
|
|
|
1955 <li><a href="#content053"> Non constructive assumptions so far</a>
|
|
|
1956 <li><a href="#content054"> Axiom which have negation form</a>
|
|
|
1957 <li><a href="#content055"> Union </a>
|
|
|
1958 <li><a href="#content056"> Axiom of replacement</a>
|
|
|
1959 <li><a href="#content057"> Validity of Power Set Axiom</a>
|
|
|
1960 <li><a href="#content058"> Axiom of regularity, Axiom of choice, ε-induction</a>
|
|
|
1961 <li><a href="#content059"> Axiom of choice and Law of Excluded Middle</a>
|
|
|
1962 <li><a href="#content060"> Relation-ship among ZF axiom</a>
|
|
|
1963 <li><a href="#content061"> Non constructive assumption in our model</a>
|
|
|
1964 <li><a href="#content062"> V </a>
|
|
|
1965 <li><a href="#content063"> L</a>
|
|
|
1966 <li><a href="#content064"> L</a>
|
|
|
1967 <li><a href="#content065"> V=L</a>
|
|
|
1968 <li><a href="#content066"> Some other ...</a>
|
|
|
1969 <li><a href="#content067"> So it this correct?</a>
|
|
|
1970 <li><a href="#content068"> How to use Agda Set Theory</a>
|
|
|
1971 <li><a href="#content069"> Topos and Set Theory</a>
|
|
|
1972 <li><a href="#content070"> Cardinal number and Continuum hypothesis</a>
|
|
|
1973 <li><a href="#content071"> Filter</a>
|
|
|
1974 <li><a href="#content072"> Programming Mathematics</a>
|
|
|
1975 <li><a href="#content073"> link</a>
|
|
273
|
1976 </ol>
|
|
|
1977
|
|
425
|
1978 <hr/> Shinji KONO / Tue Aug 4 18:09:41 2020
|
|
273
|
1979 </body></html>
|
