### changeset 262:53744836020b

CH trying ...
author Shinji KONO Sun, 22 Sep 2019 20:26:32 +0900 d9d178d1457c 2e75710a936b OD.agda ordinal.agda 2 files changed, 42 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Tue Sep 17 09:29:27 2019 +0900
+++ b/OD.agda	Sun Sep 22 20:26:32 2019 +0900
@@ -361,6 +361,9 @@
ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy

+-- minimal-2 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+-- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
+
OD→ZF : ZF
OD→ZF   = record {
ZFSet = OD
@@ -548,6 +551,16 @@
lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))

+         ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x}
+         ord⊆power a x lt = power← (Ord a) x lemma where
+                lemma : {y : OD} → x ∋ y → Ord a ∋ y
+                lemma y<x with osuc-≡< lt
+                lemma y<x | case1 refl = c<→o< y<x
+                lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
+
+         -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
+         -- continuum-hyphotheis a x = ?
+
--  assuming axiom of choice
regularity :  (x : OD) (not : ¬ (x == od∅)) →
(x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)```
```--- a/ordinal.agda	Tue Sep 17 09:29:27 2019 +0900
+++ b/ordinal.agda	Sun Sep 22 20:26:32 2019 +0900
@@ -203,7 +203,6 @@
lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1

-
open import Ordinals

C-Ordinal : {n : Level} →  Ordinals {suc n}
@@ -240,4 +239,32 @@
-- open inOrdinal C-Ordinal
open OD (C-Ordinal {n})
open OD.OD
-
+
+  o<→c< :  {x y : Ordinal } {z : OD }→ x o< y → _⊆_  (Ord x) (Ord y) {z}
+  o<→c< lt lt1 = ordtrans lt1 lt
+
+  ⊆→o< :  {x y : Ordinal } → (∀ (z : OD) → _⊆_  (Ord x) (Ord y) {z} ) →  x o< osuc y
+  ⊆→o< {x} {y}  lt with trio< x y
+  ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
+  ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
+  ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
+  ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
+
+  uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y)
+  uncountable a y = TransFinite {n} {suc n} {λ z → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od z)} caseΦ caseOSuc y where
+       caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od x))
+             → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = Φ lx }))
+       caseΦ lx prev = {!!}
+       caseOSuc : (lx : Nat) (ox : OrdinalD lx)
+             → ((y₁ : Ordinal) → y₁ o< ordinal lx (OSuc lx ox) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y₁))
+             → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = OSuc lx ox }))
+       caseOSuc lx ox prev = {!!}
+
+  continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
+  continuum-hyphotheis a x lt = lemma where
+       lemma : Ord (osuc a) ∋ x
+       lemma with IsZF.power→ isZF (Ord a) x lt {{!!}} {!!}
+       ... | t = {!!}
+
+
+```