Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 334:ba3ebb9a16c6 release
HOD
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Jul 2020 16:59:13 +0900 |
| parents | 9f926b2210bc (current diff) 214a087c78a5 (diff) |
| children | aa03b9c289c0 454bf7194b8a |
| files | .hgtags |
| diffstat | 10 files changed, 672 insertions(+), 402 deletions(-) [+] |
line wrap: on
line diff
--- a/BAlgbra.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/BAlgbra.agda Sun Jul 05 16:59:13 2020 +0900 @@ -19,60 +19,66 @@ open OD O open OD.OD open ODAxiom odAxiom +open HOD open _∧_ open _∨_ open Bool -_∩_ : ( A B : OD ) → OD -A ∩ B = record { def = λ x → def A x ∧ def B x } - -_∪_ : ( A B : OD ) → OD -A ∪ B = record { def = λ x → def A x ∨ def B x } +_∩_ : ( 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 : OD ) → OD -A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } +_∪_ : ( A B : HOD ) → HOD +A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; + odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where + lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B) + lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) + lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) -∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) +_＼_ : ( A B : HOD ) → HOD +A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) } + +∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x + lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x lemma1 {x} lt = lemma3 lt where - lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) + lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) ) lemma4 {y} z with proj1 z - lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) - lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) - lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x + lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) ) + lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) ) + lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice - lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x - lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A - (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) - lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B - (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) + lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x + lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A + (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x})) + lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B + (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x})) -∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) +∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x - lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } - lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x + lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x + lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) } + lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = - record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } + record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } -dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) +dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x + lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x lemma1 {x} lt with proj2 lt lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) - lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x + lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } -dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) +dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x + lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } - lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x + lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x lemma2 {x} lt with proj1 lt | proj2 lt lemma2 {x} lt | case1 cp | _ = case1 cp lemma2 {x} lt | _ | case1 cp = case1 cp
--- a/LEMC.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/LEMC.agda Sun Jul 05 16:59:13 2020 +0900 @@ -23,38 +23,42 @@ open import zfc ---- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice +--- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice --- -record choiced ( X : OD) : Set (suc n) where +record choiced ( X : HOD) : Set (suc n) where field - a-choice : OD + a-choice : HOD is-in : X ∋ a-choice +open HOD +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + open choiced OD→ZFC : ZFC OD→ZFC = record { - ZFSet = OD + ZFSet = HOD ; _∋_ = _∋_ - ; _≈_ = _==_ + ; _≈_ = _=h=_ ; ∅ = od∅ ; Select = Select ; isZFC = isZFC } where -- infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select + isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select isZFC = record { 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 - choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X + choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X choice-func X not = have_to_find where ψ : ( ox : Ordinal ) → Set (suc n) - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced X lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite {ψ} induction ox where - ∋-p : (A x : OD ) → Dec ( A ∋ x ) + lemma-ord ox = TransFinite1 {ψ} induction ox where + ∋-p : (A x : HOD ) → Dec ( A ∋ x ) ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM ∋-p A x | case1 (lift t) = yes t ∋-p A x | case2 t = no (λ x → t (lift x )) @@ -71,59 +75,61 @@ 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 : Ordinal) → (y o< x → odef 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 + lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) ) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X lemma = ∀-imply-or lemma1 have_to_find : choiced X have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) ¬¬X∋x nn = not record { - eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt) ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) } - record Minimal (x : OD) : Set (suc n) where + record Minimal (x : HOD) : Set (suc n) where field - min : OD + min : HOD x∋min : x ∋ min - min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) + 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 : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u ) - → (u : OD ) → (u∋x : u ∋ x) → Minimal u - induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) + 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)) ... | case1 P = record { min = x ; x∋min = u∋x ; min-empty = P } ... | case2 NP = min2 where - p : OD - p = record { def = λ y1 → def x y1 ∧ def u y1 } - np : ¬ (p == od∅) - np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) + p : HOD + p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where + lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) + lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) + np : ¬ (p =h= od∅) + np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) y1choice : choiced p y1choice = choice-func p np - y1 : OD + y1 : HOD y1 = a-choice y1choice y1prop : (x ∋ y1) ∧ (u ∋ y1) y1prop = is-in y1choice min2 : Minimal u min2 = prev (proj1 y1prop) u (proj2 y1prop) - Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u - Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) - cx : {x : OD} → ¬ (x == od∅ ) → choiced x + Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u + Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) + cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x cx {x} nx = choice-func x nx - minimal : (x : OD ) → ¬ (x == od∅ ) → OD - minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) - x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) - x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) - minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD + minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) + x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) + x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) + minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
--- a/OD.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/OD.agda Sun Jul 05 16:59:13 2020 +0900 @@ -53,28 +53,27 @@ eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m -- next assumptions are our axiom --- it defines a subset of OD, which is called HOD, usually defined as +-- +-- OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one +-- correspondence to the OD then the OD looks like a ZF Set. +-- +-- If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e. +-- bbounded ODs are ZF Set. Unbounded ODs are classes. +-- +-- In classical Set Theory, HOD is used, as a subset of OD, -- HOD = { x | TC x ⊆ OD } --- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x - -record ODAxiom : Set (suc n) where - -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) - field - od→ord : OD → Ordinal - ord→od : Ordinal → OD - c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y - oiso : {x : OD } → ord→od ( od→ord x ) ≡ x - diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x - ==→o≡ : { x y : OD } → (x == y) → x ≡ y - -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) - sup-o : ( OD → Ordinal ) → Ordinal - sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ - -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use - -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal - -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) - -postulate odAxiom : ODAxiom -open ODAxiom odAxiom +-- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x. +-- This is not possible because we don't have V yet. So we assumes HODs are bounded OD. +-- +-- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks. +-- There two contraints on the HOD order, one is ∋, the other one is ⊂. +-- ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary +-- bound on each HOD. +-- +-- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, +-- we need explict assumption on sup. +-- +-- ==→o≡ is necessary to prove axiom of extensionality. data One : Set n where OneObj : One @@ -83,100 +82,125 @@ Ords : OD Ords = record { def = λ x → One } -maxod : {x : OD} → od→ord x o< od→ord Ords -maxod {x} = c<→o< OneObj +record HOD : Set (suc n) where + field + od : OD + odmax : Ordinal + <odmax : {y : Ordinal} → def od y → y o< odmax + +open HOD + +record ODAxiom : Set (suc n) where + field + -- HOD is isomorphic to Ordinal (by means of Goedel number) + od→ord : HOD → Ordinal + ord→od : Ordinal → HOD + c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y + ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) + oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + ==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y + sup-o : (A : HOD) → (( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal + sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ + +postulate odAxiom : ODAxiom +open ODAxiom odAxiom + +-- maxod : {x : OD} → od→ord x o< od→ord Ords +-- maxod {x} = c<→o< OneObj + +-- we have not this contradiction +-- bad-bad : ⊥ +-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One }; <odmax = {!!} } } OneObj) -- Ordinal in OD ( and ZFSet ) Transitive Set -Ord : ( a : Ordinal ) → OD -Ord a = record { def = λ y → y o< a } +Ord : ( a : Ordinal ) → HOD +Ord a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where + lemma : {x : Ordinal} → x o< a → x o< a + lemma {x} lt = lt + +od∅ : HOD +od∅ = Ord o∅ -od∅ : OD -od∅ = Ord o∅ +odef : HOD → Ordinal → Set n +odef A x = def ( od A ) x + +o<→c<→HOD=Ord : ( {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x) +o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y + lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt)) + lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y + lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt ) -o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x) -o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y - lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt)) - lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y - lemma2 {y} lt = subst (λ k → def k y ) oiso (o<→c< {y} {od→ord x} lt ) +_∋_ : ( a x : HOD ) → Set n +_∋_ a x = odef a ( od→ord x ) -_∋_ : ( a x : OD ) → Set n -_∋_ a x = def a ( od→ord x ) - -_c<_ : ( x a : OD ) → Set n +_c<_ : ( x a : HOD ) → Set n x c< a = a ∋ x -cseq : {n : Level} → OD → OD -cseq x = record { def = λ y → def x (osuc y) } where - -def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x -def-subst df refl refl = df +cseq : {n : Level} → HOD → HOD +cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where + lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) + lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) -sup-od : ( OD → OD ) → OD -sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) ) +odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x +odef-subst df refl refl = df -sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) -sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ x)) )} {od→ord ( ψ x )} - lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where - lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ x)) - lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso) ) - -otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y +otrans : {n : Level} {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y otrans x<a y<x = ordtrans y<x x<a -def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X -def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso - +odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X +odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso -- avoiding lv != Zero error -orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y +orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl -==-iso : { x y : OD } → ord→od (od→ord x) == ord→od (od→ord y) → x == y +==-iso : { x y : HOD } → od (ord→od (od→ord x)) == od (ord→od (od→ord y)) → od x == od y ==-iso {x} {y} eq = record { - eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ; - eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) } + eq→ = λ d → lemma ( eq→ eq (odef-subst d (sym oiso) refl )) ; + eq← = λ d → lemma ( eq← eq (odef-subst d (sym oiso) refl )) } where - lemma : {x : OD } {z : Ordinal } → def (ord→od (od→ord x)) z → def x z - lemma {x} {z} d = def-subst d oiso refl + lemma : {x : HOD } {z : Ordinal } → odef (ord→od (od→ord x)) z → odef x z + lemma {x} {z} d = odef-subst d oiso refl -=-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) == y) -=-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) +=-iso : {x y : HOD } → (od x == od y) ≡ (od (ord→od (od→ord x)) == od y) +=-iso {_} {y} = cong ( λ k → od k == od y ) (sym oiso) -ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y +ord→== : { x y : HOD } → od→ord x ≡ od→ord y → od x == od y ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where - lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy) + lemma : ( ox oy : Ordinal ) → ox ≡ oy → od (ord→od ox) == od (ord→od oy) lemma ox ox refl = ==-refl -o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y +o≡→== : { x y : Ordinal } → x ≡ y → od (ord→od x) == od (ord→od y) o≡→== {x} {.x} refl = ==-refl o∅≡od∅ : ord→od (o∅ ) ≡ od∅ o∅≡od∅ = ==→o≡ lemma where - lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x - lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso - lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x + lemma0 : {x : Ordinal} → odef (ord→od o∅) x → odef od∅ x + lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (odef-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso + lemma1 : {x : Ordinal} → odef od∅ x → odef (ord→od o∅) x lemma1 {x} lt = ⊥-elim (¬x<0 lt) - lemma : ord→od o∅ == od∅ + lemma : od (ord→od o∅) == od od∅ lemma = record { eq→ = lemma0 ; eq← = lemma1 } ord-od∅ : od→ord (od∅ ) ≡ o∅ ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) ) -∅0 : record { def = λ x → Lift n ⊥ } == od∅ +∅0 : record { def = λ x → Lift n ⊥ } == od od∅ eq→ ∅0 {w} (lift ()) eq← ∅0 {w} lt = lift (¬x<0 lt) -∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ ) +∅< : { x y : HOD } → odef x (od→ord y ) → ¬ ( od x == od od∅ ) ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d ∅< {x} {y} d eq | lift () -∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox +∅6 : { x : HOD } → ¬ ( x ∋ x ) -- no Russel paradox ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x ) -def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x -def-iso refl t = t +odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (odef A y → odef B y) → odef A x → odef B x +odef-iso refl t = t is-o∅ : ( x : Ordinal ) → Dec ( x ≡ o∅ ) is-o∅ x with trio< x o∅ @@ -184,59 +208,72 @@ is-o∅ x | tri≈ ¬a b ¬c = yes b is-o∅ x | tri> ¬a ¬b c = no ¬b -_,_ : OD → OD → OD -x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) +_,_ : HOD → HOD → HOD +x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where + lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) + lemma {t} (case1 refl) = omax-x _ _ + lemma {t} (case2 refl) = omax-y _ _ + -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) -in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD -in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } +in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD +in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } --- Power Set of X ( or constructible by λ y → def X (od→ord y ) - -ZFSubset : (A x : OD ) → OD -ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set +-- Power Set of X ( or constructible by λ y → odef X (od→ord y ) -Def : (A : OD ) → OD -Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) +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 : OD ) → ∀{ x : OD } → Set n --- _⊆_ A B {x} = A ∋ x → B ∋ x - -record _⊆_ ( A B : OD ) : Set (suc n) where +record _⊆_ ( A B : HOD ) : Set (suc n) where field - incl : { x : OD } → A ∋ x → B ∋ x + incl : { x : HOD } → A ∋ x → B ∋ x open _⊆_ - infixr 220 _⊆_ -subset-lemma : {A x : OD } → ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) +subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset 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 } } +od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y) +od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z ))) + +power< : {A x : HOD } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x +power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) diso (lemma y x∋y ) ) where + lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y)) + lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y ) + open import Data.Unit -ε-induction : { ψ : OD → Set (suc n)} - → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) - → (x : OD ) → ψ x +ε-induction : { ψ : HOD → Set n} + → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) + → (x : HOD ) → ψ x ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy --- minimal-2 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) --- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} ) +ε-induction1 : { ψ : HOD → Set (suc n)} + → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) + → (x : HOD ) → ψ x +ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) + ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy -OD→ZF : ZF -OD→ZF = record { - ZFSet = OD +HOD→ZF : ZF +HOD→ZF = record { + ZFSet = HOD ; _∋_ = _∋_ - ; _≈_ = _==_ + ; _≈_ = _=h=_ ; ∅ = od∅ ; _,_ = _,_ ; Union = Union @@ -246,19 +283,43 @@ ; infinite = infinite ; isZF = isZF } where - ZFSet = OD -- is less than Ords because of maxod - Select : (X : OD ) → ((x : OD ) → Set n ) → OD - Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } - Replace : OD → (OD → OD ) → OD - Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x } + ZFSet = HOD -- is less than Ords because of maxod + Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD + Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } + Replace : HOD → (HOD → HOD) → HOD + Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } + ; odmax = rmax ; <odmax = rmax<} where + rmax : Ordinal + 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 { def = λ x → def A x ∧ def B x } - Union : OD → OD - Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } + 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 + umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) + umax< {y} not = lemma (FExists _ lemma1 not ) where + lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x + lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y)) + lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U + lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U)) + lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) + lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) + lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U) + lemma not with trio< y (od→ord U) + lemma not | tri< a ¬b ¬c = ordtrans a <-osuc + lemma not | tri≈ ¬a refl ¬c = <-osuc + lemma not | tri> ¬a ¬b c = ⊥-elim (not c) _∈_ : ( A B : ZFSet ) → Set n A ∈ B = B ∋ A - Power : OD → OD - Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) + + OPwr : (A : HOD ) → HOD + OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) + + Power : HOD → HOD + Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) -- ｛_｝ : ZFSet → ZFSet -- ｛ x ｝ = ( x , x ) -- it works but we don't use @@ -267,12 +328,25 @@ isuc : {x : Ordinal } → infinite-d x → infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) - infinite : OD - infinite = record { def = λ x → infinite-d x } + -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. + -- We simply assumes nfinite-d y has a maximum. + -- + -- This means that many of OD cannot be HODs because of the od→ord mapping divergence. + -- We should have some axioms to prevent this, but it may complicate thins. + -- + postulate + ωmax : Ordinal + <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax + + infinite : HOD + infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } + + _=h=_ : (x y : HOD) → Set n + x =h= y = od x == od y infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite + isZF : IsZF (HOD ) _∋_ _=h=_ od∅ _,_ Union Power Select Replace infinite isZF = record { isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans } ; pair→ = pair→ @@ -288,20 +362,20 @@ ; infinity = infinity ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} ; replacement← = replacement← - ; replacement→ = replacement→ + ; replacement→ = λ {ψ} → replacement→ {ψ} -- ; choice-func = choice-func -- ; choice = choice } where - pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) - pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) - pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) + pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x )) + pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y )) - pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t - pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) - pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) + pair← : ( x y t : ZFSet ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t + pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x)) + pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y)) - empty : (x : OD ) → ¬ (od∅ ∋ x) + empty : (x : HOD ) → ¬ (od∅ ∋ x) empty x = ¬x<0 o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) @@ -314,114 +388,167 @@ ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) - union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z + union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx - ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) - union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) + union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) union← X z UX∋z = FExists _ lemma UX∋z where - lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } - ψiso : {ψ : OD → Set n} {x y : OD } → ψ x → x ≡ y → ψ y + ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t - selection : {ψ : OD → Set n} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) + selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) selection {ψ} {X} {y} = record { proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } } - replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where + sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) + sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt ) + replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x + replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where lemma : def (in-codomain X ψ) (od→ord (ψ x)) lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) - replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) + replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) - → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y))) + lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) + → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y))) lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where - lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) == ψ (ord→od y)) - lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) - lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) ) - lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso ( proj2 not2 )) + lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y)) + lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq ) + lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) ) + lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 )) --- --- Power Set --- - --- First consider ordinals in OD + --- First consider ordinals in HOD --- - --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A + --- ZFSubset A x = record { def = λ y → odef A y ∧ odef x y } subset of A -- -- - ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) + ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) ∩-≡ {a} {b} inc = record { eq→ = λ {x} x<a → record { proj2 = x<a ; - proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; + proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 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 == t - -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t - -- Def 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 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 )) ) ) -- - ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t - ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} + 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 == t + lemma-eq : ZFSubset (Ord a) t =h= t eq→ lemma-eq {z} w = proj2 w eq← lemma-eq {z} w = record { proj2 = w ; - proj1 = def-subst {_} {_} {(Ord a)} {z} - ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } - lemma1 : {a : Ordinal } { t : OD } - → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t + 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 )) - lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) - lemma = sup-o< + 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 = sup-o< _ lemma2 -- - -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first + -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first -- then replace of all elements of the Power set by A ∩ y -- - -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) + -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y ) -- we have oly double negation form because of the replacement axiom -- - power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x) power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where a = od→ord A - lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) - lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t - lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) + lemma2 : ¬ ( (y : HOD) → ¬ (t =h= (A ∩ y))) + lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t + lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x) lemma3 y eq not = not (proj1 (eq→ eq t∋x)) - lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) - lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) - lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x)) + lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y))) + lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 )) + lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x)) lemma5 {y} eq not = (lemma3 (ord→od y) eq) not - power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where a = od→ord A - lemma0 : {x : OD} → t ∋ x → Ord a ∋ x + lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x lemma0 {x} t∋x = c<→o< (t→A t∋x) - lemma3 : Def (Ord a) ∋ t + lemma3 : OPwr (Ord a) ∋ t lemma3 = ord-power← a t lemma0 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t lemma4 = let open ≡-Reasoning in begin A ∩ ord→od (od→ord t) ≡⟨ cong (λ k → A ∩ k) oiso ⟩ A ∩ t - ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ + ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ t ∎ - lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) - lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) - lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) - lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord 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))) + 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 = 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 = 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} 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} 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 = cong (λ k → od→ord k ) ( ==→o≡ lemmac) + lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) + lemma7 with osuc-≡< lemmad + lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab ) + lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where + lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x + lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t)) + diso + (c<→o< (subst₂ (λ j k → def (od j) k) oiso (sym diso) lt ))) + lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where + lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t + lemmai = let open ≡-Reasoning in begin + od→ord (Ord (od→ord A)) + ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩ + od→ord (Ord (od→ord t)) + ≡⟨ sym diso ⟩ + od→ord (ord→od (od→ord (Ord (od→ord t)))) + ≡⟨ sym eq1 ⟩ + od→ord (ord→od (od→ord t)) + ≡⟨ diso ⟩ + od→ord t + ∎ + lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where + lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A)) + lemmak = let open ≡-Reasoning in begin + od→ord (ord→od (od→ord (Ord (od→ord t)))) + ≡⟨ diso ⟩ + od→ord (Ord (od→ord t)) + ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩ + od→ord (Ord (od→ord A)) + ∎ + lemmaj : od→ord t o< od→ord (Ord (od→ord A)) + lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt + lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) + lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) + lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) + lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) - lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) + lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A ))) + ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where - lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y + lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y lemma lt y<x with osuc-≡< lt lemma lt y<x | case1 refl = c<→o< y<x lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a @@ -429,16 +556,16 @@ continuum-hyphotheis : (a : Ordinal) → Set (suc n) continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a) - extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B - eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d - eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d + extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B + eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d + eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d - extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) + extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d infinity∅ : infinite ∋ od∅ - infinity∅ = def-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where + infinity∅ = odef-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where lemma : o∅ ≡ od→ord od∅ lemma = let open ≡-Reasoning in begin o∅ @@ -447,15 +574,15 @@ ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩ od→ord od∅ ∎ - infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) - infinity x lt = def-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where + infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) + infinity x lt = odef-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) ≡ od→ord (Union (x , (x , x))) lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso -Union = ZF.Union OD→ZF -Power = ZF.Power OD→ZF -Select = ZF.Select OD→ZF -Replace = ZF.Replace OD→ZF -isZF = ZF.isZF OD→ZF +Union = ZF.Union HOD→ZF +Power = ZF.Power HOD→ZF +Select = ZF.Select HOD→ZF +Replace = ZF.Replace HOD→ZF +isZF = ZF.isZF HOD→ZF
--- a/ODC.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/ODC.agda Sun Jul 05 16:59:13 2020 +0900 @@ -21,13 +21,20 @@ open OD._==_ open ODAxiom odAxiom +open HOD + +open _∧_ + +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + postulate -- mimimul and x∋minimal is an Axiom of choice - minimal : (x : OD ) → ¬ (x == od∅ )→ OD - -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) - x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) - -- minimality (may proved by ε-induction ) - minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD + -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) + x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) + -- minimality (may proved by ε-induction with LEM) + minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) -- @@ -35,20 +42,26 @@ -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog -- -ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p -ppp {p} {a} d = d +pred-od : ( p : Set n ) → HOD +pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ; + odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc } + +ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p +ppp {p} {a} d = proj2 d p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice -p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } )) +p∨¬p p with is-o∅ ( od→ord (pred-od p )) p∨¬p p | yes eq = case2 (¬p eq) where - ps = record { def = λ x → p } - lemma : ps == od∅ → p → ⊥ - lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) + ps = pred-od p + eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ + eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) + lemma : ps =h= od∅ → p → ⊥ + lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) ¬p : (od→ord ps ≡ o∅) → p → ⊥ - ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) + ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where - ps = record { def = λ x → p } - eqo∅ : ps == od∅ → od→ord ps ≡ o∅ + ps = pred-od p + eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) @@ -63,7 +76,7 @@ ... | yes p = p ... | no ¬p = ⊥-elim ( notnot ¬p ) -OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) +OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) OrdP x y with trio< x (od→ord y) OrdP x y | tri< a ¬b ¬c = no ¬c OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) @@ -71,26 +84,26 @@ open import zfc -OD→ZFC : ZFC -OD→ZFC = record { - ZFSet = OD +HOD→ZFC : ZFC +HOD→ZFC = record { + ZFSet = HOD ; _∋_ = _∋_ - ; _≈_ = _==_ + ; _≈_ = _=h=_ ; ∅ = od∅ ; Select = Select ; isZFC = isZFC } where -- infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select + isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select isZFC = record { choice-func = choice-func ; choice = choice } where -- Axiom of choice ( is equivalent to the existence of minimal in our case ) -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] - choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD + choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD choice-func X {x} not X∋x = minimal x not - choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A + choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimal A not
--- a/OPair.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/OPair.agda Sun Jul 05 16:59:13 2020 +0900 @@ -17,6 +17,7 @@ open inOrdinal O open OD O open OD.OD +open OD.HOD open ODAxiom odAxiom open _∧_ @@ -25,30 +26,33 @@ open _==_ -<_,_> : (x y : OD) → OD +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + +<_,_> : (x y : HOD) → HOD < x , y > = (x , x ) , (x , y ) -exg-pair : { x y : OD } → (x , y ) == ( y , x ) +exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) exg-pair {x} {y} = record { eq→ = left ; eq← = right } where - left : {z : Ordinal} → def (x , y) z → def (y , x) z + left : {z : Ordinal} → odef (x , y) z → odef (y , x) z left (case1 t) = case2 t left (case2 t) = case1 t - right : {z : Ordinal} → def (y , x) z → def (x , y) z + right : {z : Ordinal} → odef (y , x) z → odef (x , y) z right (case1 t) = case2 t right (case2 t) = case1 t -ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y +ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) -eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > +eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > eq-prod refl refl = refl -prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) +prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where - lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y + lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) @@ -57,15 +61,15 @@ lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) - lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y + lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where - lemma3 : ( x , x ) == ( y , z ) + lemma3 : ( x , x ) =h= ( y , z ) lemma3 = ==-trans eq exg-pair - lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y + lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) - lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z + lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z ... | refl with lemma2 (==-sym eq ) @@ -81,6 +85,9 @@ ... | refl with lemma4 eq -- with (x,y)≡(x,y') ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) +-- +-- unlike ordered pair, ZFProduct is not a HOD + data ord-pair : (p : Ordinal) → Set n where pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) @@ -94,35 +101,38 @@ pi1 : { p : Ordinal } → ord-pair p → Ordinal pi1 ( pair x y) = x -π1 : { p : OD } → ZFProduct ∋ p → OD +π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD π1 lt = ord→od (pi1 lt ) pi2 : { p : Ordinal } → ord-pair p → Ordinal pi2 ( pair x y ) = y -π2 : { p : OD } → ZFProduct ∋ p → OD +π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD π2 lt = ord→od (pi2 lt ) -op-cons : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > +op-cons : { ox oy : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy > )) op-cons {ox} {oy} = pair ox oy -p-cons : ( x y : OD ) → ZFProduct ∋ < x , y > -p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( - let open ≡-Reasoning in begin - od→ord < ord→od (od→ord x) , ord→od (od→ord y) > - ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ - od→ord < x , y > - ∎ ) +def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x +def-subst df refl refl = df + +p-cons : ( x y : HOD ) → def ZFProduct (od→ord ( < x , y >)) +p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( + let open ≡-Reasoning in begin + od→ord < ord→od (od→ord x) , ord→od (od→ord y) > + ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ + od→ord < x , y > + ∎ ) op-iso : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op op-iso (pair ox oy) = refl -p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x +p-iso : { x : HOD } → (p : def ZFProduct (od→ord x) ) → < π1 p , π2 p > ≡ x p-iso {x} p = ord≡→≡ (op-iso p) -p-pi1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ x +p-pi1 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π1 p ≡ x p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) )) -p-pi2 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π2 p ≡ y +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/Ordinals.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/Ordinals.agda Sun Jul 05 16:59:13 2020 +0900 @@ -13,14 +13,19 @@ open import Relation.Binary open import Relation.Binary.Core -record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where +record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field Otrans : {x y z : ord } → x o< y → y o< z → x o< z OTri : Trichotomous {n} _≡_ _o<_ ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) - TransFinite : { ψ : ord → Set (suc n) } + not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) + next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) + TransFinite : { ψ : ord → Set n } + → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord) → ψ x + TransFinite1 : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x @@ -31,7 +36,8 @@ o∅ : ord osuc : ord → ord _o<_ : ord → ord → Set n - isOrdinal : IsOrdinals ord o∅ osuc _o<_ + next : ord → ord + isOrdinal : IsOrdinals ord o∅ osuc _o<_ next module inOrdinal {n : Level} (O : Ordinals {n} ) where @@ -47,11 +53,16 @@ o∅ : Ordinal o∅ = Ordinals.o∅ O + next : Ordinal → Ordinal + next = Ordinals.next O + ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) - + TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) + next-limit = IsOrdinals.next-limit (Ordinals.isOrdinal O) + o<-dom : { x y : Ordinal } → x o< y → Ordinal o<-dom {x} _ = x @@ -104,7 +115,7 @@ proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy _o≤_ : Ordinal → Ordinal → Set n - a o≤ b = (a ≡ b) ∨ ( a o< b ) + a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob @@ -119,13 +130,13 @@ maxα x y | tri> ¬a ¬b c = x maxα x y | tri≈ ¬a refl ¬c = x - minα : Ordinal → Ordinal → Ordinal - minα x y with trio< x y - minα x y | tri< a ¬b ¬c = x - minα x y | tri> ¬a ¬b c = y - minα x y | tri≈ ¬a refl ¬c = x + omin : Ordinal → Ordinal → Ordinal + omin x y with trio< x y + omin x y | tri< a ¬b ¬c = x + omin x y | tri> ¬a ¬b c = y + omin x y | tri≈ ¬a refl ¬c = x - min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y + min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y min1 {x} {y} {z} z<x z<y with trio< x y min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x @@ -176,11 +187,14 @@ open _∧_ + o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j + o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc OrdTrans : Transitive _o≤_ - OrdTrans (case1 refl) (case1 refl) = case1 refl - OrdTrans (case1 refl) (case2 lt2) = case2 lt2 - OrdTrans (case2 lt1) (case1 refl) = case2 lt1 - OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) + OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c + OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc + OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc + OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc + OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc OrdPreorder : Preorder n n n OrdPreorder = record { Carrier = Ordinal @@ -188,7 +202,7 @@ ; _∼_ = _o≤_ ; isPreorder = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ; reflexive = case1 + ; reflexive = o≤-refl ; trans = OrdTrans } } @@ -199,3 +213,11 @@ → ¬ p FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where + field + os→ : (x : Ordinal) → x o< maxordinal → Ordinal + os← : Ordinal → Ordinal + os←limit : (x : Ordinal) → os← x o< maxordinal + os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x + os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x +
--- a/cardinal.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/cardinal.agda Sun Jul 05 16:59:13 2020 +0900 @@ -29,49 +29,48 @@ -- we have to work on Ordinal to keep OD Level n -- since we use p∨¬p which works only on Level n - -∋-p : (A x : OD ) → Dec ( A ∋ x ) +∋-p : (A x : HOD ) → Dec ( A ∋ x ) ∋-p A x with ODC.p∨¬p O ( 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 → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where +_⊗_ : (A B : HOD) → HOD +A ⊗ B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where checkAB : { p : Ordinal } → def ZFProduct p → Set n - checkAB (pair x y) = def A x ∧ def B y + checkAB (pair x y) = odef A x ∧ odef B y -func→od0 : (f : Ordinal → Ordinal ) → OD -func→od0 f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where +func→od0 : (f : Ordinal → Ordinal ) → HOD +func→od0 f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }} where checkfunc : { p : Ordinal } → def ZFProduct p → Set n checkfunc (pair x y) = f x ≡ y -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) -Func : ( A B : OD ) → OD -Func A B = record { def = λ x → def (Power (A ⊗ B)) x } +Func : ( A B : HOD ) → HOD +Func A B = record { od = record { def = λ x → odef (Power (A ⊗ B)) x } } -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) -func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD +func→od : (f : Ordinal → Ordinal ) → ( dom : HOD ) → HOD func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) -record Func←cd { dom cod : OD } {f : Ordinal } : Set n where +record Func←cd { dom cod : HOD } {f : Ordinal } : Set n where field func-1 : Ordinal → Ordinal func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom -od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f} -od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where +od→func : { dom cod : HOD } → {f : Ordinal } → odef (Func dom cod ) f → Func←cd {dom} {cod} {f} +od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o {!!} ( λ y lt → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where lemma : Ordinal → Ordinal → Ordinal - lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) + lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) lemma x y | p | no n = o∅ lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) lemma2 : {p : Ordinal} → ord-pair p → Ordinal lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x) lemma2 (pair x1 y1) | yes p = y1 lemma2 (pair x1 y1) | no ¬p = o∅ - fod : OD - fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > ) + fod : HOD + fod = Replace dom ( λ x → < x , ord→od (sup-o {!!} ( λ y lt → lemma (od→ord x) {!!} )) > ) open Func←cd @@ -91,18 +90,18 @@ -- X ---------------------------> Y -- ymap <- def Y y -- -record Onto (X Y : OD ) : Set n where +record Onto (X Y : HOD ) : Set n where field xmap : Ordinal ymap : Ordinal - xfunc : def (Func X Y) xmap - yfunc : def (Func Y X) ymap - onto-iso : {y : Ordinal } → (lty : def Y y ) → + xfunc : odef (Func X Y) xmap + yfunc : odef (Func Y X) ymap + onto-iso : {y : Ordinal } → (lty : odef Y y ) → func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y open Onto -onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y → Onto X Z +onto-restrict : {X Y Z : HOD} → Onto X Y → Z ⊆ Y → Onto X Z onto-restrict {X} {Y} {Z} onto Z⊆Y = record { xmap = xmap1 ; ymap = zmap @@ -114,23 +113,23 @@ xmap1 = od→ord (Select (ord→od (xmap onto)) {!!} ) zmap : Ordinal zmap = {!!} - xfunc1 : def (Func X Z) xmap1 + xfunc1 : odef (Func X Z) xmap1 xfunc1 = {!!} - zfunc : def (Func Z X) zmap + zfunc : odef (Func Z X) zmap zfunc = {!!} - onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func-1 (od→func xfunc1 ) (func-1 (od→func zfunc ) z ) ≡ z + onto-iso1 : {z : Ordinal } → (ltz : odef Z z ) → func-1 (od→func xfunc1 ) (func-1 (od→func zfunc ) z ) ≡ z onto-iso1 = {!!} -record Cardinal (X : OD ) : Set n where +record Cardinal (X : HOD ) : Set n where field cardinal : Ordinal conto : Onto X (Ord cardinal) cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto X (Ord y) -cardinal : (X : OD ) → Cardinal X +cardinal : (X : HOD ) → Cardinal X cardinal X = record { - cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) ) + cardinal = sup-o {!!} ( λ x lt → proj1 ( cardinal-p {!!}) ) ; conto = onto ; cmax = cmax } where @@ -138,24 +137,24 @@ cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x) ) cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } - S = sup-o (λ x → proj1 (cardinal-p {!!})) - lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) → - Lift (suc n) (x o< (osuc S) → Onto X (Ord x) ) + S = sup-o {!!} (λ x lt → proj1 (cardinal-p {!!})) + lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → (y o< (osuc S) → Onto X (Ord y))) → + (x o< (osuc S) → Onto X (Ord x) ) lemma1 x prev with trio< x (osuc S) lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a - lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} ) - lemma1 x prev | tri< a ¬b ¬c | case2 x<S = lift ( λ lt → lemma2 ) where + lemma1 x prev | tri< a ¬b ¬c | case1 x=S = ( λ lt → {!!} ) + lemma1 x prev | tri< a ¬b ¬c | case2 x<S = ( λ lt → lemma2 ) where lemma2 : Onto X (Ord x) lemma2 with prev {!!} {!!} - ... | lift t = t {!!} - lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt )) - lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt )) + ... | t = {!!} + lemma1 x prev | tri≈ ¬a b ¬c = ( λ lt → ⊥-elim ( o<¬≡ b lt )) + lemma1 x prev | tri> ¬a ¬b c = ( λ lt → ⊥-elim ( o<> c lt )) onto : Onto X (Ord S) - onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S - ... | lift t = t <-osuc + onto with TransFinite {λ x → ( x o< osuc S → Onto X (Ord x) ) } lemma1 S + ... | t = t <-osuc cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) - cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S} - (sup-o< {λ x → proj1 ( cardinal-p {!!})}{{!!}} ) lemma refl ) where + cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S} {!!} lemma refl ) where + -- (sup-o< ? {λ x lt → proj1 ( cardinal-p {!!})}{{!!}} ) lemma refl ) where lemma : proj1 (cardinal-p y) ≡ y lemma with ODC.p∨¬p O ( Onto X (Ord y) ) lemma | case1 x = refl
--- a/filter.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/filter.agda Sun Jul 05 16:59:13 2020 +0900 @@ -13,80 +13,143 @@ open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +import BAlgbra + +open BAlgbra O open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom +import ODC + open _∧_ open _∨_ open Bool -_∩_ : ( A B : OD ) → OD -A ∩ B = record { def = λ x → def A x ∧ def B x } - -_∪_ : ( A B : OD ) → OD -A ∪ B = record { def = λ x → def A x ∨ def B x } - -_＼_ : ( A B : OD ) → OD -A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } - - -record Filter ( L : OD ) : Set (suc n) where +-- Kunen p.76 and p.53, we use ⊆ +record Filter ( L : HOD ) : Set (suc n) where field - filter : OD - proper : ¬ ( filter ∋ od∅ ) - inL : filter ⊆ L - filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q - filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) + filter : HOD + f⊆PL : filter ⊆ Power L + filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q + filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) open Filter -L⊆L : (L : OD) → L ⊆ L -L⊆L L = record { incl = λ {x} lt → lt } +record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where + field + proper : ¬ (filter P ∋ od∅) + prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) + +record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where + field + proper : ¬ (filter P ∋ od∅) + ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) -L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L -L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!} +open _⊆_ + +trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C +trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } -prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n -prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) +power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A +power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where + t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) + t1 = zf.IsZF.power→ isZF A t PA∋t -ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n -ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) +∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L +∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt ) +∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L +∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } + +∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L +∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } -filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} -filter-lemma1 {L} P {p} {q} u lt = {!!} +q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q +q∩q⊆q = record { incl = λ lt → proj1 lt } -filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p} -filter-lemma2 {L} P prime p with prime {!!} -... | t = {!!} +open HOD +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + +----- +-- +-- ultra filter is prime +-- -generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) -generated-filter {L} P p = record { - proper = {!!} ; - filter = {!!} ; inL = {!!} ; - filter1 = {!!} ; filter2 = {!!} - } +filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P +filter-lemma1 {L} P u = record { + proper = ultra-filter.proper u + ; prime = lemma3 + } where + lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) + lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) + ... | case1 p∈P = case1 p∈P + ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where + lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) + lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } + ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } + } where + lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x + lemma4 x lt with proj1 lt + lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) + lemma4 x lt | case2 qx = qx + lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p)) + lemma6 = filter2 P lt ¬p∈P + lemma7 : filter P ∋ (q ∩ (L ＼ p)) + lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 + lemma8 : (q ∩ (L ＼ p)) ⊆ q + lemma8 = q∩q⊆q -record Dense (P : OD ) : Set (suc n) where - field - dense : OD - incl : dense ⊆ P - dense-f : OD → OD - dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p) +----- +-- +-- if Filter contains L, prime filter is ultra +-- --- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) +filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P +filter-lemma2 {L} P f∋L prime = record { + proper = prime-filter.proper prime + ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) + } where + open _==_ + p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) + eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) + eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x + eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) + eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) + eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p + lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) + lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L -infinite = ZF.infinite OD→ZF - -module in-countable-ordinal {n : Level} where +record Dense (P : HOD ) : Set (suc n) where + field + dense : HOD + incl : dense ⊆ P + dense-f : HOD → HOD + dense-d : { p : HOD} → P ∋ p → dense ∋ dense-f p + dense-p : { p : HOD} → P ∋ p → p ⊆ (dense-f p) - import ordinal +-- the set of finite partial functions from ω to 2 +-- +-- ph2 : Nat → Set → 2 +-- ph2 : Nat → Maybe 2 +-- +-- Hω2 : Filter (Power (Power infinite)) - -- open ordinal.C-Ordinal-with-choice - -- both Power and infinite is too ZF, it is better to use simpler one - Hω2 : Filter (Power (Power infinite)) - Hω2 = {!!} +record Ideal ( L : HOD ) : Set (suc n) where + field + ideal : HOD + i⊆PL : ideal ⊆ Power L + ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q + ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) +open Ideal + +proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n +proper-ideal {L} P {p} = ideal P ∋ od∅ + +prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n +prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) +
--- a/ordinal.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/ordinal.agda Sun Jul 05 16:59:13 2020 +0900 @@ -211,6 +211,7 @@ ; o∅ = o∅ ; osuc = osuc ; _o<_ = _o<_ + ; next = next ; isOrdinal = record { Otrans = ordtrans ; OTri = trio< @@ -218,14 +219,36 @@ ; <-osuc = <-osuc ; osuc-≡< = osuc-≡< ; TransFinite = TransFinite1 + ; TransFinite1 = TransFinite2 + ; not-limit = not-limit + ; next-limit = next-limit } } where + next : Ordinal {suc n} → Ordinal {suc n} + next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv)) + next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) + next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where + lemma : (x : Ordinal) → x o< next y → osuc x o< next y + lemma x (case1 lt) = case1 lt + not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y))) + not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () )) + not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl ) ord1 : Set (suc n) ord1 = Ordinal {suc n} - TransFinite1 : { ψ : ord1 → Set (suc (suc n)) } + TransFinite1 : { ψ : ord1 → Set (suc n) } → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord1) → ψ x - TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where + TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where + caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → + ψ (record { lv = lx ; ord = Φ lx }) + caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev + caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → + ψ (record { lv = lx ; ord = OSuc lx x₁ }) + caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev + TransFinite2 : { ψ : ord1 → Set (suc (suc n)) } + → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord1) → ψ x + TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → ψ (record { lv = lx ; ord = Φ lx }) caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev @@ -233,3 +256,4 @@ ψ (record { lv = lx ; ord = OSuc lx x₁ }) caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev +
--- a/zf.agda Sun Jun 07 20:35:14 2020 +0900 +++ b/zf.agda Sun Jul 05 16:59:13 2020 +0900 @@ -49,7 +49,7 @@ -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) -- regularity without minimum - ε-induction : { ψ : ZFSet → Set (suc m)} + ε-induction : { ψ : ZFSet → Set m} → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) → (x : ZFSet ) → ψ x -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )