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

comparison zf-in-agda.html @ 425:f7d66c84bc26

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 Wed, 05 Aug 2020 19:37:07 +0900
parents 4cbcf71b09c4
children
comparison
equal deleted inserted replaced
424:cc7909f86841 425:f7d66c84bc26
821 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.
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 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
823 <p> 823 <p>
824 824
825 <pre> 825 <pre>
826 ¬OD-order : ( od→ord : OD → Ordinal ) 826 ¬OD-order : ( &amp; : OD → Ordinal )
827 → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y) → ⊥ 827 → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( &amp; x ) → &amp; x o&lt; &amp; y) → ⊥
828 ¬OD-order od→ord ord→od c&lt;→o&lt; = ? 828 ¬OD-order &amp; * c&lt;→o&lt; = ?
829 829
830 </pre> 830 </pre>
831 Actualy we can prove this contrdction, so we need some restrctions on OD. 831 Actualy we can prove this contrdction, so we need some restrctions on OD.
832 <p> 832 <p>
833 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.
860 <h2><a name="content036">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>
861 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
862 <p> 862 <p>
863 863
864 <pre> 864 <pre>
865 od→ord : HOD → Ordinal 865 &amp; : HOD → Ordinal
866 ord→od : Ordinal → HOD 866 * : Ordinal → HOD
867 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 867 oiso : {x : HOD } → * ( &amp; x ) ≡ x
868 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 868 diso : {x : Ordinal } → &amp; ( * x ) ≡ x
869 869
870 </pre> 870 </pre>
871 we can check an HOD is an element of the OD using def. 871 we can check an HOD is an element of the OD using def.
872 <p> 872 <p>
873 A ∋ x can be define as follows. 873 A ∋ x can be define as follows.
874 <p> 874 <p>
875 875
876 <pre> 876 <pre>
877 _∋_ : ( A x : HOD ) → Set n 877 _∋_ : ( A x : HOD ) → Set n
878 _∋_ A x = def (od A) ( od→ord x ) 878 _∋_ A x = def (od A) ( &amp; x )
879 879
880 </pre> 880 </pre>
881 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then 881 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
882 <p> 882 <p>
883 883
884 <pre> 884 <pre>
885 A x = def A ( od→ord x ) = ψ (od→ord x) 885 A x = def A ( &amp; x ) = ψ (&amp; x)
886 886
887 </pre> 887 </pre>
888 They say the existing of the mappings can be proved in Classical Set Theory, but we 888 They say the existing of the mappings can be proved in Classical Set Theory, but we
889 simply assumes these non constructively. 889 simply assumes these non constructively.
890 <p> 890 <p>
896 <h2><a name="content037">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>
897 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 / ∋ ).
898 <p> 898 <p>
899 899
900 <pre> 900 <pre>
901 def (od y) ( od→ord x ) 901 def (od y) ( &amp; x )
902 902
903 </pre> 903 </pre>
904 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements 904 An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
905 have to be smaller than the corresponding ordinal of the containing OD. 905 have to be smaller than the corresponding ordinal of the containing OD.
906 We also assumes subset is always smaller. This is necessary to make a limit of Power Set. 906 We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
907 <p> 907 <p>
908 908
909 <pre> 909 <pre>
910 c&lt;→o&lt; : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y 910 c&lt;→o&lt; : {x y : HOD } → def (od y) ( &amp; x ) → &amp; x o&lt; &amp; y
911 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z) 911 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → &amp; y o&lt; osuc (&amp; z)
912 912
913 </pre> 913 </pre>
914 If wa assumes reverse order preservation, 914 If wa assumes reverse order preservation,
915 <p> 915 <p>
916 916
917 <pre> 917 <pre>
918 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (ord→od y) x 918 o&lt;→c&lt; : {n : Level} {x y : Ordinal } → x o&lt; y → def (* y) x
919 919
920 </pre> 920 </pre>
921 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model. 921 ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
922 <p> 922 <p>
923 <img src="fig/ODandOrdinals.svg"> 923 <img src="fig/ODandOrdinals.svg">
984 984
985 <pre> 985 <pre>
986 data infinite-d : ( x : Ordinal ) → Set n where 986 data infinite-d : ( x : Ordinal ) → Set n where
987 iφ : infinite-d o∅ 987 iφ : infinite-d o∅
988 isuc : {x : Ordinal } → infinite-d x → 988 isuc : {x : Ordinal } → infinite-d x →
989 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 989 infinite-d (&amp; ( Union (* x , (* x , * x ) ) ))
990 990
991 </pre> 991 </pre>
992 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.
993 <p> 993 <p>
994 994
1024 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.
1025 <p> 1025 <p>
1026 1026
1027 <pre> 1027 <pre>
1028 _,_ : HOD → HOD → HOD 1028 _,_ : HOD → HOD → HOD
1029 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ; &lt;odmax = ? } 1029 x , y = record { od = record { def = λ t → (t ≡ &amp; x ) ∨ ( t ≡ &amp; y ) } ; odmax = ? ; &lt;odmax = ? }
1030 1030
1031 </pre> 1031 </pre>
1032 It is easy to find out odmax from odmax of x and y. 1032 It is easy to find out odmax from odmax of x and y.
1033 <p> 1033 <p>
1034 ≡ 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.
1042 <pre> 1042 <pre>
1043 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 )
1044 pair→ x y t p = ? 1044 pair→ x y t p = ?
1045 1045
1046 </pre> 1046 </pre>
1047 In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) . 1047 In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ &amp; x ) ∨ ( t ≡ &amp; y ) .
1048 <p> 1048 <p>
1049 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). 1049 Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
1050 <p> 1050 <p>
1051 1051
1052 <pre> 1052 <pre>
1065 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable 1065 The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
1066 which type is 1066 which type is
1067 <p> 1067 <p>
1068 1068
1069 <pre> 1069 <pre>
1070 t≡x : od→ord t ≡ od→ord x 1070 t≡x : &amp; t ≡ &amp; x
1071 1071
1072 </pre> 1072 </pre>
1073 which is shown by an Agda command (C-C C-E : agda2-show-context ). 1073 which is shown by an Agda command (C-C C-E : agda2-show-context ).
1074 <p> 1074 <p>
1075 But we haven't defined == yet. 1075 But we haven't defined == yet.
1122 <p> 1122 <p>
1123 Actual proof is rather complicated. 1123 Actual proof is rather complicated.
1124 <p> 1124 <p>
1125 1125
1126 <pre> 1126 <pre>
1127 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 1127 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (* x))) d
1128 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 1128 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (* x))) d
1129 1129
1130 </pre> 1130 </pre>
1131 where 1131 where
1132 <p> 1132 <p>
1133 1133
1136 odef-iso refl t = t 1136 odef-iso refl t = t
1137 1137
1138 </pre> 1138 </pre>
1139 1139
1140 <hr/> 1140 <hr/>
1141 <h2><a name="content045">Validity of Axiom of Extensionality</a></h2> 1141 <h2><a name="content045">The uniqueness of HOD</a></h2>
1142 1142
1143 <p> 1143 <p>
1144 To prove extensionality or other we need ==→o≡.
1145 <p>
1146 Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
1147 We can calculate the minimum using sup if we have bound but it is tedius.
1148 Only Select has non minimum odmax. We have the same problem on 'def' itself, but we leave it, that is we assume the
1149 assumption of predicates of Agda have a unique form, it is something like the
1150 functional extensionality assumption.
1151 <p>
1152
1153 <hr/>
1154 <h2><a name="content046">Validity of Axiom of Extensionality</a></h2>
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 1155 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes
1145 <p> 1156 <p>
1146 1157
1147 <pre> 1158 <pre>
1148 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y 1159 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
1157 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 1168 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
1158 1169
1159 </pre> 1170 </pre>
1160 1171
1161 <hr/> 1172 <hr/>
1162 <h2><a name="content046">Axiom of infinity</a></h2> 1173 <h2><a name="content047">Axiom of infinity</a></h2>
1163 1174
1164 <p> 1175 <p>
1165 It means it has ω as a ZF Set. It is ususally written like this. 1176 It means it has ω as a ZF Set. It is ususally written like this.
1166 <p> 1177 <p>
1167 1178
1178 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite 1189 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
1179 1190
1180 </pre> 1191 </pre>
1181 1192
1182 <hr/> 1193 <hr/>
1183 <h2><a name="content047">ω in HOD</a></h2> 1194 <h2><a name="content048">ω in HOD</a></h2>
1184 1195
1185 <p> 1196 <p>
1186 To define an OD which arrows od→ord (Union (x , (x , x))) as a predicate, we can use Agda data structure. 1197 To define an OD which arrows &amp; (Union (x , (x , x))) as a predicate, we can use Agda data structure.
1187 <p> 1198 <p>
1188 1199
1189 <pre> 1200 <pre>
1190 data infinite-d : ( x : Ordinal ) → Set n where 1201 data infinite-d : ( x : Ordinal ) → Set n where
1191 iφ : infinite-d o∅ 1202 iφ : infinite-d o∅
1192 isuc : {x : Ordinal } → infinite-d x → 1203 isuc : {x : Ordinal } → infinite-d x →
1193 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 1204 infinite-d (&amp; ( Union (* x , (* x , * x ) ) ))
1194 1205
1195 </pre> 1206 </pre>
1196 It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now 1207 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. 1208 we can define HOD like this.
1198 <p> 1209 <p>
1200 <pre> 1211 <pre>
1201 infinite : HOD 1212 infinite : HOD
1202 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; &lt;odmax = ? } 1213 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; &lt;odmax = ? }
1203 1214
1204 </pre> 1215 </pre>
1205 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which 1216 So what is the bound of ω? Analyzing the definition, it depends on the value of &amp; (x , x), which
1206 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal. 1217 cannot know the aboslute value. This is because we don't have constructive definition of &amp; : HOD → Ordinal.
1207 <p> 1218 <p>
1208 1219
1209 <hr/> 1220 <hr/>
1210 <h2><a name="content048">HOD Ordrinal mapping</a></h2> 1221 <h2><a name="content049">HOD and Agda data structure</a></h2>
1222 We may have
1223 <p>
1224
1225 <pre>
1226 a HOD &lt;=&gt; Agda Data Strucure
1227
1228 </pre>
1229 as a data in Agda. Ex.
1230 <p>
1231
1232 <pre>
1233 data ord-pair : (p : Ordinal) → Set n where
1234 pair : (x y : Ordinal ) → ord-pair ( &amp; ( &lt; * x , * y &gt; ) )
1235 ZFProduct : OD
1236 ZFProduct = record { def = λ x → ord-pair x }
1237 pi1 : { p : Ordinal } → ord-pair p → Ordinal
1238 pi1 ( pair x y) = x
1239 π1 : { p : HOD } → def ZFProduct (&amp; p) → HOD
1240 π1 lt = * (pi1 lt )
1241 p-iso : { x : HOD } → (p : def ZFProduct (&amp; x) ) → &lt; π1 p , π2 p &gt; ≡ x
1242 p-iso {x} p = ord≡→≡ (op-iso p)
1243
1244 </pre>
1245
1246 <hr/>
1247 <h2><a name="content050">HOD Ordrinal mapping</a></h2>
1248
1249 <p>
1211 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger. 1250 We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger.
1212 The address of HOD can be larger at least it have to be larger than the content's address. 1251 The address of HOD can be larger at least it have to be larger than the content's address.
1213 We only have a relative ordering such as 1252 We only have a relative ordering such as
1214 <p> 1253 <p>
1215 1254
1216 <pre> 1255 <pre>
1217 pair-xx&lt;xy : {x y : HOD} → od→ord (x , x) o&lt; osuc (od→ord (x , y) ) 1256 pair-xx&lt;xy : {x y : HOD} → &amp; (x , x) o&lt; osuc (&amp; (x , y) )
1218 pair&lt;y : {x y : HOD } → y ∋ x → od→ord (x , x) o&lt; osuc (od→ord y) 1257 pair&lt;y : {x y : HOD } → y ∋ x → &amp; (x , x) o&lt; osuc (&amp; y)
1219 1258
1220 </pre> 1259 </pre>
1221 Basicaly, we cannot know the concrete address of HOD other than empty set. 1260 Basicaly, we cannot know the concrete address of HOD other than empty set.
1222 <p> 1261 <p>
1223 <img src="fig/address-of-HOD.svg"> 1262 <img src="fig/address-of-HOD.svg">
1224 1263
1225 <p> 1264 <p>
1226 1265
1227 <hr/> 1266 <hr/>
1228 <h2><a name="content049">Possible restriction on HOD</a></h2> 1267 <h2><a name="content051">Possible restriction on HOD</a></h2>
1229 We need some restriction on the HOD-Ordinal mapping. Simple one is this. 1268 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
1230 <p> 1269 <p>
1231 1270
1232 <pre> 1271 <pre>
1233 ωmax : Ordinal 1272 ωmax : Ordinal
1237 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be 1276 It depends on infinite-d and put no assuption on the other similar construction. A more general one may be
1238 <p> 1277 <p>
1239 1278
1240 <pre> 1279 <pre>
1241 hod-ord&lt; : {x : HOD } → Set n 1280 hod-ord&lt; : {x : HOD } → Set n
1242 hod-ord&lt; {x} = od→ord x o&lt; next (odmax x) 1281 hod-ord&lt; {x} = &amp; x o&lt; next (odmax x)
1243 1282
1244 </pre> 1283 </pre>
1245 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and 1284 next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and
1246 its bound. 1285 its bound.
1247 <p> 1286 <p>
1248 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound. 1287 In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound.
1249 This is the reason of necessity of Axiom of infinite. 1288 This is the reason of necessity of Axiom of infinite.
1250 <p> 1289 <p>
1251 1290
1252 <hr/> 1291 <hr/>
1253 <h2><a name="content050">increment pase of address of HOD</a></h2> 1292 <h2><a name="content052">increment pase of address of HOD</a></h2>
1254 Assuming, hod-ord&lt; , we have 1293 Assuming, hod-ord&lt; , we have
1255 <p> 1294 <p>
1256 1295
1257 <pre> 1296 <pre>
1258 pair-ord&lt; : {x : HOD } → ( {y : HOD } → od→ord y o&lt; next (odmax y) ) → od→ord ( x , x ) o&lt; next (od→ord x) 1297 pair-ord&lt; : {x : HOD } → ( {y : HOD } → &amp; y o&lt; next (odmax y) ) → &amp; ( x , x ) o&lt; next (&amp; x)
1259 pair-ord&lt; {x} ho&lt; = subst (λ k → od→ord (x , x) o&lt; k ) lemmab0 lemmab1 where 1298 pair-ord&lt; {x} ho&lt; = subst (λ k → &amp; (x , x) o&lt; k ) lemmab0 lemmab1 where
1260 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) 1299 lemmab0 : next (odmax (x , x)) ≡ next (&amp; x)
1261 1300
1262 </pre> 1301 </pre>
1263 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove 1302 So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
1264 <p> 1303 <p>
1265 1304
1266 <pre> 1305 <pre>
1267 infinite-bound : ({x : HOD} → od→ord x o&lt; next (odmax x)) → {y : Ordinal} → infinite-d y → y o&lt; next o∅ 1306 infinite-bound : ({x : HOD} → &amp; x o&lt; next (odmax x)) → {y : Ordinal} → infinite-d y → y o&lt; next o∅
1268 1307
1269 </pre> 1308 </pre>
1270 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x), c&lt;→o&lt; can be drived from ⊆→o≤ . 1309 We also notice that if we have &amp; (x , x) ≡ osuc (&amp; x), c&lt;→o&lt; can be drived from ⊆→o≤ .
1271 <p> 1310 <p>
1272 1311
1273 <pre> 1312 <pre>
1274 ⊆→o≤→c&lt;→o&lt; : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) 1313 ⊆→o≤→c&lt;→o&lt; : ({x : HOD} → &amp; (x , x) ≡ osuc (&amp; x) )
1275 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z) ) 1314 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → &amp; y o&lt; osuc (&amp; z) )
1276 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y 1315 → {x y : HOD } → def (od y) ( &amp; x ) → &amp; x o&lt; &amp; y
1277 1316
1278 </pre> 1317 </pre>
1279 1318
1280 <hr/> 1319 <hr/>
1281 <h2><a name="content051">Non constructive assumptions so far</a></h2> 1320 <h2><a name="content053">Non constructive assumptions so far</a></h2>
1282 1321
1283 <p> 1322 <p>
1284 1323
1285 <pre> 1324 <pre>
1286 od→ord : HOD → Ordinal 1325 &amp; : HOD → Ordinal
1287 ord→od : Ordinal → HOD 1326 * : Ordinal → HOD
1288 c&lt;→o&lt; : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y 1327 c&lt;→o&lt; : {x y : HOD } → def (od y) ( &amp; x ) → &amp; x o&lt; &amp; y
1289 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z) 1328 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → &amp; y o&lt; osuc (&amp; z)
1290 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 1329 oiso : {x : HOD } → * ( &amp; x ) ≡ x
1291 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 1330 diso : {x : Ordinal } → &amp; ( * x ) ≡ x
1292 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y 1331 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
1293 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal 1332 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
1294 sup-o&lt; : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o&lt; sup-o A ψ 1333 sup-o&lt; : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o&lt; sup-o A ψ
1295 1334
1296 </pre> 1335 </pre>
1297 1336
1298 <hr/> 1337 <hr/>
1299 <h2><a name="content052">Axiom which have negation form</a></h2> 1338 <h2><a name="content054">Axiom which have negation form</a></h2>
1300 1339
1301 <p> 1340 <p>
1302 1341
1303 <pre> 1342 <pre>
1304 Union, Selection 1343 Union, Selection
1318 </pre> 1357 </pre>
1319 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. 1358 If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
1320 <p> 1359 <p>
1321 1360
1322 <hr/> 1361 <hr/>
1323 <h2><a name="content053">Union </a></h2> 1362 <h2><a name="content055">Union </a></h2>
1324 The original form of the Axiom of Union is 1363 The original form of the Axiom of Union is
1325 <p> 1364 <p>
1326 1365
1327 <pre> 1366 <pre>
1328 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) 1367 ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
1339 The definition of Union in HOD is like this. 1378 The definition of Union in HOD is like this.
1340 <p> 1379 <p>
1341 1380
1342 <pre> 1381 <pre>
1343 Union : HOD → HOD 1382 Union : HOD → HOD
1344 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } 1383 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) }
1345 ; odmax = osuc (od→ord U) ; &lt;odmax = ? } 1384 ; odmax = osuc (&amp; U) ; &lt;odmax = ? }
1346 1385
1347 </pre> 1386 </pre>
1348 The bound of Union is evident, but its proof is rather complicated. 1387 The bound of Union is evident, but its proof is rather complicated.
1349 <p> 1388 <p>
1350 Proof of validity is straight forward. 1389 Proof of validity is straight forward.
1351 <p> 1390 <p>
1352 1391
1353 <pre> 1392 <pre>
1354 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 1393 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
1355 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx 1394 union→ X z u xx not = ⊥-elim ( not (&amp; u) ( record { proj1 = proj1 xx
1356 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) 1395 ; proj2 = subst ( λ k → odef k (&amp; z)) (sym oiso) (proj2 xx) } ))
1357 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) 1396 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
1358 union← X z UX∋z = FExists _ lemma UX∋z where 1397 union← X z UX∋z = FExists _ lemma UX∋z where
1359 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) 1398 lemma : {y : Ordinal} → odef X y ∧ odef (* y) (&amp; z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
1360 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 1399 lemma {y} xx not = not (* y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
1361 1400
1362 </pre> 1401 </pre>
1363 where 1402 where
1364 <p> 1403 <p>
1365 1404
1373 </pre> 1412 </pre>
1374 which checks existence using contra-position. 1413 which checks existence using contra-position.
1375 <p> 1414 <p>
1376 1415
1377 <hr/> 1416 <hr/>
1378 <h2><a name="content054">Axiom of replacement</a></h2> 1417 <h2><a name="content056">Axiom of replacement</a></h2>
1379 We can replace the elements of a set by a function and it becomes a set. From the book, 1418 We can replace the elements of a set by a function and it becomes a set. From the book,
1380 <p> 1419 <p>
1381 1420
1382 <pre> 1421 <pre>
1383 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 1422 ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
1402 negation form of existential quantifier in the definition. 1441 negation form of existential quantifier in the definition.
1403 <p> 1442 <p>
1404 1443
1405 <pre> 1444 <pre>
1406 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD 1445 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
1407 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } 1446 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ &amp; (ψ (* y ))))) }
1408 1447
1409 </pre> 1448 </pre>
1410 in-codomain is a logical relation-ship, and it is written in OD. 1449 in-codomain is a logical relation-ship, and it is written in OD.
1411 <p> 1450 <p>
1412 1451
1413 <pre> 1452 <pre>
1414 Replace : HOD → (HOD → HOD) → HOD 1453 Replace : HOD → (HOD → HOD) → HOD
1415 Replace X ψ = record { od = record { def = λ x → (x o&lt; sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } 1454 Replace X ψ = record { od = record { def = λ x → (x o&lt; sup-o X (λ y X∋y → &amp; (ψ (* y)))) ∧ def (in-codomain X ψ) x }
1416 ; odmax = rmax ; &lt;odmax = rmax&lt;} where 1455 ; odmax = rmax ; &lt;odmax = rmax&lt;} where
1417 rmax : Ordinal 1456 rmax : Ordinal
1418 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) 1457 rmax = sup-o X (λ y X∋y → &amp; (ψ (* y)))
1419 rmax&lt; : {y : Ordinal} → (y o&lt; rmax) ∧ def (in-codomain X ψ) y → y o&lt; rmax 1458 rmax&lt; : {y : Ordinal} → (y o&lt; rmax) ∧ def (in-codomain X ψ) y → y o&lt; rmax
1420 rmax&lt; lt = proj1 lt 1459 rmax&lt; lt = proj1 lt
1421 1460
1422 </pre> 1461 </pre>
1423 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set. 1462 The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set.
1424 <p> 1463 <p>
1425 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship. 1464 Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship.
1426 <p> 1465 <p>
1427 1466
1428 <hr/> 1467 <hr/>
1429 <h2><a name="content055">Validity of Power Set Axiom</a></h2> 1468 <h2><a name="content057">Validity of Power Set Axiom</a></h2>
1430 The original Power Set Axiom is this. 1469 The original Power Set Axiom is this.
1431 <p> 1470 <p>
1432 1471
1433 <pre> 1472 <pre>
1434 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 1473 ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
1482 1521
1483 <pre> 1522 <pre>
1484 Ord : ( a : Ordinal ) → OD 1523 Ord : ( a : Ordinal ) → OD
1485 Ord a = record { def = λ y → y o&lt; a } 1524 Ord a = record { def = λ y → y o&lt; a }
1486 Def : (A : OD ) → OD 1525 Def : (A : OD ) → OD
1487 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 1526 Def A = Ord ( sup-o ( λ x → &amp; ( ZFSubset A (* x )) ) )
1488 1527
1489 </pre> 1528 </pre>
1490 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). 1529 This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
1491 <p> 1530 <p>
1492 1531
1493 <pre> 1532 <pre>
1494 Power : OD → OD 1533 Power : OD → OD
1495 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 1534 Power A = Replace (Def (Ord (&amp; A))) ( λ x → A ∩ x )
1496 1535
1497 </pre> 1536 </pre>
1498 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. 1537 Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
1499 <p> 1538 <p>
1500 1539
1517 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 1556 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
1518 1557
1519 </pre> 1558 </pre>
1520 1559
1521 <hr/> 1560 <hr/>
1522 <h2><a name="content056">Axiom of regularity, Axiom of choice, ε-induction</a></h2> 1561 <h2><a name="content058">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
1523 1562
1524 <p> 1563 <p>
1525 Axiom of regularity requires non self intersectable elements (which is called minimum), if we 1564 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
1526 replace it by a function, it becomes a choice function. It makes axiom of choice valid. 1565 replace it by a function, it becomes a choice function. It makes axiom of choice valid.
1527 <p> 1566 <p>
1529 choice also becomes valid. 1568 choice also becomes valid.
1530 <p> 1569 <p>
1531 1570
1532 <pre> 1571 <pre>
1533 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD 1572 minimal : (x : HOD ) → ¬ (x == od∅ )→ OD
1534 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) 1573 x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( &amp; ( minimal x ne ) )
1535 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) 1574 minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (&amp; y)) ∧ (def x (&amp; y) )
1536 1575
1537 </pre> 1576 </pre>
1538 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). 1577 We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
1539 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. 1578 Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
1540 <p> 1579 <p>
1564 </pre> 1603 </pre>
1565 It does not requires ∅ ∉ X . 1604 It does not requires ∅ ∉ X .
1566 <p> 1605 <p>
1567 1606
1568 <hr/> 1607 <hr/>
1569 <h2><a name="content057">Axiom of choice and Law of Excluded Middle</a></h2> 1608 <h2><a name="content059">Axiom of choice and Law of Excluded Middle</a></h2>
1570 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, 1609 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
1571 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, 1610 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
1572 but it requires law of the exclude middle. 1611 but it requires law of the exclude middle.
1573 <p> 1612 <p>
1574 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can 1613 Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
1584 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice 1623 We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
1585 and Law of Excluded Middle is equivalent in our mode. 1624 and Law of Excluded Middle is equivalent in our mode.
1586 <p> 1625 <p>
1587 1626
1588 <hr/> 1627 <hr/>
1589 <h2><a name="content058">Relation-ship among ZF axiom</a></h2> 1628 <h2><a name="content060">Relation-ship among ZF axiom</a></h2>
1590 <img src="fig/axiom-dependency.svg"> 1629 <img src="fig/axiom-dependency.svg">
1591 1630
1592 <p> 1631 <p>
1593 1632
1594 <hr/> 1633 <hr/>
1595 <h2><a name="content059">Non constructive assumption in our model</a></h2> 1634 <h2><a name="content061">Non constructive assumption in our model</a></h2>
1596 mapping between HOD and Ordinals 1635 mapping between HOD and Ordinals
1597 <p> 1636 <p>
1598 1637
1599 <pre> 1638 <pre>
1600 od→ord : HOD → Ordinal 1639 &amp; : HOD → Ordinal
1601 ord→od : Ordinal → OD 1640 * : Ordinal → OD
1602 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 1641 oiso : {x : HOD } → * ( &amp; x ) ≡ x
1603 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 1642 diso : {x : Ordinal } → &amp; ( * x ) ≡ x
1604 c&lt;→o&lt; : {x y : HOD } → def y ( od→ord x ) → od→ord x o&lt; od→ord y 1643 c&lt;→o&lt; : {x y : HOD } → def y ( &amp; x ) → &amp; x o&lt; &amp; y
1605 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z) 1644 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → &amp; y o&lt; osuc (&amp; z)
1606 1645
1607 </pre> 1646 </pre>
1608 Equivalence on OD 1647 Equivalence on OD
1609 <p> 1648 <p>
1610 1649
1622 </pre> 1661 </pre>
1623 In order to have bounded ω, 1662 In order to have bounded ω,
1624 <p> 1663 <p>
1625 1664
1626 <pre> 1665 <pre>
1627 hod-ord&lt; : {x : HOD} → od→ord x o&lt; next (odmax x) 1666 hod-ord&lt; : {x : HOD} → &amp; x o&lt; next (odmax x)
1628 1667
1629 </pre> 1668 </pre>
1630 Axiom of choice and strong axiom of regularity. 1669 Axiom of choice and strong axiom of regularity.
1631 <p> 1670 <p>
1632 1671
1633 <pre> 1672 <pre>
1634 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD 1673 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
1635 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) 1674 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( &amp; ( minimal x ne ) )
1636 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) 1675 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (&amp; y)) ∧ (odef x (&amp; y) )
1637 1676
1638 </pre> 1677 </pre>
1639 1678
1640 <hr/> 1679 <hr/>
1641 <h2><a name="content060">So it this correct?</a></h2> 1680 <h2><a name="content062">V </a></h2>
1642 1681
1643 <p> 1682 <p>
1683 The cumulative hierarchy
1684 <pre>
1685 V 0 := ∅
1686 V α + 1 := P ( V α )
1687 V α := ⋃ { V β | β &lt; α }
1688
1689 </pre>
1690 Using TransFinite induction
1691 <p>
1692
1693 <pre>
1694 V : ( β : Ordinal ) → HOD
1695 V β = TransFinite V1 β where
1696 V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o&lt; x → HOD ) → HOD
1697 V1 x V0 with trio&lt; x o∅
1698 V1 x V0 | tri&lt; a ¬b ¬c = ⊥-elim ( ¬x&lt;0 a)
1699 V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
1700 V1 x V0 | tri&gt; ¬a ¬b c with Oprev-p x
1701 V1 x V0 | tri&gt; ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o&lt; k) (Oprev.oprev=x p) &lt;-osuc ))
1702 V1 x V0 | tri&gt; ¬a ¬b c | no ¬p =
1703 record { od = record { def = λ y → (y o&lt; x ) ∧ ((lt : y o&lt; x ) → odef (V0 y lt) x ) } ;
1704 odmax = x; &lt;odmax = λ {x} lt → proj1 lt }
1705
1706 </pre>
1707 In our system, clearly V ⊆ HOD。
1708 <p>
1709
1710 <hr/>
1711 <h2><a name="content063">L</a></h2>
1712 The constructible Sets
1713 <pre>
1714 L 0 := ∅
1715 L α + 1 := Df (L α) -- Definable Power Set
1716 V α := ⋃ { L β | β &lt; α }
1717
1718 </pre>
1719 What is Df? In our system, Power x is definable by Sup.
1720 <p>
1721
1722 <pre>
1723 record Definitions : Set (suc n) where
1724 field
1725 Definition : HOD → HOD
1726 open Definitions
1727 Df : Definitions → (x : HOD) → HOD
1728 Df D x = Power x ∩ Definition D x
1729
1730 </pre>
1731
1732 <hr/>
1733 <h2><a name="content064">L</a></h2>
1734
1735 <p>
1736
1737 <pre>
1738 L : ( β : Ordinal ) → Definitions → HOD
1739 L β D = TransFinite L1 β where
1740 L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o&lt; x → HOD ) → HOD
1741 L1 x L0 with trio&lt; x o∅
1742 L1 x L0 | tri&lt; a ¬b ¬c = ⊥-elim ( ¬x&lt;0 a)
1743 L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
1744 L1 x L0 | tri&gt; ¬a ¬b c with Oprev-p x
1745 L1 x L0 | tri&gt; ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o&lt; k) (Oprev.oprev=x p) &lt;-osuc ))
1746 L1 x L0 | tri&gt; ¬a ¬b c | no ¬p =
1747 record { od = record { def = λ y → (y o&lt; x ) ∧ ((lt : y o&lt; x ) → odef (L0 y lt) x ) } ;
1748 odmax = x; &lt;odmax = λ {x} lt → proj1 lt }
1749
1750 </pre>
1751
1752 <hr/>
1753 <h2><a name="content065">V=L</a></h2>
1754
1755 <p>
1756
1757 <pre>
1758 V=L0 : Set (suc n)
1759 V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
1760
1761 </pre>
1762 is obvious. Definitions should have some restrictions, such as it includes Nat.
1763 <p>
1764
1765 <hr/>
1766 <h2><a name="content066">Some other ...</a></h2>
1767
1768 <hr/>
1769 <h2><a name="content067">So it this correct?</a></h2>
1644 Our axiom are syntactically the same in the text book, but negations are slightly different. 1770 Our axiom are syntactically the same in the text book, but negations are slightly different.
1645 <p> 1771 <p>
1646 If we assumes excluded middle, these are exactly same. 1772 If we assumes excluded middle, these are exactly same.
1647 <p> 1773 <p>
1648 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. 1774 Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
1656 <p> 1782 <p>
1657 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. 1783 Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
1658 <p> 1784 <p>
1659 1785
1660 <hr/> 1786 <hr/>
1661 <h2><a name="content061">How to use Agda Set Theory</a></h2> 1787 <h2><a name="content068">How to use Agda Set Theory</a></h2>
1662 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be 1788 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
1663 postulated or assuming law of excluded middle. 1789 postulated or assuming law of excluded middle.
1664 <p> 1790 <p>
1665 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check 1791 Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
1666 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. 1792 these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
1667 <p> 1793 <p>
1668 ZF record itself is not necessary, for example, topology theory without ZF can be possible. 1794 ZF record itself is not necessary, for example, topology theory without ZF can be possible.
1669 <p> 1795 <p>
1670 1796
1671 <hr/> 1797 <hr/>
1672 <h2><a name="content062">Topos and Set Theory</a></h2> 1798 <h2><a name="content069">Topos and Set Theory</a></h2>
1673 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a 1799 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
1674 sub-object classifier. 1800 sub-object classifier.
1675 <p> 1801 <p>
1676 Topos itself is model of intuitionistic logic. 1802 Topos itself is model of intuitionistic logic.
1677 <p> 1803 <p>
1685 <p> 1811 <p>
1686 Our Agda model is a proof theoretic version of it. 1812 Our Agda model is a proof theoretic version of it.
1687 <p> 1813 <p>
1688 1814
1689 <hr/> 1815 <hr/>
1690 <h2><a name="content063">Cardinal number and Continuum hypothesis</a></h2> 1816 <h2><a name="content070">Cardinal number and Continuum hypothesis</a></h2>
1691 Axiom of choice is required to define cardinal number 1817 Axiom of choice is required to define cardinal number
1692 <p> 1818 <p>
1693 definition of cardinal number is not yet done 1819 definition of cardinal number is not yet done
1694 <p> 1820 <p>
1695 definition of filter is not yet done 1821 definition of filter is not yet done
1703 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) 1829 continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
1704 1830
1705 </pre> 1831 </pre>
1706 1832
1707 <hr/> 1833 <hr/>
1708 <h2><a name="content064">Filter</a></h2> 1834 <h2><a name="content071">Filter</a></h2>
1709 1835
1710 <p> 1836 <p>
1711 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number 1837 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
1712 is depends on axiom of choice. 1838 is depends on axiom of choice.
1713 <p> 1839 <p>
1726 <p> 1852 <p>
1727 This may be simpler than classical forcing theory ( not yet done). 1853 This may be simpler than classical forcing theory ( not yet done).
1728 <p> 1854 <p>
1729 1855
1730 <hr/> 1856 <hr/>
1731 <h2><a name="content065">Programming Mathematics</a></h2> 1857 <h2><a name="content072">Programming Mathematics</a></h2>
1732 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical 1858 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
1733 structure are 1859 structure are
1734 <p> 1860 <p>
1735 1861
1736 <pre> 1862 <pre>
1751 </pre> 1877 </pre>
1752 are proved in Agda. 1878 are proved in Agda.
1753 <p> 1879 <p>
1754 1880
1755 <hr/> 1881 <hr/>
1756 <h2><a name="content066">link</a></h2> 1882 <h2><a name="content073">link</a></h2>
1757 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> 1883 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>
1758 <p> 1884 <p>
1759 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 1885 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
1760 </a> 1886 </a>
1761 <p> 1887 <p>
1816 <li><a href="#content040"> Pure logical axioms</a> 1942 <li><a href="#content040"> Pure logical axioms</a>
1817 <li><a href="#content041"> Axiom of Pair</a> 1943 <li><a href="#content041"> Axiom of Pair</a>
1818 <li><a href="#content042"> pair in OD</a> 1944 <li><a href="#content042"> pair in OD</a>
1819 <li><a href="#content043"> Validity of Axiom of Pair</a> 1945 <li><a href="#content043"> Validity of Axiom of Pair</a>
1820 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a> 1946 <li><a href="#content044"> Equality of OD and Axiom of Extensionality </a>
1821 <li><a href="#content045"> Validity of Axiom of Extensionality</a> 1947 <li><a href="#content045"> The uniqueness of HOD</a>
1822 <li><a href="#content046"> Axiom of infinity</a> 1948 <li><a href="#content046"> Validity of Axiom of Extensionality</a>
1823 <li><a href="#content047"> ω in HOD</a> 1949 <li><a href="#content047"> Axiom of infinity</a>
1824 <li><a href="#content048"> HOD Ordrinal mapping</a> 1950 <li><a href="#content048"> ω in HOD</a>
1825 <li><a href="#content049"> Possible restriction on HOD</a> 1951 <li><a href="#content049"> HOD and Agda data structure</a>
1826 <li><a href="#content050"> increment pase of address of HOD</a> 1952 <li><a href="#content050"> HOD Ordrinal mapping</a>
1827 <li><a href="#content051"> Non constructive assumptions so far</a> 1953 <li><a href="#content051"> Possible restriction on HOD</a>
1828 <li><a href="#content052"> Axiom which have negation form</a> 1954 <li><a href="#content052"> increment pase of address of HOD</a>
1829 <li><a href="#content053"> Union </a> 1955 <li><a href="#content053"> Non constructive assumptions so far</a>
1830 <li><a href="#content054"> Axiom of replacement</a> 1956 <li><a href="#content054"> Axiom which have negation form</a>
1831 <li><a href="#content055"> Validity of Power Set Axiom</a> 1957 <li><a href="#content055"> Union </a>
1832 <li><a href="#content056"> Axiom of regularity, Axiom of choice, ε-induction</a> 1958 <li><a href="#content056"> Axiom of replacement</a>
1833 <li><a href="#content057"> Axiom of choice and Law of Excluded Middle</a> 1959 <li><a href="#content057"> Validity of Power Set Axiom</a>
1834 <li><a href="#content058"> Relation-ship among ZF axiom</a> 1960 <li><a href="#content058"> Axiom of regularity, Axiom of choice, ε-induction</a>
1835 <li><a href="#content059"> Non constructive assumption in our model</a> 1961 <li><a href="#content059"> Axiom of choice and Law of Excluded Middle</a>
1836 <li><a href="#content060"> So it this correct?</a> 1962 <li><a href="#content060"> Relation-ship among ZF axiom</a>
1837 <li><a href="#content061"> How to use Agda Set Theory</a> 1963 <li><a href="#content061"> Non constructive assumption in our model</a>
1838 <li><a href="#content062"> Topos and Set Theory</a> 1964 <li><a href="#content062"> V </a>
1839 <li><a href="#content063"> Cardinal number and Continuum hypothesis</a> 1965 <li><a href="#content063"> L</a>
1840 <li><a href="#content064"> Filter</a> 1966 <li><a href="#content064"> L</a>
1841 <li><a href="#content065"> Programming Mathematics</a> 1967 <li><a href="#content065"> V=L</a>
1842 <li><a href="#content066"> link</a> 1968 <li><a href="#content066"> Some other ...</a>
1969 <li><a href="#content067"> So it this correct?</a>
1970 <li><a href="#content068"> How to use Agda Set Theory</a>
1971 <li><a href="#content069"> Topos and Set Theory</a>
1972 <li><a href="#content070"> Cardinal number and Continuum hypothesis</a>
1973 <li><a href="#content071"> Filter</a>
1974 <li><a href="#content072"> Programming Mathematics</a>
1975 <li><a href="#content073"> link</a>
1843 </ol> 1976 </ol>
1844 1977
1845 <hr/> Shinji KONO / Fri Jul 17 13:42:02 2020 1978 <hr/> Shinji KONO / Tue Aug 4 18:09:41 2020
1846 </body></html> 1979 </body></html>