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

changeset 166:ea0e7927637a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use double negation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Jul 2019 10:52:31 +0900
parents d16b8bf29f4f
children 4724f7be00e3
files HOD.agda ordinal-definable.agda ordinal.agda zf.agda
diffstat 4 files changed, 32 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Tue Jul 16 09:57:01 2019 +0900
+++ b/HOD.agda	Wed Jul 17 10:52:31 2019 +0900
@@ -57,8 +57,8 @@
   -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
   od→ord : {n : Level} → OD {n} → Ordinal {n}
   ord→od : {n : Level} → Ordinal {n} → OD {n} 
-  c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
-  oiso   : {n : Level} {x : OD {n}}     → ord→od ( od→ord x ) ≡ x
+  c<→o<  : {n : Level} {x y : OD {n} }   → def y ( od→ord x ) → od→ord x o< od→ord y
+  oiso   : {n : Level} {x : OD {n}}      → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   -- we should prove this in agda, but simply put here
   ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
@@ -319,10 +319,9 @@
          union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
               ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
          union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
-         union← X z UX∋z =  TransFiniteExists' _ lemma UX∋z where
+         union← X z UX∋z =  TransFiniteExists _ lemma UX∋z where
               lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
               lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
-              -- ( λ {y} xx →  
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
@@ -377,22 +376,27 @@
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
+         -- double-neg-eilm : {n  : Level } {A : Set n} → ¬ ¬ A → A
+         -- double-neg-eilm {n} {A} notnot = ⊥-elim (notnot (λ A → {!!} ))
          -- 
          -- Every set in OD is a subset of Ordinals
          -- 
          -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
-         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = TransFiniteExists _ -- (λ y → (t ==  (A ∩ ord→od y)))
-                 lemma4 lemma5  where
+
+         -- we have oly double negation form because of the replacement axiom
+         --
+         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         power→ A t P∋t {x} t∋x = TransFiniteExists _ lemma5 lemma4 where
               a = od→ord A
               lemma2 : ¬ ( (y : OD) → ¬ (t ==  (A ∩ y)))
               lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
-              lemma3 : (y : OD) → t == ( A ∩ y ) → A ∋ x
-              lemma3 y eq = proj1 (eq→ eq t∋x)
+              lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
+              lemma3 y eq not = not (proj1 (eq→ eq t∋x))
               lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y)))
               lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 ))
-              lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → def A (od→ord x)
-              lemma5 {y} eq = lemma3 (ord→od y) eq
+              lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) →  ¬ ¬  (def A (od→ord x))
+              lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
+
          power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
               a = od→ord A
--- a/ordinal-definable.agda	Tue Jul 16 09:57:01 2019 +0900
+++ b/ordinal-definable.agda	Wed Jul 17 10:52:31 2019 +0900
@@ -368,8 +368,8 @@
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
          --
-         power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = proj1 lemma-s where
+         power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         power→ A t P∋t {x} t∋x = double-neg (proj1 lemma-s) where
               minsup :  OD
               minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
               lemma-t : csuc minsup ∋ t
--- a/ordinal.agda	Tue Jul 16 09:57:01 2019 +0900
+++ b/ordinal.agda	Wed Jul 17 10:52:31 2019 +0900
@@ -321,21 +321,20 @@
 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
 
+-- we cannot prove this in intutonistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
---      may be we can prove this...
-postulate 
- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
-  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
-  → p
-
--- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
---     lemma : (y : Ordinal {n} ) → ¬ ψ y
---     lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy
-TransFiniteExists' : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
+-- postulate 
+--  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
+--   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+--   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
+--   → p
+--
+-- Instead we prove
+--
+TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
   → ¬ p
-TransFiniteExists' {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
    
--- a/zf.agda	Tue Jul 16 09:57:01 2019 +0900
+++ b/zf.agda	Wed Jul 17 10:52:31 2019 +0900
@@ -25,6 +25,9 @@
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a ) 
 
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_
@@ -64,7 +67,7 @@
   field
      empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
      -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
-     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  _⊆_ t A {x} 
+     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} 
      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