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

changeset 78:9a7a64b2388c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite and replacement begin no Russel Pradox
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 10:19:52 +0900
parents 75ba8cf64707
children c07c548b2ac1
files ordinal-definable.agda zf.agda
diffstat 2 files changed, 21 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sun Jun 02 15:12:26 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 03 10:19:52 2019 +0900
@@ -119,27 +119,11 @@
      mino : Ordinal {n}
      min<x :  mino o< x
 
-ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x
-ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
-ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
-ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ())
-ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< }
-ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { mino = record { lv = lv ; ord = Φ lv } ; min<x = case1 (s≤s ≤-refl)}
-ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl}
-ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
-ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lx ; ord = Φ (Suc lx) } ; min<x = case2 ℵΦ<  }
-ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case2 ())
-
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
 ∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n)
 
-∅8 : {n : Level} →  ( x : Ordinal {n} )  → ¬  x o< o∅ {n}
-∅8 {n} x (case1 ())
-∅8 {n} x (case2 ())
-
 ord-iso : {n : Level} {y : Ordinal {n} } → record { lv = lv (od→ord (ord→od y)) ; ord = ord (od→ord (ord→od y)) } ≡ record { lv = lv y ; ord = ord y }
 ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
 
@@ -166,13 +150,6 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
-∅7 : {n : Level} →  { x : OD {n} } → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
-∅7 {n} {x} eq = record { eq→ = e1 (orefl eq) ; eq← = e2 } where
-   e2 : {y : Ordinal {n}} → def od∅ y → def x y 
-   e2 {y} (lift ())
-   e1 : {ox y : Ordinal {n}} → ox ≡ o∅ {n}  →  def x y → def od∅ y
-   e1 {o∅} {y} refl x>y = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
-
 =→¬< : {x : Nat  } → ¬ ( x < x )
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
@@ -227,31 +204,16 @@
 c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b ( c<→o< x<y )
 c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y
 
-∅2 : {n : Level} →  { x : OD {n} } → o∅ {n} o<  od→ord x → ¬ ( x  == od∅ {n} )
-∅2 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal (od→ord x ) lt
-... | min with eq→ ( def-subst (o<→c< (Minimumo.min<x min)) oiso refl )
-... | ()
-       
-∅0 : {n : Level} →  { x : Ordinal {n} } → o∅ {n} o< x → ¬ ( ord→od x  == od∅ {n} )
-∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt
-... | min with eq→ (o<→c< (Minimumo.min<x min))
-... | ()
-
 ∅< : {n : Level} →  { x y : OD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
 ∅< {n} {x} {y} d eq with eq→ eq d
 ∅< {n} {x} {y} d eq | lift ()
        
+∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
+∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x
 
 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
 
-is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
-is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
-is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) ) 
-is-od∅ {n} x | tri< (case1 ()) ¬b ¬c
-is-od∅ {n} x | tri< (case2 ()) ¬b ¬c
-is-od∅ {n} x | tri> ¬a ¬b c = no ( ∅2 c )
-
 is-∋ : {n : Level} →  ( x y : OD {suc n} ) → Dec ( x ∋ y )
 is-∋ {n} x y with tri-c< x y
 is-∋ {n} x y | tri< a ¬b ¬c = no ¬c
@@ -265,14 +227,6 @@
 
 open _∧_
 
-∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x
-∅9 {_} {x} not = ∅5  lemma where
-   lemma : ¬ od→ord x ≡ o∅
-   lemma eq = not ( ∅7  eq )
-
-∅10 : {n : Level} →  {ox : Ordinal {n}} → (not : ¬ (ord→od ox == od∅)) → o∅ o< ox
-∅10 {n} {ox} not = subst (λ k → o∅ o< k) diso (∅9 not)
-
 ¬∅=→∅∈ :  {n : Level} →  { x : OD {suc n} } → ¬ (  x  == od∅ {suc n} ) → x ∋ od∅ {suc n} 
 ¬∅=→∅∈  {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
      lemma : (ox : Ordinal {suc n}) →  ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
@@ -296,7 +250,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero  }  }
+    ; infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
@@ -322,7 +276,7 @@
     infixr  200 _∈_
     infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero }  })
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ))
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -335,7 +289,7 @@
        ;   extensionality = extensionality
        ;   minimul = minimul
        ;   regularity = regularity
-       ;   infinity∅ = {!!}
+       ;   infinity∅ = infinity∅
        ;   infinity = {!!}
        ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
        ;   replacement = {!!}
@@ -393,3 +347,16 @@
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+         next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
+         eq→ (next x ) {y} z = {!!}
+         eq← (next x ) {y} z = {!!}
+         infinite : OD {suc n}
+         infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
+         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ) ∋ od∅ {suc n}
+         infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
+              (o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅→od∅ )
+         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
+         infinity x ∞∋x = {!!}
+         replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
+         replacement {ψ} X x = {!!}
+
--- a/zf.agda	Sun Jun 02 15:12:26 2019 +0900
+++ b/zf.agda	Mon Jun 03 10:19:52 2019 +0900
@@ -53,6 +53,8 @@
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B) 
+  ｛_｝ : ZFSet → ZFSet
+  ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_ 
@@ -68,7 +70,7 @@
      regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
-     infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ Select X (  λ y → x ≈ y )) ∈ infinite 
+     infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
      selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )