Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 921:c0cf2b383064
UnionZF
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 Oct 2022 10:32:31 +0900 |
| parents | a2f8d14012aa |
| children | 620c2f3440f5 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 88 insertions(+), 78 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Oct 16 17:26:49 2022 +0900 +++ b/src/zorn.agda Mon Oct 17 10:32:31 2022 +0900 @@ -685,79 +685,6 @@ m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } - --- - --- the maximum chain has fix point of any ≤-monotonic function - --- - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) - (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc) - sp0 f mf {x} ay zc = ZChain.sup zc o≤-refl - - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) - → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) - fixpoint f mf zc = z14 where - chain = ZChain.chain zc - supf = ZChain.supf zc - sp1 : SUP A chain - sp1 = sp0 f mf as0 zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) - → HasPrev A chain b f ∨ IsSup A chain {b} ab - → * a < * b → odef chain b - z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) - z22 : & (SUP.sup sp1) o< & A - z22 = c<→o< ( SUP.as sp1 ) - z21 : supf (& (SUP.sup sp1)) o< supf (& A) - z21 = ? - -- z21 : supf (& (SUP.sup sp1)) o< & A - -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) - z12 : odef chain (& (SUP.sup sp1)) - z12 with o≡? (& s) (& (SUP.sup sp1)) - ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) - (case2 z19 ) z13 where - z13 : * (& s) < * (& (SUP.sup sp1)) - z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) - ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) - ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt - z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) - z19 = record { x<sup = z20 } where - z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) - z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy) - ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) - ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) - ztotal : IsTotalOrderSet (ZChain.chain zc) - ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where - uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) - z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) - z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 - ... | tri< a ¬b ¬c = ⊥-elim z16 where - z16 : ⊥ - z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) - ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) - ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) - ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) - ... | tri> ¬a ¬b c = ⊥-elim z17 where - z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) - z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) - z17 : ⊥ - z17 with z15 - ... | case1 eq = ¬b eq - ... | case2 lt = ¬a lt - - -- ZChain contradicts ¬ Maximal - -- - -- ZChain forces fix point on any ≤-monotonic function (fixpoint) - -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain - -- - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ - z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) - (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄ - (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x - sp1 : SUP A (ZChain.chain zc) - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc - c = & (SUP.sup sp1) - uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {z} cz → subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (A∋fc y f mf cz ))) } @@ -1366,8 +1293,93 @@ -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}; asupf = {!!} } -- where -- x is a sup of (zc ?) ... | case2 ¬x=sup = no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention - SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) - SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A) + --- + --- the maximum chain has fix point of any ≤-monotonic function + --- + + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x + SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) x + + record ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (z : Ordinal) : Set n where + field + uz : Ordinal + zc : odef (ZChain.chain (SZ f mf ay uz)) z + + UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → HOD + UnionZF f mf {y} ay = record { od = record { def = λ x → ZChainP f mf ay x } ; odmax = & A ; <odmax = λ lt → ∈∧P→o< ( ZChainP.zc lt) } + + uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → + IsTotalOrderSet (UnionZF f mf ay) + uztotal f mf ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + uz01 = ? + + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → SUP A (UnionZF f mf ay ) + -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay) + sp0 f mf {x} ay = ? -- + + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) + → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 )) + fixpoint f mf = z14 where + chain = UnionZF f mf as0 + supf : Ordinal → Ordinal + supf = ? + sp1 : SUP A ? + sp1 = sp0 f mf as0 + z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) + → HasPrev A chain b f ∨ IsSup A chain {b} ab + → * a < * b → odef chain b + z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) ) + z22 : & (SUP.sup sp1) o< & A + z22 = c<→o< ( SUP.as sp1 ) + z21 : supf (& (SUP.sup sp1)) o< supf (& A) + z21 = ? + -- z21 : supf (& (SUP.sup sp1)) o< & A + -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) + z12 : odef chain (& (SUP.sup sp1)) + z12 with o≡? (& s) (& (SUP.sup sp1)) + ... | yes eq = subst (λ k → odef chain k) eq ? -- ( ZChain.chain∋init zc ) + ... | no ne = ? where -- ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) + -- (case2 ? ) z13 where + z13 : * (& s) < * (& (SUP.sup sp1)) + z13 with SUP.x<sup sp1 ? + ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) + ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt + z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) + z19 = record { x<sup = z20 } where + z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) + z20 {y} zy with SUP.x<sup sp1 ? + ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) + ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) + z14 : f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 )) + z14 = ? -- with ? +-- ... | tri< a ¬b ¬c = ⊥-elim z16 where +-- z16 : ⊥ +-- z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) +-- ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) +-- ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) +-- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) +-- ... | tri> ¬a ¬b c = ⊥-elim z17 where +-- z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) +-- z15 = SUP.x<sup sp1 ? -- (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) +-- z17 : ⊥ +-- z17 with z15 +-- ... | case1 eq = ¬b eq +-- ... | case2 lt = ¬a lt + + -- ZChain contradicts ¬ Maximal + -- + -- ZChain forces fix point on any ≤-monotonic function (fixpoint) + -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain + -- + z04 : (nmx : ¬ Maximal A ) → ⊥ + z04 nmx = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) + (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) ))) -- x ≡ f x ̄ + (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x + sp1 : SUP A ? + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 + c = & (SUP.sup sp1) zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -1379,14 +1391,12 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 ) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx ) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) zc5 = ⟪ Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ - zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) - zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) -- usage (see filter.agda ) --