### changeset 330:0faa7120e4b5

...
author Shinji KONO Sun, 05 Jul 2020 15:49:00 +0900 5544f4921a44 12071f79f3cf LEMC.agda OD.agda ODC.agda Ordinals.agda ordinal.agda 5 files changed, 65 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
```--- a/LEMC.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/LEMC.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -23,38 +23,42 @@

open import zfc

---- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+--- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
---
-record choiced  ( X : OD) : Set (suc n) where
+record choiced  ( X : HOD) : Set (suc n) where
field
-     a-choice : OD
+     a-choice : HOD
is-in : X ∋ a-choice

+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
open choiced

OD→ZFC : ZFC
OD→ZFC   = record {
-    ZFSet = OD
+    ZFSet = HOD
; _∋_ = _∋_
-    ; _≈_ = _==_
+    ; _≈_ = _=h=_
; ∅  = od∅
; Select = Select
; isZFC = isZFC
} where
-- infixr  200 _∈_
-- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
isZFC = record {
choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
choice = λ A {X} A∋X not → is-in (choice-func X not)
} where
-         choice-func :  (X : OD ) → ¬ ( X == od∅ ) → choiced X
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
choice-func  X not = have_to_find where
ψ : ( ox : Ordinal ) → Set (suc n)
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced X
lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
-                    ∋-p : (A x : OD ) → Dec ( A ∋ x )
+                 lemma-ord  ox = TransFinite1 {ψ} induction ox where
+                    ∋-p : (A x : HOD ) → 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 ))
@@ -71,59 +75,61 @@
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 : Ordinal) → (y o< x → odef 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
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef 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 : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt)
; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
}
-         record Minimal (x : OD)  : Set (suc n) where
+         record Minimal (x : HOD)  : Set (suc n) where
field
-               min : OD
+               min : HOD
x∋min :   x ∋ min
-               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+               min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
open Minimal
open _∧_
--
--  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
--
-         induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
-              →  (u : OD ) → (u∋x : u ∋ x) → Minimal u
-         induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
+              →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u
+         induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
... | case1 P =
record { min = x
;     x∋min = u∋x
;     min-empty = P
}
... | case2 NP =  min2 where
-              p : OD
-              p  = record { def = λ y1 → def x  y1 ∧ def u y1 }
-              np : ¬ (p == od∅)
+              p : HOD
+              p  = record { od = record { def = λ y1 → odef x  y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
+                 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
+                 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
+              np : ¬ (p =h= od∅)
np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ )
y1choice : choiced p
y1choice = choice-func p np
-              y1 : OD
+              y1 : HOD
y1 = a-choice y1choice
y1prop : (x ∋ y1) ∧ (u ∋ y1)
y1prop = is-in y1choice
min2 : Minimal u
min2 = prev (proj1 y1prop) u (proj2 y1prop)
-         Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u
-         Min2 x u u∋x = (ε-induction {λ y →  (u : OD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x )
-         cx : {x : OD} →  ¬ (x == od∅ ) → choiced x
+         Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
+         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x )
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x
cx {x} nx = choice-func x nx
-         minimal : (x : OD  ) → ¬ (x == od∅ ) → OD
+         minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD
minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not)))
-         x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne)))
-         minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y

```
```--- a/OD.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/OD.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -260,6 +260,15 @@
ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy

+ε-induction1 : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+
HOD→ZF : ZF
HOD→ZF   = record {
ZFSet = HOD ```
```--- a/ODC.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/ODC.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -31,7 +31,7 @@
minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD
-- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
-  -- minimality (may proved by ε-induction )
+  -- minimality (may proved by ε-induction with LEM)
minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )

@@ -40,8 +40,8 @@
--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
--

--- ppp :  { p : Set n } { a : HOD  } → record { def = λ x → p } ∋ a → p
--- ppp  {p} {a} d = d
+ppp :  { p : Set n } { a : HOD  } → record { od = record { def = λ x → p } ; odmax = {!!} ; <odmax = {!!} } ∋ 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 { odef = λ x → p } ))```
```--- a/Ordinals.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -25,6 +25,9 @@
TransFinite : { ψ : ord  → Set n }
→ ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : ord)  → ψ x
+     TransFinite1 : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x

record Ordinals {n : Level} : Set (suc (suc n)) where
@@ -57,6 +60,7 @@
osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
<-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
+        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)

o<-dom :   { x y : Ordinal } → x o< y → Ordinal ```
```--- a/ordinal.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -219,6 +219,7 @@
; <-osuc = <-osuc
; osuc-≡< = osuc-≡<
; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
; not-limit = not-limit
; next-limit = next-limit
}
@@ -244,4 +245,15 @@
caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
ψ (record { lv = lx ; ord = OSuc lx x₁ })
caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev

+```