Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 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 | af60c40298a4 |
| children | 846e0926bb89 |
| files | OD.agda cardinal.agda ordinal.agda |
| diffstat | 3 files changed, 69 insertions(+), 78 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Mon Aug 12 13:28:59 2019 +0900 +++ b/OD.agda Tue Aug 13 22:21:10 2019 +0900 @@ -33,7 +33,7 @@ eq→ : ∀ { x : Ordinal } → def a x → def b x eq← : ∀ { x : Ordinal } → def b x → def a x -id : {n : Level} {A : Set n} → A → A +id : {A : Set n} → A → A id x = x eq-refl : { x : OD } → x == x @@ -193,13 +193,13 @@ lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) -∋-p : ( p : Set n ) → Dec p -- assuming axiom of choice -∋-p p with p∨¬p p -∋-p p | case1 x = yes x -∋-p p | case2 x = no x +decp : ( p : Set n ) → Dec p -- assuming axiom of choice +decp p with p∨¬p p +decp p | case1 x = yes x +decp p | case2 x = no x double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic -double-neg-eilm {A} notnot with ∋-p A -- assuming axiom of choice +double-neg-eilm {A} notnot with decp A -- assuming axiom of choice ... | yes p = p ... | no ¬p = ⊥-elim ( notnot ¬p ) @@ -477,6 +477,53 @@ choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimul A not + --- + --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice + --- + record choiced ( X : OD) : Set (suc n) where + field + a-choice : OD + is-in : X ∋ a-choice + + choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X + choice-func' X p∨¬p not = have_to_find where + ψ : ( ox : Ordinal ) → Set (suc n) + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X + lemma-ord : ( ox : Ordinal ) → ψ ox + lemma-ord ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where + ∋-p : (A x : OD ) → Dec ( A ∋ x ) + ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) + ∋-p A x | case1 (lift t) = yes t + ∋-p A x | case2 t = no (λ x → t (lift x )) + ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } + → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B + ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) + ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where + lemma : ¬ ((x : Ordinal ) → A x) → B + lemma not with p∨¬p B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x + induction x prev with ∋-p X ( ord→od x) + ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) + ... | no ¬p = lemma where + lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X + lemma1 y with ∋-p X (ord→od y) + lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) + lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X + lemma = ∀-imply-or lemma1 + have_to_find : choiced X + have_to_find with lemma-ord (od→ord X ) + have_to_find | t = dont-or t ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) + ¬¬X∋x nn = not record { + eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) + } + + _,_ = ZF._,_ OD→ZF Union = ZF.Union OD→ZF Power = ZF.Power OD→ZF
--- a/cardinal.agda Mon Aug 12 13:28:59 2019 +0900 +++ b/cardinal.agda Tue Aug 13 22:21:10 2019 +0900 @@ -37,6 +37,11 @@ open SetProduct +∋-p : (A x : OD ) → Dec ( A ∋ x ) +∋-p A x with p∨¬p ( A ∋ x ) +∋-p A x | case1 t = yes t +∋-p A x | case2 t = no t + _⊗_ : (A B : OD) → OD A ⊗ B = record { def = λ x → SetProduct A B x } -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) } @@ -48,12 +53,16 @@ -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) -func←od : { dom cod : OD } → {f : OD } → Func dom cod ∋ f → (Ordinal → Ordinal ) +func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where + lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt lemma : Ordinal → Ordinal - lemma y with IsZF.power→ isZF (dom ⊗ cod) f lt - lemma y | p with double-neg-eilm ( p {ord→od y} {!!} ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) - ... | t = π2 t + lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y) + lemma y | p | no n = o∅ + lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) + ... | t with decp ( x ≡ π1 t ) + ... | yes _ = π2 t + ... | no _ = o∅ func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) @@ -80,7 +89,8 @@ ymap : Ordinal xfunc : def (Func X Y) xmap yfunc : def (Func Y X) ymap - onto-iso : {y : Ordinal } → (lty : def Y y ) → func←od {!!} ( func←od {!!} y ) ≡ y + onto-iso : {y : Ordinal } → (lty : def Y y ) → + func←od {X} {Y} {xmap} xfunc ( func←od yfunc y ) ≡ y open Onto @@ -100,7 +110,7 @@ xfunc1 = {!!} zfunc : def (Func Z X) zmap zfunc = {!!} - onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od {!!} ( func←od zfunc z ) ≡ z + onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od xfunc1 ( func←od zfunc z ) ≡ z onto-iso1 = {!!}
--- a/ordinal.agda Mon Aug 12 13:28:59 2019 +0900 +++ b/ordinal.agda Tue Aug 13 22:21:10 2019 +0900 @@ -322,69 +322,3 @@ dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x dz<dz refl = s<refl - --- - --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice - --- - record choiced ( X : OD) : Set (suc (suc n)) where - field - a-choice : OD - is-in : X ∋ a-choice - - choice-func' : (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X - choice-func' X p∨¬p not = have_to_find where - ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n)) - ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X - lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox - lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where - ∋-p' : (A x : OD ) → Dec ( A ∋ x ) - ∋-p' A x with p∨¬p ( A ∋ x ) - ∋-p' A x | case1 t = yes t - ∋-p' A x | case2 t = no t - ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) } - → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B - ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x) - ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t - ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where - lemma : ¬ ((x : Ordinal {suc n}) → A x) → B - lemma not with p∨¬p B - lemma not | case1 b = b - lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) - caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) - caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) )) - caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) - caseΦ lx prev | no ¬p = lemma where - lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X) - lemma1 x with trio< x (ordinal lx (Φ lx)) - lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where - lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx) - lemma2 (case1 lt) = case1 lt - lemma1 x | tri< a ¬b ¬c | case2 found = case2 found - lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df ) - lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt )) - lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c )) - lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X - lemma = ∀-imply-or lemma1 - caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) ) - caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } ) - caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) - caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where - lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥ - lemma y lt with trio< y (ordinal lx x ) - lemma y lt | tri< a ¬b ¬c = not_found y a - lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p - lemma y lt | tri> ¬a ¬b c with osuc-≡< lt - lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) - lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) - caseOSuc lx x (case2 found) | no ¬p = case2 found - caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) → - ψ (record { lv = lx ; ord = OSuc lx x }) - caseOSuc1 lx x lt = caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl)) - have_to_find : choiced X - have_to_find with lemma-ord (od→ord X ) - have_to_find | t = dont-or t ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥) - ¬¬X∋x nn = not record { - eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) - ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) - } -