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 )