...
author Shinji KONO Fri, 16 Aug 2019 15:53:29 +0900 846e0926bb89 521290e85527 cardinal.agda filter.agda ordinal.agda zf.agda 4 files changed, 56 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
```--- a/cardinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/cardinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -27,7 +27,7 @@
<_,_> : (x y : OD) → OD
< x , y > = (x , x ) , (x , y )

-record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where
+record SetProduct ( A B : OD )  : Set n where
field
π1 : Ordinal
π2 : Ordinal
@@ -43,7 +43,7 @@
∋-p A x | case2 t = no t

_⊗_  : (A B : OD) → OD
-A ⊗ B  = record { def = λ x → SetProduct A B x }
+A ⊗ B  = record { def = λ x → SetProduct A B  }
-- A ⊗ B  = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }

--  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
@@ -63,9 +63,27 @@
... | yes _ = π2 t
... | no _ = o∅

+
func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )

+record Func←cd { dom cod : OD } {f : Ordinal } (f<F :  def (Func dom cod ) f) : Set n where
+   field
+      func-1 : Ordinal → Ordinal
+      func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
+
+func←od1 : { dom cod : OD } → {f : Ordinal }  → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
+func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
+   lemma : Ordinal → Ordinal → Ordinal
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y | p | no n  = o∅
+   lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
+   ... | t with decp ( x  ≡ π1 t )
+   ... | yes _ = π2 t
+   ... | no _ = o∅
+
+func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom
+func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} }

-- contra position of sup-o<
--```
```--- a/filter.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/filter.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -1,8 +1,10 @@
open import Level
-open import OD
+open import Ordinals
+module filter {n : Level } (O : Ordinals {n})   where
+
open import zf
-open import ordinal
-module filter ( n : Level )  where
+open import logic
+import OD

open import Relation.Nullary
open import Relation.Binary
@@ -12,23 +14,28 @@
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )

-od = OD→ZF {n}
-
+open inOrdinal O
+open OD O
+open OD.OD

-record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+open _∧_
+open _∨_
+open Bool
+
+record Filter  ( P max : OD  )  : Set (suc n) where
field
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
-       G : OD {suc n}
+       _⊇_ : OD  → OD  → Set n
+       G : OD
G∋1 : G ∋ max
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  max
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gmax : { p : OD  } → P ∋ p → p ⊇  max
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))

-dense :  {n : Level} → Set (suc (suc n))
-dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
+dense :   Set (suc n)
+dense = { D P p : OD  } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))

-record NatFilter {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+record NatFilter  ( P : Nat → Set n)  : Set (suc n) where
field
GN : Nat → Set n
GN∋1 : GN 0
@@ -46,16 +53,16 @@

-- H(ω,2) = Power ( Power ω ) = Def ( Def ω))

-Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
-Pred {n} dom = record {
-      def = λ x → def dom x → Set n
+Pred :  ( Dom : OD  ) → OD
+Pred  dom = record {
+      def = λ x → def dom x → {!!}
}

-Hω2 : {n : Level} →  OD {suc n}
-Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+Hω2 :   OD
+Hω2  = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }

-Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
-Hω2Filter {n} = record {
+Hω2Filter :     Filter  Hω2 od∅
+Hω2Filter  = record {
_⊇_ = _⊇_
; G = {!!}
; G∋1 = {!!}
@@ -64,17 +71,17 @@
; Gcompat = {!!}
} where
P = Hω2
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ : OD  → OD  → Set n
_⊇_ = {!!}
-       G : OD {suc n}
+       G : OD
G = {!!}
G∋1 : G ∋ od∅
G∋1 = {!!}
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax : { p : OD  } → P ∋ p → p ⊇  od∅
Gmax = {!!}
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
Gless = {!!}
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
Gcompat = {!!}
```
```--- a/ordinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/ordinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -204,21 +204,6 @@
lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1

--- we cannot prove this in intutionistic logic
---  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
--- 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 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 )

open import Ordinals
```
```--- a/zf.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/zf.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -34,7 +34,7 @@
_∩_ : ( A B : ZFSet  ) → ZFSet
A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
_∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
+  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
｛_｝ : ZFSet → ZFSet
｛ x ｝ = ( x ,  x )
infixr  200 _∈_```