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

comparison zf-in-agda.ind @ 361:4cbcf71b09c4

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 Fri, 17 Jul 2020 16:33:30 +0900
parents 5e22b23ee3fd
children aad9249d1e8f
comparison
equal deleted inserted replaced
360:2a8a51375e49 361:4cbcf71b09c4
669 HOD / Hereditarily Ordinal Definable 669 HOD / Hereditarily Ordinal Definable
670 OD / equational formula on Ordinals 670 OD / equational formula on Ordinals
671 Agda Set / Type / it also has a level 671 Agda Set / Type / it also has a level
672 672
673 673
674 --Fixes on ZF to intuitionistic logic 674 --Fixing ZF axom to fit intuitionistic logic
675 675
676 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define 676 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
677 ZF axioms in Agda. 677 ZF axioms in Agda.
678 678
679 It may not valid in our model. We have to debug it. 679 It may not valid in our model. We have to debug it.
852 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? } 852 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? }
853 853
854 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which 854 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which
855 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal. 855 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal.
856 856
857 --HOD Ordrinal mapping
858
859 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger.
860 The address of HOD can be larger at least it have to be larger than the content's address.
861 We only have a relative ordering such as
862
863 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
864 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y)
865
866 Basicaly, we cannot know the concrete address of HOD other than empty set.
867
868 <center><img src="fig/address-of-HOD.svg"></center>
869
870 --Possible restriction on HOD
871
857 We need some restriction on the HOD-Ordinal mapping. Simple one is this. 872 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
858 873
859 ωmax : Ordinal 874 ωmax : Ordinal
860 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax 875 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
861 876
870 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. 885 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound.
871 This is the reason of necessity of Axiom of infinite. 886 This is the reason of necessity of Axiom of infinite.
872 887
873 --increment pase of address of HOD 888 --increment pase of address of HOD
874 889
875 The address of HOD may have obvious bound, but it is defined in a relative way. 890 Assuming, hod-ord< , we have
876
877 pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
878 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y)
879
880 Basicaly, we cannot know the concrete address of HOD other than empty set.
881
882 Assuming, previous assuption, we have
883 891
884 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) 892 pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
885 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where 893 pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where
886 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) 894 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
887 895
888 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. 896 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
897
898 infinite-bound : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
889 899
890 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c<→o< can be drived from ⊆→o≤ . 900 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c<→o< can be drived from ⊆→o≤ .
891 901
892 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) 902 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
893 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) 903 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )