Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 276:6f10c47e4e7a
separate choice
fix sup-o
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 May 2020 09:02:52 +0900 |
| parents | 455792eaa611 |
| children | d9d3654baee1 |
| files | BAlgbra.agda OD.agda ODC.agda README.md cardinal.agda filter.agda ordinal.agda zf.agda zfc.agda |
| diffstat | 9 files changed, 212 insertions(+), 203 deletions(-) [+] |
line wrap: on
line diff
--- a/BAlgbra.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/BAlgbra.agda Sat May 09 09:02:52 2020 +0900 @@ -5,6 +5,7 @@ open import zf open import logic import OD +import ODC open import Relation.Nullary open import Relation.Binary @@ -40,7 +41,7 @@ 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 - lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice + 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}))
--- a/OD.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/OD.agda Sat May 09 09:02:52 2020 +0900 @@ -75,18 +75,21 @@ -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x -- ord→od x ≡ Ord x results the same - -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound ) - sup-o : ( Ordinal → Ordinal ) → Ordinal - sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + -- 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 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) - -- 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) ) + +data One : Set n where + OneObj : One + +Ords : OD +Ords = record { def = λ x → One } + +maxod : {x : OD} → od→ord x o< od→ord Ords +maxod {x} = c<→o< OneObj 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 @@ -108,12 +111,12 @@ def-subst df refl refl = df sup-od : ( OD → OD ) → OD -sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) +sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) ) sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) -sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {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 (ψ (ord→od x))) + 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 @@ -181,45 +184,6 @@ _,_ : OD → OD → OD x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) --- --- Axiom of choice in intutionistic logic implies the exclude middle --- 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 - -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 | 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 ) - ¬p : (od→ord ps ≡ o∅) → p → ⊥ - ¬p eq = lemma ( subst₂ (λ j k → j == 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∅ - 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)) - -decp : ( p : Set n ) → Dec p -- assuming axiom of choice -decp p with p∨¬p p -decp p | case1 x = yes x -decp p | case2 x = no x - -double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic -double-neg-eilm {A} notnot with decp A -- assuming axiom of choice -... | yes p = p -... | no ¬p = ⊥-elim ( notnot ¬p ) - -OrdP : ( x : Ordinal ) ( y : OD ) → 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 ) -OrdP x y | tri> ¬a ¬b c = yes c - -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) @@ -232,7 +196,7 @@ ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set Def : (A : OD ) → OD -Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) +Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n -- _⊆_ A B {x} = A ∋ x → B ∋ x @@ -283,7 +247,7 @@ 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 (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x } _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = record { def = λ x → def A x ∧ def B x } Union : OD → OD @@ -406,7 +370,7 @@ lemma1 : {a : Ordinal } { t : OD } → (eq : ZFSubset (Ord a) t == 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) (ord→od x))) + lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) lemma = sup-o< -- @@ -444,9 +408,9 @@ ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ t ∎ - lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) - lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) - lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord 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) 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)) @@ -459,21 +423,8 @@ lemma lt y<x | case1 refl = c<→o< y<x lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a - -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) - -- continuum-hyphotheis a = ? - - -- assuming axiom of choice - regularity : (x : OD) (not : ¬ (x == od∅)) → - (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - proj1 (regularity x not ) = x∋minimal x not - proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where - lemma1 : {x₁ : Ordinal} → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ - lemma1 {x₁} s = ⊥-elim ( minimal-1 x not (ord→od x₁) lemma3 ) where - lemma3 : def (minimal x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) - lemma3 = record { proj1 = def-subst {_} {_} {minimal x not} {_} (proj1 s) refl (sym diso) - ; proj2 = proj2 (proj2 s) } - lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁ - lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) + 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 @@ -499,58 +450,6 @@ ≡ od→ord (Union (x , (x , x))) lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso - -- 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 {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 {A} X∋A not = x∋minimal A not - - --- - --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice - --- - record choiced ( X : OD) : Set (suc n) where - field - a-choice : OD - is-in : X ∋ a-choice - - choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X - choice-func' X p∨¬p not = have_to_find where - ψ : ( ox : Ordinal ) → Set (suc n) - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X - lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite {ψ} induction ox where - ∋-p : (A x : OD ) → 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 )) - ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } - → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B - ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM - ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t - ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where - lemma : ¬ ((x : Ordinal ) → A x) → B - lemma not with p∨¬p B - lemma not | case1 b = b - lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) - induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x - induction x prev with ∋-p X ( ord→od x) - ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) - ... | no ¬p = lemma where - lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X - lemma1 y with ∋-p X (ord→od y) - lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) - lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) - lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X - lemma = ∀-imply-or lemma1 - have_to_find : choiced X - have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) - ¬¬X∋x nn = not record { - eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) - ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) - } - Union = ZF.Union OD→ZF Power = ZF.Power OD→ZF
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ODC.agda Sat May 09 09:02:52 2020 +0900 @@ -0,0 +1,139 @@ +open import Level +open import Ordinals +module ODC {n : Level } (O : Ordinals {n} ) where + +open import zf +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Relation.Binary.PropositionalEquality +open import Data.Nat.Properties +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary +open import Relation.Binary.Core + +open import logic +open import nat +import OD + +open inOrdinal O +open OD O +open OD.OD +open OD._==_ + +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) ) + + +-- +-- Axiom of choice in intutionistic logic implies the exclude middle +-- 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 + +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 | 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 ) + ¬p : (od→ord ps ≡ o∅) → p → ⊥ + ¬p eq = lemma ( subst₂ (λ j k → j == 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∅ + 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)) + +decp : ( p : Set n ) → Dec p -- assuming axiom of choice +decp p with p∨¬p p +decp p | case1 x = yes x +decp p | case2 x = no x + +double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic +double-neg-eilm {A} notnot with decp A -- assuming axiom of choice +... | yes p = p +... | no ¬p = ⊥-elim ( notnot ¬p ) + +OrdP : ( x : Ordinal ) ( y : OD ) → 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 ) +OrdP x y | tri> ¬a ¬b c = yes c + +open import zfc + +OD→ZFC : ZFC +OD→ZFC = record { + ZFSet = OD + ; _∋_ = _∋_ + ; _≈_ = _==_ + ; ∅ = od∅ + ; Select = Select + ; isZFC = isZFC + } where + -- infixr 200 _∈_ + -- infixr 230 _∩_ _∪_ + isZFC : IsZFC (OD ) _∋_ _==_ 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 {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 {A} X∋A not = x∋minimal A not + + --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice + --- + record choiced ( X : OD) : Set (suc n) where + field + a-choice : OD + is-in : X ∋ a-choice + + choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X + choice-func' X p∨¬p not = have_to_find where + ψ : ( ox : Ordinal ) → Set (suc n) + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X + lemma-ord : ( ox : Ordinal ) → ψ ox + lemma-ord ox = TransFinite {ψ} induction ox where + ∋-p : (A x : OD ) → 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 )) + ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } + → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B + ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM + ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where + lemma : ¬ ((x : Ordinal ) → A x) → B + lemma not with p∨¬p B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x + induction x prev with ∋-p X ( ord→od x) + ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) + ... | no ¬p = lemma where + lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X + lemma1 y with ∋-p X (ord→od y) + lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) + lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X + lemma = ∀-imply-or lemma1 + have_to_find : choiced X + have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) + ¬¬X∋x nn = not record { + eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) + } +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/README.md Sat May 09 09:02:52 2020 +0900 @@ -0,0 +1,1 @@ +zf-in-agda.ind \ No newline at end of file
--- a/cardinal.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/cardinal.agda Sat May 09 09:02:52 2020 +0900 @@ -5,6 +5,7 @@ open import zf open import logic import OD +import ODC import OPair open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality @@ -29,7 +30,7 @@ ∋-p : (A x : OD ) → Dec ( A ∋ x ) -∋-p A x with p∨¬p ( 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 @@ -59,17 +60,17 @@ 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 y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where +od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → 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 | p | no n = o∅ - lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) + 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 decp ( x1 ≡ x) + 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) y )) > ) + fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > ) open Func←cd @@ -128,15 +129,15 @@ cardinal : (X : OD ) → Cardinal X cardinal X = record { - cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) + cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) ) ; conto = onto ; cmax = cmax } where cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto X (Ord x) ) ) - cardinal-p x with p∨¬p ( Onto X (Ord x) ) + 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 x)) + 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) ) lemma1 x prev with trio< x (osuc S) @@ -153,9 +154,9 @@ ... | lift 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 x)}{y} ) lemma refl ) where + (sup-o< {λ x → proj1 ( cardinal-p {!!})}{{!!}} ) lemma refl ) where lemma : proj1 (cardinal-p y) ≡ y - lemma with p∨¬p ( Onto X (Ord y) ) + lemma with ODC.p∨¬p O ( Onto X (Ord y) ) lemma | case1 x = refl lemma | case2 not = ⊥-elim ( not ontoy )
--- a/filter.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/filter.agda Sat May 09 09:02:52 2020 +0900 @@ -81,7 +81,7 @@ import ordinal - open ordinal.C-Ordinal-with-choice + -- open ordinal.C-Ordinal-with-choice Hω2 : Filter (Power (Power infinite)) Hω2 = {!!}
--- a/ordinal.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/ordinal.agda Sat May 09 09:02:52 2020 +0900 @@ -233,62 +233,3 @@ ψ (record { lv = lx ; ord = OSuc lx x₁ }) caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev -module C-Ordinal-with-choice {n : Level} where - - import OD - -- open inOrdinal C-Ordinal - open OD (C-Ordinal {n}) - open OD.OD - open _⊆_ - - o<→c< : {x y : Ordinal } → x o< y → Ord x ⊆ Ord y - o<→c< lt = record { incl = λ lt1 → ordtrans lt1 lt } - - ⊆→o< : {x y : Ordinal } → Ord x ⊆ Ord y → x o< osuc y - ⊆→o< {x} {y} lt with trio< x y - ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc - ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc - ⊆→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 )) - - -- ZFSubset : (A x : OD ) → OD - -- ZFSubset A x = record { def = λ y → def A y ∧ def x y } - - -- Def : (A : OD ) → OD - -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) - - Ord-lemma : (a : Ordinal) → ord→od a ⊆ Ord a - Ord-lemma a = record { incl = λ lt → o<-subst (c<→o< lt ) refl diso } - - ⊆-trans : {a b c x : OD} → a ⊆ b → b ⊆ c → a ⊆ c - ⊆-trans a⊆b b⊆c = record { incl = λ a∋x → incl b⊆c (incl a⊆b a∋x) } - - _∩_ = IsZF._∩_ isZF - --- --- ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a) --- ord-power-lemma {a} = record { eq→ = left ; eq← = right } where --- left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x --- left {x} lt = lemma1 where --- lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y))) --- lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} --- lemma1 : x o< sup-o ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) --- lemma1 = {!!} --- right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x --- right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso --- --- uncountable : (a y : Ordinal) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) --- uncountable a y = ⊆→o< lemma where --- lemma-a : (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x} --- lemma-a x lt = proj1 lt --- lemma : (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x} --- lemma x = {!!} --- --- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} --- continuum-hyphotheis a x = lemma2 where --- lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a --- lemma1 = {!!} --- lemma : _⊆_ (Def (Ord a)) (Ord (osuc a)) {x} --- lemma = o<→c< lemma1 --- lemma2 : _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} --- lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma
--- a/zf.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/zf.agda Sat May 09 09:02:52 2020 +0900 @@ -48,11 +48,7 @@ power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t -- 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 ) - -- This form of regurality forces choice function - -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) - -- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet - -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimal x not ∈ x ∧ ( minimal x not ∩ x ≈ ∅ ) ) - -- another form of regularity + -- regularity without minimum ε-induction : { ψ : ZFSet → Set (suc m)} → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) → (x : ZFSet ) → ψ x @@ -63,9 +59,6 @@ -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) ) - -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] - -- choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet - -- choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where infixr 210 _,_
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/zfc.agda Sat May 09 09:02:52 2020 +0900 @@ -0,0 +1,34 @@ +module zfc where + +open import Level +open import Relation.Binary +open import Relation.Nullary +open import logic + +record IsZFC {n m : Level } + (ZFSet : Set n) + (_∋_ : ( A x : ZFSet ) → Set m) + (_≈_ : Rel ZFSet m) + (∅ : ZFSet) + (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) + : Set (suc (n ⊔ suc m)) where + field + -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet + choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A + infixr 200 _∈_ + infixr 230 _∩_ + _∈_ : ( A B : ZFSet ) → Set m + A ∈ B = B ∋ A + _∩_ : ( A B : ZFSet ) → ZFSet + A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) + +record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where + field + ZFSet : Set n + _∋_ : ( A x : ZFSet ) → Set m + _≈_ : ( A B : ZFSet ) → Set m + ∅ : ZFSet + Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet + isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select +