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

comparison OD.agda @ 312:c1581ed5f38b

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 Thu, 02 Jul 2020 19:05:55 +0900
parents bf01e924e62e
children 8b5c8b685883
comparison
equal deleted inserted replaced
311:bf01e924e62e 312:c1581ed5f38b
86 field 86 field
87 -- HOD is isomorphic to Ordinal (by means of Goedel number) 87 -- HOD is isomorphic to Ordinal (by means of Goedel number)
88 od→ord : HOD → Ordinal 88 od→ord : HOD → Ordinal
89 ord→od : Ordinal → HOD 89 ord→od : Ordinal → HOD
90 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y 90 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y
91 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
91 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 92 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
92 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 93 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
93 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y 94 ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
94 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal 95 sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
95 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ 96 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
216 ZFSubset : (A x : HOD ) → HOD 217 ZFSubset : (A x : HOD ) → HOD
217 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set 218 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set
218 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) 219 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
219 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and)) 220 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
220 221
221
222 OPwr : (A : HOD ) → HOD
223 OPwr A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
224
225 record _⊆_ ( A B : HOD ) : Set (suc n) where 222 record _⊆_ ( A B : HOD ) : Set (suc n) where
226 field 223 field
227 incl : { x : HOD } → A ∋ x → B ∋ x 224 incl : { x : HOD } → A ∋ x → B ∋ x
228 225
229 open _⊆_ 226 open _⊆_
230
231 infixr 220 _⊆_ 227 infixr 220 _⊆_
232 228
233 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) 229 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
234 subset-lemma {A} {x} = record { 230 subset-lemma {A} {x} = record {
235 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } 231 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) }
236 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 232 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
237 } 233 }
234
235 power< : {A x : HOD } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
236 power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) diso (lemma y x∋y ) ) where
237 lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
238 lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
238 239
239 open import Data.Unit 240 open import Data.Unit
240 241
241 ε-induction : { ψ : HOD → Set (suc n)} 242 ε-induction : { ψ : HOD → Set (suc n)}
242 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) 243 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
270 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))} 271 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
271 Union : HOD → HOD 272 Union : HOD → HOD
272 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} } 273 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} }
273 _∈_ : ( A B : ZFSet ) → Set n 274 _∈_ : ( A B : ZFSet ) → Set n
274 A ∈ B = B ∋ A 275 A ∈ B = B ∋ A
276
277 OPwr : (A : HOD ) → HOD
278 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
279
275 Power : HOD → HOD 280 Power : HOD → HOD
276 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) 281 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
277 -- ｛_｝ : ZFSet → ZFSet 282 -- ｛_｝ : ZFSet → ZFSet
278 -- ｛ x ｝ = ( x , x ) -- it works but we don't use 283 -- ｛ x ｝ = ( x , x ) -- it works but we don't use
279 284
391 proj1 = odef-subst {_} {_} {(Ord a)} {z} 396 proj1 = odef-subst {_} {_} {(Ord a)} {z}
392 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 397 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
393 lemma1 : {a : Ordinal } { t : HOD } 398 lemma1 : {a : Ordinal } { t : HOD }
394 → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 399 → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
395 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 400 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
396 lemma2 : def (od (Ord a)) (od→ord t) 401 lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
397 lemma2 = {!!} 402 lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t)))
398 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x))) 403 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
399 lemma = sup-o< _ lemma2 404 lemma = sup-o< _ lemma2
400 405
401 -- 406 --
402 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first 407 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
403 -- then replace of all elements of the Power set by A ∩ y 408 -- then replace of all elements of the Power set by A ∩ y
431 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 436 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
432 A ∩ t 437 A ∩ t
433 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 438 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
434 t 439 t
435 ∎ 440 ∎
441 --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))))
436 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 442 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
437 lemma7 = {!!} 443 lemma7 = ordtrans {!!} (sup-o< {!!} {!!})
438 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) 444 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
439 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) 445 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))))
440 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) 446 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
441 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) 447 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
442 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 448 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where