Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1097:40345abc0949
add README
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Dec 2022 11:39:30 +0900 |
| parents | 55ab5de1ae02 |
| children | 9dcbf3524a5c |
| files | src/NSet.agda src/OD.agda src/README.md src/zorn.agda |
| diffstat | 4 files changed, 250 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/NSet.agda Sat Dec 24 11:39:30 2022 +0900 @@ -0,0 +1,105 @@ +open import Level +module NSet (n : Level) where + +open import logic +open import nat +open import Data.Nat hiding (suc ; zero) +open import Data.Nat.Properties +open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +-- +-- Primitive Set on ℕ +-- + +record NSet : Set (suc zero) where + field + def : ℕ → Set + +-- +-- Set as an equation on ℕ +-- +eqa1 : NSet +eqa1 = record { def = λ x → x * x + 6 ≡ 5 * x } + +open NSet + +_∋_ : NSet → ℕ → Set +S ∋ x = def S x + +eq1∋2 : eqa1 ∋ 2 +eq1∋2 = refl + +eq1∋3 : eqa1 ∋ 3 +eq1∋3 = refl + +-- +-- The solution +-- + +eqa2 : NSet +eqa2 = record { def = λ x → (x ≡ 2) ∨ ( x ≡ 3 ) } + +eq2∋3 : eqa2 ∋ 3 +eq2∋3 = case2 refl + +record _==_ ( a b : NSet ) : Set where + field + eq→ : ∀ { x : ℕ } → def a x → def b x + eq← : ∀ { x : ℕ } → def b x → def a x + +_⊆_ : (a b : NSet ) → Set +_⊆_ a b = ∀ {x : ℕ} → def a x → def b x + +eq2⊆eq1 : eqa2 ⊆ eqa1 +eq2⊆eq1 {2} (case1 refl) = refl +eq2⊆eq1 {3} (case2 refl) = refl + +-- the other way is slightly difficut + +data ⊥ : Set where + +⊥-elim : {A : Set } → ⊥ → A +⊥-elim () + +¬_ : Set → Set +¬ A = A → ⊥ + +n∅ : NSet +n∅ = record { def = λ y → y < 0 } + +¬n∅∋x : {x : ℕ } → ¬ ( n∅ ∋ x ) +¬n∅∋x () + +¬n∅∋x' : {x : ℕ } → ¬ ( n∅ ∋ x ) +¬n∅∋x' {x} nx = ⊥-elim ( n1 nx ) where + n1 : x < 0 → ⊥ + n1 () + +-- +-- Set of subset of ℕ +-- + +record NSetSet : Set (suc zero) where + field + ndef : NSet → Set + +open NSetSet + +record _=n=_ ( a b : NSetSet ) : Set (suc zero) where + field + eq→ : ∀ { x : NSet } → ndef a x → ndef b x + eq← : ∀ { x : NSet } → ndef b x → ndef a x + +eqa3 : NSetSet +eqa3 = record { ndef = λ x → x == eqa2 } + +-- +-- Can we defined hierarchy of Set in monothic and consitent way? +-- equations on Ordinal is an solution (Ordinal Definable Set) +-- but we need some axioms to achive ZF Set Theory +-- + + + +
--- a/src/OD.agda Fri Dec 23 12:54:05 2022 +0900 +++ b/src/OD.agda Sat Dec 24 11:39:30 2022 +0900 @@ -99,9 +99,9 @@ *iso : {x : HOD } → * ( & x ) ≡ x &iso : {x : Ordinal } → & ( * 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 ) → Ordinal -- required in Replace sup-o≤ : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤ sup-o A ψ --- possible order restriction +-- possible order restriction (required in the axiom of infinite ) ho< : {x : HOD} → & x o< next (odmax x) @@ -402,12 +402,7 @@ -- This means that many of OD may not be HODs because of the & mapping divergence. -- We should have some axioms to prevent this such as & x o< next (odmax x). -- --- 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 } +-- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho< infinite : HOD infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/README.md Sat Dec 24 11:39:30 2022 +0900 @@ -0,0 +1,117 @@ +Constructing ZF Set Theory in Agda +============ + +Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus + +## ZF in Agda + +``` + zf.agda axiom of ZF + zfc.agda axiom of choice + Ordinals.agda axiom of Ordinals + ordinal.agda countable model of Ordinals + OD.agda model of ZF based on Ordinal Definable Set with assumptions + ODC.agda Law of exclude middle from axiom of choice assumptions + LEMC.agda model of choice with assumption of the Law of exclude middle + OPair.agda ordered pair on OD + zorn.agda Zorn Lemma + + BAlgbra.agda Boolean algebra on OD (not yet done) + filter.agda Filter on OD (not yet done) + cardinal.agda Caedinal number on OD (not yet done) + + logic.agda some basics on logic + nat.agda some basics on Nat + + NSet.agda primitve set thoery examples + + ODUtil.agda + OrdUtil.agda + PFOD.agda + Topology.agda + VL.agda + generic-filter.agda + partfunc.agda + +``` + +## Ordinal Definable Set + +It is a predicate has an Ordinal argument. + +In Agda, OD is defined as follows. + +``` + record OD : Set (suc n ) where + field + def : (x : Ordinal ) → Set n +``` + +This is not a ZF Set, because it can contain entire Ordinals. + +## HOD : Hereditarily Ordinal Definable + +What we need is a bounded OD, the containment is limited by an ordinal. + +``` + record HOD : Set (suc n) where + field + od : OD + odmax : Ordinal + <odmax : {y : Ordinal} → def od y → y o< odmax +``` + +In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means + +``` + HOD = { x | TC x ⊆ OD } +``` + +TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But +what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. + +## 1 to 1 mapping between an HOD and an Ordinal + +HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping + +``` + od→ord : HOD → Ordinal + ord→od : Ordinal → HOD + oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x +``` + +we can check an HOD is an element of the OD using def. + +A ∋ x can be define as follows. + +``` + _∋_ : ( A x : HOD ) → Set n + _∋_ A x = def (od A) ( od→ord x ) + +``` +In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then + + A x = def A ( od→ord x ) = ψ (od→ord x) + +They say the existing of the mappings can be proved in Classical Set Theory, but we +simply assumes these non constructively. + +## we need some more axiom to achive ZF Set Theory + +``` + record ODAxiom : Set (suc n) where + field + -- HOD is isomorphic to Ordinal (by means of Goedel number) + & : HOD → Ordinal + * : Ordinal → HOD + c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y + ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) + *iso : {x : HOD } → * ( & x ) ≡ x + &iso : {x : Ordinal } → & ( * x ) ≡ x + ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y + sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal -- required in Replace + sup-o≤ : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤ sup-o A ψ + -- possible order restriction (required in the axiom of infinite ) + ho< : {x : HOD} → & x o< next (odmax x) +```
--- a/src/zorn.agda Fri Dec 23 12:54:05 2022 +0900 +++ b/src/zorn.agda Sat Dec 24 11:39:30 2022 +0900 @@ -243,6 +243,9 @@ -- -- Our Proof strategy of the Zorn Lemma -- +-- As ZChain.cfcs closure of supf z is smaller than next supf z1, and supf z o< supfz1, because of mf< +-- if have to be stopped since we have upper bound & A, so there is a Maximul element. +-- -- f (f ( ... (supf y))) f (f ( ... (supf z1))) -- / | / | -- / | / | @@ -250,7 +253,6 @@ -- o< o< -- -- if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1 --- this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal. -- fc-stop : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } @@ -312,9 +314,6 @@ x≤sup = IsMinSUP.x≤sup isMinSUP minsup = IsMinSUP.minsup isMinSUP -z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A -z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) - chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b → odef (UnionCF A f ay supf a) c → odef (UnionCF A f ay supf b) c @@ -326,11 +325,11 @@ field supf : Ordinal → Ordinal + asupf : {x : Ordinal } → odef A (supf x) + is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) supf-mono : {a b : Ordinal } → a o≤ b → supf a o≤ supf b cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w - asupf : {x : Ordinal } → odef A (supf x) - zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x - is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) + zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x -- because of mf< chain : HOD chain = UnionCF A f ay supf z @@ -357,7 +356,10 @@ ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) - csupf : {b : Ordinal } → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) -- supf z is not an element of this chain + -- another kind of maximality of the chain + -- note that supf z is not an element of this chain + -- + csupf : {b : Ordinal } → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) csupf {b} sb<sz sb<z = cfcs (supf-inject sb<sz) o≤-refl sb<z (init asupf refl) minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f ay supf x) @@ -390,6 +392,9 @@ ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) + -- + -- supf is minsup, so its UniofCF are equal, these are equal + -- supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( @@ -398,6 +403,9 @@ ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) + -- + -- supf a over b and supf a is not included in UnionCF a nor UnionCF b, so UnionCF b is equal to the UnionCF a + -- union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b union-max {a} {b} b≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w @@ -613,7 +621,7 @@ ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫ ) ... | case2 notz = case1 (λ _ → notz ) m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z) - m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where + m03 not = ⊥-elim ( not s1 (odef< (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where S : SUP A B S = supP B B⊆A total s1 = & (SUP.sup S) @@ -682,9 +690,9 @@ is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) ... | case2 sb<sx = m10 where b<A : b o< & A - b<A = z09 ab + b<A = odef< ab m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (odef< ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } m10 : odef (UnionCF A f ay supf x) b m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where @@ -700,7 +708,7 @@ m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (odef< ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -732,7 +740,7 @@ m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x) m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } + m05 = ZChain.sup=u zc ab (o<→≤ (odef< ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -802,7 +810,7 @@ ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x)) } ; odmax = & A ; <odmax = zc00 } where zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x) )→ z o< & A zc00 {z} (case1 lt) = z07 lt - zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf (proj1 fc) ) + zc00 {z} (case2 fc) = odef< ( A∋fc (supf0 px) f mf (proj1 fc) ) zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b ∧ ( supf0 px o< x) → a ≤ b zc02 {a} {b} ca fb = zc05 (proj1 fb) where @@ -1241,7 +1249,7 @@ ∨ (FClosure A f spu0 z ∧ (spu0 o< x)) } ; odmax = & A ; <odmax = zc00 } where zc00 : {z : Ordinal } → (odef A z ∧ IChain ay supfz z ) ∨ (FClosure A f spu0 z ∧ (spu0 o< x) )→ z o< & A zc00 {z} (case1 lt) = z07 lt - zc00 {z} (case2 fc) = z09 ( A∋fc spu0 f mf (proj1 fc) ) + zc00 {z} (case2 fc) = odef< ( A∋fc spu0 f mf (proj1 fc) ) zc02 : { a b : Ordinal } → odef A a ∧ IChain ay supfz a → FClosure A f spu0 b ∧ ( spu0 o< x) → a ≤ b zc02 {a} {b} ca fb = zc05 (proj1 fb) where @@ -1518,11 +1526,11 @@ → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl ) z22 : sp o< & A - z22 = z09 asp + z22 = odef< asp z12 : odef chain sp z12 with o≡? (& s) sp ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) - ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where + ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (odef< asp) asp (case2 z19 ) z13 where z13 : * (& s) < * sp z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne eq )