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

changeset 1439:900c98ffde05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2023 09:28:09 +0900
parents 5d69ed581269
children a7d46b1c2a70
files src/bijection.agda src/cardinal.agda src/logic.agda
diffstat 3 files changed, 100 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jul 02 20:36:08 2023 +0900
+++ b/src/bijection.agda	Tue Jul 04 09:28:09 2023 +0900
@@ -525,7 +525,8 @@
     --
     --     an     f     g     cn
     --   ℕ ↔   A  →  B  →  C  ↔   ℕ
-    --
+    --            B = Image A f ∪ (B \ Image A f )
+    -- 
     open Bijection
     f = InjectiveF.f fi
     g = InjectiveF.f gi
--- a/src/cardinal.agda	Sun Jul 02 20:36:08 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 09:28:09 2023 +0900
@@ -141,6 +141,13 @@
           fbiso x (case1 b) = fiso→ ab x b
           fbiso x (case2 d) = fiso→ cd x d
 
+--
+--  f : A → B        OrdBijection A           (Image A f)
+--  g : B → A        OrdBijection (Image B g) B
+--                     UC (closure of g ∙ f from ¬ Image B g )
+--                         A =   UC ∪ (A \ Image B g )
+--                         B =   (Image B g) UC 
+--
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b)
 Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })
      = subst₂ (λ j k → HODBijection j k ) (sym a=UC∨a-UC) (sym b=fUC∨b-fUC) (bi-∪  bi-UC  bi-fUC)
@@ -307,7 +314,7 @@
 
 
 _c<_ : ( A B : HOD ) → Set n
-A c< B = ¬ ( Injection (& A)  (& B) )
+A c< B = ¬ ( Injection (& B)  (& A) )
 
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ HODBijection (* a) (* x) }
@@ -321,11 +328,98 @@
 -- Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
 -- Cardinal∈ = {!!}
 
--- Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
+-- Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t ) -- this is not valid
 -- Cardinal⊆ = {!!}
 
-Cantor1 : { u : HOD } → u c< Power u
-Cantor1 = {!!}
+-- HBool : HOD
+-- HBool = record { od = record { def = λ x → (x ≡ o∅) ∨ (x ≡ osuc o∅ ) } ; odmax = osuc (osuc o∅) ; <odmax = ? }
+
+PtoF : {u : HOD} {x s : Ordinal } → odef (Power u) s → odef u x → Bool
+PtoF {u} {x} {s} su ux with ODC.p∨¬p O (odef (* s) x )
+... | case1 a = true
+... | case2 b = false
+
+--    S
+--    t ⊆ S    ( Power S ∋ t )
+--    S   s₀    s₁      ...  sn
+--    t   true  false   ...  false
+---
+Cantor1 : { S : HOD } → {s : Ordinal } → odef S s → S c< Power S
+Cantor1 {S} {s} ss f = diagn1 ss ? where
+     f1 : Injection (& S) (& (Power S))
+     f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = ? }where
+         c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
+         c00 x lt = subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z  )) where
+             c01 : (y : Ordinal ) → odef (* x , * x ) y  → odef S y
+             c01 y (case1 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
+             c01 y (case2 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
+     f2 : Injection (& (Power S)) (& S) 
+     f2 = f
+     b : HODBijection (Power S) S 
+     b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)
+
+     decS : (S : HOD) (x : Ordinal) → odef S x ∨ ( ¬ odef S x )
+     decS S x = ODC.p∨¬p O (odef S x )
+
+     record T : Set n where
+        field
+           x : Ordinal
+           Sx : odef S x
+
+     --  HODBijection (Power S) S  → Bijection ( T → Bool ) T
+     -- 
+     --  bt : Bijection (T → Bool) T
+     --    fun← : T → (T → Bool)
+     --    fun→ : (T → Bool) → T  
+
+     record TT ( isT : T → Bool ) (x : Ordinal) : Set n where
+        field
+           sx : odef S x
+           T=true : isT record { x = x ; Sx = sx } ≡ true
+
+     sx→T : {x : Ordinal } → odef S x → T 
+     sx→T {x} sx = record { x = x ; Sx = sx }
+
+     tb : (T → Bool ) → Ordinal
+     tb fx = & record { od = record { def = λ x → TT fx x} ; odmax = & S ; <odmax = ? } 
+
+     TB→PS : (fx : T → Bool ) → odef (Power S) (tb fx)
+     TB→PS  fx y txy with subst (λ k → odef k y ) *iso txy
+     ... | tt = TT.sx tt
+
+     PS→TB : {x : Ordinal } → odef (Power S) x → T → Bool
+     PS→TB {x} psx t with decS (* x) (T.x t) 
+     ... | case1 iss  = true 
+     ... | case2 niss = false
+
+     s← : T → (T → Bool )
+     s← t = PS→TB ( funA b (T.x t) (T.Sx t) )
+
+     s→ : (T → Bool) → T 
+     s→ fx  = record { x = fun← b (tb fx) (TB→PS fx) ; Sx = funB b (tb fx) (TB→PS fx) }   
+
+     --   we can prove bt here
+     --   but prove contradiction directly
+
+     ---  if t ∋ x then false else true 
+     ---    diag : T → Bool
+
+     diag : {x : Ordinal } → odef S x → Bool
+     diag {x} sx = not (s← (sx→T sx) (sx→T sx) ) 
+
+     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x sx ≡ x )
+     diagn1 {x} sx dn = ¬t=f (diag sx ) ( begin
+           not (diag  sx  )
+        ≡⟨⟩
+           not (not (s← (sx→T sx) (sx→T sx) ) )
+        ≡⟨ cong (λ k → not k ) (sym ? ) ⟩
+           not (s← (s→ (λ t → diag (T.Sx t)) ) (sx→T sx) )
+        ≡⟨ cong (λ k → not ? ) dn ⟩
+           not (s← (sx→T sx) (sx→T sx) ) 
+        ≡⟨⟩
+           diag  sx 
+        ∎ ) where open ≡-Reasoning
+
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}
--- a/src/logic.agda	Sun Jul 02 20:36:08 2023 +0900
+++ b/src/logic.agda	Tue Jul 04 09:28:09 2023 +0900
@@ -5,7 +5,6 @@
 open import Relation.Binary hiding (_⇔_ )
 open import Data.Empty
 
-
 data Bool : Set where
     true : Bool
     false : Bool