Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison zf-in-agda.html @ 359:5e22b23ee3fd
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 14 Jul 2020 15:02:59 +0900 |
parents | bca043423554 |
children | 4cbcf71b09c4 |
comparison
equal
deleted
inserted
replaced
358:811152bf2f47 | 359:5e22b23ee3fd |
---|---|
339 <p> | 339 <p> |
340 Fields of Ordinal is existential objects in the mathematical structure. | 340 Fields of Ordinal is existential objects in the mathematical structure. |
341 <p> | 341 <p> |
342 | 342 |
343 <hr/> | 343 <hr/> |
344 <h2><a name="content013"> A Model and a theory</a></h2> | 344 <h2><a name="content013"> Limit Ordinal</a></h2> |
345 If an ordinal is not a succesor of other, it is called limit ordinal. We need predicate to decide it. | |
346 <p> | |
347 | |
348 <pre> | |
349 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) | |
350 | |
351 </pre> | |
352 An ordinal may have an imeditate limit ordinal, we call it next x. Axiom of nrext is this. | |
353 <p> | |
354 | |
355 <pre> | |
356 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) | |
357 (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where | |
358 field | |
359 x<nx : { y : ord } → (y o< next y ) | |
360 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y | |
361 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z)) | |
362 | |
363 </pre> | |
364 We show some intresting lemma. | |
365 <p> | |
366 | |
367 <pre> | |
368 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z | |
369 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y | |
370 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) | |
371 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) | |
372 | |
373 </pre> | |
374 These are proved from the axiom. Our countable ordinal satisfies these. | |
375 <p> | |
376 | |
377 <hr/> | |
378 <h2><a name="content014"> A Model and a theory</a></h2> | |
345 Agda record is a type, so we can write it in the argument, but is it really exists? | 379 Agda record is a type, so we can write it in the argument, but is it really exists? |
346 <p> | 380 <p> |
347 If we have a value of the record, it simply exists, that is, we need to create all the existence | 381 If we have a value of the record, it simply exists, that is, we need to create all the existence |
348 in the record satisfies all the axioms (= field of IsOrdinal) should be valid. | 382 in the record satisfies all the axioms (= field of IsOrdinal) should be valid. |
349 <p> | 383 <p> |
356 We call the value of the record as a model. If mathematical structure has a | 390 We call the value of the record as a model. If mathematical structure has a |
357 model, it exists. Pretty Obvious. | 391 model, it exists. Pretty Obvious. |
358 <p> | 392 <p> |
359 | 393 |
360 <hr/> | 394 <hr/> |
361 <h2><a name="content014"> postulate と module</a></h2> | 395 <h2><a name="content015"> postulate と module</a></h2> |
362 Agda proofs are separated by modules, which are large records. | 396 Agda proofs are separated by modules, which are large records. |
363 <p> | 397 <p> |
364 postulates are assumptions. We can assume a type without proofs. | 398 postulates are assumptions. We can assume a type without proofs. |
365 <p> | 399 <p> |
366 | 400 |
380 postulate can be inconsistent, which result everything has a proof. Actualy this assumption | 414 postulate can be inconsistent, which result everything has a proof. Actualy this assumption |
381 doesnot work for Ordinals, we discuss this later. | 415 doesnot work for Ordinals, we discuss this later. |
382 <p> | 416 <p> |
383 | 417 |
384 <hr/> | 418 <hr/> |
385 <h2><a name="content015"> A ∨ B</a></h2> | 419 <h2><a name="content016"> A ∨ B</a></h2> |
386 | 420 |
387 <pre> | 421 <pre> |
388 data _∨_ (A B : Set) : Set where | 422 data _∨_ (A B : Set) : Set where |
389 case1 : A → A ∨ B | 423 case1 : A → A ∨ B |
390 case2 : B → A ∨ B | 424 case2 : B → A ∨ B |
409 </pre> | 443 </pre> |
410 Proof schema of ∨ is omit due to the complexity. | 444 Proof schema of ∨ is omit due to the complexity. |
411 <p> | 445 <p> |
412 | 446 |
413 <hr/> | 447 <hr/> |
414 <h2><a name="content016"> Negation</a></h2> | 448 <h2><a name="content017"> Negation</a></h2> |
415 | 449 |
416 <pre> | 450 <pre> |
417 ⊥ | 451 ⊥ |
418 ------------- ⊥-elim | 452 ------------- ⊥-elim |
419 A | 453 A |
445 ¬ A = A → ⊥ | 479 ¬ A = A → ⊥ |
446 | 480 |
447 </pre> | 481 </pre> |
448 | 482 |
449 <hr/> | 483 <hr/> |
450 <h2><a name="content017">Equality </a></h2> | 484 <h2><a name="content018">Equality </a></h2> |
451 | 485 |
452 <p> | 486 <p> |
453 All the value in Agda are terms. If we have the same normalized form, two terms are equal. | 487 All the value in Agda are terms. If we have the same normalized form, two terms are equal. |
454 If we have variables in the terms, we will perform an unification. unifiable terms are equal. | 488 If we have variables in the terms, we will perform an unification. unifiable terms are equal. |
455 We don't go further on the unification. | 489 We don't go further on the unification. |
479 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y | 513 ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y |
480 | 514 |
481 </pre> | 515 </pre> |
482 | 516 |
483 <hr/> | 517 <hr/> |
484 <h2><a name="content018">Equivalence relation</a></h2> | 518 <h2><a name="content019">Equivalence relation</a></h2> |
485 | 519 |
486 <p> | 520 <p> |
487 | 521 |
488 <pre> | 522 <pre> |
489 refl' : {A : Set} {x : A } → x ≡ x | 523 refl' : {A : Set} {x : A } → x ≡ x |
496 cong = ? | 530 cong = ? |
497 | 531 |
498 </pre> | 532 </pre> |
499 | 533 |
500 <hr/> | 534 <hr/> |
501 <h2><a name="content019">Ordering</a></h2> | 535 <h2><a name="content020">Ordering</a></h2> |
502 | 536 |
503 <p> | 537 <p> |
504 Relation is a predicate on two value which has a same type. | 538 Relation is a predicate on two value which has a same type. |
505 <p> | 539 <p> |
506 | 540 |
517 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n | 551 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n |
518 | 552 |
519 </pre> | 553 </pre> |
520 | 554 |
521 <hr/> | 555 <hr/> |
522 <h2><a name="content020">Quantifier</a></h2> | 556 <h2><a name="content021">Quantifier</a></h2> |
523 | 557 |
524 <p> | 558 <p> |
525 Handling quantifier in an intuitionistic logic requires special cares. | 559 Handling quantifier in an intuitionistic logic requires special cares. |
526 <p> | 560 <p> |
527 In the input of a function, there are no restriction on it, that is, it has | 561 In the input of a function, there are no restriction on it, that is, it has |
541 If we use a function which can be defined globally which has stronger meaning the | 575 If we use a function which can be defined globally which has stronger meaning the |
542 usage of ∃ x in a logical expression. | 576 usage of ∃ x in a logical expression. |
543 <p> | 577 <p> |
544 | 578 |
545 <hr/> | 579 <hr/> |
546 <h2><a name="content021">Can we do math in this way?</a></h2> | 580 <h2><a name="content022">Can we do math in this way?</a></h2> |
547 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). | 581 Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). |
548 <p> | 582 <p> |
549 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). | 583 In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). |
550 <p> | 584 <p> |
551 | 585 |
554 program inferences as if we have proofs in variables | 588 program inferences as if we have proofs in variables |
555 | 589 |
556 </pre> | 590 </pre> |
557 | 591 |
558 <hr/> | 592 <hr/> |
559 <h2><a name="content022">Things which Agda cannot prove</a></h2> | 593 <h2><a name="content023">Things which Agda cannot prove</a></h2> |
560 | 594 |
561 <p> | 595 <p> |
562 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which | 596 The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which |
563 leads uniqueness of a functor in Category Theory. | 597 leads uniqueness of a functor in Category Theory. |
564 <p> | 598 <p> |
584 | 618 |
585 | 619 |
586 </pre> | 620 </pre> |
587 | 621 |
588 <hr/> | 622 <hr/> |
589 <h2><a name="content023">Classical story of ZF Set Theory</a></h2> | 623 <h2><a name="content024">Classical story of ZF Set Theory</a></h2> |
590 | 624 |
591 <p> | 625 <p> |
592 <a name="set-theory"> | 626 <a name="set-theory"> |
593 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads | 627 Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads |
594 a relative consistency proof of the Set Theory. | 628 a relative consistency proof of the Set Theory. |
601 <img src="fig/set-theory.svg"> | 635 <img src="fig/set-theory.svg"> |
602 | 636 |
603 <p> | 637 <p> |
604 | 638 |
605 <hr/> | 639 <hr/> |
606 <h2><a name="content024">Ordinals</a></h2> | 640 <h2><a name="content025">Ordinals</a></h2> |
607 Ordinals are our intuition of infinite things, which has ∅ and orders on the things. | 641 Ordinals are our intuition of infinite things, which has ∅ and orders on the things. |
608 It also has a successor osuc. | 642 It also has a successor osuc. |
609 <p> | 643 <p> |
610 | 644 |
611 <pre> | 645 <pre> |
621 It is different from natural numbers in way. The order of Ordinals is not defined in terms | 655 It is different from natural numbers in way. The order of Ordinals is not defined in terms |
622 of successor. It is given from outside, which make it possible to have higher order infinity. | 656 of successor. It is given from outside, which make it possible to have higher order infinity. |
623 <p> | 657 <p> |
624 | 658 |
625 <hr/> | 659 <hr/> |
626 <h2><a name="content025">Axiom of Ordinals</a></h2> | 660 <h2><a name="content026">Axiom of Ordinals</a></h2> |
627 Properties of infinite things. We request a transfinite induction, which states that if | 661 Properties of infinite things. We request a transfinite induction, which states that if |
628 some properties are satisfied below all possible ordinals, the properties are true on all | 662 some properties are satisfied below all possible ordinals, the properties are true on all |
629 ordinals. | 663 ordinals. |
630 <p> | 664 <p> |
631 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals | 665 Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals |
649 → ∀ (x : ord) → ψ x | 683 → ∀ (x : ord) → ψ x |
650 | 684 |
651 </pre> | 685 </pre> |
652 | 686 |
653 <hr/> | 687 <hr/> |
654 <h2><a name="content026">Concrete Ordinals or Countable Ordinals</a></h2> | 688 <h2><a name="content027">Concrete Ordinals or Countable Ordinals</a></h2> |
655 | 689 |
656 <p> | 690 <p> |
657 We can define a list like structure with level, which is a kind of two dimensional infinite array. | 691 We can define a list like structure with level, which is a kind of two dimensional infinite array. |
658 <p> | 692 <p> |
659 | 693 |
682 Osuc 0 (Φ 0) d< Φ 1 | 716 Osuc 0 (Φ 0) d< Φ 1 |
683 | 717 |
684 </pre> | 718 </pre> |
685 | 719 |
686 <hr/> | 720 <hr/> |
687 <h2><a name="content027">Model of Ordinals</a></h2> | 721 <h2><a name="content028">Model of Ordinals</a></h2> |
688 | 722 |
689 <p> | 723 <p> |
690 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. | 724 It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. |
691 <p> | 725 <p> |
692 So our Ordinals has a mode. This means axiom of Ordinals are consistent. | 726 So our Ordinals has a mode. This means axiom of Ordinals are consistent. |
693 <p> | 727 <p> |
694 | 728 |
695 <hr/> | 729 <hr/> |
696 <h2><a name="content028">Debugging axioms using Model</a></h2> | 730 <h2><a name="content029">Debugging axioms using Model</a></h2> |
697 Whether axiom is correct or not can be checked by a validity on a mode. | 731 Whether axiom is correct or not can be checked by a validity on a mode. |
698 <p> | 732 <p> |
699 If not, we may fix the axioms or the model, such as the definitions of the order. | 733 If not, we may fix the axioms or the model, such as the definitions of the order. |
700 <p> | 734 <p> |
701 We can also ask whether the inputs exist. | 735 We can also ask whether the inputs exist. |
702 <p> | 736 <p> |
703 | 737 |
704 <hr/> | 738 <hr/> |
705 <h2><a name="content029">Countable Ordinals can contains uncountable set?</a></h2> | 739 <h2><a name="content030">Countable Ordinals can contains uncountable set?</a></h2> |
706 Yes, the ordinals contains any level of infinite Set in the axioms. | 740 Yes, the ordinals contains any level of infinite Set in the axioms. |
707 <p> | 741 <p> |
708 If we handle real-number in the model, only countable number of real-number is used. | 742 If we handle real-number in the model, only countable number of real-number is used. |
709 <p> | 743 <p> |
710 | 744 |
718 <p> | 752 <p> |
719 We don't show the definition of cardinal number here. | 753 We don't show the definition of cardinal number here. |
720 <p> | 754 <p> |
721 | 755 |
722 <hr/> | 756 <hr/> |
723 <h2><a name="content030">What is Set</a></h2> | 757 <h2><a name="content031">What is Set</a></h2> |
724 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). | 758 The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). |
725 <p> | 759 <p> |
726 From naive point view, a set i a list, but in Agda, elements have all the same type. | 760 From naive point view, a set i a list, but in Agda, elements have all the same type. |
727 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. | 761 A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. |
728 <p> | 762 <p> |
729 Finite set may be written in finite series of ∨, but ... | 763 Finite set may be written in finite series of ∨, but ... |
730 <p> | 764 <p> |
731 | 765 |
732 <hr/> | 766 <hr/> |
733 <h2><a name="content031">We don't ask the contents of Set. It can be anything.</a></h2> | 767 <h2><a name="content032">We don't ask the contents of Set. It can be anything.</a></h2> |
734 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, | 768 From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, |
735 and all of them, and again we repeat this. | 769 and all of them, and again we repeat this. |
736 <p> | 770 <p> |
737 | 771 |
738 <pre> | 772 <pre> |
749 The idea is to use an ordinal as a pointer to a record which defines a Set. | 783 The idea is to use an ordinal as a pointer to a record which defines a Set. |
750 If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set. | 784 If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set. |
751 <p> | 785 <p> |
752 | 786 |
753 <hr/> | 787 <hr/> |
754 <h2><a name="content032">Ordinal Definable Set</a></h2> | 788 <h2><a name="content033">Ordinal Definable Set</a></h2> |
755 We can define a sbuset of Ordinals using predicates. What is a subset? | 789 We can define a sbuset of Ordinals using predicates. What is a subset? |
756 <p> | 790 <p> |
757 | 791 |
758 <pre> | 792 <pre> |
759 a predicate has an Ordinal argument | 793 a predicate has an Ordinal argument |
780 means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set. | 814 means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set. |
781 You can say OD is a class in ZF Set Theory term. | 815 You can say OD is a class in ZF Set Theory term. |
782 <p> | 816 <p> |
783 | 817 |
784 <hr/> | 818 <hr/> |
785 <h2><a name="content033">OD is not ZF Set</a></h2> | 819 <h2><a name="content034">OD is not ZF Set</a></h2> |
786 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like | 820 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like |
787 a Set. The idea is to use an ordinal as a pointer to OD. | 821 a Set. The idea is to use an ordinal as a pointer to OD. |
788 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like | 822 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like |
789 <p> | 823 <p> |
790 | 824 |
798 <p> | 832 <p> |
799 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. | 833 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. |
800 <p> | 834 <p> |
801 | 835 |
802 <hr/> | 836 <hr/> |
803 <h2><a name="content034"> HOD : Hereditarily Ordinal Definable</a></h2> | 837 <h2><a name="content035"> HOD : Hereditarily Ordinal Definable</a></h2> |
804 What we need is a bounded OD, the containment is limited by an ordinal. | 838 What we need is a bounded OD, the containment is limited by an ordinal. |
805 <p> | 839 <p> |
806 | 840 |
807 <pre> | 841 <pre> |
808 record HOD : Set (suc n) where | 842 record HOD : Set (suc n) where |
821 </pre> | 855 </pre> |
822 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. | 856 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. |
823 <p> | 857 <p> |
824 | 858 |
825 <hr/> | 859 <hr/> |
826 <h2><a name="content035">1 to 1 mapping between an HOD and an Ordinal</a></h2> | 860 <h2><a name="content036">1 to 1 mapping between an HOD and an Ordinal</a></h2> |
827 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping | 861 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping |
828 <p> | 862 <p> |
829 | 863 |
830 <pre> | 864 <pre> |
831 od→ord : HOD → Ordinal | 865 od→ord : HOD → Ordinal |
857 <img src="fig/ord-od-mapping.svg"> | 891 <img src="fig/ord-od-mapping.svg"> |
858 | 892 |
859 <p> | 893 <p> |
860 | 894 |
861 <hr/> | 895 <hr/> |
862 <h2><a name="content036">Order preserving in the mapping of OD and Ordinal</a></h2> | 896 <h2><a name="content037">Order preserving in the mapping of OD and Ordinal</a></h2> |
863 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). | 897 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). |
864 <p> | 898 <p> |
865 | 899 |
866 <pre> | 900 <pre> |
867 def (od y) ( od→ord x ) | 901 def (od y) ( od→ord x ) |
889 <img src="fig/ODandOrdinals.svg"> | 923 <img src="fig/ODandOrdinals.svg"> |
890 | 924 |
891 <p> | 925 <p> |
892 | 926 |
893 <hr/> | 927 <hr/> |
894 <h2><a name="content037">Various Sets</a></h2> | 928 <h2><a name="content038">Various Sets</a></h2> |
895 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. | 929 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. |
896 <p> | 930 <p> |
897 | 931 |
898 <pre> | 932 <pre> |
899 Ordinal / things satisfies axiom of Ordinal / extension of natural number | 933 Ordinal / things satisfies axiom of Ordinal / extension of natural number |
904 Agda Set / Type / it also has a level | 938 Agda Set / Type / it also has a level |
905 | 939 |
906 </pre> | 940 </pre> |
907 | 941 |
908 <hr/> | 942 <hr/> |
909 <h2><a name="content038">Fixes on ZF to intuitionistic logic</a></h2> | 943 <h2><a name="content039">Fixes on ZF to intuitionistic logic</a></h2> |
910 | 944 |
911 <p> | 945 <p> |
912 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define | 946 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define |
913 ZF axioms in Agda. | 947 ZF axioms in Agda. |
914 <p> | 948 <p> |
922 <a href="fig/zf-record.html"> | 956 <a href="fig/zf-record.html"> |
923 ZFのrecord </a> | 957 ZFのrecord </a> |
924 <p> | 958 <p> |
925 | 959 |
926 <hr/> | 960 <hr/> |
927 <h2><a name="content039">Pure logical axioms</a></h2> | 961 <h2><a name="content040">Pure logical axioms</a></h2> |
928 | 962 |
929 <pre> | 963 <pre> |
930 empty, pair, select, ε-induction??infinity | 964 empty, pair, select, ε-induction??infinity |
931 | 965 |
932 </pre> | 966 </pre> |
957 </pre> | 991 </pre> |
958 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. | 992 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. |
959 <p> | 993 <p> |
960 | 994 |
961 <hr/> | 995 <hr/> |
962 <h2><a name="content040">Axiom of Pair</a></h2> | 996 <h2><a name="content041">Axiom of Pair</a></h2> |
963 In the Tanaka's book, axiom of pair is as follows. | 997 In the Tanaka's book, axiom of pair is as follows. |
964 <p> | 998 <p> |
965 | 999 |
966 <pre> | 1000 <pre> |
967 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) | 1001 ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) |
984 </pre> | 1018 </pre> |
985 This is already written in Agda, so we use these as axioms. All inputs have ∀. | 1019 This is already written in Agda, so we use these as axioms. All inputs have ∀. |
986 <p> | 1020 <p> |
987 | 1021 |
988 <hr/> | 1022 <hr/> |
989 <h2><a name="content041">pair in OD</a></h2> | 1023 <h2><a name="content042">pair in OD</a></h2> |
990 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. | 1024 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. |
991 <p> | 1025 <p> |
992 | 1026 |
993 <pre> | 1027 <pre> |
994 _,_ : HOD → HOD → HOD | 1028 _,_ : HOD → HOD → HOD |
999 <p> | 1033 <p> |
1000 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. | 1034 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. |
1001 <p> | 1035 <p> |
1002 | 1036 |
1003 <hr/> | 1037 <hr/> |
1004 <h2><a name="content042">Validity of Axiom of Pair</a></h2> | 1038 <h2><a name="content043">Validity of Axiom of Pair</a></h2> |
1005 Assuming ZFSet is OD, we are going to prove pair→ . | 1039 Assuming ZFSet is OD, we are going to prove pair→ . |
1006 <p> | 1040 <p> |
1007 | 1041 |
1008 <pre> | 1042 <pre> |
1009 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) | 1043 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) |
1040 <p> | 1074 <p> |
1041 But we haven't defined == yet. | 1075 But we haven't defined == yet. |
1042 <p> | 1076 <p> |
1043 | 1077 |
1044 <hr/> | 1078 <hr/> |
1045 <h2><a name="content043">Equality of OD and Axiom of Extensionality </a></h2> | 1079 <h2><a name="content044">Equality of OD and Axiom of Extensionality </a></h2> |
1046 OD is defined by a predicates, if we compares normal form of the predicates, even if | 1080 OD is defined by a predicates, if we compares normal form of the predicates, even if |
1047 it contains the same elements, it may be different, which is no good as an equality of | 1081 it contains the same elements, it may be different, which is no good as an equality of |
1048 Sets. | 1082 Sets. |
1049 <p> | 1083 <p> |
1050 Axiom of Extensionality requires sets having the same elements are handled in the same way | 1084 Axiom of Extensionality requires sets having the same elements are handled in the same way |
1102 odef-iso refl t = t | 1136 odef-iso refl t = t |
1103 | 1137 |
1104 </pre> | 1138 </pre> |
1105 | 1139 |
1106 <hr/> | 1140 <hr/> |
1107 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2> | 1141 <h2><a name="content045">Validity of Axiom of Extensionality</a></h2> |
1108 | 1142 |
1109 <p> | 1143 <p> |
1110 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes | 1144 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes |
1111 <p> | 1145 <p> |
1112 | 1146 |
1123 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d | 1157 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d |
1124 | 1158 |
1125 </pre> | 1159 </pre> |
1126 | 1160 |
1127 <hr/> | 1161 <hr/> |
1128 <h2><a name="content045">Non constructive assumptions so far</a></h2> | 1162 <h2><a name="content046">Axiom of infinity</a></h2> |
1163 | |
1164 <p> | |
1165 It means it has ω as a ZF Set. It is ususally written like this. | |
1166 <p> | |
1167 | |
1168 <pre> | |
1169 ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) | |
1170 | |
1171 </pre> | |
1172 x ∪ { x } is Union (x , (x , x)) in our notation. It contains existential quantifier, so we introduce a function | |
1173 <p> | |
1174 | |
1175 <pre> | |
1176 infinite : ZFSet | |
1177 infinity∅ : ∅ ∈ infinite | |
1178 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ { x }) ∈ infinite | |
1179 | |
1180 </pre> | |
1181 | |
1182 <hr/> | |
1183 <h2><a name="content047">ω in HOD</a></h2> | |
1184 | |
1185 <p> | |
1186 To define an OD which arrows od→ord (Union (x , (x , x))) as a predicate, we can use Agda data structure. | |
1187 <p> | |
1188 | |
1189 <pre> | |
1190 data infinite-d : ( x : Ordinal ) → Set n where | |
1191 iφ : infinite-d o∅ | |
1192 isuc : {x : Ordinal } → infinite-d x → | |
1193 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | |
1194 | |
1195 </pre> | |
1196 It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now | |
1197 we can define HOD like this. | |
1198 <p> | |
1199 | |
1200 <pre> | |
1201 infinite : HOD | |
1202 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? } | |
1203 | |
1204 </pre> | |
1205 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which | |
1206 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal. | |
1207 <p> | |
1208 We need some restriction on the HOD-Ordinal mapping. Simple one is this. | |
1209 <p> | |
1210 | |
1211 <pre> | |
1212 ωmax : Ordinal | |
1213 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax | |
1214 | |
1215 </pre> | |
1216 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be | |
1217 <p> | |
1218 | |
1219 <pre> | |
1220 hod-ord< : {x : HOD } → Set n | |
1221 hod-ord< {x} = od→ord x o< next (odmax x) | |
1222 | |
1223 </pre> | |
1224 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and | |
1225 its bound. | |
1226 <p> | |
1227 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. | |
1228 This is the reason of necessity of Axiom of infinite. | |
1229 <p> | |
1230 | |
1231 <hr/> | |
1232 <h2><a name="content048">increment pase of address of HOD</a></h2> | |
1233 The address of HOD may have obvious bound, but it is defined in a relative way. | |
1234 <p> | |
1235 | |
1236 <pre> | |
1237 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) ) | |
1238 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y) | |
1239 | |
1240 </pre> | |
1241 Basicaly, we cannot know the concrete address of HOD other than empty set. | |
1242 <p> | |
1243 Assuming, previous assuption, we have | |
1244 <p> | |
1245 | |
1246 <pre> | |
1247 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) | |
1248 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where | |
1249 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) | |
1250 | |
1251 </pre> | |
1252 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. | |
1253 <p> | |
1254 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c<→o< can be drived from ⊆→o≤ . | |
1255 <p> | |
1256 | |
1257 <pre> | |
1258 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) | |
1259 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) | |
1260 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | |
1261 | |
1262 </pre> | |
1263 | |
1264 <hr/> | |
1265 <h2><a name="content049">Non constructive assumptions so far</a></h2> | |
1129 | 1266 |
1130 <p> | 1267 <p> |
1131 | 1268 |
1132 <pre> | 1269 <pre> |
1133 od→ord : HOD → Ordinal | 1270 od→ord : HOD → Ordinal |
1141 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ | 1278 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
1142 | 1279 |
1143 </pre> | 1280 </pre> |
1144 | 1281 |
1145 <hr/> | 1282 <hr/> |
1146 <h2><a name="content046">Axiom which have negation form</a></h2> | 1283 <h2><a name="content050">Axiom which have negation form</a></h2> |
1147 | 1284 |
1148 <p> | 1285 <p> |
1149 | 1286 |
1150 <pre> | 1287 <pre> |
1151 Union, Selection | 1288 Union, Selection |
1165 </pre> | 1302 </pre> |
1166 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. | 1303 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. |
1167 <p> | 1304 <p> |
1168 | 1305 |
1169 <hr/> | 1306 <hr/> |
1170 <h2><a name="content047">Union </a></h2> | 1307 <h2><a name="content051">Union </a></h2> |
1171 The original form of the Axiom of Union is | 1308 The original form of the Axiom of Union is |
1172 <p> | 1309 <p> |
1173 | 1310 |
1174 <pre> | 1311 <pre> |
1175 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) | 1312 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) |
1181 <pre> | 1318 <pre> |
1182 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z | 1319 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z |
1183 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) | 1320 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) |
1184 | 1321 |
1185 </pre> | 1322 </pre> |
1186 The definition of Union in OD is like this. | 1323 The definition of Union in HOD is like this. |
1187 <p> | 1324 <p> |
1188 | 1325 |
1189 <pre> | 1326 <pre> |
1190 Union : OD → OD | 1327 Union : HOD → HOD |
1191 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } | 1328 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } |
1192 | 1329 ; odmax = osuc (od→ord U) ; <odmax = ? } |
1193 </pre> | 1330 |
1331 </pre> | |
1332 The bound of Union is evident, but its proof is rather complicated. | |
1333 <p> | |
1194 Proof of validity is straight forward. | 1334 Proof of validity is straight forward. |
1195 <p> | 1335 <p> |
1196 | 1336 |
1197 <pre> | 1337 <pre> |
1198 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z | 1338 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z |
1199 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx | 1339 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx |
1200 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) | 1340 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) |
1201 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) | 1341 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) |
1202 union← X z UX∋z = FExists _ lemma UX∋z where | 1342 union← X z UX∋z = FExists _ lemma UX∋z where |
1203 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) | 1343 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) |
1204 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } | 1344 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } |
1205 | 1345 |
1206 </pre> | 1346 </pre> |
1207 where | 1347 where |
1208 <p> | 1348 <p> |
1209 | 1349 |
1217 </pre> | 1357 </pre> |
1218 which checks existence using contra-position. | 1358 which checks existence using contra-position. |
1219 <p> | 1359 <p> |
1220 | 1360 |
1221 <hr/> | 1361 <hr/> |
1222 <h2><a name="content048">Axiom of replacement</a></h2> | 1362 <h2><a name="content052">Axiom of replacement</a></h2> |
1223 We can replace the elements of a set by a function and it becomes a set. From the book, | 1363 We can replace the elements of a set by a function and it becomes a set. From the book, |
1224 <p> | 1364 <p> |
1225 | 1365 |
1226 <pre> | 1366 <pre> |
1227 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) | 1367 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) |
1229 </pre> | 1369 </pre> |
1230 The existential quantifier can be related by a function, | 1370 The existential quantifier can be related by a function, |
1231 <p> | 1371 <p> |
1232 | 1372 |
1233 <pre> | 1373 <pre> |
1234 Replace : OD → (OD → OD ) → OD | 1374 Replace : HOD → (HOD → HOD ) → HOD |
1235 | 1375 |
1236 </pre> | 1376 </pre> |
1237 The axioms becomes as follows. | 1377 The axioms becomes as follows. |
1238 <p> | 1378 <p> |
1239 | 1379 |
1249 <pre> | 1389 <pre> |
1250 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD | 1390 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD |
1251 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } | 1391 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } |
1252 | 1392 |
1253 </pre> | 1393 </pre> |
1254 Besides this upper bounds is required. | 1394 in-codomain is a logical relation-ship, and it is written in OD. |
1255 <p> | 1395 <p> |
1256 | 1396 |
1257 <pre> | 1397 <pre> |
1258 Replace : OD → (OD → OD ) → OD | 1398 Replace : HOD → (HOD → HOD) → HOD |
1259 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } | 1399 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } |
1260 | 1400 ; odmax = rmax ; <odmax = rmax<} where |
1261 </pre> | 1401 rmax : Ordinal |
1262 We omit the proof of the validity, but it is rather straight forward. | 1402 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) |
1263 <p> | 1403 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax |
1264 | 1404 rmax< lt = proj1 lt |
1265 <hr/> | 1405 |
1266 <h2><a name="content049">Validity of Power Set Axiom</a></h2> | 1406 </pre> |
1407 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set. | |
1408 <p> | |
1409 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship. | |
1410 <p> | |
1411 | |
1412 <hr/> | |
1413 <h2><a name="content053">Validity of Power Set Axiom</a></h2> | |
1267 The original Power Set Axiom is this. | 1414 The original Power Set Axiom is this. |
1268 <p> | 1415 <p> |
1269 | 1416 |
1270 <pre> | 1417 <pre> |
1271 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) | 1418 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) |
1298 The validity of the axioms are slight complicated, we have to define set of all subset. We define | 1445 The validity of the axioms are slight complicated, we have to define set of all subset. We define |
1299 subset in a different form. | 1446 subset in a different form. |
1300 <p> | 1447 <p> |
1301 | 1448 |
1302 <pre> | 1449 <pre> |
1303 ZFSubset : (A x : OD ) → OD | 1450 ZFSubset : (A x : HOD ) → HOD |
1304 ZFSubset A x = record { def = λ y → def A y ∧ def x y } | 1451 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where |
1452 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) | |
1453 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and)) | |
1305 | 1454 |
1306 </pre> | 1455 </pre> |
1307 We can prove, | 1456 We can prove, |
1308 <p> | 1457 <p> |
1309 | 1458 |
1310 <pre> | 1459 <pre> |
1311 ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) | 1460 ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) |
1312 | 1461 |
1313 </pre> | 1462 </pre> |
1314 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals, | 1463 We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals, |
1315 which is an Ordinals with our Model. | 1464 which is an Ordinals with our Model. |
1316 <p> | 1465 <p> |
1332 </pre> | 1481 </pre> |
1333 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. | 1482 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. |
1334 <p> | 1483 <p> |
1335 | 1484 |
1336 <pre> | 1485 <pre> |
1337 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) | 1486 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a ) |
1338 | 1487 |
1339 </pre> | 1488 </pre> |
1340 In case of Ord a intro of Power Set axiom becomes valid. | 1489 In case of Ord a intro of Power Set axiom becomes valid. |
1341 <p> | 1490 <p> |
1342 | 1491 |
1343 <pre> | 1492 <pre> |
1344 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t | 1493 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t |
1345 | 1494 |
1346 </pre> | 1495 </pre> |
1347 Using this, we can prove, | 1496 Using this, we can prove, |
1348 <p> | 1497 <p> |
1349 | 1498 |
1350 <pre> | 1499 <pre> |
1351 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) | 1500 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x) |
1352 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t | 1501 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t |
1353 | 1502 |
1354 </pre> | 1503 </pre> |
1355 | 1504 |
1356 <hr/> | 1505 <hr/> |
1357 <h2><a name="content050">Axiom of regularity, Axiom of choice, ε-induction</a></h2> | 1506 <h2><a name="content054">Axiom of regularity, Axiom of choice, ε-induction</a></h2> |
1358 | 1507 |
1359 <p> | 1508 <p> |
1360 Axiom of regularity requires non self intersectable elements (which is called minimum), if we | 1509 Axiom of regularity requires non self intersectable elements (which is called minimum), if we |
1361 replace it by a function, it becomes a choice function. It makes axiom of choice valid. | 1510 replace it by a function, it becomes a choice function. It makes axiom of choice valid. |
1362 <p> | 1511 <p> |
1363 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of | 1512 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of |
1364 choice also becomes valid. | 1513 choice also becomes valid. |
1365 <p> | 1514 <p> |
1366 | 1515 |
1367 <pre> | 1516 <pre> |
1368 minimal : (x : OD ) → ¬ (x == od∅ )→ OD | 1517 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD |
1369 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 1518 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) |
1370 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 1519 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) |
1371 | 1520 |
1372 </pre> | 1521 </pre> |
1373 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). | 1522 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). |
1374 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. | 1523 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. |
1375 <p> | 1524 <p> |
1376 | 1525 |
1377 <pre> | 1526 <pre> |
1378 ε-induction : { ψ : OD → Set (suc n)} | 1527 ε-induction : { ψ : HOD → Set (suc n)} |
1379 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) | 1528 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) |
1380 → (x : OD ) → ψ x | 1529 → (x : HOD ) → ψ x |
1381 | 1530 |
1382 </pre> | 1531 </pre> |
1383 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals. | 1532 In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals. |
1384 <p> | 1533 <p> |
1385 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia. | 1534 The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia. |
1399 </pre> | 1548 </pre> |
1400 It does not requires ∅ ∉ X . | 1549 It does not requires ∅ ∉ X . |
1401 <p> | 1550 <p> |
1402 | 1551 |
1403 <hr/> | 1552 <hr/> |
1404 <h2><a name="content051">Axiom of choice and Law of Excluded Middle</a></h2> | 1553 <h2><a name="content055">Axiom of choice and Law of Excluded Middle</a></h2> |
1405 In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, | 1554 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, |
1406 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, | 1555 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, |
1407 but it requires law of the exclude middle. | 1556 but it requires law of the exclude middle. |
1408 <p> | 1557 <p> |
1409 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can | 1558 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can |
1410 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the | 1559 perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the |
1411 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) . | 1560 set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) . |
1412 <p> | 1561 <p> |
1413 | 1562 |
1414 <pre> | 1563 <pre> |
1415 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p | 1564 ppp : { p : Set n } { a : HOD } → record { def = λ x → p } ∋ a → p |
1416 ppp {p} {a} d = d | 1565 ppp {p} {a} d = d |
1417 | 1566 |
1418 </pre> | 1567 </pre> |
1419 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice | 1568 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice |
1420 and Law of Excluded Middle is equivalent in our mode. | 1569 and Law of Excluded Middle is equivalent in our mode. |
1421 <p> | 1570 <p> |
1422 | 1571 |
1423 <hr/> | 1572 <hr/> |
1424 <h2><a name="content052">Relation-ship among ZF axiom</a></h2> | 1573 <h2><a name="content056">Relation-ship among ZF axiom</a></h2> |
1425 <img src="fig/axiom-dependency.svg"> | 1574 <img src="fig/axiom-dependency.svg"> |
1426 | 1575 |
1427 <p> | 1576 <p> |
1428 | 1577 |
1429 <hr/> | 1578 <hr/> |
1430 <h2><a name="content053">Non constructive assumption in our model</a></h2> | 1579 <h2><a name="content057">Non constructive assumption in our model</a></h2> |
1431 mapping between OD and Ordinals | 1580 mapping between HOD and Ordinals |
1432 <p> | 1581 <p> |
1433 | 1582 |
1434 <pre> | 1583 <pre> |
1435 od→ord : OD → Ordinal | 1584 od→ord : HOD → Ordinal |
1436 ord→od : Ordinal → OD | 1585 ord→od : Ordinal → OD |
1437 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x | 1586 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x |
1438 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 1587 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
1439 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y | 1588 c<→o< : {x y : HOD } → def y ( od→ord x ) → od→ord x o< od→ord y |
1589 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) | |
1440 | 1590 |
1441 </pre> | 1591 </pre> |
1442 Equivalence on OD | 1592 Equivalence on OD |
1443 <p> | 1593 <p> |
1444 | 1594 |
1445 <pre> | 1595 <pre> |
1446 ==→o≡ : { x y : OD } → (x == y) → x ≡ y | 1596 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y |
1447 | 1597 |
1448 </pre> | 1598 </pre> |
1449 Upper bound | 1599 Upper bound |
1450 <p> | 1600 <p> |
1451 | 1601 |
1452 <pre> | 1602 <pre> |
1453 sup-o : ( Ordinal → Ordinal ) → Ordinal | 1603 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
1454 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ | 1604 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
1605 | |
1606 </pre> | |
1607 In order to have bounded ω, | |
1608 <p> | |
1609 | |
1610 <pre> | |
1611 hod-ord< : {x : HOD} → od→ord x o< next (odmax x) | |
1455 | 1612 |
1456 </pre> | 1613 </pre> |
1457 Axiom of choice and strong axiom of regularity. | 1614 Axiom of choice and strong axiom of regularity. |
1458 <p> | 1615 <p> |
1459 | 1616 |
1460 <pre> | 1617 <pre> |
1461 minimal : (x : OD ) → ¬ (x == od∅ )→ OD | 1618 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD |
1462 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 1619 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) |
1463 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 1620 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) |
1464 | 1621 |
1465 </pre> | 1622 </pre> |
1466 | 1623 |
1467 <hr/> | 1624 <hr/> |
1468 <h2><a name="content054">So it this correct?</a></h2> | 1625 <h2><a name="content058">So it this correct?</a></h2> |
1469 | 1626 |
1470 <p> | 1627 <p> |
1471 Our axiom are syntactically the same in the text book, but negations are slightly different. | 1628 Our axiom are syntactically the same in the text book, but negations are slightly different. |
1472 <p> | 1629 <p> |
1473 If we assumes excluded middle, these are exactly same. | 1630 If we assumes excluded middle, these are exactly same. |
1474 <p> | 1631 <p> |
1475 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. | 1632 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. |
1476 <p> | 1633 <p> |
1477 Except the upper bound, axioms are simple logical relation. | 1634 Except the upper bound, axioms are simple logical relation. |
1478 <p> | 1635 <p> |
1479 Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not. | 1636 Proof of existence of mapping between HOD and Ordinals are not obvious. We don't know we prove it or not. |
1480 <p> | 1637 <p> |
1481 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts, | 1638 Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts, |
1482 but we don't have explicit upper limit on Ordinals. | 1639 but we don't have explicit upper limit on Ordinals. |
1483 <p> | 1640 <p> |
1484 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. | 1641 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. |
1485 <p> | 1642 <p> |
1486 | 1643 |
1487 <hr/> | 1644 <hr/> |
1488 <h2><a name="content055">How to use Agda Set Theory</a></h2> | 1645 <h2><a name="content059">How to use Agda Set Theory</a></h2> |
1489 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be | 1646 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be |
1490 postulated or assuming law of excluded middle. | 1647 postulated or assuming law of excluded middle. |
1491 <p> | 1648 <p> |
1492 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check | 1649 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check |
1493 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. | 1650 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. |
1494 <p> | 1651 <p> |
1495 ZF record itself is not necessary, for example, topology theory without ZF can be possible. | 1652 ZF record itself is not necessary, for example, topology theory without ZF can be possible. |
1496 <p> | 1653 <p> |
1497 | 1654 |
1498 <hr/> | 1655 <hr/> |
1499 <h2><a name="content056">Topos and Set Theory</a></h2> | 1656 <h2><a name="content060">Topos and Set Theory</a></h2> |
1500 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a | 1657 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a |
1501 sub-object classifier. | 1658 sub-object classifier. |
1502 <p> | 1659 <p> |
1503 Topos itself is model of intuitionistic logic. | 1660 Topos itself is model of intuitionistic logic. |
1504 <p> | 1661 <p> |
1512 <p> | 1669 <p> |
1513 Our Agda model is a proof theoretic version of it. | 1670 Our Agda model is a proof theoretic version of it. |
1514 <p> | 1671 <p> |
1515 | 1672 |
1516 <hr/> | 1673 <hr/> |
1517 <h2><a name="content057">Cardinal number and Continuum hypothesis</a></h2> | 1674 <h2><a name="content061">Cardinal number and Continuum hypothesis</a></h2> |
1518 Axiom of choice is required to define cardinal number | 1675 Axiom of choice is required to define cardinal number |
1519 <p> | 1676 <p> |
1520 definition of cardinal number is not yet done | 1677 definition of cardinal number is not yet done |
1521 <p> | 1678 <p> |
1522 definition of filter is not yet done | 1679 definition of filter is not yet done |
1530 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) | 1687 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) |
1531 | 1688 |
1532 </pre> | 1689 </pre> |
1533 | 1690 |
1534 <hr/> | 1691 <hr/> |
1535 <h2><a name="content058">Filter</a></h2> | 1692 <h2><a name="content062">Filter</a></h2> |
1536 | 1693 |
1537 <p> | 1694 <p> |
1538 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number | 1695 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number |
1539 is depends on axiom of choice. | 1696 is depends on axiom of choice. |
1540 <p> | 1697 <p> |
1541 | 1698 |
1542 <pre> | 1699 <pre> |
1543 record Filter ( L : OD ) : Set (suc n) where | 1700 record Filter ( L : HOD ) : Set (suc n) where |
1544 field | 1701 field |
1545 filter : OD | 1702 filter : OD |
1546 proper : ¬ ( filter ∋ od∅ ) | 1703 proper : ¬ ( filter ∋ od∅ ) |
1547 inL : filter ⊆ L | 1704 inL : filter ⊆ L |
1548 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q | 1705 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
1549 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) | 1706 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) |
1550 | 1707 |
1551 </pre> | 1708 </pre> |
1552 We may construct a model of non standard analysis or set theory. | 1709 We may construct a model of non standard analysis or set theory. |
1553 <p> | 1710 <p> |
1554 This may be simpler than classical forcing theory ( not yet done). | 1711 This may be simpler than classical forcing theory ( not yet done). |
1555 <p> | 1712 <p> |
1556 | 1713 |
1557 <hr/> | 1714 <hr/> |
1558 <h2><a name="content059">Programming Mathematics</a></h2> | 1715 <h2><a name="content063">Programming Mathematics</a></h2> |
1559 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical | 1716 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical |
1560 structure are | 1717 structure are |
1561 <p> | 1718 <p> |
1562 | 1719 |
1563 <pre> | 1720 <pre> |
1578 </pre> | 1735 </pre> |
1579 are proved in Agda. | 1736 are proved in Agda. |
1580 <p> | 1737 <p> |
1581 | 1738 |
1582 <hr/> | 1739 <hr/> |
1583 <h2><a name="content060">link</a></h2> | 1740 <h2><a name="content064">link</a></h2> |
1584 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> | 1741 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> |
1585 <p> | 1742 <p> |
1586 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 | 1743 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 |
1587 </a> | 1744 </a> |
1588 <p> | 1745 <p> |
1611 <li><a href="#content008"> introduction と elimination</a> | 1768 <li><a href="#content008"> introduction と elimination</a> |
1612 <li><a href="#content009"> To prove A → B </a> | 1769 <li><a href="#content009"> To prove A → B </a> |
1613 <li><a href="#content010"> A ∧ B</a> | 1770 <li><a href="#content010"> A ∧ B</a> |
1614 <li><a href="#content011"> record</a> | 1771 <li><a href="#content011"> record</a> |
1615 <li><a href="#content012"> Mathematical structure</a> | 1772 <li><a href="#content012"> Mathematical structure</a> |
1616 <li><a href="#content013"> A Model and a theory</a> | 1773 <li><a href="#content013"> Limit Ordinal</a> |
1617 <li><a href="#content014"> postulate と module</a> | 1774 <li><a href="#content014"> A Model and a theory</a> |
1618 <li><a href="#content015"> A ∨ B</a> | 1775 <li><a href="#content015"> postulate と module</a> |
1619 <li><a href="#content016"> Negation</a> | 1776 <li><a href="#content016"> A ∨ B</a> |
1620 <li><a href="#content017"> Equality </a> | 1777 <li><a href="#content017"> Negation</a> |
1621 <li><a href="#content018"> Equivalence relation</a> | 1778 <li><a href="#content018"> Equality </a> |
1622 <li><a href="#content019"> Ordering</a> | 1779 <li><a href="#content019"> Equivalence relation</a> |
1623 <li><a href="#content020"> Quantifier</a> | 1780 <li><a href="#content020"> Ordering</a> |
1624 <li><a href="#content021"> Can we do math in this way?</a> | 1781 <li><a href="#content021"> Quantifier</a> |
1625 <li><a href="#content022"> Things which Agda cannot prove</a> | 1782 <li><a href="#content022"> Can we do math in this way?</a> |
1626 <li><a href="#content023"> Classical story of ZF Set Theory</a> | 1783 <li><a href="#content023"> Things which Agda cannot prove</a> |
1627 <li><a href="#content024"> Ordinals</a> | 1784 <li><a href="#content024"> Classical story of ZF Set Theory</a> |
1628 <li><a href="#content025"> Axiom of Ordinals</a> | 1785 <li><a href="#content025"> Ordinals</a> |
1629 <li><a href="#content026"> Concrete Ordinals or Countable Ordinals</a> | 1786 <li><a href="#content026"> Axiom of Ordinals</a> |
1630 <li><a href="#content027"> Model of Ordinals</a> | 1787 <li><a href="#content027"> Concrete Ordinals or Countable Ordinals</a> |
1631 <li><a href="#content028"> Debugging axioms using Model</a> | 1788 <li><a href="#content028"> Model of Ordinals</a> |
1632 <li><a href="#content029"> Countable Ordinals can contains uncountable set?</a> | 1789 <li><a href="#content029"> Debugging axioms using Model</a> |
1633 <li><a href="#content030"> What is Set</a> | 1790 <li><a href="#content030"> Countable Ordinals can contains uncountable set?</a> |
1634 <li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a> | 1791 <li><a href="#content031"> What is Set</a> |
1635 <li><a href="#content032"> Ordinal Definable Set</a> | 1792 <li><a href="#content032"> We don't ask the contents of Set. It can be anything.</a> |
1636 <li><a href="#content033"> OD is not ZF Set</a> | 1793 <li><a href="#content033"> Ordinal Definable Set</a> |
1637 <li><a href="#content034"> HOD : Hereditarily Ordinal Definable</a> | 1794 <li><a href="#content034"> OD is not ZF Set</a> |
1638 <li><a href="#content035"> 1 to 1 mapping between an HOD and an Ordinal</a> | 1795 <li><a href="#content035"> HOD : Hereditarily Ordinal Definable</a> |
1639 <li><a href="#content036"> Order preserving in the mapping of OD and Ordinal</a> | 1796 <li><a href="#content036"> 1 to 1 mapping between an HOD and an Ordinal</a> |
1640 <li><a href="#content037"> Various Sets</a> | 1797 <li><a href="#content037"> Order preserving in the mapping of OD and Ordinal</a> |
1641 <li><a href="#content038"> Fixes on ZF to intuitionistic logic</a> | 1798 <li><a href="#content038"> Various Sets</a> |
1642 <li><a href="#content039"> Pure logical axioms</a> | 1799 <li><a href="#content039"> Fixes on ZF to intuitionistic logic</a> |
1643 <li><a href="#content040"> Axiom of Pair</a> | 1800 <li><a href="#content040"> Pure logical axioms</a> |
1644 <li><a href="#content041"> pair in OD</a> | 1801 <li><a href="#content041"> Axiom of Pair</a> |
1645 <li><a href="#content042"> Validity of Axiom of Pair</a> | 1802 <li><a href="#content042"> pair in OD</a> |
1646 <li><a href="#content043"> Equality of OD and Axiom of Extensionality </a> | 1803 <li><a href="#content043"> Validity of Axiom of Pair</a> |
1647 <li><a href="#content044"> Validity of Axiom of Extensionality</a> | 1804 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a> |
1648 <li><a href="#content045"> Non constructive assumptions so far</a> | 1805 <li><a href="#content045"> Validity of Axiom of Extensionality</a> |
1649 <li><a href="#content046"> Axiom which have negation form</a> | 1806 <li><a href="#content046"> Axiom of infinity</a> |
1650 <li><a href="#content047"> Union </a> | 1807 <li><a href="#content047"> ω in HOD</a> |
1651 <li><a href="#content048"> Axiom of replacement</a> | 1808 <li><a href="#content048"> increment pase of address of HOD</a> |
1652 <li><a href="#content049"> Validity of Power Set Axiom</a> | 1809 <li><a href="#content049"> Non constructive assumptions so far</a> |
1653 <li><a href="#content050"> Axiom of regularity, Axiom of choice, ε-induction</a> | 1810 <li><a href="#content050"> Axiom which have negation form</a> |
1654 <li><a href="#content051"> Axiom of choice and Law of Excluded Middle</a> | 1811 <li><a href="#content051"> Union </a> |
1655 <li><a href="#content052"> Relation-ship among ZF axiom</a> | 1812 <li><a href="#content052"> Axiom of replacement</a> |
1656 <li><a href="#content053"> Non constructive assumption in our model</a> | 1813 <li><a href="#content053"> Validity of Power Set Axiom</a> |
1657 <li><a href="#content054"> So it this correct?</a> | 1814 <li><a href="#content054"> Axiom of regularity, Axiom of choice, ε-induction</a> |
1658 <li><a href="#content055"> How to use Agda Set Theory</a> | 1815 <li><a href="#content055"> Axiom of choice and Law of Excluded Middle</a> |
1659 <li><a href="#content056"> Topos and Set Theory</a> | 1816 <li><a href="#content056"> Relation-ship among ZF axiom</a> |
1660 <li><a href="#content057"> Cardinal number and Continuum hypothesis</a> | 1817 <li><a href="#content057"> Non constructive assumption in our model</a> |
1661 <li><a href="#content058"> Filter</a> | 1818 <li><a href="#content058"> So it this correct?</a> |
1662 <li><a href="#content059"> Programming Mathematics</a> | 1819 <li><a href="#content059"> How to use Agda Set Theory</a> |
1663 <li><a href="#content060"> link</a> | 1820 <li><a href="#content060"> Topos and Set Theory</a> |
1821 <li><a href="#content061"> Cardinal number and Continuum hypothesis</a> | |
1822 <li><a href="#content062"> Filter</a> | |
1823 <li><a href="#content063"> Programming Mathematics</a> | |
1824 <li><a href="#content064"> link</a> | |
1664 </ol> | 1825 </ol> |
1665 | 1826 |
1666 <hr/> Shinji KONO / Tue Jul 7 15:44:35 2020 | 1827 <hr/> Shinji KONO / Tue Jul 14 15:02:38 2020 |
1667 </body></html> | 1828 </body></html> |