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

comparison ordinal-definable.agda @ 100:a402881cc341

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 10 Jun 2019 09:50:44 +0900
parents 74330d0cdcbc
children c8b79d303867
comparison
equal deleted inserted replaced
99:74330d0cdcbc 100:a402881cc341
43 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } 43 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
44 44
45 od∅ : {n : Level} → OD {n} 45 od∅ : {n : Level} → OD {n}
46 od∅ {n} = record { def = λ _ → Lift n ⊥ } 46 od∅ {n} = record { def = λ _ → Lift n ⊥ }
47 47
48 -- OD can be iso to a subset of Ordinal 48
49 postulate 49 postulate
50 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
50 od→ord : {n : Level} → OD {n} → Ordinal {n} 51 od→ord : {n : Level} → OD {n} → Ordinal {n}
51 ord→od : {n : Level} → Ordinal {n} → OD {n} 52 ord→od : {n : Level} → Ordinal {n} → OD {n}
52 c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y 53 c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y
53 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x 54 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x
54 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 55 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
55 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 56 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
57 -- supermum as Replacement Axiom
56 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 58 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
57 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 59 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
60 -- a property of supermum required in Power Set Axiom
58 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 61 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
59 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 62 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
60 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) 63 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ )
61 64
62 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 65 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
338 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 341 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
339 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 342 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
340 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 343 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
341 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 344 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
342 empty x () 345 empty x ()
343 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } 346 ---
344 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 347 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
348 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
349 --
350 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t
351 -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
352 -- In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
353 --
345 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 354 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
346 power→ A t P∋t {x} t∋x = proj1 lemma-s where 355 power→ A t P∋t {x} t∋x = proj1 lemma-s where
347 minsup : OD 356 minsup : OD
348 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 357 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))
349 lemma-t : csuc minsup ∋ t 358 lemma-t : csuc minsup ∋ t
350 lemma-t = o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 359 lemma-t = o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl )
351 lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x 360 lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x
352 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso ) 361 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso )
353 lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl 362 lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl
354 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst (o<→c< lt) oiso refl ) t∋x 363 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst (o<→c< lt) oiso refl ) t∋x
355 -- = {!!} -- transitive {!!} t∋x 364 --
365 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
366 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
367 --
356 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 368 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
357 power← A t t→A = def-subst {suc n} {_} {_} {Power A} {od→ord t} 369 power← A t t→A = def-subst {suc n} {_} {_} {Power A} {od→ord t}
358 ( o<→c< {suc n} {od→ord (ZFSubset A (ord→od (od→ord t)) )} {sup-o (λ x → od→ord (ZFSubset A (ord→od x)))} 370 ( o<→c< {suc n} {od→ord (ZFSubset A (ord→od (od→ord t)) )} {sup-o (λ x → od→ord (ZFSubset A (ord→od x)))}
359 lemma ) refl lemma1 where 371 lemma ) refl lemma1 where
360 lemma-eq : ZFSubset A t == t 372 lemma-eq : ZFSubset A t == t