Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 29:fce60b99dc55
posturate OD is isomorphic to Ordinal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 May 2019 18:18:43 +0900 |
| parents | f36e40d5d2c3 |
| children | 3b0fdb95618e |
| files | constructible-set.agda ordinal-definable.agda ordinal.agda set-of-agda.agda zf.agda |
| diffstat | 5 files changed, 331 insertions(+), 351 deletions(-) [+] |
line wrap: on
line diff
--- a/constructible-set.agda Sun May 19 18:13:42 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,246 +0,0 @@ -open import Level -module constructible-set where - -open import zf - -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) - -open import Relation.Binary.PropositionalEquality - -data OrdinalD {n : Level} : (lv : Nat) → Set n where - Φ : (lv : Nat) → OrdinalD lv - OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv - ℵ_ : (lv : Nat) → OrdinalD (Suc lv) - -record Ordinal {n : Level} : Set n where - field - lv : Nat - ord : OrdinalD {n} lv - -data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where - Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x - s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y - ℵΦ< : {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 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 - -open import Relation.Binary -open import Relation.Binary.Core - -o∅ : {n : Level} → Ordinal {n} -o∅ = record { lv = Zero ; ord = Φ Zero } - - -≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ -≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t - -trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ -trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = - trio<> s t - -trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ -trio<≡ refl = ≡→¬d< - -trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ -trio>≡ refl = ≡→¬d< - -triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) -triO {n} {lx} {ly} x y = <-cmp lx ly - -triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) -triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< -triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d< -triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) -triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< (ℵΦ< {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) ) -triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ< {_} {lv} {Φ (Suc lv)} ) -triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} ) ) (λ ()) (ℵ< {_} {lv} {y} ) -triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< ) -triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y -triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) -triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< -triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c) - -d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y -d<→lv Φ< = refl -d<→lv (s< lt) = refl -d<→lv ℵΦ< = refl -d<→lv ℵ< = refl - -orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z -orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< -orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y} -orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) -orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ< -orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< () -orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< () - -max : (x y : Nat) → Nat -max Zero Zero = Zero -max Zero (Suc x) = (Suc x) -max (Suc x) Zero = (Suc x) -max (Suc x) (Suc y) = Suc ( max x y ) - -maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx -maxαd x y with triOrdd x y -maxαd x y | tri< a ¬b ¬c = y -maxαd x y | tri≈ ¬a b ¬c = x -maxαd x y | tri> ¬a ¬b c = x - -maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal -maxα x y with <-cmp (lv x) (lv y) -maxα x y | tri< a ¬b ¬c = x -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) - lemma1 (case1 x) = ¬c x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl -trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where - lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b) - lemma1 (case1 x) = ¬a x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl -trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b ) -trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where - lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b - lemma1 refl = refl - lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x) - lemma2 (case1 x) = ¬a x - lemma2 (case2 x) = trio<> x a -trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where - lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b - lemma1 refl = refl - lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b) - lemma2 (case1 x) = ¬a x - lemma2 (case2 x) = trio<> x c -trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where - lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b) - lemma1 (case1 x) = ¬a x - lemma1 (case2 x) = ≡→¬d< x - -OrdTrans : {n : Level} → Transitive {suc n} _o≤_ -OrdTrans (case1 refl) (case1 refl) = case1 refl -OrdTrans (case1 refl) (case2 lt2) = case2 lt2 -OrdTrans (case2 lt1) (case1 refl) = case2 lt1 -OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) ) -OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y -OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x ) -OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x -OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y) -OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y -OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y )) - -OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) -OrdPreorder {n} = record { Carrier = Ordinal - ; _≈_ = _≡_ - ; _∼_ = _o≤_ - ; isPreorder = record { - isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ; reflexive = case1 - ; trans = OrdTrans - } - } - -TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) - → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) - → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) - → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) - → ∀ (x : Ordinal) → ψ x -TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv -TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁ - ( 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β ) ' - --- Ordinal Definable Set - -record OD {n : Level} : Set (suc n) where - field - α : Ordinal {n} - def : (x : Ordinal {n} ) → x o< α → Set n - -open OD -open import Data.Unit - -postulate -- this is proved by Godel numbering of def - _c<_ : {n : Level } → (x y : OD {n} ) → Set (suc n) - ODpre : {n : Level} → IsPreorder {suc n} {suc n} {suc n} _≡_ _c<_ - --- 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 - --- 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 ) ) .... --- --- Heritic Ordinal Definable --- --- ( HOD = {x | TC x ⊆ OD } ) ⊆ OD --- - -HOD = OD - -c∅ : {n : Level} → HOD {n} -c∅ {n} = record { α = o∅ ; def = λ x y → Lift n ⊥ } - -HOD→ZF : {n : Level} → ZF {suc n} {suc n} -HOD→ZF {n} = record { - ZFSet = HOD - ; _∋_ = λ a b → b c< a - ; _≈_ = _≡_ - ; ∅ = c∅ - ; _,_ = _,_ - ; Union = Union - ; Power = {!!} - ; Select = Select - ; Replace = Replace - ; infinite = {!!} - ; isZF = {!!} - } where - Select : (X : HOD {n}) → (HOD {n} → Set (suc n)) → HOD {n} - Select X ψ = record { α = α X ; def = λ x → {!!} } where - select : Ordinal → Set n - select x with ψ (record { α = x ; def = λ x → {!!} }) - ... | t = Lift n ⊤ - Replace : (X : HOD {n} ) → (HOD → HOD) → HOD - Replace X ψ = record { α = {!!} ; def = λ x → {!!} } - _,_ : HOD {n} → HOD → HOD - a , b = record { α = maxα (α a) (α b) ; def = λ x x<ab → ( ) } where - a∨b : Ordinal {suc n} → Set n - a∨b = {!!} - Union : HOD → HOD - Union a = {!!}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ordinal-definable.agda Mon May 20 18:18:43 2019 +0900 @@ -0,0 +1,151 @@ +open import Level +module ordinal-definable where + +open import zf +open import ordinal + +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) + +open import Relation.Binary.PropositionalEquality + +open import Data.Nat.Properties +open import Data.Empty +open import Relation.Nullary + +open import Relation.Binary +open import Relation.Binary.Core + + +-- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' + +-- Ordinal Definable Set + +-- 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 + +-- 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 ) ) .... +-- +-- Heritic Ordinal Definable +-- +-- ( HOD = {x | TC x ⊆ OD } ) ⊆ OD x ∈ OD here +-- + +record OD {n : Level} : Set (suc n) where + field + def : (x : Ordinal {n} ) → Set n + +open OD +open import Data.Unit + +postulate + od→ord : {n : Level} → OD {n} → Ordinal {n} + +ord→od : {n : Level} → Ordinal {n} → OD {n} +ord→od x = record { def = λ y → x ≡ y } + +_∋_ : { n : Level } → ( a x : OD {n} ) → Set n +_∋_ {n} a x = def a ( od→ord x ) + +_c<_ : { n : Level } → ( a x : OD {n} ) → Set n +x c< a = a ∋ x + +_c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) +a c≤ b = (a ≡ b) ∨ ( b ∋ a ) + +postulate + c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord x + o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od x + oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x + diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x + sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} + sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ + +HOD = OD + +od∅ : {n : Level} → HOD {n} +od∅ {n} = record { def = λ _ → Lift n ⊥ } + +∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) +∅1 {n} x (lift ()) + +HOD→ZF : {n : Level} → ZF {suc n} {suc n} +HOD→ZF {n} = record { + ZFSet = OD {n} + ; _∋_ = λ a x → Lift (suc n) ( a ∋ x ) + ; _≈_ = _≡_ + ; ∅ = od∅ + ; _,_ = _,_ + ; Union = Union + ; Power = Power + ; Select = Select + ; Replace = Replace + ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } } + ; isZF = isZF + } where + Replace : OD {n} → (OD {n} → OD {n} ) → OD {n} + Replace X ψ = sup-od ψ + Select : OD {n} → (OD {n} → Set (suc n) ) → OD {n} + Select X ψ = record { def = λ x → select ( ord→od x ) } where + select : OD {n} → Set n + select x with ψ x + ... | t = Lift n ⊤ + _,_ : OD {n} → OD {n} → OD {n} + x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } + Union : OD {n} → OD {n} + Union x = record { def = λ y → {z : Ordinal {n}} → def x z → def (ord→od z) y } + Power : OD {n} → OD {n} + Power x = record { def = λ y → (z : Ordinal {n} ) → ( def x y ∧ def (ord→od z) y ) } + ZFSet = OD {n} + _∈_ : ( A B : ZFSet ) → Set n + A ∈ B = B ∋ A + _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set n + _⊆_ A B {x} = A ∋ x → B ∋ x + _∩_ : ( A B : ZFSet ) → ZFSet + A ∩ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∧ (Lift (suc n) ( B ∋ x ) )) + _∪_ : ( A B : ZFSet ) → ZFSet + A ∪ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∨ (Lift (suc n) ( B ∋ x ) )) + infixr 200 _∈_ + infixr 230 _∩_ _∪_ + infixr 220 _⊆_ + isZF : IsZF (OD {n}) (λ a x → Lift (suc n) ( a ∋ x )) _≡_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }) + isZF = record { + isEquivalence = record { refl = refl ; sym = sym ; trans = trans } + ; pair = pair + ; union→ = {!!} + ; union← = {!!} + ; empty = empty + ; power→ = {!!} + ; power← = {!!} + ; extentionality = {!!} + ; minimul = {!!} + ; regularity = {!!} + ; infinity∅ = {!!} + ; infinity = {!!} + ; selection = {!!} + ; replacement = {!!} + } where + open _∧_ + pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B) + proj1 (pair A B ) = lift ( case1 refl ) + proj2 (pair A B ) = lift ( case2 refl ) + empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x) + empty x (lift (lift ())) + union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y) + union→ X x y (lift X∋x) (lift x∋y) = lift lemma where + lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y + lemma {z} X∋z = {!!} + + + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ordinal.agda Mon May 20 18:18:43 2019 +0900 @@ -0,0 +1,179 @@ +open import Level +module ordinal where + +open import zf + +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) + +open import Relation.Binary.PropositionalEquality + +data OrdinalD {n : Level} : (lv : Nat) → Set n where + Φ : (lv : Nat) → OrdinalD lv + OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv + ℵ_ : (lv : Nat) → OrdinalD (Suc lv) + +record Ordinal {n : Level} : Set n where + field + lv : Nat + ord : OrdinalD {n} lv + +data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where + Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x + s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y + ℵΦ< : {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 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 + +open import Relation.Binary +open import Relation.Binary.Core + +o∅ : {n : Level} → Ordinal {n} +o∅ = record { lv = Zero ; ord = Φ Zero } + + +≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ +≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t + +trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ +trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = + trio<> s t + +trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ +trio<≡ refl = ≡→¬d< + +trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ +trio>≡ refl = ≡→¬d< + +triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) +triO {n} {lx} {ly} x y = <-cmp lx ly + +triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) +triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< +triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d< +triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) +triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< (ℵΦ< {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) ) +triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ< {_} {lv} {Φ (Suc lv)} ) +triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} ) ) (λ ()) (ℵ< {_} {lv} {y} ) +triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< +triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< ) +triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y +triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) +triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< +triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c) + +d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y +d<→lv Φ< = refl +d<→lv (s< lt) = refl +d<→lv ℵΦ< = refl +d<→lv ℵ< = refl + +orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z +orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< +orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y} +orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) +orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ< +orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< () +orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< () + +max : (x y : Nat) → Nat +max Zero Zero = Zero +max Zero (Suc x) = (Suc x) +max (Suc x) Zero = (Suc x) +max (Suc x) (Suc y) = Suc ( max x y ) + +maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx +maxαd x y with triOrdd x y +maxαd x y | tri< a ¬b ¬c = y +maxαd x y | tri≈ ¬a b ¬c = x +maxαd x y | tri> ¬a ¬b c = x + +maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal +maxα x y with <-cmp (lv x) (lv y) +maxα x y | tri< a ¬b ¬c = x +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) + lemma1 (case1 x) = ¬c x + lemma1 (case2 x) with d<→lv x + lemma1 (case2 x) | refl = ¬b refl +trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where + lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b) + lemma1 (case1 x) = ¬a x + lemma1 (case2 x) with d<→lv x + lemma1 (case2 x) | refl = ¬b refl +trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b ) +trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where + lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b + lemma1 refl = refl + lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x) + lemma2 (case1 x) = ¬a x + lemma2 (case2 x) = trio<> x a +trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where + lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b + lemma1 refl = refl + lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b) + lemma2 (case1 x) = ¬a x + lemma2 (case2 x) = trio<> x c +trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where + lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b) + lemma1 (case1 x) = ¬a x + lemma1 (case2 x) = ≡→¬d< x + +OrdTrans : {n : Level} → Transitive {suc n} _o≤_ +OrdTrans (case1 refl) (case1 refl) = case1 refl +OrdTrans (case1 refl) (case2 lt2) = case2 lt2 +OrdTrans (case2 lt1) (case1 refl) = case2 lt1 +OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) ) +OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y +OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x ) +OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x +OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y) +OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y +OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y )) + +OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) +OrdPreorder {n} = record { Carrier = Ordinal + ; _≈_ = _≡_ + ; _∼_ = _o≤_ + ; isPreorder = record { + isEquivalence = record { refl = refl ; sym = sym ; trans = trans } + ; reflexive = case1 + ; trans = OrdTrans + } + } + +TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) + → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) + → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) + → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) + → ∀ (x : Ordinal) → ψ x +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁ + ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ +
--- a/set-of-agda.agda Sun May 19 18:13:42 2019 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -module set-of-agda where - -open import Level -open import Data.Bool - --- infix 50 _∧_ - --- record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where --- constructor _×_ --- field --- proj1 : A --- proj2 : B - --- open _∧_ - --- infix 50 _∨_ - --- data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where --- case1 : A → A ∨ B --- case2 : B → A ∨ B - -data ZFSet {n : Level} : Set (suc (suc n)) where - elem : { A : Set n } ( a : A ) → ZFSet - ∅ : ZFSet {n} - pair : {A B : Set n} (a : A ) (b : B ) → ZFSet - union : (A : Set (suc n) ) → ZFSet - -- repl : ( ψ : ZFSet {n} → Set zero ) → ZFSet - infinite : ZFSet - power : (A : ZFSet {n}) → ZFSet - -infix 60 _∋_ _∈_ - -open import Relation.Binary.PropositionalEquality - -data _∈_ {n : Level} : {A : Set n} ( a : A ) ( Z : ZFSet {n} ) → Set (suc n) where - ∈-elm : {A : Set n } {a : A} → a ∈ (elem a) - ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A} → a ∈ (pair a b) - ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B} → b ∈ (pair a b) --- ∈-union : {Z : Set (suc n)} {A : Z } → {a : {!!} } → a ∈ (union Z) --- ∈-repl : {A : Set n } { B : Set n} → { ψ : B → A } → { b : B } → ψ b ∈ {!!} -- (repl {!!}) - -- ∈-infinite-1 : ∅ ∈ infinite --- ∈-infinite : {A : Set n} {a : A} → _∈_ infinite {A} a - ∈-power : {A B : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈ (power Z) - --- _∈_ : {n : Level} { A : ZFSet {n} } → {B : Set n} → (a : B ) → Set n → Bool --- _∈_ {_} {A} a _ = A ∋ a - -infix 40 _⇔_ - --- _⇔_ : {n : Level} (A B : Set n) → Set n --- A ⇔ B = ( ∀ {x : A } → x ∈ B ) ∧ ( ∀ {x : B } → x ∈ A ) - --- Axiom of extentionality --- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ] - --- set-extentionality : {n : Level } {x y : Set n } → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n)) → ( x ∈ w ⇔ y ∈ w ) --- proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x ) --- proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y ) - - -open import Relation.Nullary -open import Data.Empty - --- data ∅ : Set where - -infix 50 _∩_ - --- record _∩_ {n m : Level} (A : Set n) ( B : Set m) : Set (n ⊔ m) where --- field --- inL : {x : A } → x ∈ A --- inR : {x : B } → x ∈ B - --- open _∩_ - --- lemma : {n m : Level} (A : Set n) ( B : Set m) → (a : A ) → a ∈ (A ∩ B) --- lemma A B a A∩B = inL A∩B - --- Axiom of regularity --- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) - --- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x ⇔ ∅ ) --- set-regularity = {!!} - --- Axiom of pairing --- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z). - --- pair : {n m : Level} ( x : Set n ) ( y : Set m ) → Set (n ⊔ m) --- pair x y = {!!} -- ( x × y ) - --- Axiom of Union --- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x)) - --- axiom of infinity --- ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) - --- axiom of replacement --- ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) - --- axiom of power set --- ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) - - - -
--- a/zf.agda Sun May 19 18:13:42 2019 +0900 +++ b/zf.agda Mon May 20 18:18:43 2019 +0900 @@ -55,7 +55,7 @@ (infinite : ZFSet) : Set (suc (n ⊔ m)) where field - isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ + isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t ∈ x))