Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison zf-in-agda.ind @ 425:f7d66c84bc26
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 05 Aug 2020 19:37:07 +0900 |
parents | aad9249d1e8f |
children |
comparison
equal
deleted
inserted
replaced
424:cc7909f86841 | 425:f7d66c84bc26 |
---|---|
586 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like | 586 If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like |
587 a Set. The idea is to use an ordinal as a pointer to OD. | 587 a Set. The idea is to use an ordinal as a pointer to OD. |
588 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, | 588 Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, |
589 which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like | 589 which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like |
590 | 590 |
591 ¬OD-order : ( od→ord : OD → Ordinal ) | 591 ¬OD-order : ( & : OD → Ordinal ) |
592 → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ | 592 → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ |
593 ¬OD-order od→ord ord→od c<→o< = ? | 593 ¬OD-order & * c<→o< = ? |
594 | 594 |
595 Actualy we can prove this contrdction, so we need some restrctions on OD. | 595 Actualy we can prove this contrdction, so we need some restrctions on OD. |
596 | 596 |
597 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. | 597 This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself. |
598 | 598 |
615 | 615 |
616 --1 to 1 mapping between an HOD and an Ordinal | 616 --1 to 1 mapping between an HOD and an Ordinal |
617 | 617 |
618 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping | 618 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping |
619 | 619 |
620 od→ord : HOD → Ordinal | 620 & : HOD → Ordinal |
621 ord→od : Ordinal → HOD | 621 * : Ordinal → HOD |
622 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | 622 oiso : {x : HOD } → * ( & x ) ≡ x |
623 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 623 diso : {x : Ordinal } → & ( * x ) ≡ x |
624 | 624 |
625 we can check an HOD is an element of the OD using def. | 625 we can check an HOD is an element of the OD using def. |
626 | 626 |
627 A ∋ x can be define as follows. | 627 A ∋ x can be define as follows. |
628 | 628 |
629 _∋_ : ( A x : HOD ) → Set n | 629 _∋_ : ( A x : HOD ) → Set n |
630 _∋_ A x = def (od A) ( od→ord x ) | 630 _∋_ A x = def (od A) ( & x ) |
631 | 631 |
632 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then | 632 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then |
633 | 633 |
634 A x = def A ( od→ord x ) = ψ (od→ord x) | 634 A x = def A ( & x ) = ψ (& x) |
635 | 635 |
636 They say the existing of the mappings can be proved in Classical Set Theory, but we | 636 They say the existing of the mappings can be proved in Classical Set Theory, but we |
637 simply assumes these non constructively. | 637 simply assumes these non constructively. |
638 | 638 |
639 <center><img src="fig/ord-od-mapping.svg"></center> | 639 <center><img src="fig/ord-od-mapping.svg"></center> |
640 | 640 |
641 --Order preserving in the mapping of OD and Ordinal | 641 --Order preserving in the mapping of OD and Ordinal |
642 | 642 |
643 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). | 643 Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). |
644 | 644 |
645 def (od y) ( od→ord x ) | 645 def (od y) ( & x ) |
646 | 646 |
647 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements | 647 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements |
648 have to be smaller than the corresponding ordinal of the containing OD. | 648 have to be smaller than the corresponding ordinal of the containing OD. |
649 We also assumes subset is always smaller. This is necessary to make a limit of Power Set. | 649 We also assumes subset is always smaller. This is necessary to make a limit of Power Set. |
650 | 650 |
651 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | 651 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y |
652 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) | 652 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) |
653 | 653 |
654 If wa assumes reverse order preservation, | 654 If wa assumes reverse order preservation, |
655 | 655 |
656 o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x | 656 o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (* y) x |
657 | 657 |
658 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model. | 658 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model. |
659 | 659 |
660 <center><img src="fig/ODandOrdinals.svg"></center> | 660 <center><img src="fig/ODandOrdinals.svg"></center> |
661 | 661 |
705 finitely can be define by Agda data. | 705 finitely can be define by Agda data. |
706 | 706 |
707 data infinite-d : ( x : Ordinal ) → Set n where | 707 data infinite-d : ( x : Ordinal ) → Set n where |
708 iφ : infinite-d o∅ | 708 iφ : infinite-d o∅ |
709 isuc : {x : Ordinal } → infinite-d x → | 709 isuc : {x : Ordinal } → infinite-d x → |
710 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | 710 infinite-d (& ( Union (* x , (* x , * x ) ) )) |
711 | 711 |
712 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. | 712 Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. |
713 | 713 |
714 --Axiom of Pair | 714 --Axiom of Pair |
715 | 715 |
731 --pair in OD | 731 --pair in OD |
732 | 732 |
733 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. | 733 OD is an equation on Ordinals, we can simply write axiom of pair in the OD. |
734 | 734 |
735 _,_ : HOD → HOD → HOD | 735 _,_ : HOD → HOD → HOD |
736 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ; <odmax = ? } | 736 x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = ? ; <odmax = ? } |
737 | 737 |
738 It is easy to find out odmax from odmax of x and y. | 738 It is easy to find out odmax from odmax of x and y. |
739 | 739 |
740 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. | 740 ≡ is an equality of λ terms, but please not that this is equality on Ordinals. |
741 | 741 |
745 | 745 |
746 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) | 746 pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) |
747 pair→ x y t p = ? | 747 pair→ x y t p = ? |
748 | 748 |
749 In this program, type of p is ( x , y ) ∋ t , that is | 749 In this program, type of p is ( x , y ) ∋ t , that is |
750 def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) . | 750 def ( x , y ) that is, (t ≡ & x ) ∨ ( t ≡ & y ) . |
751 | 751 |
752 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). | 752 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). |
753 | 753 |
754 pair→ x y t (case1 t≡x ) = ? | 754 pair→ x y t (case1 t≡x ) = ? |
755 pair→ x y t (case2 t≡y ) = ? | 755 pair→ x y t (case2 t≡y ) = ? |
760 pair→ x y t (case2 t≡y ) = case2 ? | 760 pair→ x y t (case2 t≡y ) = case2 ? |
761 | 761 |
762 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable | 762 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable |
763 which type is | 763 which type is |
764 | 764 |
765 t≡x : od→ord t ≡ od→ord x | 765 t≡x : & t ≡ & x |
766 | 766 |
767 which is shown by an Agda command (C-C C-E : agda2-show-context ). | 767 which is shown by an Agda command (C-C C-E : agda2-show-context ). |
768 | 768 |
769 But we haven't defined == yet. | 769 But we haven't defined == yet. |
770 | 770 |
801 | 801 |
802 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . | 802 ? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . |
803 | 803 |
804 Actual proof is rather complicated. | 804 Actual proof is rather complicated. |
805 | 805 |
806 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d | 806 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (* x))) d |
807 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d | 807 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (* x))) d |
808 | 808 |
809 where | 809 where |
810 | 810 |
811 odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x | 811 odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x |
812 odef-iso refl t = t | 812 odef-iso refl t = t |
847 infinity∅ : ∅ ∈ infinite | 847 infinity∅ : ∅ ∈ infinite |
848 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ { x }) ∈ infinite | 848 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ { x }) ∈ infinite |
849 | 849 |
850 --ω in HOD | 850 --ω in HOD |
851 | 851 |
852 To define an OD which arrows od→ord (Union (x , (x , x))) as a predicate, we can use Agda data structure. | 852 To define an OD which arrows & (Union (x , (x , x))) as a predicate, we can use Agda data structure. |
853 | 853 |
854 data infinite-d : ( x : Ordinal ) → Set n where | 854 data infinite-d : ( x : Ordinal ) → Set n where |
855 iφ : infinite-d o∅ | 855 iφ : infinite-d o∅ |
856 isuc : {x : Ordinal } → infinite-d x → | 856 isuc : {x : Ordinal } → infinite-d x → |
857 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | 857 infinite-d (& ( Union (* x , (* x , * x ) ) )) |
858 | 858 |
859 It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now | 859 It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now |
860 we can define HOD like this. | 860 we can define HOD like this. |
861 | 861 |
862 infinite : HOD | 862 infinite : HOD |
863 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? } | 863 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? } |
864 | 864 |
865 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which | 865 So what is the bound of ω? Analyzing the definition, it depends on the value of & (x , x), which |
866 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal. | 866 cannot know the aboslute value. This is because we don't have constructive definition of & : HOD → Ordinal. |
867 | |
868 --HOD and Agda data structure | |
869 | |
870 We may have | |
871 | |
872 a HOD <=> Agda Data Strucure | |
873 | |
874 as a data in Agda. Ex. | |
875 | |
876 data ord-pair : (p : Ordinal) → Set n where | |
877 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) | |
878 | |
879 ZFProduct : OD | |
880 ZFProduct = record { def = λ x → ord-pair x } | |
881 | |
882 pi1 : { p : Ordinal } → ord-pair p → Ordinal | |
883 pi1 ( pair x y) = x | |
884 | |
885 π1 : { p : HOD } → def ZFProduct (& p) → HOD | |
886 π1 lt = * (pi1 lt ) | |
887 | |
888 p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x | |
889 p-iso {x} p = ord≡→≡ (op-iso p) | |
890 | |
867 | 891 |
868 --HOD Ordrinal mapping | 892 --HOD Ordrinal mapping |
869 | 893 |
870 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger. | 894 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger. |
871 The address of HOD can be larger at least it have to be larger than the content's address. | 895 The address of HOD can be larger at least it have to be larger than the content's address. |
872 We only have a relative ordering such as | 896 We only have a relative ordering such as |
873 | 897 |
874 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) ) | 898 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) |
875 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y) | 899 pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y) |
876 | 900 |
877 Basicaly, we cannot know the concrete address of HOD other than empty set. | 901 Basicaly, we cannot know the concrete address of HOD other than empty set. |
878 | 902 |
879 <center><img src="fig/address-of-HOD.svg"></center> | 903 <center><img src="fig/address-of-HOD.svg"></center> |
880 | 904 |
886 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax | 910 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax |
887 | 911 |
888 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be | 912 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be |
889 | 913 |
890 hod-ord< : {x : HOD } → Set n | 914 hod-ord< : {x : HOD } → Set n |
891 hod-ord< {x} = od→ord x o< next (odmax x) | 915 hod-ord< {x} = & x o< next (odmax x) |
892 | 916 |
893 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and | 917 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and |
894 its bound. | 918 its bound. |
895 | 919 |
896 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. | 920 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. |
898 | 922 |
899 --increment pase of address of HOD | 923 --increment pase of address of HOD |
900 | 924 |
901 Assuming, hod-ord< , we have | 925 Assuming, hod-ord< , we have |
902 | 926 |
903 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) | 927 pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) |
904 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where | 928 pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where |
905 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) | 929 lemmab0 : next (odmax (x , x)) ≡ next (& x) |
906 | 930 |
907 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove | 931 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove |
908 | 932 |
909 infinite-bound : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ | 933 infinite-bound : ({x : HOD} → & x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ |
910 | 934 |
911 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c<→o< can be drived from ⊆→o≤ . | 935 We also notice that if we have & (x , x) ≡ osuc (& x), c<→o< can be drived from ⊆→o≤ . |
912 | 936 |
913 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) | 937 ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) ) |
914 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) | 938 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) ) |
915 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | 939 → {x y : HOD } → def (od y) ( & x ) → & x o< & y |
916 | 940 |
917 --Non constructive assumptions so far | 941 --Non constructive assumptions so far |
918 | 942 |
919 od→ord : HOD → Ordinal | 943 & : HOD → Ordinal |
920 ord→od : Ordinal → HOD | 944 * : Ordinal → HOD |
921 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | 945 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y |
922 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) | 946 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) |
923 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | 947 oiso : {x : HOD } → * ( & x ) ≡ x |
924 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 948 diso : {x : Ordinal } → & ( * x ) ≡ x |
925 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y | 949 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y |
926 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal | 950 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
927 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ | 951 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
928 | 952 |
929 --Axiom which have negation form | 953 --Axiom which have negation form |
953 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) | 977 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) |
954 | 978 |
955 The definition of Union in HOD is like this. | 979 The definition of Union in HOD is like this. |
956 | 980 |
957 Union : HOD → HOD | 981 Union : HOD → HOD |
958 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } | 982 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) } |
959 ; odmax = osuc (od→ord U) ; <odmax = ? } | 983 ; odmax = osuc (& U) ; <odmax = ? } |
960 | 984 |
961 The bound of Union is evident, but its proof is rather complicated. | 985 The bound of Union is evident, but its proof is rather complicated. |
962 | 986 |
963 Proof of validity is straight forward. | 987 Proof of validity is straight forward. |
964 | 988 |
965 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z | 989 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z |
966 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx | 990 union→ X z u xx not = ⊥-elim ( not (& u) ( record { proj1 = proj1 xx |
967 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) | 991 ; proj2 = subst ( λ k → odef k (& z)) (sym oiso) (proj2 xx) } )) |
968 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) | 992 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) |
969 union← X z UX∋z = FExists _ lemma UX∋z where | 993 union← X z UX∋z = FExists _ lemma UX∋z where |
970 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) | 994 lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) |
971 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } | 995 lemma {y} xx not = not (* y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } |
972 | 996 |
973 where | 997 where |
974 | 998 |
975 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) | 999 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) |
976 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) | 1000 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) |
997 | 1021 |
998 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has | 1022 In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has |
999 negation form of existential quantifier in the definition. | 1023 negation form of existential quantifier in the definition. |
1000 | 1024 |
1001 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD | 1025 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD |
1002 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } | 1026 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ & (ψ (* y ))))) } |
1003 | 1027 |
1004 in-codomain is a logical relation-ship, and it is written in OD. | 1028 in-codomain is a logical relation-ship, and it is written in OD. |
1005 | 1029 |
1006 Replace : HOD → (HOD → HOD) → HOD | 1030 Replace : HOD → (HOD → HOD) → HOD |
1007 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 } | 1031 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x } |
1008 ; odmax = rmax ; <odmax = rmax<} where | 1032 ; odmax = rmax ; <odmax = rmax<} where |
1009 rmax : Ordinal | 1033 rmax : Ordinal |
1010 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) | 1034 rmax = sup-o X (λ y X∋y → & (ψ (* y))) |
1011 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax | 1035 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax |
1012 rmax< lt = proj1 lt | 1036 rmax< lt = proj1 lt |
1013 | 1037 |
1014 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set. | 1038 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set. |
1015 | 1039 |
1053 | 1077 |
1054 Ord : ( a : Ordinal ) → OD | 1078 Ord : ( a : Ordinal ) → OD |
1055 Ord a = record { def = λ y → y o< a } | 1079 Ord a = record { def = λ y → y o< a } |
1056 | 1080 |
1057 Def : (A : OD ) → OD | 1081 Def : (A : OD ) → OD |
1058 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | 1082 Def A = Ord ( sup-o ( λ x → & ( ZFSubset A (* x )) ) ) |
1059 | 1083 |
1060 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). | 1084 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). |
1061 | 1085 |
1062 Power : OD → OD | 1086 Power : OD → OD |
1063 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) | 1087 Power A = Replace (Def (Ord (& A))) ( λ x → A ∩ x ) |
1064 | 1088 |
1065 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. | 1089 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. |
1066 | 1090 |
1067 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a ) | 1091 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a ) |
1068 | 1092 |
1083 | 1107 |
1084 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of | 1108 This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of |
1085 choice also becomes valid. | 1109 choice also becomes valid. |
1086 | 1110 |
1087 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD | 1111 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD |
1088 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 1112 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( & ( minimal x ne ) ) |
1089 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 1113 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (& y)) ∧ (def x (& y) ) |
1090 | 1114 |
1091 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). | 1115 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). |
1092 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. | 1116 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. |
1093 | 1117 |
1094 ε-induction : { ψ : HOD → Set (suc n)} | 1118 ε-induction : { ψ : HOD → Set (suc n)} |
1130 | 1154 |
1131 --Non constructive assumption in our model | 1155 --Non constructive assumption in our model |
1132 | 1156 |
1133 mapping between HOD and Ordinals | 1157 mapping between HOD and Ordinals |
1134 | 1158 |
1135 od→ord : HOD → Ordinal | 1159 & : HOD → Ordinal |
1136 ord→od : Ordinal → OD | 1160 * : Ordinal → OD |
1137 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x | 1161 oiso : {x : HOD } → * ( & x ) ≡ x |
1138 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 1162 diso : {x : Ordinal } → & ( * x ) ≡ x |
1139 c<→o< : {x y : HOD } → def y ( od→ord x ) → od→ord x o< od→ord y | 1163 c<→o< : {x y : HOD } → def y ( & x ) → & x o< & y |
1140 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) | 1164 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) |
1141 | 1165 |
1142 Equivalence on OD | 1166 Equivalence on OD |
1143 | 1167 |
1144 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y | 1168 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y |
1145 | 1169 |
1148 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal | 1172 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
1149 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ | 1173 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
1150 | 1174 |
1151 In order to have bounded ω, | 1175 In order to have bounded ω, |
1152 | 1176 |
1153 hod-ord< : {x : HOD} → od→ord x o< next (odmax x) | 1177 hod-ord< : {x : HOD} → & x o< next (odmax x) |
1154 | 1178 |
1155 Axiom of choice and strong axiom of regularity. | 1179 Axiom of choice and strong axiom of regularity. |
1156 | 1180 |
1157 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD | 1181 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD |
1158 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) | 1182 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) |
1159 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) | 1183 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) |
1184 | |
1185 --V | |
1186 | |
1187 The cumulative hierarchy | |
1188 V 0 := ∅ | |
1189 V α + 1 := P ( V α ) | |
1190 V α := ⋃ { V β | β < α } | |
1191 | |
1192 Using TransFinite induction | |
1193 | |
1194 V : ( β : Ordinal ) → HOD | |
1195 V β = TransFinite V1 β where | |
1196 V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD | |
1197 V1 x V0 with trio< x o∅ | |
1198 V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) | |
1199 V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅ | |
1200 V1 x V0 | tri> ¬a ¬b c with Oprev-p x | |
1201 V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) | |
1202 V1 x V0 | tri> ¬a ¬b c | no ¬p = | |
1203 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; | |
1204 odmax = x; <odmax = λ {x} lt → proj1 lt } | |
1205 | |
1206 In our system, clearly V ⊆ HOD。 | |
1207 | |
1208 --L | |
1209 | |
1210 The constructible Sets | |
1211 L 0 := ∅ | |
1212 L α + 1 := Df (L α) -- Definable Power Set | |
1213 V α := ⋃ { L β | β < α } | |
1214 | |
1215 What is Df? In our system, Power x is definable by Sup. | |
1216 | |
1217 record Definitions : Set (suc n) where | |
1218 field | |
1219 Definition : HOD → HOD | |
1220 | |
1221 open Definitions | |
1222 | |
1223 Df : Definitions → (x : HOD) → HOD | |
1224 Df D x = Power x ∩ Definition D x | |
1225 | |
1226 --L | |
1227 | |
1228 L : ( β : Ordinal ) → Definitions → HOD | |
1229 L β D = TransFinite L1 β where | |
1230 L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD | |
1231 L1 x L0 with trio< x o∅ | |
1232 L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) | |
1233 L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅ | |
1234 L1 x L0 | tri> ¬a ¬b c with Oprev-p x | |
1235 L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) | |
1236 L1 x L0 | tri> ¬a ¬b c | no ¬p = | |
1237 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ; | |
1238 odmax = x; <odmax = λ {x} lt → proj1 lt } | |
1239 | |
1240 --V=L | |
1241 | |
1242 V=L0 : Set (suc n) | |
1243 V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y } | |
1244 | |
1245 is obvious. Definitions should have some restrictions, such as it includes Nat. | |
1246 | |
1247 --Some other ... | |
1160 | 1248 |
1161 --So it this correct? | 1249 --So it this correct? |
1162 | 1250 |
1163 Our axiom are syntactically the same in the text book, but negations are slightly different. | 1251 Our axiom are syntactically the same in the text book, but negations are slightly different. |
1164 | 1252 |