Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 262:53744836020b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CH trying ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2019 20:26:32 +0900
parents d9d178d1457c
children 2e75710a936b
files OD.agda ordinal.agda
diffstat 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 = {!!}
+
+
+