Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 258:63df67b6281c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 04 Sep 2019 01:12:18 +0900 |
| parents | 53b7acd63481 |
| children | f714fe999102 |
| files | OD.agda Ordinals.agda cardinal.agda zf.agda |
| diffstat | 4 files changed, 44 insertions(+), 36 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Fri Aug 30 15:37:04 2019 +0900 +++ b/OD.agda Wed Sep 04 01:12:18 2019 +0900 @@ -58,6 +58,11 @@ od∅ : OD od∅ = Ord o∅ +-- next assumptions are our axiom +-- it defines a subset of OD, which is called HOD, usually defined as +-- 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 + postulate -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) od→ord : OD → Ordinal @@ -67,7 +72,7 @@ diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x -- we should prove this in agda, but simply put here ==→o≡ : { x y : OD } → (x == y) → x ≡ y - -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set + -- 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 @@ -76,12 +81,19 @@ -- 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∋minimul is an Axiom of choice - minimul : (x : OD ) → ¬ (x == od∅ )→ OD + -- 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∋minimul : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) - -- minimulity (may proved by ε-induction ) - minimul-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) + 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) ) + +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 : OD ) → Set n _∋_ a x = def a ( od→ord x ) @@ -89,9 +101,6 @@ _c<_ : ( x a : OD ) → Set n x c< a = a ∋ x -_c≤_ : OD → OD → Set (suc n) -a c≤ b = (a ≡ b) ∨ ( b ∋ a ) - cseq : {n : Level} → OD → OD cseq x = record { def = λ y → def x (osuc y) } where @@ -113,6 +122,7 @@ 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 + -- avoiding lv != Zero error orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl @@ -136,9 +146,6 @@ o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y o≡→== {x} {.x} refl = eq-refl -c≤-refl : {n : Level} → ( x : OD ) → x c≤ x -c≤-refl x = case1 refl - o∅≡od∅ : ord→od (o∅ ) ≡ od∅ o∅≡od∅ = ==→o≡ lemma where lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x @@ -296,12 +303,12 @@ 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} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where +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 ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) - lemma = x∋minimul ps (λ eq → ¬p (eqo∅ 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 @@ -431,7 +438,7 @@ 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 ))) - union← X z UX∋z = TransFiniteExists _ lemma UX∋z where + 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 } @@ -462,7 +469,6 @@ --- First consider ordinals in OD --- --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A - --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A -- -- ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) @@ -471,8 +477,10 @@ proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; eq← = λ {x} x<a∩b → proj2 x<a∩b } -- - -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t - -- Power A is a sup of ZFSubset A t, so Power A ∋ t + -- 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 )) ) ) -- 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} @@ -489,14 +497,15 @@ lemma = sup-o< -- - -- Every set in OD is a subset of Ordinals + -- Every set in OD is a subset of Ordinals, so make Def (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 ) -- 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 P∋t {x} t∋x = TransFiniteExists _ lemma5 lemma4 where + 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 @@ -534,15 +543,15 @@ -- assuming axiom of choice regularity : (x : OD) (not : ¬ (x == od∅)) → - (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - proj1 (regularity x not ) = x∋minimul x not + (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 (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ - lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where - lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) - lemma3 = record { proj1 = def-subst {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso) + 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 (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ + 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) )) extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B @@ -569,12 +578,12 @@ ≡ 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 minimul in our case ) + -- 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 = minimul x not + 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∋minimul A not + choice X {A} X∋A not = x∋minimal A not --- --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
--- a/Ordinals.agda Fri Aug 30 15:37:04 2019 +0900 +++ b/Ordinals.agda Wed Sep 04 01:12:18 2019 +0900 @@ -193,9 +193,9 @@ } } - TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m ) + FExists : {m l : Level} → ( ψ : Ordinal → Set m ) → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) → (exists : ¬ (∀ y → ¬ ( ψ y ) )) → ¬ p - TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
--- a/cardinal.agda Fri Aug 30 15:37:04 2019 +0900 +++ b/cardinal.agda Wed Sep 04 01:12:18 2019 +0900 @@ -48,7 +48,6 @@ -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) - func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
--- a/zf.agda Fri Aug 30 15:37:04 2019 +0900 +++ b/zf.agda Wed Sep 04 01:12:18 2019 +0900 @@ -50,8 +50,8 @@ 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 = ∅ ) ) - -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet - -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) + -- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet + -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimal x not ∈ x ∧ ( minimal x not ∩ x ≈ ∅ ) ) -- another form of regularity -- ε-induction : { ψ : ZFSet → Set m} -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x )