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

comparison zf-in-agda.html @ 279:197e0b3d39dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 16:41:40 +0900
parents 9ccf8514c323
children bca043423554
comparison
equal deleted inserted replaced
278:bfb5e807718b 279:197e0b3d39dc
36 <p> 36 <p>
37 37
38 <author> Shinji KONO</author> 38 <author> Shinji KONO</author>
39 39
40 <hr/> 40 <hr/>
41 <h2><a name="content000">Programming Mathematics</a></h2> 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>
42 Programming is processing data structure with λ terms. 64 Programming is processing data structure with λ terms.
43 <p> 65 <p>
44 We are going to handle Mathematics in intuitionistic logic with λ terms. 66 We are going to handle Mathematics in intuitionistic logic with λ terms.
45 <p> 67 <p>
46 Mathematics is a functional programming which values are proofs. 68 Mathematics is a functional programming which values are proofs.
47 <p> 69 <p>
48 Programming ZF Set Theory in Agda 70 Programming ZF Set Theory in Agda
49 <p> 71 <p>
50 72
51 <hr/> 73 <hr/>
52 <h2><a name="content001">Target</a></h2> 74 <h2><a name="content002">Target</a></h2>
53 75
54 <pre> 76 <pre>
55 Describe ZF axioms in Agda 77 Describe ZF axioms in Agda
56 Construction a Model of ZF Set Theory in Agda 78 Construction a Model of ZF Set Theory in Agda
57 Show necessary assumptions for the model 79 Show necessary assumptions for the model
65 ZF in Agda https://github.com/shinji-kono/zf-in-agda 87 ZF in Agda https://github.com/shinji-kono/zf-in-agda
66 </a> 88 </a>
67 <p> 89 <p>
68 90
69 <hr/> 91 <hr/>
70 <h2><a name="content002">Why Set Theory</a></h2> 92 <h2><a name="content003">Why Set Theory</a></h2>
71 If we can formulate Set theory, it suppose to work on any mathematical theory. 93 If we can formulate Set theory, it suppose to work on any mathematical theory.
72 <p> 94 <p>
73 Set Theory is a difficult point for beginners especially axiom of choice. 95 Set Theory is a difficult point for beginners especially axiom of choice.
74 <p> 96 <p>
75 It has some amount of difficulty and self circulating discussion. 97 It has some amount of difficulty and self circulating discussion.
78 <p> 100 <p>
79 This is done during from May to September. 101 This is done during from May to September.
80 <p> 102 <p>
81 103
82 <hr/> 104 <hr/>
83 <h2><a name="content003">Agda and Intuitionistic Logic </a></h2> 105 <h2><a name="content004">Agda and Intuitionistic Logic </a></h2>
84 Curry Howard Isomorphism 106 Curry Howard Isomorphism
85 <p> 107 <p>
86 108
87 <pre> 109 <pre>
88 Proposition : Proof ⇔ Type : Value 110 Proposition : Proof ⇔ Type : Value
100 <p> 122 <p>
101 Coq is specialized in proof assistance such as command and tactics . 123 Coq is specialized in proof assistance such as command and tactics .
102 <p> 124 <p>
103 125
104 <hr/> 126 <hr/>
105 <h2><a name="content004">Introduction of Agda </a></h2> 127 <h2><a name="content005">Introduction of Agda </a></h2>
106 A length of a list of type A. 128 A length of a list of type A.
107 <p> 129 <p>
108 130
109 <pre> 131 <pre>
110 length : {A : Set } → List A → Nat 132 length : {A : Set } → List A → Nat
119 <p> 141 <p>
120 {} means implicit variable which can be omitted if Agda infers its value. 142 {} means implicit variable which can be omitted if Agda infers its value.
121 <p> 143 <p>
122 144
123 <hr/> 145 <hr/>
124 <h2><a name="content005">data ( Sum type )</a></h2> 146 <h2><a name="content006">data ( Sum type )</a></h2>
125 A data type which as exclusive multiple constructors. A similar one as 147 A data type which as exclusive multiple constructors. A similar one as
126 union in C or case class in Scala. 148 union in C or case class in Scala.
127 <p> 149 <p>
128 It has a similar syntax as Haskell but it has a slight difference. 150 It has a similar syntax as Haskell but it has a slight difference.
129 <p> 151 <p>
146 suc : Nat → Nat 168 suc : Nat → Nat
147 169
148 </pre> 170 </pre>
149 171
150 <hr/> 172 <hr/>
151 <h2><a name="content006"> A → B means "A implies B"</a></h2> 173 <h2><a name="content007"> A → B means "A implies B"</a></h2>
152 174
153 <p> 175 <p>
154 In Agda, a type can be a value of a variable, which is usually called dependent type. 176 In Agda, a type can be a value of a variable, which is usually called dependent type.
155 Type has a name Set in Agda. 177 Type has a name Set in Agda.
156 <p> 178 <p>
170 A value of A → B can be interpreted as an inference from the formula A to the formula B, which 192 A value of A → B can be interpreted as an inference from the formula A to the formula B, which
171 can be a function from a proof of A to a proof of B. 193 can be a function from a proof of A to a proof of B.
172 <p> 194 <p>
173 195
174 <hr/> 196 <hr/>
175 <h2><a name="content007">introduction と elimination</a></h2> 197 <h2><a name="content008">introduction と elimination</a></h2>
176 For a logical operator, there are two types of inference, an introduction and an elimination. 198 For a logical operator, there are two types of inference, an introduction and an elimination.
177 <p> 199 <p>
178 200
179 <pre> 201 <pre>
180 intro creating symbol / constructor / introduction 202 intro creating symbol / constructor / introduction
218 </pre> 240 </pre>
219 This makes currying of function easy. 241 This makes currying of function easy.
220 <p> 242 <p>
221 243
222 <hr/> 244 <hr/>
223 <h2><a name="content008"> To prove A → B </a></h2> 245 <h2><a name="content009"> To prove A → B </a></h2>
224 Make a left type as an argument. (intros in Coq) 246 Make a left type as an argument. (intros in Coq)
225 <p> 247 <p>
226 248
227 <pre> 249 <pre>
228 ex5 : {A B C : Set } → A → B → C → ? 250 ex5 : {A B C : Set } → A → B → C → ?
234 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), 256 We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
235 insufficient proof or instance (Yellow), Non-termination, the proof is completed. 257 insufficient proof or instance (Yellow), Non-termination, the proof is completed.
236 <p> 258 <p>
237 259
238 <hr/> 260 <hr/>
239 <h2><a name="content009"> A ∧ B</a></h2> 261 <h2><a name="content010"> A ∧ B</a></h2>
240 Well known conjunction's introduction and elimination is as follow. 262 Well known conjunction's introduction and elimination is as follow.
241 <p> 263 <p>
242 264
243 <pre> 265 <pre>
244 A B A ∧ B A ∧ B 266 A B A ∧ B A ∧ B
248 </pre> 270 </pre>
249 We can introduce a corresponding structure in our functional programming language. 271 We can introduce a corresponding structure in our functional programming language.
250 <p> 272 <p>
251 273
252 <hr/> 274 <hr/>
253 <h2><a name="content010"> record</a></h2> 275 <h2><a name="content011"> record</a></h2>
254 276
255 <pre> 277 <pre>
256 record _∧_ A B : Set 278 record _∧_ A B : Set
257 field 279 field
258 proj1 : A 280 proj1 : A
284 <p> 306 <p>
285 Defining record can be recursively, but we don't use the recursion here. 307 Defining record can be recursively, but we don't use the recursion here.
286 <p> 308 <p>
287 309
288 <hr/> 310 <hr/>
289 <h2><a name="content011"> Mathematical structure</a></h2> 311 <h2><a name="content012"> Mathematical structure</a></h2>
290 We have types of elements and the relationship in a mathematical structure. 312 We have types of elements and the relationship in a mathematical structure.
291 <p> 313 <p>
292 314
293 <pre> 315 <pre>
294 logical relation has no ordering 316 logical relation has no ordering
315 <p> 337 <p>
316 Fields of Ordinal is existential objects in the mathematical structure. 338 Fields of Ordinal is existential objects in the mathematical structure.
317 <p> 339 <p>
318 340
319 <hr/> 341 <hr/>
320 <h2><a name="content012"> A Model and a theory</a></h2> 342 <h2><a name="content013"> A Model and a theory</a></h2>
321 Agda record is a type, so we can write it in the argument, but is it really exists? 343 Agda record is a type, so we can write it in the argument, but is it really exists?
322 <p> 344 <p>
323 If we have a value of the record, it simply exists, that is, we need to create all the existence 345 If we have a value of the record, it simply exists, that is, we need to create all the existence
324 in the record satisfies all the axioms (= field of IsOrdinal) should be valid. 346 in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
325 <p> 347 <p>
332 We call the value of the record as a model. If mathematical structure has a 354 We call the value of the record as a model. If mathematical structure has a
333 model, it exists. Pretty Obvious. 355 model, it exists. Pretty Obvious.
334 <p> 356 <p>
335 357
336 <hr/> 358 <hr/>
337 <h2><a name="content013"> postulate と module</a></h2> 359 <h2><a name="content014"> postulate と module</a></h2>
338 Agda proofs are separated by modules, which are large records. 360 Agda proofs are separated by modules, which are large records.
339 <p> 361 <p>
340 postulates are assumptions. We can assume a type without proofs. 362 postulates are assumptions. We can assume a type without proofs.
341 <p> 363 <p>
342 364
355 <p> 377 <p>
356 postulate can be inconsistent, which result everything has a proof. 378 postulate can be inconsistent, which result everything has a proof.
357 <p> 379 <p>
358 380
359 <hr/> 381 <hr/>
360 <h2><a name="content014"> A ∨ B</a></h2> 382 <h2><a name="content015"> A ∨ B</a></h2>
361 383
362 <pre> 384 <pre>
363 data _∨_ (A B : Set) : Set where 385 data _∨_ (A B : Set) : Set where
364 case1 : A → A ∨ B 386 case1 : A → A ∨ B
365 case2 : B → A ∨ B 387 case2 : B → A ∨ B
384 </pre> 406 </pre>
385 Proof schema of ∨ is omit due to the complexity. 407 Proof schema of ∨ is omit due to the complexity.
386 <p> 408 <p>
387 409
388 <hr/> 410 <hr/>
389 <h2><a name="content015"> Negation</a></h2> 411 <h2><a name="content016"> Negation</a></h2>
390 412
391 <pre> 413 <pre>
392 ⊥ 414 ⊥
393 ------------- ⊥-elim 415 ------------- ⊥-elim
394 A 416 A
420 ¬ A = A → ⊥ 442 ¬ A = A → ⊥
421 443
422 </pre> 444 </pre>
423 445
424 <hr/> 446 <hr/>
425 <h2><a name="content016">Equality </a></h2> 447 <h2><a name="content017">Equality </a></h2>
426 448
427 <p> 449 <p>
428 All the value in Agda are terms. If we have the same normalized form, two terms are equal. 450 All the value in Agda are terms. If we have the same normalized form, two terms are equal.
429 If we have variables in the terms, we will perform an unification. unifiable terms are equal. 451 If we have variables in the terms, we will perform an unification. unifiable terms are equal.
430 We don't go further on the unification. 452 We don't go further on the unification.
454 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y 476 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
455 477
456 </pre> 478 </pre>
457 479
458 <hr/> 480 <hr/>
459 <h2><a name="content017">Equivalence relation</a></h2> 481 <h2><a name="content018">Equivalence relation</a></h2>
460 482
461 <p> 483 <p>
462 484
463 <pre> 485 <pre>
464 refl' : {A : Set} {x : A } → x ≡ x 486 refl' : {A : Set} {x : A } → x ≡ x
471 cong = ? 493 cong = ?
472 494
473 </pre> 495 </pre>
474 496
475 <hr/> 497 <hr/>
476 <h2><a name="content018">Ordering</a></h2> 498 <h2><a name="content019">Ordering</a></h2>
477 499
478 <p> 500 <p>
479 Relation is a predicate on two value which has a same type. 501 Relation is a predicate on two value which has a same type.
480 <p> 502 <p>
481 503
492 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n 514 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
493 515
494 </pre> 516 </pre>
495 517
496 <hr/> 518 <hr/>
497 <h2><a name="content019">Quantifier</a></h2> 519 <h2><a name="content020">Quantifier</a></h2>
498 520
499 <p> 521 <p>
500 Handling quantifier in an intuitionistic logic requires special cares. 522 Handling quantifier in an intuitionistic logic requires special cares.
501 <p> 523 <p>
502 In the input of a function, there are no restriction on it, that is, it has 524 In the input of a function, there are no restriction on it, that is, it has
516 If we use a function which can be defined globally which has stronger meaning the 538 If we use a function which can be defined globally which has stronger meaning the
517 usage of ∃ x in a logical expression. 539 usage of ∃ x in a logical expression.
518 <p> 540 <p>
519 541
520 <hr/> 542 <hr/>
521 <h2><a name="content020">Can we do math in this way?</a></h2> 543 <h2><a name="content021">Can we do math in this way?</a></h2>
522 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). 544 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
523 <p> 545 <p>
524 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). 546 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
525 <p> 547 <p>
526 548
529 program inferences as if we have proofs in variables 551 program inferences as if we have proofs in variables
530 552
531 </pre> 553 </pre>
532 554
533 <hr/> 555 <hr/>
534 <h2><a name="content021">Things which Agda cannot prove</a></h2> 556 <h2><a name="content022">Things which Agda cannot prove</a></h2>
535 557
536 <p> 558 <p>
537 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which 559 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
538 leads uniqueness of a functor in Category Theory. 560 leads uniqueness of a functor in Category Theory.
539 <p> 561 <p>
559 581
560 582
561 </pre> 583 </pre>
562 584
563 <hr/> 585 <hr/>
564 <h2><a name="content022">Classical story of ZF Set Theory</a></h2> 586 <h2><a name="content023">Classical story of ZF Set Theory</a></h2>
565 587
566 <p> 588 <p>
567 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads 589 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
568 a relative consistency proof of the Set Theory. 590 a relative consistency proof of the Set Theory.
569 Ordinal number is used in the flow. 591 Ordinal number is used in the flow.
575 <img src="fig/set-theory.svg"> 597 <img src="fig/set-theory.svg">
576 598
577 <p> 599 <p>
578 600
579 <hr/> 601 <hr/>
580 <h2><a name="content023">Ordinals</a></h2> 602 <h2><a name="content024">Ordinals</a></h2>
581 Ordinals are our intuition of infinite things, which has ∅ and orders on the things. 603 Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
582 It also has a successor osuc. 604 It also has a successor osuc.
583 <p> 605 <p>
584 606
585 <pre> 607 <pre>
595 It is different from natural numbers in way. The order of Ordinals is not defined in terms 617 It is different from natural numbers in way. The order of Ordinals is not defined in terms
596 of successor. It is given from outside, which make it possible to have higher order infinity. 618 of successor. It is given from outside, which make it possible to have higher order infinity.
597 <p> 619 <p>
598 620
599 <hr/> 621 <hr/>
600 <h2><a name="content024">Axiom of Ordinals</a></h2> 622 <h2><a name="content025">Axiom of Ordinals</a></h2>
601 Properties of infinite things. We request a transfinite induction, which states that if 623 Properties of infinite things. We request a transfinite induction, which states that if
602 some properties are satisfied below all possible ordinals, the properties are true on all 624 some properties are satisfied below all possible ordinals, the properties are true on all
603 ordinals. 625 ordinals.
604 <p> 626 <p>
605 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals 627 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
623 → ∀ (x : ord) → ψ x 645 → ∀ (x : ord) → ψ x
624 646
625 </pre> 647 </pre>
626 648
627 <hr/> 649 <hr/>
628 <h2><a name="content025">Concrete Ordinals</a></h2> 650 <h2><a name="content026">Concrete Ordinals</a></h2>
629 651
630 <p> 652 <p>
631 We can define a list like structure with level, which is a kind of two dimensional infinite array. 653 We can define a list like structure with level, which is a kind of two dimensional infinite array.
632 <p> 654 <p>
633 655
656 Osuc 0 (Φ 0) d&lt; Φ 1 678 Osuc 0 (Φ 0) d&lt; Φ 1
657 679
658 </pre> 680 </pre>
659 681
660 <hr/> 682 <hr/>
661 <h2><a name="content026">Model of Ordinals</a></h2> 683 <h2><a name="content027">Model of Ordinals</a></h2>
662 684
663 <p> 685 <p>
664 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. 686 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
665 <p> 687 <p>
666 So our Ordinals has a mode. This means axiom of Ordinals are consistent. 688 So our Ordinals has a mode. This means axiom of Ordinals are consistent.
667 <p> 689 <p>
668 690
669 <hr/> 691 <hr/>
670 <h2><a name="content027">Debugging axioms using Model</a></h2> 692 <h2><a name="content028">Debugging axioms using Model</a></h2>
671 Whether axiom is correct or not can be checked by a validity on a mode. 693 Whether axiom is correct or not can be checked by a validity on a mode.
672 <p> 694 <p>
673 If not, we may fix the axioms or the model, such as the definitions of the order. 695 If not, we may fix the axioms or the model, such as the definitions of the order.
674 <p> 696 <p>
675 We can also ask whether the inputs exist. 697 We can also ask whether the inputs exist.
676 <p> 698 <p>
677 699
678 <hr/> 700 <hr/>
679 <h2><a name="content028">Countable Ordinals can contains uncountable set?</a></h2> 701 <h2><a name="content029">Countable Ordinals can contains uncountable set?</a></h2>
680 Yes, the ordinals contains any level of infinite Set in the axioms. 702 Yes, the ordinals contains any level of infinite Set in the axioms.
681 <p> 703 <p>
682 If we handle real-number in the model, only countable number of real-number is used. 704 If we handle real-number in the model, only countable number of real-number is used.
683 <p> 705 <p>
684 706
692 <p> 714 <p>
693 We don't show the definition of cardinal number here. 715 We don't show the definition of cardinal number here.
694 <p> 716 <p>
695 717
696 <hr/> 718 <hr/>
697 <h2><a name="content029">What is Set</a></h2> 719 <h2><a name="content030">What is Set</a></h2>
698 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). 720 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
699 <p> 721 <p>
700 From naive point view, a set i a list, but in Agda, elements have all the same type. 722 From naive point view, a set i a list, but in Agda, elements have all the same type.
701 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. 723 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
702 <p> 724 <p>
703 Finite set may be written in finite series of ∨, but ... 725 Finite set may be written in finite series of ∨, but ...
704 <p> 726 <p>
705 727
706 <hr/> 728 <hr/>
707 <h2><a name="content030">We don't ask the contents of Set. It can be anything.</a></h2> 729 <h2><a name="content031">We don't ask the contents of Set. It can be anything.</a></h2>
708 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, 730 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
709 and all of them, and again we repeat this. 731 and all of them, and again we repeat this.
710 <p> 732 <p>
711 733
712 <pre> 734 <pre>
720 <p> 742 <p>
721 But in our case, we have no ZF theory, so we are going to use Ordinals. 743 But in our case, we have no ZF theory, so we are going to use Ordinals.
722 <p> 744 <p>
723 745
724 <hr/> 746 <hr/>
725 <h2><a name="content031">Ordinal Definable Set</a></h2> 747 <h2><a name="content032">Ordinal Definable Set</a></h2>
726 We can define a sbuset of Ordinals using predicates. What is a subset? 748 We can define a sbuset of Ordinals using predicates. What is a subset?
727 <p> 749 <p>
728 750
729 <pre> 751 <pre>
730 a predicate has an Ordinal argument 752 a predicate has an Ordinal argument
749 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory, 771 means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
750 but we don't care about it. 772 but we don't care about it.
751 <p> 773 <p>
752 774
753 <hr/> 775 <hr/>
754 <h2><a name="content032">∋ in OD</a></h2> 776 <h2><a name="content033">∋ in OD</a></h2>
755 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping 777 OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
756 <p> 778 <p>
757 779
758 <pre> 780 <pre>
759 od→ord : OD → Ordinal 781 od→ord : OD → Ordinal
776 A x = def A ( od→ord x ) = ψ (od→ord x) 798 A x = def A ( od→ord x ) = ψ (od→ord x)
777 799
778 </pre> 800 </pre>
779 801
780 <hr/> 802 <hr/>
781 <h2><a name="content033">1 to 1 mapping between an OD and an Ordinal</a></h2> 803 <h2><a name="content034">1 to 1 mapping between an OD and an Ordinal</a></h2>
782 804
783 <p> 805 <p>
784 806
785 <pre> 807 <pre>
786 od→ord : OD → Ordinal 808 od→ord : OD → Ordinal
798 <img src="fig/ord-od-mapping.svg"> 820 <img src="fig/ord-od-mapping.svg">
799 821
800 <p> 822 <p>
801 823
802 <hr/> 824 <hr/>
803 <h2><a name="content034">Order preserving in the mapping of OD and Ordinal</a></h2> 825 <h2><a name="content035">Order preserving in the mapping of OD and Ordinal</a></h2>
804 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). 826 Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
805 <p> 827 <p>
806 828
807 <pre> 829 <pre>
808 def y ( od→ord x ) 830 def y ( od→ord x )
831 <img src="fig/ODandOrdinals.svg"> 853 <img src="fig/ODandOrdinals.svg">
832 854
833 <p> 855 <p>
834 856
835 <hr/> 857 <hr/>
836 <h2><a name="content035">ISO</a></h2> 858 <h2><a name="content036">ISO</a></h2>
837 It also requires isomorphisms, 859 It also requires isomorphisms,
838 <p> 860 <p>
839 861
840 <pre> 862 <pre>
841 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x 863 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
842 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 864 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
843 865
844 </pre> 866 </pre>
845 867
846 <hr/> 868 <hr/>
847 <h2><a name="content036">Various Sets</a></h2> 869 <h2><a name="content037">Various Sets</a></h2>
848 870
849 <p> 871 <p>
850 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. 872 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
851 <p> 873 <p>
852 874
858 Agda Set / Type / it also has a level 880 Agda Set / Type / it also has a level
859 881
860 </pre> 882 </pre>
861 883
862 <hr/> 884 <hr/>
863 <h2><a name="content037">Fixes on ZF to intuitionistic logic</a></h2> 885 <h2><a name="content038">Fixes on ZF to intuitionistic logic</a></h2>
864 886
865 <p> 887 <p>
866 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define 888 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
867 ZF axioms in Agda. 889 ZF axioms in Agda.
868 <p> 890 <p>
876 <a href="fig/zf-record.html"> 898 <a href="fig/zf-record.html">
877 ZFのrecord </a> 899 ZFのrecord </a>
878 <p> 900 <p>
879 901
880 <hr/> 902 <hr/>
881 <h2><a name="content038">Pure logical axioms</a></h2> 903 <h2><a name="content039">Pure logical axioms</a></h2>
882 904
883 <pre> 905 <pre>
884 empty, pair, select, ε-inductioninfinity 906 empty, pair, select, ε-induction??infinity
885 907
886 </pre> 908 </pre>
887 These are logical relations among OD. 909 These are logical relations among OD.
888 <p> 910 <p>
889 911
911 </pre> 933 </pre>
912 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. 934 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
913 <p> 935 <p>
914 936
915 <hr/> 937 <hr/>
916 <h2><a name="content039">Axiom of Pair</a></h2> 938 <h2><a name="content040">Axiom of Pair</a></h2>
917 In the Tanaka's book, axiom of pair is as follows. 939 In the Tanaka's book, axiom of pair is as follows.
918 <p> 940 <p>
919 941
920 <pre> 942 <pre>
921 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) 943 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
938 </pre> 960 </pre>
939 This is already written in Agda, so we use these as axioms. All inputs have ∀. 961 This is already written in Agda, so we use these as axioms. All inputs have ∀.
940 <p> 962 <p>
941 963
942 <hr/> 964 <hr/>
943 <h2><a name="content040">pair in OD</a></h2> 965 <h2><a name="content041">pair in OD</a></h2>
944 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. 966 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
945 <p> 967 <p>
946 968
947 <pre> 969 <pre>
948 _,_ : OD → OD → OD 970 _,_ : OD → OD → OD
951 </pre> 973 </pre>
952 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. 974 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
953 <p> 975 <p>
954 976
955 <hr/> 977 <hr/>
956 <h2><a name="content041">Validity of Axiom of Pair</a></h2> 978 <h2><a name="content042">Validity of Axiom of Pair</a></h2>
957 Assuming ZFSet is OD, we are going to prove pair→ . 979 Assuming ZFSet is OD, we are going to prove pair→ .
958 <p> 980 <p>
959 981
960 <pre> 982 <pre>
961 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) 983 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
992 <p> 1014 <p>
993 But we haven't defined == yet. 1015 But we haven't defined == yet.
994 <p> 1016 <p>
995 1017
996 <hr/> 1018 <hr/>
997 <h2><a name="content042">Equality of OD and Axiom of Extensionality </a></h2> 1019 <h2><a name="content043">Equality of OD and Axiom of Extensionality </a></h2>
998 OD is defined by a predicates, if we compares normal form of the predicates, even if 1020 OD is defined by a predicates, if we compares normal form of the predicates, even if
999 it contains the same elements, it may be different, which is no good as an equality of 1021 it contains the same elements, it may be different, which is no good as an equality of
1000 Sets. 1022 Sets.
1001 <p> 1023 <p>
1002 Axiom of Extensionality requires sets having the same elements are handled in the same way 1024 Axiom of Extensionality requires sets having the same elements are handled in the same way
1054 def-iso refl t = t 1076 def-iso refl t = t
1055 1077
1056 </pre> 1078 </pre>
1057 1079
1058 <hr/> 1080 <hr/>
1059 <h2><a name="content043">Validity of Axiom of Extensionality</a></h2> 1081 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2>
1060 1082
1061 <p> 1083 <p>
1062 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes 1084 If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes
1063 <p> 1085 <p>
1064 1086
1077 </pre> 1099 </pre>
1078 This assumption means we may have an equivalence set on any predicates. 1100 This assumption means we may have an equivalence set on any predicates.
1079 <p> 1101 <p>
1080 1102
1081 <hr/> 1103 <hr/>
1082 <h2><a name="content044">Non constructive assumptions so far</a></h2> 1104 <h2><a name="content045">Non constructive assumptions so far</a></h2>
1083 We have correspondence between OD and Ordinals and one directional order preserving. 1105 We have correspondence between OD and Ordinals and one directional order preserving.
1084 <p> 1106 <p>
1085 We also have equality assumption. 1107 We also have equality assumption.
1086 <p> 1108 <p>
1087 1109
1094 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 1116 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
1095 1117
1096 </pre> 1118 </pre>
1097 1119
1098 <hr/> 1120 <hr/>
1099 <h2><a name="content045">Axiom which have negation form</a></h2> 1121 <h2><a name="content046">Axiom which have negation form</a></h2>
1100 1122
1101 <p> 1123 <p>
1102 1124
1103 <pre> 1125 <pre>
1104 Union, Selection 1126 Union, Selection
1118 </pre> 1140 </pre>
1119 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. 1141 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
1120 <p> 1142 <p>
1121 1143
1122 <hr/> 1144 <hr/>
1123 <h2><a name="content046">Union </a></h2> 1145 <h2><a name="content047">Union </a></h2>
1124 The original form of the Axiom of Union is 1146 The original form of the Axiom of Union is
1125 <p> 1147 <p>
1126 1148
1127 <pre> 1149 <pre>
1128 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) 1150 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
1170 </pre> 1192 </pre>
1171 which checks existence using contra-position. 1193 which checks existence using contra-position.
1172 <p> 1194 <p>
1173 1195
1174 <hr/> 1196 <hr/>
1175 <h2><a name="content047">Axiom of replacement</a></h2> 1197 <h2><a name="content048">Axiom of replacement</a></h2>
1176 We can replace the elements of a set by a function and it becomes a set. From the book, 1198 We can replace the elements of a set by a function and it becomes a set. From the book,
1177 <p> 1199 <p>
1178 1200
1179 <pre> 1201 <pre>
1180 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 1202 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
1214 </pre> 1236 </pre>
1215 We omit the proof of the validity, but it is rather straight forward. 1237 We omit the proof of the validity, but it is rather straight forward.
1216 <p> 1238 <p>
1217 1239
1218 <hr/> 1240 <hr/>
1219 <h2><a name="content048">Validity of Power Set Axiom</a></h2> 1241 <h2><a name="content049">Validity of Power Set Axiom</a></h2>
1220 The original Power Set Axiom is this. 1242 The original Power Set Axiom is this.
1221 <p> 1243 <p>
1222 1244
1223 <pre> 1245 <pre>
1224 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 1246 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
1305 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 1327 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1306 1328
1307 </pre> 1329 </pre>
1308 1330
1309 <hr/> 1331 <hr/>
1310 <h2><a name="content049">Axiom of regularity, Axiom of choice, ε-induction</a></h2> 1332 <h2><a name="content050">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
1311 1333
1312 <p> 1334 <p>
1313 Axiom of regularity requires non self intersectable elements (which is called minimum), if we 1335 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
1314 replace it by a function, it becomes a choice function. It makes axiom of choice valid. 1336 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
1315 <p> 1337 <p>
1352 </pre> 1374 </pre>
1353 It does not requires ∅ ∉ X . 1375 It does not requires ∅ ∉ X .
1354 <p> 1376 <p>
1355 1377
1356 <hr/> 1378 <hr/>
1357 <h2><a name="content050">Axiom of choice and Law of Excluded Middle</a></h2> 1379 <h2><a name="content051">Axiom of choice and Law of Excluded Middle</a></h2>
1358 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, 1380 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
1359 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, 1381 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
1360 but it requires law of the exclude middle. 1382 but it requires law of the exclude middle.
1361 <p> 1383 <p>
1362 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can 1384 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
1372 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice 1394 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
1373 and Law of Excluded Middle is equivalent in our mode. 1395 and Law of Excluded Middle is equivalent in our mode.
1374 <p> 1396 <p>
1375 1397
1376 <hr/> 1398 <hr/>
1377 <h2><a name="content051">Relation-ship among ZF axiom</a></h2> 1399 <h2><a name="content052">Relation-ship among ZF axiom</a></h2>
1378 <img src="fig/axiom-dependency.svg"> 1400 <img src="fig/axiom-dependency.svg">
1379 1401
1380 <p> 1402 <p>
1381 1403
1382 <hr/> 1404 <hr/>
1383 <h2><a name="content052">Non constructive assumption in our model</a></h2> 1405 <h2><a name="content053">Non constructive assumption in our model</a></h2>
1384 mapping between OD and Ordinals 1406 mapping between OD and Ordinals
1385 <p> 1407 <p>
1386 1408
1387 <pre> 1409 <pre>
1388 od→ord : OD → Ordinal 1410 od→ord : OD → Ordinal
1416 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) 1438 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
1417 1439
1418 </pre> 1440 </pre>
1419 1441
1420 <hr/> 1442 <hr/>
1421 <h2><a name="content053">So it this correct?</a></h2> 1443 <h2><a name="content054">So it this correct?</a></h2>
1422 1444
1423 <p> 1445 <p>
1424 Our axiom are syntactically the same in the text book, but negations are slightly different. 1446 Our axiom are syntactically the same in the text book, but negations are slightly different.
1425 <p> 1447 <p>
1426 If we assumes excluded middle, these are exactly same. 1448 If we assumes excluded middle, these are exactly same.
1436 <p> 1458 <p>
1437 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. 1459 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
1438 <p> 1460 <p>
1439 1461
1440 <hr/> 1462 <hr/>
1441 <h2><a name="content054">How to use Agda Set Theory</a></h2> 1463 <h2><a name="content055">How to use Agda Set Theory</a></h2>
1442 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be 1464 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
1443 postulated or assuming law of excluded middle. 1465 postulated or assuming law of excluded middle.
1444 <p> 1466 <p>
1445 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check 1467 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
1446 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. 1468 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
1447 <p> 1469 <p>
1448 ZF record itself is not necessary, for example, topology theory without ZF can be possible. 1470 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
1449 <p> 1471 <p>
1450 1472
1451 <hr/> 1473 <hr/>
1452 <h2><a name="content055">Topos and Set Theory</a></h2> 1474 <h2><a name="content056">Topos and Set Theory</a></h2>
1453 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a 1475 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
1454 sub-object classifier. 1476 sub-object classifier.
1455 <p> 1477 <p>
1456 Topos itself is model of intuitionistic logic. 1478 Topos itself is model of intuitionistic logic.
1457 <p> 1479 <p>
1465 <p> 1487 <p>
1466 Our Agda model is a proof theoretic version of it. 1488 Our Agda model is a proof theoretic version of it.
1467 <p> 1489 <p>
1468 1490
1469 <hr/> 1491 <hr/>
1470 <h2><a name="content056">Cardinal number and Continuum hypothesis</a></h2> 1492 <h2><a name="content057">Cardinal number and Continuum hypothesis</a></h2>
1471 Axiom of choice is required to define cardinal number 1493 Axiom of choice is required to define cardinal number
1472 <p> 1494 <p>
1473 definition of cardinal number is not yet done 1495 definition of cardinal number is not yet done
1474 <p> 1496 <p>
1475 definition of filter is not yet done 1497 definition of filter is not yet done
1483 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) 1505 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
1484 1506
1485 </pre> 1507 </pre>
1486 1508
1487 <hr/> 1509 <hr/>
1488 <h2><a name="content057">Filter</a></h2> 1510 <h2><a name="content058">Filter</a></h2>
1489 1511
1490 <p> 1512 <p>
1491 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number 1513 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
1492 is depends on axiom of choice. 1514 is depends on axiom of choice.
1493 <p> 1515 <p>
1506 <p> 1528 <p>
1507 This may be simpler than classical forcing theory ( not yet done). 1529 This may be simpler than classical forcing theory ( not yet done).
1508 <p> 1530 <p>
1509 1531
1510 <hr/> 1532 <hr/>
1511 <h2><a name="content058">Programming Mathematics</a></h2> 1533 <h2><a name="content059">Programming Mathematics</a></h2>
1512 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical 1534 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
1513 structure are 1535 structure are
1514 <p> 1536 <p>
1515 1537
1516 <pre> 1538 <pre>
1531 </pre> 1553 </pre>
1532 are proved in Agda. 1554 are proved in Agda.
1533 <p> 1555 <p>
1534 1556
1535 <hr/> 1557 <hr/>
1536 <h2><a name="content059">link</a></h2> 1558 <h2><a name="content060">link</a></h2>
1537 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> 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>
1538 <p> 1560 <p>
1539 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 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
1540 </a> 1562 </a>
1541 <p> 1563 <p>
1551 </a> 1573 </a>
1552 <p> 1574 <p>
1553 </div> 1575 </div>
1554 <ol class="side" id="menu"> 1576 <ol class="side" id="menu">
1555 Constructing ZF Set Theory in Agda 1577 Constructing ZF Set Theory in Agda
1556 <li><a href="#content000"> Programming Mathematics</a> 1578 <li><a href="#content000"> ZF in Agda</a>
1557 <li><a href="#content001"> Target</a> 1579 <li><a href="#content001"> Programming Mathematics</a>
1558 <li><a href="#content002"> Why Set Theory</a> 1580 <li><a href="#content002"> Target</a>
1559 <li><a href="#content003"> Agda and Intuitionistic Logic </a> 1581 <li><a href="#content003"> Why Set Theory</a>
1560 <li><a href="#content004"> Introduction of Agda </a> 1582 <li><a href="#content004"> Agda and Intuitionistic Logic </a>
1561 <li><a href="#content005"> data ( Sum type )</a> 1583 <li><a href="#content005"> Introduction of Agda </a>
1562 <li><a href="#content006"> A → B means "A implies B"</a> 1584 <li><a href="#content006"> data ( Sum type )</a>
1563 <li><a href="#content007"> introduction と elimination</a> 1585 <li><a href="#content007"> A → B means "A implies B"</a>
1564 <li><a href="#content008"> To prove A → B </a> 1586 <li><a href="#content008"> introduction と elimination</a>
1565 <li><a href="#content009"> A ∧ B</a> 1587 <li><a href="#content009"> To prove A → B </a>
1566 <li><a href="#content010"> record</a> 1588 <li><a href="#content010"> A ∧ B</a>
1567 <li><a href="#content011"> Mathematical structure</a> 1589 <li><a href="#content011"> record</a>
1568 <li><a href="#content012"> A Model and a theory</a> 1590 <li><a href="#content012"> Mathematical structure</a>
1569 <li><a href="#content013"> postulate と module</a> 1591 <li><a href="#content013"> A Model and a theory</a>
1570 <li><a href="#content014"> A ∨ B</a> 1592 <li><a href="#content014"> postulate と module</a>
1571 <li><a href="#content015"> Negation</a> 1593 <li><a href="#content015"> A ∨ B</a>
1572 <li><a href="#content016"> Equality </a> 1594 <li><a href="#content016"> Negation</a>
1573 <li><a href="#content017"> Equivalence relation</a> 1595 <li><a href="#content017"> Equality </a>
1574 <li><a href="#content018"> Ordering</a> 1596 <li><a href="#content018"> Equivalence relation</a>
1575 <li><a href="#content019"> Quantifier</a> 1597 <li><a href="#content019"> Ordering</a>
1576 <li><a href="#content020"> Can we do math in this way?</a> 1598 <li><a href="#content020"> Quantifier</a>
1577 <li><a href="#content021"> Things which Agda cannot prove</a> 1599 <li><a href="#content021"> Can we do math in this way?</a>
1578 <li><a href="#content022"> Classical story of ZF Set Theory</a> 1600 <li><a href="#content022"> Things which Agda cannot prove</a>
1579 <li><a href="#content023"> Ordinals</a> 1601 <li><a href="#content023"> Classical story of ZF Set Theory</a>
1580 <li><a href="#content024"> Axiom of Ordinals</a> 1602 <li><a href="#content024"> Ordinals</a>
1581 <li><a href="#content025"> Concrete Ordinals</a> 1603 <li><a href="#content025"> Axiom of Ordinals</a>
1582 <li><a href="#content026"> Model of Ordinals</a> 1604 <li><a href="#content026"> Concrete Ordinals</a>
1583 <li><a href="#content027"> Debugging axioms using Model</a> 1605 <li><a href="#content027"> Model of Ordinals</a>
1584 <li><a href="#content028"> Countable Ordinals can contains uncountable set?</a> 1606 <li><a href="#content028"> Debugging axioms using Model</a>
1585 <li><a href="#content029"> What is Set</a> 1607 <li><a href="#content029"> Countable Ordinals can contains uncountable set?</a>
1586 <li><a href="#content030"> We don't ask the contents of Set. It can be anything.</a> 1608 <li><a href="#content030"> What is Set</a>
1587 <li><a href="#content031"> Ordinal Definable Set</a> 1609 <li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a>
1588 <li><a href="#content032"> ∋ in OD</a> 1610 <li><a href="#content032"> Ordinal Definable Set</a>
1589 <li><a href="#content033"> 1 to 1 mapping between an OD and an Ordinal</a> 1611 <li><a href="#content033"> ∋ in OD</a>
1590 <li><a href="#content034"> Order preserving in the mapping of OD and Ordinal</a> 1612 <li><a href="#content034"> 1 to 1 mapping between an OD and an Ordinal</a>
1591 <li><a href="#content035"> ISO</a> 1613 <li><a href="#content035"> Order preserving in the mapping of OD and Ordinal</a>
1592 <li><a href="#content036"> Various Sets</a> 1614 <li><a href="#content036"> ISO</a>
1593 <li><a href="#content037"> Fixes on ZF to intuitionistic logic</a> 1615 <li><a href="#content037"> Various Sets</a>
1594 <li><a href="#content038"> Pure logical axioms</a> 1616 <li><a href="#content038"> Fixes on ZF to intuitionistic logic</a>
1595 <li><a href="#content039"> Axiom of Pair</a> 1617 <li><a href="#content039"> Pure logical axioms</a>
1596 <li><a href="#content040"> pair in OD</a> 1618 <li><a href="#content040"> Axiom of Pair</a>
1597 <li><a href="#content041"> Validity of Axiom of Pair</a> 1619 <li><a href="#content041"> pair in OD</a>
1598 <li><a href="#content042"> Equality of OD and Axiom of Extensionality </a> 1620 <li><a href="#content042"> Validity of Axiom of Pair</a>
1599 <li><a href="#content043"> Validity of Axiom of Extensionality</a> 1621 <li><a href="#content043"> Equality of OD and Axiom of Extensionality </a>
1600 <li><a href="#content044"> Non constructive assumptions so far</a> 1622 <li><a href="#content044"> Validity of Axiom of Extensionality</a>
1601 <li><a href="#content045"> Axiom which have negation form</a> 1623 <li><a href="#content045"> Non constructive assumptions so far</a>
1602 <li><a href="#content046"> Union </a> 1624 <li><a href="#content046"> Axiom which have negation form</a>
1603 <li><a href="#content047"> Axiom of replacement</a> 1625 <li><a href="#content047"> Union </a>
1604 <li><a href="#content048"> Validity of Power Set Axiom</a> 1626 <li><a href="#content048"> Axiom of replacement</a>
1605 <li><a href="#content049"> Axiom of regularity, Axiom of choice, ε-induction</a> 1627 <li><a href="#content049"> Validity of Power Set Axiom</a>
1606 <li><a href="#content050"> Axiom of choice and Law of Excluded Middle</a> 1628 <li><a href="#content050"> Axiom of regularity, Axiom of choice, ε-induction</a>
1607 <li><a href="#content051"> Relation-ship among ZF axiom</a> 1629 <li><a href="#content051"> Axiom of choice and Law of Excluded Middle</a>
1608 <li><a href="#content052"> Non constructive assumption in our model</a> 1630 <li><a href="#content052"> Relation-ship among ZF axiom</a>
1609 <li><a href="#content053"> So it this correct?</a> 1631 <li><a href="#content053"> Non constructive assumption in our model</a>
1610 <li><a href="#content054"> How to use Agda Set Theory</a> 1632 <li><a href="#content054"> So it this correct?</a>
1611 <li><a href="#content055"> Topos and Set Theory</a> 1633 <li><a href="#content055"> How to use Agda Set Theory</a>
1612 <li><a href="#content056"> Cardinal number and Continuum hypothesis</a> 1634 <li><a href="#content056"> Topos and Set Theory</a>
1613 <li><a href="#content057"> Filter</a> 1635 <li><a href="#content057"> Cardinal number and Continuum hypothesis</a>
1614 <li><a href="#content058"> Programming Mathematics</a> 1636 <li><a href="#content058"> Filter</a>
1615 <li><a href="#content059"> link</a> 1637 <li><a href="#content059"> Programming Mathematics</a>
1638 <li><a href="#content060"> link</a>
1616 </ol> 1639 </ol>
1617 1640
1618 <hr/> Shinji KONO / Sat Jan 11 20:04:01 2020 1641 <hr/> Shinji KONO / Sat May 9 16:41:10 2020
1619 </body></html> 1642 </body></html>