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

changeset 183:de3d87b7494f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix zf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Jul 2019 17:56:12 +0900
parents 9f3c0e0b2bc9
children 65e1b2e415bb
files OD.agda ordinal.agda zf.agda
diffstat 3 files changed, 15 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sun Jul 21 12:11:50 2019 +0900
+++ b/OD.agda	Sun Jul 21 17:56:12 2019 +0900
@@ -71,10 +71,11 @@
   -- sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   -- sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
-  -- mimimul and x∋minimul is a weaker form of Axiom of choice
+  -- mimimul and x∋minimul is an Axiom of choice
   minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
+  -- 
   minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
@@ -292,13 +293,14 @@
        ;   power→ = power→  
        ;   power← = power← 
        ;   extensionality = extensionality
-       ;   minimul = minimul
-       ;   regularity = regularity
+       ;   ε-induction = ε-induction
        ;   infinity∅ = infinity∅
        ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
        ;   replacement→ = replacement→
+       ;   choice-func = choice-func
+       ;   choice = choice
      } where
 
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
--- a/ordinal.agda	Sun Jul 21 12:11:50 2019 +0900
+++ b/ordinal.agda	Sun Jul 21 17:56:12 2019 +0900
@@ -343,4 +343,3 @@
   → ¬ p
 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
-   
--- a/zf.agda	Sun Jul 21 12:11:50 2019 +0900
+++ b/zf.agda	Sun Jul 21 17:56:12 2019 +0900
@@ -71,9 +71,14 @@
      power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → A ≈ B
+     -- 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  ≈ ∅ ) )
+     -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
+     -- regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )
+     -- another form of regularity
+     ε-induction : { ψ : ZFSet → Set m}
+             → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
+             → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
@@ -81,9 +86,9 @@
      -- 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 ∈ X → ψ x ∈  Replace X ψ 
      replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
-   -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
-   -- axiom-of-choice : Set (suc n) 
-   -- axiom-of-choice = ?
+     -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
+     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
 
 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
   infixr  210 _,_