Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 360:2a8a51375e49
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 Jul 2020 08:42:30 +0900 |
| parents | 5e22b23ee3fd |
| children | 4cbcf71b09c4 |
| files | BAlgbra.agda LEMC.agda OD.agda OPair.agda |
| diffstat | 4 files changed, 46 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/BAlgbra.agda Tue Jul 14 15:02:59 2020 +0900 +++ b/BAlgbra.agda Wed Jul 15 08:42:30 2020 +0900 @@ -25,9 +25,9 @@ open _∨_ open Bool -_∩_ : ( A B : HOD ) → HOD -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)) } +--_∩_ : ( A B : HOD ) → HOD +--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)) } _∪_ : ( A B : HOD ) → HOD A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
--- a/LEMC.agda Tue Jul 14 15:02:59 2020 +0900 +++ b/LEMC.agda Wed Jul 15 08:42:30 2020 +0900 @@ -52,6 +52,9 @@ choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); choice = λ A {X} A∋X not → is-in (choice-func X not) } where + -- + -- the axiom choice from LEM and OD ordering + -- choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X choice-func X not = have_to_find where ψ : ( ox : Ordinal ) → Set (suc n) @@ -88,6 +91,12 @@ eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt) ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) } + + -- + -- axiom regurality from ε-induction (using axiom of choice above) + -- + -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only + -- record Minimal (x : HOD) : Set (suc n) where field min : HOD @@ -95,9 +104,6 @@ min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y) open Minimal open _∧_ - -- - -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only - -- induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u ) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
--- a/OD.agda Tue Jul 14 15:02:59 2020 +0900 +++ b/OD.agda Wed Jul 15 08:42:30 2020 +0900 @@ -249,10 +249,9 @@ in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } -ZFSubset : (A x : HOD ) → HOD -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 - lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) - lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and)) +_∩_ : ( A B : HOD ) → HOD +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))} record _⊆_ ( A B : HOD ) : Set (suc n) where field @@ -281,7 +280,7 @@ lemma1 : osuc (od→ord y) o< od→ord (x , x) lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) -subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) +subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) subset-lemma {A} {x} = record { proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } @@ -337,9 +336,6 @@ rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax rmax< lt = proj1 lt - _∩_ : ( A B : ZFSet ) → ZFSet - 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))} Union : HOD → HOD Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = osuc (od→ord U) ; <odmax = umax< } where @@ -360,7 +356,7 @@ A ∈ B = B ∋ A OPwr : (A : HOD ) → HOD - OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) + OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) ) Power : HOD → HOD Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) @@ -495,7 +491,7 @@ --- --- First consider ordinals in HOD --- - --- ZFSubset A x = record { def = λ y → odef A y ∧ odef x y } subset of A + --- A ∩ x = record { def = λ y → odef A y ∧ odef x y } subset of A -- -- ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) @@ -505,24 +501,24 @@ eq← = λ {x} x<a∩b → proj2 x<a∩b } -- -- Transitive Set case - -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t =h= t - -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t - -- OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) + -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t + -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t + -- OPwr A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) ) -- ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t} lemma refl (lemma1 lemma-eq )where - lemma-eq : ZFSubset (Ord a) t =h= t + lemma-eq : ((Ord a) ∩ t) =h= t eq→ lemma-eq {z} w = proj2 w eq← lemma-eq {z} w = record { proj2 = w ; proj1 = odef-subst {_} {_} {(Ord a)} {z} ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } lemma1 : {a : Ordinal } { t : HOD } - → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t - lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) + → (eq : ((Ord a) ∩ t) =h= t) → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t + lemma1 {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) lemma2 : (od→ord t) o< (osuc (od→ord (Ord a))) 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))) - 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))) + lemma : od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x))) lemma = sup-o< _ lemma2 -- @@ -561,20 +557,20 @@ t ∎ sup1 : Ordinal - sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))) + sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x))) lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) lemma9 = <-osuc - lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 + lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 lemmad : Ord (osuc (od→ord A)) ∋ t lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) - lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A) + lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A) lemmac = record { eq→ = lemmaf ; eq← = lemmag } where - lemmaf : {x : Ordinal} → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x + lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x lemmaf {x} lt = proj1 lt - lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x + lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } - lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) + lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) lemma7 with osuc-≡< lemmad
--- a/OPair.agda Tue Jul 14 15:02:59 2020 +0900 +++ b/OPair.agda Wed Jul 15 08:42:30 2020 +0900 @@ -136,3 +136,18 @@ p-pi2 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π2 p ≡ y p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p))) + +_⊗_ : (A B : HOD) → HOD +A ⊗ B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ; + odmax = pmax; <odmax = <pmax } where + checkAB : { p : Ordinal } → def ZFProduct p → Set n + checkAB (pair x y) = odef A x ∧ odef B y + pmax : Ordinal + pmax = omax (odmax A) (odmax B) + <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A) (odmax B) + <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A) (odmax B)} ind y where + ind : (x : Ordinal) + → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B))) + → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B)) + ind = {!!} +