Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 234:e06b76e5b682
ac from LEM in abstract ordinal
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 13 Aug 2019 22:21:10 +0900 |
parents | 49736efc822b |
children | 846e0926bb89 |
comparison
equal
deleted
inserted
replaced
233:af60c40298a4 | 234:e06b76e5b682 |
---|---|
31 record _==_ ( a b : OD ) : Set n where | 31 record _==_ ( a b : OD ) : Set n where |
32 field | 32 field |
33 eq→ : ∀ { x : Ordinal } → def a x → def b x | 33 eq→ : ∀ { x : Ordinal } → def a x → def b x |
34 eq← : ∀ { x : Ordinal } → def b x → def a x | 34 eq← : ∀ { x : Ordinal } → def b x → def a x |
35 | 35 |
36 id : {n : Level} {A : Set n} → A → A | 36 id : {A : Set n} → A → A |
37 id x = x | 37 id x = x |
38 | 38 |
39 eq-refl : { x : OD } → x == x | 39 eq-refl : { x : OD } → x == x |
40 eq-refl {x} = record { eq→ = id ; eq← = id } | 40 eq-refl {x} = record { eq→ = id ; eq← = id } |
41 | 41 |
191 eqo∅ : ps == od∅ → od→ord ps ≡ o∅ | 191 eqo∅ : ps == od∅ → od→ord ps ≡ o∅ |
192 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | 192 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) |
193 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) | 193 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) |
194 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) | 194 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) |
195 | 195 |
196 ∋-p : ( p : Set n ) → Dec p -- assuming axiom of choice | 196 decp : ( p : Set n ) → Dec p -- assuming axiom of choice |
197 ∋-p p with p∨¬p p | 197 decp p with p∨¬p p |
198 ∋-p p | case1 x = yes x | 198 decp p | case1 x = yes x |
199 ∋-p p | case2 x = no x | 199 decp p | case2 x = no x |
200 | 200 |
201 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic | 201 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic |
202 double-neg-eilm {A} notnot with ∋-p A -- assuming axiom of choice | 202 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice |
203 ... | yes p = p | 203 ... | yes p = p |
204 ... | no ¬p = ⊥-elim ( notnot ¬p ) | 204 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
205 | 205 |
206 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) | 206 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) |
207 OrdP x y with trio< x (od→ord y) | 207 OrdP x y with trio< x (od→ord y) |
475 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 475 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
476 choice-func X {x} not X∋x = minimul x not | 476 choice-func X {x} not X∋x = minimul x not |
477 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 477 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
478 choice X {A} X∋A not = x∋minimul A not | 478 choice X {A} X∋A not = x∋minimul A not |
479 | 479 |
480 --- | |
481 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice | |
482 --- | |
483 record choiced ( X : OD) : Set (suc n) where | |
484 field | |
485 a-choice : OD | |
486 is-in : X ∋ a-choice | |
487 | |
488 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X | |
489 choice-func' X p∨¬p not = have_to_find where | |
490 ψ : ( ox : Ordinal ) → Set (suc n) | |
491 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X | |
492 lemma-ord : ( ox : Ordinal ) → ψ ox | |
493 lemma-ord ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where | |
494 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | |
495 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) | |
496 ∋-p A x | case1 (lift t) = yes t | |
497 ∋-p A x | case2 t = no (λ x → t (lift x )) | |
498 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } | |
499 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B | |
500 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) | |
501 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t | |
502 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where | |
503 lemma : ¬ ((x : Ordinal ) → A x) → B | |
504 lemma not with p∨¬p B | |
505 lemma not | case1 b = b | |
506 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) | |
507 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x | |
508 induction x prev with ∋-p X ( ord→od x) | |
509 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) | |
510 ... | no ¬p = lemma where | |
511 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X | |
512 lemma1 y with ∋-p X (ord→od y) | |
513 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) | |
514 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) | |
515 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X | |
516 lemma = ∀-imply-or lemma1 | |
517 have_to_find : choiced X | |
518 have_to_find with lemma-ord (od→ord X ) | |
519 have_to_find | t = dont-or t ¬¬X∋x where | |
520 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) | |
521 ¬¬X∋x nn = not record { | |
522 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | |
523 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | |
524 } | |
525 | |
526 | |
480 _,_ = ZF._,_ OD→ZF | 527 _,_ = ZF._,_ OD→ZF |
481 Union = ZF.Union OD→ZF | 528 Union = ZF.Union OD→ZF |
482 Power = ZF.Power OD→ZF | 529 Power = ZF.Power OD→ZF |
483 Select = ZF.Select OD→ZF | 530 Select = ZF.Select OD→ZF |
484 Replace = ZF.Replace OD→ZF | 531 Replace = ZF.Replace OD→ZF |