Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison zf-in-agda.html @ 288:4fcac1eebc74 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
axiom of choice clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jun 2020 20:31:30 +0900
parents 197e0b3d39dc
children bca043423554
comparison
equal deleted inserted replaced
256:6e1c60866788 288:4fcac1eebc74
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/>
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>
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/>
74 <h2><a name="content002">Target</a></h2>
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/>
92 <h2><a name="content003">Why Set Theory</a></h2>
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>
101 This is done during from May to September.
102 <p>
103
104 <hr/>
105 <h2><a name="content004">Agda and Intuitionistic Logic </a></h2>
106 Curry Howard Isomorphism
107 <p>
108
109 <pre>
110 Proposition : Proof ⇔ Type : Value
111
112 </pre>
113 which means
114 <p>
115 　　constructing a typed lambda calculus which corresponds a logic
116 <p>
117 Typed lambda calculus which allows complex type as a value of a variable (System FC)
118 <p>
119 　　First class Type / Dependent Type
120 <p>
121 Agda is a such a programming language which has similar syntax of Haskell
122 <p>
123 Coq is specialized in proof assistance such as command and tactics .
124 <p>
125
126 <hr/>
127 <h2><a name="content005">Introduction of Agda </a></h2>
128 A length of a list of type A.
129 <p>
130
131 <pre>
132 length : {A : Set } → List A → Nat
133 length [] = zero
134 length (_ ∷ t) = suc ( length t )
135
136 </pre>
137 Simple functional programming language. Type declaration is mandatory.
138 A colon means type, an equal means value. Indentation based.
139 <p>
140 Set is a base type (which may have a level ).
141 <p>
142 {} means implicit variable which can be omitted if Agda infers its value.
143 <p>
144
145 <hr/>
146 <h2><a name="content006">data ( Sum type )</a></h2>
147 A data type which as exclusive multiple constructors. A similar one as
148 union in C or case class in Scala.
149 <p>
150 It has a similar syntax as Haskell but it has a slight difference.
151 <p>
152
153 <pre>
154 data List (A : Set ) : Set where
155 [] : List A
156 _∷_ : A → List A → List A
157
158 </pre>
159 _∷_ means infix operator. If use explicit _, it can be used in a normal function
160 syntax.
161 <p>
162 Natural number can be defined as a usual way.
163 <p>
164
165 <pre>
166 data Nat : Set where
167 zero : Nat
168 suc : Nat → Nat
169
170 </pre>
171
172 <hr/>
173 <h2><a name="content007"> A → B means "A implies B"</a></h2>
174
175 <p>
176 In Agda, a type can be a value of a variable, which is usually called dependent type.
177 Type has a name Set in Agda.
178 <p>
179
180 <pre>
181 ex3 : {A B : Set} → Set
182 ex3 {A}{B} = A → B
183
184 </pre>
185 ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
186 <p>
187
188 <pre>
189 A type is a formula, the value is the proof
190
191 </pre>
192 A value of A → B can be interpreted as an inference from the formula A to the formula B, which
193 can be a function from a proof of A to a proof of B.
194 <p>
195
196 <hr/>
197 <h2><a name="content008">introduction と elimination</a></h2>
198 For a logical operator, there are two types of inference, an introduction and an elimination.
199 <p>
200
201 <pre>
202 intro creating symbol / constructor / introduction
203 elim using symbolic / accessors / elimination
204
205 </pre>
206 In Natural deduction, this can be written in proof schema.
207 <p>
208
209 <pre>
210 A
211 :
212 B A A → B
213 ------------- →intro ------------------ →elim
214 A → B B
215
216 </pre>
217 In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
218 <p>
219
220 <pre>
221 →intro : {A B : Set } → A → B → ( A → B )
222 →intro _ b = λ x → b
223 →elim : {A B : Set } → A → ( A → B ) → B
224 →elim a f = f a
225
226 </pre>
227 Important
228 <p>
229
230 <pre>
231 {A B : Set } → A → B → ( A → B )
232
233 </pre>
234 is
235 <p>
236
237 <pre>
238 {A B : Set } → ( A → ( B → ( A → B ) ))
239
240 </pre>
241 This makes currying of function easy.
242 <p>
243
244 <hr/>
245 <h2><a name="content009"> To prove A → B </a></h2>
246 Make a left type as an argument. (intros in Coq)
247 <p>
248
249 <pre>
250 ex5 : {A B C : Set } → A → B → C → ?
251 ex5 a b c = ?
252
253 </pre>
254 ? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
255 <p>
256 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
257 insufficient proof or instance (Yellow), Non-termination, the proof is completed.
258 <p>
259
260 <hr/>
261 <h2><a name="content010"> A ∧ B</a></h2>
262 Well known conjunction's introduction and elimination is as follow.
263 <p>
264
265 <pre>
266 A B A ∧ B A ∧ B
267 ------------- ----------- proj1 ---------- proj2
268 A ∧ B A B
269
270 </pre>
271 We can introduce a corresponding structure in our functional programming language.
272 <p>
273
274 <hr/>
275 <h2><a name="content011"> record</a></h2>
276
277 <pre>
278 record _∧_ A B : Set
279 field
280 proj1 : A
281 proj2 : B
282
283 </pre>
284 _∧_　means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) )
285 <p>
286 This a type which constructed from type A and type B. You may think this as an object
287 or struct.
288 <p>
289
290 <pre>
291 record { proj1 = x ; proj2 = y }
292
293 </pre>
294 is a constructor of _∧_.
295 <p>
296
297 <pre>
298 ex3 : {A B : Set} → A → B → ( A ∧ B )
299 ex3 a b = record { proj1 = a ; proj2 = b }
300 ex1 : {A B : Set} → ( A ∧ B ) → A
301 ex1 a∧b = proj1 a∧b
302
303 </pre>
304 a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
305 except parenthesis or colons. A symbol requires space separation such as a type defining colon.
306 <p>
307 Defining record can be recursively, but we don't use the recursion here.
308 <p>
309
310 <hr/>
311 <h2><a name="content012"> Mathematical structure</a></h2>
312 We have types of elements and the relationship in a mathematical structure.
313 <p>
314
315 <pre>
316 logical relation has no ordering
317 there is a natural ordering in arguments and a value in a function
318
319 </pre>
320 So we have typical definition style of mathematical structure with records.
321 <p>
322
323 <pre>
324 record IsOrdinals {n : Level} (ord : Set n)
325 (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
326 field
327 Otrans : {x y z : ord } → x o&lt; y → y o&lt; z → x o&lt; z
328 record Ordinals {n : Level} : Set (suc (suc n)) where
329 field
330 ord : Set n
331 _o&lt;_ : ord → ord → Set n
332 isOrdinal : IsOrdinals ord _o&lt;_
333
334 </pre>
335 In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
336 inputs and outputs are put in the field including IsOrdinal.
337 <p>
338 Fields of Ordinal is existential objects in the mathematical structure.
339 <p>
340
341 <hr/>
342 <h2><a name="content013"> A Model and a theory</a></h2>
343 Agda record is a type, so we can write it in the argument, but is it really exists?
344 <p>
345 If we have a value of the record, it simply exists, that is, we need to create all the existence
346 in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
347 <p>
348
349 <pre>
350 type of record = theory
351 value of record = model
352
353 </pre>
354 We call the value of the record as a model. If mathematical structure has a
355 model, it exists. Pretty Obvious.
356 <p>
357
358 <hr/>
359 <h2><a name="content014"> postulate と module</a></h2>
360 Agda proofs are separated by modules, which are large records.
361 <p>
362 postulates are assumptions. We can assume a type without proofs.
363 <p>
364
365 <pre>
366 postulate
367 sup-o : ( Ordinal → Ordinal ) → Ordinal
368 sup-o&lt; : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o&lt; sup-o ψ
369
370 </pre>
371 sup-o is an example of upper bound of a function and sup-o&lt; assumes it actually satisfies all the value is less than upper bound.
372 <p>
373 Writing some type in a module argument is the same as postulating a type, but
374 postulate can be written the middle of a proof.
375 <p>
376 postulate can be constructive.
377 <p>
378 postulate can be inconsistent, which result everything has a proof.
379 <p>
380
381 <hr/>
382 <h2><a name="content015"> A ∨ B</a></h2>
383
384 <pre>
385 data _∨_ (A B : Set) : Set where
386 case1 : A → A ∨ B
387 case2 : B → A ∨ B
388
389 </pre>
390 As Haskell, case1/case2 are patterns.
391 <p>
392
393 <pre>
394 ex3 : {A B : Set} → ( A ∨ A ) → A
395 ex3 = ?
396
397 </pre>
398 In a case statement, Agda command C-C C-C generates possible cases in the head.
399 <p>
400
401 <pre>
402 ex3 : {A B : Set} → ( A ∨ A ) → A
403 ex3 (case1 x) = ?
404 ex3 (case2 x) = ?
405
406 </pre>
407 Proof schema of ∨ is omit due to the complexity.
408 <p>
409
410 <hr/>
411 <h2><a name="content016"> Negation</a></h2>
412
413 <pre>
414 ⊥
415 ------------- ⊥-elim
416 A
417
418 </pre>
419 Anything can be derived from bottom, in this case a Set A. There is no introduction rule
420 in ⊥, which can be implemented as data which has no constructor.
421 <p>
422
423 <pre>
424 data ⊥ : Set where
425
426 </pre>
427 ⊥-elim can be proved like this.
428 <p>
429
430 <pre>
431 ⊥-elim : {A : Set } -&gt; ⊥ -&gt; A
432 ⊥-elim ()
433
434 </pre>
435 () means no match argument nor value.
436 <p>
437 A negation can be defined using ⊥ like this.
438 <p>
439
440 <pre>
441 ¬_ : Set → Set
442 ¬ A = A → ⊥
443
444 </pre>
445
446 <hr/>
447 <h2><a name="content017">Equality </a></h2>
448
449 <p>
450 All the value in Agda are terms. If we have the same normalized form, two terms are equal.
451 If we have variables in the terms, we will perform an unification. unifiable terms are equal.
452 We don't go further on the unification.
453 <p>
454
455 <pre>
456 { x : A } x ≡ y f x y
457 --------------- ≡-intro --------------------- ≡-elim
458 x ≡ x f x x
459
460 </pre>
461 equality _≡_ can be defined as a data.
462 <p>
463
464 <pre>
465 data _≡_ {A : Set } : A → A → Set where
466 refl : {x : A} → x ≡ x
467
468 </pre>
469 The elimination of equality is a substitution in a term.
470 <p>
471
472 <pre>
473 subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
474 subst {A} {x} {y} f refl fx = fx
475 ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
476 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
477
478 </pre>
479
480 <hr/>
481 <h2><a name="content018">Equivalence relation</a></h2>
482
483 <p>
484
485 <pre>
486 refl' : {A : Set} {x : A } → x ≡ x
487 refl' = ?
488 sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
489 sym = ?
490 trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
491 trans = ?
492 cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
493 cong = ?
494
495 </pre>
496
497 <hr/>
498 <h2><a name="content019">Ordering</a></h2>
499
500 <p>
501 Relation is a predicate on two value which has a same type.
502 <p>
503
504 <pre>
505 A → A → Set
506
507 </pre>
508 Defining order is the definition of this type with predicate or a data.
509 <p>
510
511 <pre>
512 data _≤_ : Rel ℕ 0ℓ where
513 z≤n : ∀ {n} → zero ≤ n
514 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
515
516 </pre>
517
518 <hr/>
519 <h2><a name="content020">Quantifier</a></h2>
520
521 <p>
522 Handling quantifier in an intuitionistic logic requires special cares.
523 <p>
524 In the input of a function, there are no restriction on it, that is, it has
525 a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
526 <p>
527 There is no ∃ in agda, the one way is using negation like this.
528 <p>
529 　∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
530 <p>
531 On the another way, f : A can be used like this.
532 <p>
533
534 <pre>
535 p f
536
537 </pre>
538 If we use a function which can be defined globally which has stronger meaning the
539 usage of ∃ x in a logical expression.
540 <p>
541
542 <hr/>
543 <h2><a name="content021">Can we do math in this way?</a></h2>
544 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
545 <p>
546 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
547 <p>
548
549 <pre>
550 define mathematical structure as a record
551 program inferences as if we have proofs in variables
552
553 </pre>
554
555 <hr/>
556 <h2><a name="content022">Things which Agda cannot prove</a></h2>
557
558 <p>
559 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
560 leads uniqueness of a functor in Category Theory.
561 <p>
562 Functional extensionality cannot be proved.
563 <pre>
564 (∀ x → f x ≡ g x) → f ≡ g
565
566 </pre>
567 Agda has no law of exclude middle.
568 <p>
569
570 <pre>
571 a ∨ ( ¬ a )
572
573 </pre>
574 For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
575 <p>
576 It also other problems such as termination, type inference or unification which we may overcome with
577 efforts or devices or may not.
578 <p>
579 If we cannot prove something, we can safely postulate it unless it leads a contradiction.
580 <pre>
581
582
583 </pre>
584
585 <hr/>
586 <h2><a name="content023">Classical story of ZF Set Theory</a></h2>
587
588 <p>
589 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
590 a relative consistency proof of the Set Theory.
591 Ordinal number is used in the flow.
592 <p>
593 In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
594 We need some non constructive assumptions in the construction. A model of Set theory is
595 constructed based on these assumptions.
596 <p>
597 <img src="fig/set-theory.svg">
598
599 <p>
600
601 <hr/>
602 <h2><a name="content024">Ordinals</a></h2>
603 Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
604 It also has a successor osuc.
605 <p>
606
607 <pre>
608 record Ordinals {n : Level} : Set (suc (suc n)) where
609 field
610 ord : Set n
611 o∅ : ord
612 osuc : ord → ord
613 _o&lt;_ : ord → ord → Set n
614 isOrdinal : IsOrdinals ord o∅ osuc _o&lt;_
615
616 </pre>
617 It is different from natural numbers in way. The order of Ordinals is not defined in terms
618 of successor. It is given from outside, which make it possible to have higher order infinity.
619 <p>
620
621 <hr/>
622 <h2><a name="content025">Axiom of Ordinals</a></h2>
623 Properties of infinite things. We request a transfinite induction, which states that if
624 some properties are satisfied below all possible ordinals, the properties are true on all
625 ordinals.
626 <p>
627 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
628 which is not a successor of any ordinals. It is called limit ordinal.
629 <p>
630 Any two ordinal can be compared, that is less, equal or more, that is total order.
631 <p>
632
633 <pre>
634 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
635 (osuc : ord → ord )
636 (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
637 field
638 Otrans : {x y z : ord } → x o&lt; y → y o&lt; z → x o&lt; z
639 OTri : Trichotomous {n} _≡_ _o&lt;_
640 ¬x&lt;0 : { x : ord } → ¬ ( x o&lt; o∅ )
641 &lt;-osuc : { x : ord } → x o&lt; osuc x
642 osuc-≡&lt; : { a x : ord } → x o&lt; osuc a → (x ≡ a ) ∨ (x o&lt; a)
643 TransFinite : { ψ : ord → Set (suc n) }
644 → ( (x : ord) → ( (y : ord ) → y o&lt; x → ψ y ) → ψ x )
645 → ∀ (x : ord) → ψ x
646
647 </pre>
648
649 <hr/>
650 <h2><a name="content026">Concrete Ordinals</a></h2>
651
652 <p>
653 We can define a list like structure with level, which is a kind of two dimensional infinite array.
654 <p>
655
656 <pre>
657 data OrdinalD {n : Level} : (lv : Nat) → Set n where
658 Φ : (lv : Nat) → OrdinalD lv
659 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
660
661 </pre>
662 The order of the OrdinalD can be defined in this way.
663 <p>
664
665 <pre>
666 data _d&lt;_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
667 Φ&lt; : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d&lt; OSuc lx x
668 s&lt; : {lx : Nat} → {x y : OrdinalD {n} lx} → x d&lt; y → OSuc lx x d&lt; OSuc lx y
669
670 </pre>
671 This is a simple data structure, it has no abstract assumptions, and it is countable many data
672 structure.
673 <p>
674
675 <pre>
676 Φ 0
677 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
678 Osuc 0 (Φ 0) d&lt; Φ 1
679
680 </pre>
681
682 <hr/>
683 <h2><a name="content027">Model of Ordinals</a></h2>
684
685 <p>
686 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
687 <p>
688 So our Ordinals has a mode. This means axiom of Ordinals are consistent.
689 <p>
690
691 <hr/>
692 <h2><a name="content028">Debugging axioms using Model</a></h2>
693 Whether axiom is correct or not can be checked by a validity on a mode.
694 <p>
695 If not, we may fix the axioms or the model, such as the definitions of the order.
696 <p>
697 We can also ask whether the inputs exist.
698 <p>
699
700 <hr/>
701 <h2><a name="content029">Countable Ordinals can contains uncountable set?</a></h2>
702 Yes, the ordinals contains any level of infinite Set in the axioms.
703 <p>
704 If we handle real-number in the model, only countable number of real-number is used.
705 <p>
706
707 <pre>
708 from the outside view point, it is countable
709 from the internal view point, it is uncountable
710
711 </pre>
712 The definition of countable/uncountable is the same, but the properties are different
713 depending on the context.
714 <p>
715 We don't show the definition of cardinal number here.
716 <p>
717
718 <hr/>
719 <h2><a name="content030">What is Set</a></h2>
720 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
721 <p>
722 From naive point view, a set i a list, but in Agda, elements have all the same type.
723 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
724 <p>
725 Finite set may be written in finite series of ∨, but ...
726 <p>
727
728 <hr/>
729 <h2><a name="content031">We don't ask the contents of Set. It can be anything.</a></h2>
730 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
731 and all of them, and again we repeat this.
732 <p>
733
734 <pre>
735 φ {φ} {φ,{φ}}, {φ,{φ},...}
736
737 </pre>
738 It is called V.
739 <p>
740 This operation can be performed within a ZF Set theory. Classical Set Theory assumes
741 ZF, so this kind of thing is allowed.
742 <p>
743 But in our case, we have no ZF theory, so we are going to use Ordinals.
744 <p>
745
746 <hr/>
747 <h2><a name="content032">Ordinal Definable Set</a></h2>
748 We can define a sbuset of Ordinals using predicates. What is a subset?
749 <p>
750
751 <pre>
752 a predicate has an Ordinal argument
753
754 </pre>
755 is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
756 <p>
757
758 <pre>
759 record OD : Set (suc n ) where
760 field
761 def : (x : Ordinal ) → Set n
762
763 </pre>
764 Ordinals itself is not a set in a ZF Set theory but a class. In OD,
765 <p>
766
767 <pre>
768 record { def = λ x → true }
769
770 </pre>
771 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
772 but we don't care about it.
773 <p>
774
775 <hr/>
776 <h2><a name="content033">∋ in OD</a></h2>
777 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
778 <p>
779
780 <pre>
781 od→ord : OD → Ordinal
782
783 </pre>
784 we may check an OD is an element of the OD using def.
785 <p>
786 A ∋ x can be define as follows.
787 <p>
788
789 <pre>
790 _∋_ : ( A x : OD ) → Set n
791 _∋_ A x = def A ( od→ord x )
792
793 </pre>
794 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
795 <p>
796
797 <pre>
798 A x = def A ( od→ord x ) = ψ (od→ord x)
799
800 </pre>
801
802 <hr/>
803 <h2><a name="content034">1 to 1 mapping between an OD and an Ordinal</a></h2>
804
805 <p>
806
807 <pre>
808 od→ord : OD → Ordinal
809 ord→od : Ordinal → OD
810 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
811 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
812
813 </pre>
814 They say the existing of the mappings can be proved in Classical Set Theory, but we
815 simply assumes these non constructively.
816 <p>
817 We use postulate, it may contains additional restrictions which are not clear now. It look like the mapping should be a subset of Ordinals, but we don't explicitly
818 state it.
819 <p>
820 <img src="fig/ord-od-mapping.svg">
821
822 <p>
823
824 <hr/>
825 <h2><a name="content035">Order preserving in the mapping of OD and Ordinal</a></h2>
826 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
827 <p>
828
829 <pre>
830 def y ( od→ord x )
831
832 </pre>
833 An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
834 have to be smaller than the corresponding ordinal of the containing OD.
835 <p>
836
837 <pre>
838 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
839
840 </pre>
841 This is also said to be provable in classical Set Theory, but we simply assumes it.
842 <p>
843 OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation,
844 <p>
845
846 <pre>
847 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (ord→od y) x
848
849 </pre>
850 is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
851 the model.
852 <p>
853 <img src="fig/ODandOrdinals.svg">
854
855 <p>
856
857 <hr/>
858 <h2><a name="content036">ISO</a></h2>
859 It also requires isomorphisms,
860 <p>
861
862 <pre>
863 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
864 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
865
866 </pre>
867
868 <hr/>
869 <h2><a name="content037">Various Sets</a></h2>
870
871 <p>
872 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
873 <p>
874
875 <pre>
876 Ordinal / things satisfies axiom of Ordinal / extension of natural number
877 V / hierarchical construction of Set from φ
878 L / hierarchical predicate definable construction of Set from φ
879 OD / equational formula on Ordinals
880 Agda Set / Type / it also has a level
881
882 </pre>
883
884 <hr/>
885 <h2><a name="content038">Fixes on ZF to intuitionistic logic</a></h2>
886
887 <p>
888 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
889 ZF axioms in Agda.
890 <p>
891 It may not valid in our model. We have to debug it.
892 <p>
893 Fixes are depends on axioms.
894 <p>
895 <img src="fig/axiom-type.svg">
896
897 <p>
898 <a href="fig/zf-record.html">
899 ZFのrecord </a>
900 <p>
901
902 <hr/>
903 <h2><a name="content039">Pure logical axioms</a></h2>
904
905 <pre>
906 empty, pair, select, ε-induction??infinity
907
908 </pre>
909 These are logical relations among OD.
910 <p>
911
912 <pre>
913 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
914 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
915 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
916 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
917 infinity∅ : ∅ ∈ infinite
918 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
919 ε-induction : { ψ : OD → Set (suc n)}
920 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
921 → (x : OD ) → ψ x
922
923 </pre>
924 finitely can be define by Agda data.
925 <p>
926
927 <pre>
928 data infinite-d : ( x : Ordinal ) → Set n where
929 iφ : infinite-d o∅
930 isuc : {x : Ordinal } → infinite-d x →
931 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
932
933 </pre>
934 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
935 <p>
936
937 <hr/>
938 <h2><a name="content040">Axiom of Pair</a></h2>
939 In the Tanaka's book, axiom of pair is as follows.
940 <p>
941
942 <pre>
943 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
944
945 </pre>
946 We have fix ∃ z, a function (x , y) is defined, which is _,_ .
947 <p>
948
949 <pre>
950 _,_ : ( A B : ZFSet ) → ZFSet
951
952 </pre>
953 using this, we can define two directions in separates axioms, like this.
954 <p>
955
956 <pre>
957 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
958 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
959
960 </pre>
961 This is already written in Agda, so we use these as axioms. All inputs have ∀.
962 <p>
963
964 <hr/>
965 <h2><a name="content041">pair in OD</a></h2>
966 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
967 <p>
968
969 <pre>
970 _,_ : OD → OD → OD
971 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) }
972
973 </pre>
974 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
975 <p>
976
977 <hr/>
978 <h2><a name="content042">Validity of Axiom of Pair</a></h2>
979 Assuming ZFSet is OD, we are going to prove pair→ .
980 <p>
981
982 <pre>
983 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
984 pair→ x y t p = ?
985
986 </pre>
987 In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) .
988 <p>
989 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
990 <p>
991
992 <pre>
993 pair→ x y t (case1 t≡x ) = ?
994 pair→ x y t (case2 t≡y ) = ?
995
996 </pre>
997 The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ .
998 <p>
999
1000 <pre>
1001 pair→ x y t (case1 t≡x ) = case1 ?
1002 pair→ x y t (case2 t≡y ) = case2 ?
1003
1004 </pre>
1005 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
1006 which type is
1007 <p>
1008
1009 <pre>
1010 t≡x : od→ord t ≡ od→ord x
1011
1012 </pre>
1013 which is shown by an Agda command (C-C C-E : agda2-show-context ).
1014 <p>
1015 But we haven't defined == yet.
1016 <p>
1017
1018 <hr/>
1019 <h2><a name="content043">Equality of OD and Axiom of Extensionality </a></h2>
1020 OD is defined by a predicates, if we compares normal form of the predicates, even if
1021 it contains the same elements, it may be different, which is no good as an equality of
1022 Sets.
1023 <p>
1024 Axiom of Extensionality requires sets having the same elements are handled in the same way
1025 each other.
1026 <p>
1027
1028 <pre>
1029 ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
1030
1031 </pre>
1032 We can write this axiom in Agda as follows.
1033 <p>
1034
1035 <pre>
1036 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
1037
1038 </pre>
1039 So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
1040 A ∈ w ⇔ B ∈ w from A == B.
1041 <p>
1042 x == y can be defined in this way.
1043 <p>
1044
1045 <pre>
1046 record _==_ ( a b : OD ) : Set n where
1047 field
1048 eq→ : ∀ { x : Ordinal } → def a x → def b x
1049 eq← : ∀ { x : Ordinal } → def b x → def a x
1050
1051 </pre>
1052 Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
1053 <p>
1054
1055 <pre>
1056 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
1057 eq→ (extensionality0 {A} {B} eq ) {x} d = ?
1058 eq← (extensionality0 {A} {B} eq ) {x} d = ?
1059
1060 </pre>
1061 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
1062 <p>
1063 Actual proof is rather complicated.
1064 <p>
1065
1066 <pre>
1067 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
1068 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
1069
1070 </pre>
1071 where
1072 <p>
1073
1074 <pre>
1075 def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x
1076 def-iso refl t = t
1077
1078 </pre>
1079
1080 <hr/>
1081 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2>
1082
1083 <p>
1084 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes
1085 <p>
1086
1087 <pre>
1088 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1089
1090 </pre>
1091 Using this, we have
1092 <p>
1093
1094 <pre>
1095 extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
1096 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
1097 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
1098
1099 </pre>
1100 This assumption means we may have an equivalence set on any predicates.
1101 <p>
1102
1103 <hr/>
1104 <h2><a name="content045">Non constructive assumptions so far</a></h2>
1105 We have correspondence between OD and Ordinals and one directional order preserving.
1106 <p>
1107 We also have equality assumption.
1108 <p>
1109
1110 <pre>
1111 od→ord : OD → Ordinal
1112 ord→od : Ordinal → OD
1113 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
1114 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
1115 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
1116 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1117
1118 </pre>
1119
1120 <hr/>
1121 <h2><a name="content046">Axiom which have negation form</a></h2>
1122
1123 <p>
1124
1125 <pre>
1126 Union, Selection
1127
1128 </pre>
1129 These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
1130 <p>
1131 Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
1132 <p>
1133 Power Set axiom requires double negation,
1134 <p>
1135
1136 <pre>
1137 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
1138 power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
1139
1140 </pre>
1141 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
1142 <p>
1143
1144 <hr/>
1145 <h2><a name="content047">Union </a></h2>
1146 The original form of the Axiom of Union is
1147 <p>
1148
1149 <pre>
1150 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
1151
1152 </pre>
1153 Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃.
1154 <p>
1155
1156 <pre>
1157 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
1158 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
1159
1160 </pre>
1161 The definition of Union in OD is like this.
1162 <p>
1163
1164 <pre>
1165 Union : OD → OD
1166 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
1167
1168 </pre>
1169 Proof of validity is straight forward.
1170 <p>
1171
1172 <pre>
1173 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
1174 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
1175 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
1176 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
1177 union← X z UX∋z = FExists _ lemma UX∋z where
1178 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
1179 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
1180
1181 </pre>
1182 where
1183 <p>
1184
1185 <pre>
1186 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
1187 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
1188 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
1189 → ¬ p
1190 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
1191
1192 </pre>
1193 which checks existence using contra-position.
1194 <p>
1195
1196 <hr/>
1197 <h2><a name="content048">Axiom of replacement</a></h2>
1198 We can replace the elements of a set by a function and it becomes a set. From the book,
1199 <p>
1200
1201 <pre>
1202 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
1203
1204 </pre>
1205 The existential quantifier can be related by a function,
1206 <p>
1207
1208 <pre>
1209 Replace : OD → (OD → OD ) → OD
1210
1211 </pre>
1212 The axioms becomes as follows.
1213 <p>
1214
1215 <pre>
1216 replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
1217 replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
1218
1219 </pre>
1220 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
1221 negation form of existential quantifier in the definition.
1222 <p>
1223
1224 <pre>
1225 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
1226 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
1227
1228 </pre>
1229 Besides this upper bounds is required.
1230 <p>
1231
1232 <pre>
1233 Replace : OD → (OD → OD ) → OD
1234 Replace X ψ = record { def = λ x → (x o&lt; sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
1235
1236 </pre>
1237 We omit the proof of the validity, but it is rather straight forward.
1238 <p>
1239
1240 <hr/>
1241 <h2><a name="content049">Validity of Power Set Axiom</a></h2>
1242 The original Power Set Axiom is this.
1243 <p>
1244
1245 <pre>
1246 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
1247
1248 </pre>
1249 The existential quantifier is replaced by a function
1250 <p>
1251
1252 <pre>
1253 Power : ( A : OD ) → OD
1254
1255 </pre>
1256 t ⊆ X is a record like this.
1257 <p>
1258
1259 <pre>
1260 record _⊆_ ( A B : OD ) : Set (suc n) where
1261 field
1262 incl : { x : OD } → A ∋ x → B ∋ x
1263
1264 </pre>
1265 Axiom becomes likes this.
1266 <p>
1267
1268 <pre>
1269 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
1270 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1271
1272 </pre>
1273 The validity of the axioms are slight complicated, we have to define set of all subset. We define
1274 subset in a different form.
1275 <p>
1276
1277 <pre>
1278 ZFSubset : (A x : OD ) → OD
1279 ZFSubset A x = record { def = λ y → def A y ∧ def x y }
1280
1281 </pre>
1282 We can prove,
1283 <p>
1284
1285 <pre>
1286 ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
1287
1288 </pre>
1289 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
1290 which is an Ordinals with our Model.
1291 <p>
1292
1293 <pre>
1294 Ord : ( a : Ordinal ) → OD
1295 Ord a = record { def = λ y → y o&lt; a }
1296 Def : (A : OD ) → OD
1297 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
1298
1299 </pre>
1300 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
1301 <p>
1302
1303 <pre>
1304 Power : OD → OD
1305 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
1306
1307 </pre>
1308 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
1309 <p>
1310
1311 <pre>
1312 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
1313
1314 </pre>
1315 In case of Ord a intro of Power Set axiom becomes valid.
1316 <p>
1317
1318 <pre>
1319 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
1320
1321 </pre>
1322 Using this, we can prove,
1323 <p>
1324
1325 <pre>
1326 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
1327 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1328
1329 </pre>
1330
1331 <hr/>
1332 <h2><a name="content050">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
1333
1334 <p>
1335 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
1336 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
1337 <p>
1338 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
1339 choice also becomes valid.
1340 <p>
1341
1342 <pre>
1343 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
1344 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
1345 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
1346
1347 </pre>
1348 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
1349 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
1350 <p>
1351
1352 <pre>
1353 ε-induction : { ψ : OD → Set (suc n)}
1354 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
1355 → (x : OD ) → ψ x
1356
1357 </pre>
1358 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
1359 <p>
1360 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
1361 <p>
1362
1363 <pre>
1364 ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
1365
1366 </pre>
1367 We can formulate like this.
1368 <p>
1369
1370 <pre>
1371 choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
1372 choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
1373
1374 </pre>
1375 It does not requires ∅ ∉ X .
1376 <p>
1377
1378 <hr/>
1379 <h2><a name="content051">Axiom of choice and Law of Excluded Middle</a></h2>
1380 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
1381 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
1382 but it requires law of the exclude middle.
1383 <p>
1384 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
1385 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
1386 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) .
1387 <p>
1388
1389 <pre>
1390 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
1391 ppp {p} {a} d = d
1392
1393 </pre>
1394 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
1395 and Law of Excluded Middle is equivalent in our mode.
1396 <p>
1397
1398 <hr/>
1399 <h2><a name="content052">Relation-ship among ZF axiom</a></h2>
1400 <img src="fig/axiom-dependency.svg">
1401
1402 <p>
1403
1404 <hr/>
1405 <h2><a name="content053">Non constructive assumption in our model</a></h2>
1406 mapping between OD and Ordinals
1407 <p>
1408
1409 <pre>
1410 od→ord : OD → Ordinal
1411 ord→od : Ordinal → OD
1412 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
1413 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
1414 c&lt;→o&lt; : {x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y
1415
1416 </pre>
1417 Equivalence on OD
1418 <p>
1419
1420 <pre>
1421 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1422
1423 </pre>
1424 Upper bound
1425 <p>
1426
1427 <pre>
1428 sup-o : ( Ordinal → Ordinal ) → Ordinal
1429 sup-o&lt; : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o&lt; sup-o ψ
1430
1431 </pre>
1432 Axiom of choice and strong axiom of regularity.
1433 <p>
1434
1435 <pre>
1436 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
1437 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
1438 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
1439
1440 </pre>
1441
1442 <hr/>
1443 <h2><a name="content054">So it this correct?</a></h2>
1444
1445 <p>
1446 Our axiom are syntactically the same in the text book, but negations are slightly different.
1447 <p>
1448 If we assumes excluded middle, these are exactly same.
1449 <p>
1450 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
1451 <p>
1452 Except the upper bound, axioms are simple logical relation.
1453 <p>
1454 Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not.
1455 <p>
1456 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
1457 but we don't have explicit upper limit on Ordinals.
1458 <p>
1459 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
1460 <p>
1461
1462 <hr/>
1463 <h2><a name="content055">How to use Agda Set Theory</a></h2>
1464 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
1465 postulated or assuming law of excluded middle.
1466 <p>
1467 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
1468 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
1469 <p>
1470 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
1471 <p>
1472
1473 <hr/>
1474 <h2><a name="content056">Topos and Set Theory</a></h2>
1475 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
1476 sub-object classifier.
1477 <p>
1478 Topos itself is model of intuitionistic logic.
1479 <p>
1480 Transitive Sets are objects of Cartesian closed category.
1481 It is possible to introduce Power Set Functor on it
1482 <p>
1483 We can use replacement A ∩ x for each element in Transitive Set,
1484 in the similar way of our power set axiom. I
1485 <p>
1486 A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus.
1487 <p>
1488 Our Agda model is a proof theoretic version of it.
1489 <p>
1490
1491 <hr/>
1492 <h2><a name="content057">Cardinal number and Continuum hypothesis</a></h2>
1493 Axiom of choice is required to define cardinal number
1494 <p>
1495 definition of cardinal number is not yet done
1496 <p>
1497 definition of filter is not yet done
1498 <p>
1499 we may have a model without axiom of choice or without continuum hypothesis
1500 <p>
1501 Possible representation of continuum hypothesis is this.
1502 <p>
1503
1504 <pre>
1505 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
1506
1507 </pre>
1508
1509 <hr/>
1510 <h2><a name="content058">Filter</a></h2>
1511
1512 <p>
1513 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
1514 is depends on axiom of choice.
1515 <p>
1516
1517 <pre>
1518 record Filter ( L : OD ) : Set (suc n) where
1519 field
1520 filter : OD
1521 proper : ¬ ( filter ∋ od∅ )
1522 inL : filter ⊆ L
1523 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
1524 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
1525
1526 </pre>
1527 We may construct a model of non standard analysis or set theory.
1528 <p>
1529 This may be simpler than classical forcing theory ( not yet done).
1530 <p>
1531
1532 <hr/>
1533 <h2><a name="content059">Programming Mathematics</a></h2>
1534 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
1535 structure are
1536 <p>
1537
1538 <pre>
1539 record and data
1540
1541 </pre>
1542 Proof is check by type consistency not by the computation, but it may include some normalization.
1543 <p>
1544 Type inference and termination is not so clear in multi recursions.
1545 <p>
1546 Defining Agda record is a good way to understand mathematical theory, for examples,
1547 <p>
1548
1549 <pre>
1550 Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
1551 Automaton ( Subset construction、Language containment)
1552
1553 </pre>
1554 are proved in Agda.
1555 <p>
1556
1557 <hr/>
1558 <h2><a name="content060">link</a></h2>
1559 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>
1560 <p>
1561 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
1562 </a>
1563 <p>
1564 Agda
1565 <br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a>
1566 <p>
1567 ZF-in-Agda source
1568 <br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git
1569 </a>
1570 <p>
1571 Category theory in Agda source
1572 <br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda
1573 </a>
1574 <p>
1575 </div>
1576 <ol class="side" id="menu">
1577 Constructing ZF Set Theory in Agda
1578 <li><a href="#content000"> ZF in Agda</a>
1579 <li><a href="#content001"> Programming Mathematics</a>
1580 <li><a href="#content002"> Target</a>
1581 <li><a href="#content003"> Why Set Theory</a>
1582 <li><a href="#content004"> Agda and Intuitionistic Logic </a>
1583 <li><a href="#content005"> Introduction of Agda </a>
1584 <li><a href="#content006"> data ( Sum type )</a>
1585 <li><a href="#content007"> A → B means "A implies B"</a>
1586 <li><a href="#content008"> introduction と elimination</a>
1587 <li><a href="#content009"> To prove A → B </a>
1588 <li><a href="#content010"> A ∧ B</a>
1589 <li><a href="#content011"> record</a>
1590 <li><a href="#content012"> Mathematical structure</a>
1591 <li><a href="#content013"> A Model and a theory</a>
1592 <li><a href="#content014"> postulate と module</a>
1593 <li><a href="#content015"> A ∨ B</a>
1594 <li><a href="#content016"> Negation</a>
1595 <li><a href="#content017"> Equality </a>
1596 <li><a href="#content018"> Equivalence relation</a>
1597 <li><a href="#content019"> Ordering</a>
1598 <li><a href="#content020"> Quantifier</a>
1599 <li><a href="#content021"> Can we do math in this way?</a>
1600 <li><a href="#content022"> Things which Agda cannot prove</a>
1601 <li><a href="#content023"> Classical story of ZF Set Theory</a>
1602 <li><a href="#content024"> Ordinals</a>
1603 <li><a href="#content025"> Axiom of Ordinals</a>
1604 <li><a href="#content026"> Concrete Ordinals</a>
1605 <li><a href="#content027"> Model of Ordinals</a>
1606 <li><a href="#content028"> Debugging axioms using Model</a>
1607 <li><a href="#content029"> Countable Ordinals can contains uncountable set?</a>
1608 <li><a href="#content030"> What is Set</a>
1609 <li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a>
1610 <li><a href="#content032"> Ordinal Definable Set</a>
1611 <li><a href="#content033"> ∋ in OD</a>
1612 <li><a href="#content034"> 1 to 1 mapping between an OD and an Ordinal</a>
1613 <li><a href="#content035"> Order preserving in the mapping of OD and Ordinal</a>
1614 <li><a href="#content036"> ISO</a>
1615 <li><a href="#content037"> Various Sets</a>
1616 <li><a href="#content038"> Fixes on ZF to intuitionistic logic</a>
1617 <li><a href="#content039"> Pure logical axioms</a>
1618 <li><a href="#content040"> Axiom of Pair</a>
1619 <li><a href="#content041"> pair in OD</a>
1620 <li><a href="#content042"> Validity of Axiom of Pair</a>
1621 <li><a href="#content043"> Equality of OD and Axiom of Extensionality </a>
1622 <li><a href="#content044"> Validity of Axiom of Extensionality</a>
1623 <li><a href="#content045"> Non constructive assumptions so far</a>
1624 <li><a href="#content046"> Axiom which have negation form</a>
1625 <li><a href="#content047"> Union </a>
1626 <li><a href="#content048"> Axiom of replacement</a>
1627 <li><a href="#content049"> Validity of Power Set Axiom</a>
1628 <li><a href="#content050"> Axiom of regularity, Axiom of choice, ε-induction</a>
1629 <li><a href="#content051"> Axiom of choice and Law of Excluded Middle</a>
1630 <li><a href="#content052"> Relation-ship among ZF axiom</a>
1631 <li><a href="#content053"> Non constructive assumption in our model</a>
1632 <li><a href="#content054"> So it this correct?</a>
1633 <li><a href="#content055"> How to use Agda Set Theory</a>
1634 <li><a href="#content056"> Topos and Set Theory</a>
1635 <li><a href="#content057"> Cardinal number and Continuum hypothesis</a>
1636 <li><a href="#content058"> Filter</a>
1637 <li><a href="#content059"> Programming Mathematics</a>
1638 <li><a href="#content060"> link</a>
1639 </ol>
1640
1641 <hr/> Shinji KONO / Sat May 9 16:41:10 2020
1642 </body></html>