Members/kono/Proof/ZF-in-agda: constructible-set.agda comparison

comparison constructible-set.agda @ 27:bade0a35fdd9

OD, HOD, TC

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 19 May 2019 15:30:04 +0900
parents	a53ba59c5bda
children	f36e40d5d2c3

comparison

equal deleted inserted replaced

-:a53ba59c5bda
+:bade0a35fdd9
 ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx)
 ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  OSuc  (Suc lx) x d< (ℵ lx)
 open Ordinal
-_o<_ : {n : Level} ( x y : Ordinal ) → Set (suc n)
+_o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 maxα x y | tri> ¬a ¬b c = y
 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
+ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+... | refl = case1 x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+... | refl = case1 x₂
+ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
+... | refl | refl = case2 ( orddtrans x₁ x₂ )
 trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_
 trio< a b with <-cmp (lv a) (lv b)
 trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
 lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
-record ConstructibleSet {n : Level} : Set (suc n) where
+-- Ordinal Definable Set
+record OD {n : Level}  : Set (suc n) where
 field
-α : Ordinal {suc n}
+α :  Ordinal {n}
-constructible : Ordinal {suc n} → Set n
+def : (x : Ordinal {n} ) → x o< α → Set n
--- constructible : (x : Ordinal {suc n} ) → x o< α → Set n
+open OD
-open ConstructibleSet
+open import Data.Unit
-_∋_  : {n : Level} →  (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set (suc n)
+postulate      -- this is proved by Godel numbering of def
-a ∋ x  = ( α x o< α a ) ∧ constructible a ( α x )
+_c<_ : {n : Level } → (x y : OD {n} ) → Set n
+ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {n} _≡_ _c<_
-c∅ : {n : Level} → ConstructibleSet
-c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ }
+-- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
+-- o∋ a x x<A  = def a x x<A
-record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m  ) (ψ : S → S ) (X : S) : Set ((suc n) ⊔ m)  where
+-- TC u : Transitive Closure of OD u
+--
+--    all elements of u or elements of elements of u, etc...
+--
+-- TC Zero = u
+-- TC (suc n) = ∪ (TC n)
+--
+-- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
+--
+--     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
+--
+--    HOD = {x | TC x ⊆ OD }  ⊆ OD
+--
+record HOD {n : Level}  : Set (suc n) where
 field
-sup : S
+hod : OD {n}
-smax  : ∀ { x : S } → x ≤ X  → ψ x ≤ sup
+tc : ?
-suniq : {max : S} → ( ∀ { x :  S } → x ≤ X  → ψ x ≤ max ) → max ≤ sup
-open SupR
-record dom-ψ {n m : Level} (X : ConstructibleSet {n}) (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) :  Set (suc (suc n) ⊔ suc m) where
-field
-αψ : Ordinal {suc n}
-inψ : (x : Ordinal {suc n} ) → Set m
-X∋x : (x : ConstructibleSet {n} ) → inψ (α x) → X ∋ x
-vψ : (x : Ordinal {suc n} ) → inψ x  → ConstructibleSet {n}
-cset≡ψ : (x : ConstructibleSet {n} ) → (t : inψ (α x) ) → x ≡ ψ ( vψ (α x) t )
-open dom-ψ
-postulate
-ψ→C : {n m : Level} (X : ConstructibleSet {n})  (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) → dom-ψ {n} {m} X ψ
-_⊆_ : {n : Level} → ( A B : ConstructibleSet  ) → ∀{ x : ConstructibleSet } →  Set (suc n)
-_⊆_ A B {x} = A ∋ x →  B ∋ x
-suptraverse : {n : Level} → (X : ConstructibleSet {n}) ( max : ConstructibleSet {n}) ( ψ : ConstructibleSet  {n} → ConstructibleSet  {n}) → ConstructibleSet {n}
-suptraverse X max ψ  = {!!}
-Sup : {n : Level } → (ψ : ConstructibleSet → ConstructibleSet )  → (X : ConstructibleSet)  → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
-sup  (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ
-smax (Sup ψ X ) = {!!}
-suniq (Sup ψ X ) = {!!}
-open import Data.Unit
-open SupR
-ConstructibleSet→ZF : {n : Level} → ZF {suc n} {suc n}
-ConstructibleSet→ZF {n}  = record {
-ZFSet = ConstructibleSet
-; _∋_ = _∋_
-; _≈_ = _≡_
-; ∅  = c∅
-; _,_ = _,_
-; Union = Union
-; Power = {!!}
-; Select = Select
-; Replace = Replace
-; infinite = {!!}
-; isZF = {!!}
-} where
-Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n}
-Select X ψ = record { α = α X ; constructible = λ x →  select x } where
-select : Ordinal → Set n
-select x with  ψ (record { α = x ; constructible = λ x → constructible X x })
-... | t = Lift n ⊤
-Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
-Replace X ψ  = record { α = αψ {n} {suc (suc n)} (ψ→C X ψ)  ; constructible = λ x → inψ (ψ→C X ψ) x }
-_,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
-a , b  = record { α = maxα (α a) (α b) ; constructible =  a∨b }  where
-a∨b : Ordinal {suc n} → Set n
-a∨b x with (x ≡ α a ) ∨ ( x ≡ α b )
-... | t = Lift n  ⊤
-Union : ConstructibleSet → ConstructibleSet
-Union a = {!!}

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

comparison constructible-set.agda @ 27:bade0a35fdd9