Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 338:bca043423554
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Jul 2020 12:32:42 +0900 |
parents | daafa2213dd2 |
children | feb0fcc430a9 |
comparison
equal
deleted
inserted
replaced
337:de2c472bcbcd | 338:bca043423554 |
---|---|
101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y | 102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y |
103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal | 103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ | 104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
105 | 105 |
106 -- another form of infinite | |
107 -- pair-ord< : {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x) | |
108 | |
106 postulate odAxiom : ODAxiom | 109 postulate odAxiom : ODAxiom |
107 open ODAxiom odAxiom | 110 open ODAxiom odAxiom |
108 | 111 |
109 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD | 112 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD |
110 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ | 113 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ |
210 is-o∅ x | tri< a ¬b ¬c = no ¬b | 213 is-o∅ x | tri< a ¬b ¬c = no ¬b |
211 is-o∅ x | tri≈ ¬a b ¬c = yes b | 214 is-o∅ x | tri≈ ¬a b ¬c = yes b |
212 is-o∅ x | tri> ¬a ¬b c = no ¬b | 215 is-o∅ x | tri> ¬a ¬b c = no ¬b |
213 | 216 |
214 -- the pair | 217 -- the pair |
215 _,_ : HOD → HOD → HOD | 218 _,_ : HOD → HOD → HOD |
216 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where | 219 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where |
217 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) | 220 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) |
218 lemma {t} (case1 refl) = omax-x _ _ | 221 lemma {t} (case1 refl) = omax-x _ _ |
219 lemma {t} (case2 refl) = omax-y _ _ | 222 lemma {t} (case2 refl) = omax-y _ _ |
220 | 223 |
245 pair<y {x} {y} y∋x = ⊆→o≤ lemma where | 248 pair<y {x} {y} y∋x = ⊆→o≤ lemma where |
246 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z | 249 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z |
247 lemma (case1 refl) = y∋x | 250 lemma (case1 refl) = y∋x |
248 lemma (case2 refl) = y∋x | 251 lemma (case2 refl) = y∋x |
249 | 252 |
250 -- ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) | 253 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) |
251 -- → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) | 254 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) |
252 -- → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y | 255 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y |
253 -- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y) | 256 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y) |
254 -- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a | 257 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a |
255 -- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → def (od k) (od→ord x)) {!!} y∋x))) | 258 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x ))) |
256 -- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → def (od k) (od→ord x)) {!!} y∋x))) | 259 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c = |
260 ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where | |
261 lemma : {z : Ordinal} → (z ≡ od→ord x) ∨ (z ≡ od→ord x) → od→ord x ≡ z | |
262 lemma (case1 refl) = refl | |
263 lemma (case2 refl) = refl | |
264 y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z | |
265 y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x | |
266 lemma1 : osuc (od→ord y) o< od→ord (x , x) | |
267 lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) | |
257 | 268 |
258 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) | 269 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) |
259 subset-lemma {A} {x} = record { | 270 subset-lemma {A} {x} = record { |
260 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } | 271 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } |
261 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } | 272 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } |
345 iφ : infinite-d o∅ | 356 iφ : infinite-d o∅ |
346 isuc : {x : Ordinal } → infinite-d x → | 357 isuc : {x : Ordinal } → infinite-d x → |
347 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | 358 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) |
348 | 359 |
349 -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. | 360 -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. |
350 -- We simply assumes nfinite-d y has a maximum. | 361 -- We simply assumes infinite-d y has a maximum. |
351 -- | 362 -- |
352 -- This means that many of OD cannot be HODs because of the od→ord mapping divergence. | 363 -- This means that many of OD may not be HODs because of the od→ord mapping divergence. |
353 -- We should have some axioms to prevent this, but it may complicate thins. | 364 -- We should have some axioms to prevent this. |
354 -- | 365 -- |
355 postulate | 366 postulate |
356 ωmax : Ordinal | 367 ωmax : Ordinal |
357 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax | 368 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax |
358 | 369 |
359 infinite : HOD | 370 infinite : HOD |
360 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } | 371 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } |
372 | |
373 -- infinite' : HOD | |
374 -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where | |
375 -- u : (y : Ordinal ) → HOD | |
376 -- u y = Union (ord→od y , (ord→od y , ord→od y)) | |
377 -- lemma : {y : Ordinal} → infinite-d y → y o< next o∅ | |
378 -- lemma {o∅} iφ = {!!} | |
379 -- lemma (isuc {y} x) = {!!} where | |
380 -- lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y ))) | |
381 -- lemma1 = {!!} | |
382 | |
361 | 383 |
362 _=h=_ : (x y : HOD) → Set n | 384 _=h=_ : (x y : HOD) → Set n |
363 x =h= y = od x == od y | 385 x =h= y = od x == od y |
364 | 386 |
365 infixr 200 _∈_ | 387 infixr 200 _∈_ |