### changeset 258:63df67b6281c

...
author Shinji KONO Wed, 04 Sep 2019 01:12:18 +0900 53b7acd63481 f714fe999102 OD.agda Ordinals.agda cardinal.agda zf.agda 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 )```