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

comparison zf.agda @ 10:8022e14fce74

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add constructible set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 May 2019 18:25:38 +0900
parents 5ed16e2d8eb7
children 2df90eb0896c
comparison
equal deleted inserted replaced
9:5ed16e2d8eb7 10:8022e14fce74
30 infixr 140 _∨_ 30 infixr 140 _∨_
31 infixr 150 _⇔_ 31 infixr 150 _⇔_
32 32
33 record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where 33 record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where
34 field 34 field
35 Restrict : ZFSet
36 rel : Rel ZFSet m 35 rel : Rel ZFSet m
37 dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y 36 dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y
38 fun-eq : { x y z : ZFSet } → ( rel x y ∧ rel x z ) → y ≈ z 37 fun-eq : { x y z : ZFSet } → ( rel x y ∧ rel x z ) → y ≈ z
39 38
40 open Func 39 open Func
46 (_≈_ : Rel ZFSet m) 45 (_≈_ : Rel ZFSet m)
47 (∅ : ZFSet) 46 (∅ : ZFSet)
48 (_×_ : ( A B : ZFSet ) → ZFSet) 47 (_×_ : ( A B : ZFSet ) → ZFSet)
49 (Union : ( A : ZFSet ) → ZFSet) 48 (Union : ( A : ZFSet ) → ZFSet)
50 (Power : ( A : ZFSet ) → ZFSet) 49 (Power : ( A : ZFSet ) → ZFSet)
50 (Select : ( ZFSet → Set m ) → ZFSet )
51 (Replace : ( ZFSet → ZFSet ) → ZFSet )
51 (infinite : ZFSet) 52 (infinite : ZFSet)
52 : Set (suc (n ⊔ m)) where 53 : Set (suc (n ⊔ m)) where
53 field 54 field
54 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ 55 isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_
55 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) 56 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
59 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y 60 union← : ( X x y : ZFSet ) → Union X ∋ y → X ∋ x → x ∋ y
60 _∈_ : ( A B : ZFSet ) → Set m 61 _∈_ : ( A B : ZFSet ) → Set m
61 A ∈ B = B ∋ A 62 A ∈ B = B ∋ A
62 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m 63 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
63 _⊆_ A B {x} {A∋x} = B ∋ x 64 _⊆_ A B {x} {A∋x} = B ∋ x
64 Repl : ( ψ : ZFSet → Set m ) → Func ZFSet _≈_
65 Repl ψ = record { Restrict = {!!} ; rel = {!!} ; dom = {!!} ; fun-eq = {!!} }
66 _∩_ : ( A B : ZFSet ) → ZFSet 65 _∩_ : ( A B : ZFSet ) → ZFSet
67 A ∩ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ) 66 A ∩ B = Select ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
68 _∪_ : ( A B : ZFSet ) → ZFSet 67 _∪_ : ( A B : ZFSet ) → ZFSet
69 A ∪ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) ) 68 A ∪ B = Select ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) )
70 infixr 200 _∈_ 69 infixr 200 _∈_
71 infixr 230 _∩_ _∪_ 70 infixr 230 _∩_ _∪_
72 infixr 220 _⊆_ 71 infixr 220 _⊆_
73 field 72 field
74 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 73 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
76 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} {y} → _⊆_ t A {x} {y} 75 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} {y} → _⊆_ t A {x} {y}
77 power← : ∀( A t : ZFSet ) → ∀ {x} {y} → _⊆_ t A {x} {y} → Power A ∋ t 76 power← : ∀( A t : ZFSet ) → ∀ {x} {y} → _⊆_ t A {x} {y} → Power A ∋ t
78 -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) 77 -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
79 extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B 78 extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
80 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 79 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
81 smaller : ZFSet → ZFSet 80 minimul : ZFSet → ZFSet
82 regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( smaller x ∈ x ∧ ( smaller x ∩ x ≈ ∅ ) ) 81 regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( minimul x ∈ x ∧ ( minimul x ∩ x ≈ ∅ ) )
83 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 82 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
84 infinity∅ : ∅ ∈ infinite 83 infinity∅ : ∅ ∈ infinite
85 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ Restrict ( Repl ( λ y → x ≈ y ))) ∈ infinite 84 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ Select ( λ y → x ≈ y )) ∈ infinite
85 selection : { ψ : ZFSet → Set m } → ∀ ( y : ZFSet ) → ( y ∈ Select ψ ) → ψ y
86 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 86 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
87 -- this form looks like specification 87 replacement : {ψ : ZFSet → ZFSet} → ∀ ( x : ZFSet ) → ( ψ x ∈ Replace ψ )
88 replacement : ( ψ : Func ZFSet _≈_ ) → ∀ ( y : ZFSet ) → ( y ∈ Restrict ψ ) → {!!} -- dom ψ y
89 88
90 record ZF {n m : Level } : Set (suc (n ⊔ m)) where 89 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
91 infixr 210 _×_ 90 infixr 210 _×_
92 infixl 200 _∋_ 91 infixl 200 _∋_
93 infixr 220 _≈_ 92 infixr 220 _≈_
98 -- ZF Set constructor 97 -- ZF Set constructor
99 ∅ : ZFSet 98 ∅ : ZFSet
100 _×_ : ( A B : ZFSet ) → ZFSet 99 _×_ : ( A B : ZFSet ) → ZFSet
101 Union : ( A : ZFSet ) → ZFSet 100 Union : ( A : ZFSet ) → ZFSet
102 Power : ( A : ZFSet ) → ZFSet 101 Power : ( A : ZFSet ) → ZFSet
102 Select : ( ZFSet → Set m ) → ZFSet
103 Replace : ( ZFSet → ZFSet ) → ZFSet
103 infinite : ZFSet 104 infinite : ZFSet
104 isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power infinite 105 isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Select Replace infinite
105 106
106 module reguraliry-m {n m : Level } ( zf : ZF {m} {n} ) where 107 module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where
107 108
108 open import Relation.Nullary 109 _≈_ = ZF._≈_ zf
109 open import Data.Empty 110 ZFSet = ZF.ZFSet zf
110 open import Relation.Binary.PropositionalEquality 111 Select = ZF.Select zf
112 ∅ = ZF.∅ zf
113 _∩_ = ( IsZF._∩_ ) (ZF.isZF zf)
114 _∋_ = ZF._∋_ zf
115 replacement = IsZF.replacement ( ZF.isZF zf )
116 selection = IsZF.selection ( ZF.isZF zf )
117 minimul = IsZF.minimul ( ZF.isZF zf )
118 regularity = IsZF.regularity ( ZF.isZF zf )
111 119
112 _≈_ = ZF._≈_ zf 120 russel : Select ( λ x → x ∋ x ) ≈ ∅
113 ZFSet = ZF.ZFSet 121 russel with Select ( λ x → x ∋ x )
114 ∅ = ZF.∅ zf 122 ... | s = {!!}
115 _∩_ = ( IsZF._∩_ ) (ZF.isZF zf)
116 _∋_ = ZF._∋_ zf
117 replacement = IsZF.replacement ( ZF.isZF zf )
118 123
119 -- russel : ( x : ZFSet zf ) → x ≈ Restrict ( λ x → ¬ ( x ∋ x ) ) → ⊥ 124 module constructible-set where
120 -- russel x eq with x ∋ x
121 -- ... | x∋x with replacement ( λ x → ¬ ( x ∋ x )) x {!!}
122 -- ... | r1 = {!!}
123 125
126 data Nat : Set zero where
127 Zero : Nat
128 Suc : Nat → Nat
129
130 prev : Nat → Nat
131 prev (Suc n) = n
132 prev Zero = Zero
133
134 open import Relation.Binary.PropositionalEquality
135
136 data Transtive {n : Level } : ( lv : Nat) → Set n where
137 Φ : {lv : Nat} → Transtive {n} lv
138 T-suc : {lv : Nat} → Transtive {n} lv → Transtive lv
139 ℵ_ : (lv : Nat) → Transtive (Suc lv)
140
141 data Constructible {n : Level } {lv : Nat} ( α : Transtive {n} lv ) : Set (suc n) where
142 fsub : ( ψ : Transtive {n} lv → Set n ) → Constructible α
143 xself : Transtive {n} lv → Constructible α
144
145 record ConstructibleSet {n : Level } : Set (suc n) where
146 field
147 level : Nat
148 α : Transtive {n} level
149 constructible : Constructible α
150
151 open ConstructibleSet
152
153 data _c∋_ {n : Level } {lv lv' : Nat} {α : Transtive {n} lv } {α' : Transtive {n} lv' } :
154 Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
155 xself-fsub : (ta : Transtive {n} lv ) ( ψ : Transtive {n} lv' → Set n ) → (xself ta ) t∋ ( fsub ψ)
156 xself-xself : (ta : Transtive {n} lv ) (tx : Transtive {n} lv' ) → (xself ta ) t∋ ( xself tx)
157 fsub-fsub : ( ψ : Transtive {n} lv → Set n ) ( ψ₁ : Transtive {n} lv' → Set n ) →( fsub ψ ) t∋ ( fsub ψ₁)
158 fsub-xself : ( ψ : Transtive {n} lv → Set n ) (tx : Transtive {n} lv' ) → (fsub ψ ) t∋ ( xself tx)
124 159
125 160 _∋_ : {n m : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set m
126 161 _∋_ = {!!}
127 data Nat : Set zero where 162
128 Zero : Nat 163
129 Suc : Nat → Nat 164 Transtive→ZF : {n m : Level } → ZF {suc n} {m}
130 165 Transtive→ZF {n} {m} = record {
131 prev : Nat → Nat 166 ZFSet = ConstructibleSet
132 prev (Suc n) = n 167 ; _∋_ = _∋_
133 prev Zero = Zero 168 ; _≈_ = {!!}
134 169 ; ∅ = record { level = Zero ; α = Φ ; constructible = xself Φ }
135 open import Relation.Binary.PropositionalEquality 170 ; _×_ = {!!}
136 171 ; Union = {!!}
137 172 ; Power = {!!}
138 data Transtive {n : Level } : ( lv : Nat) → Set n where 173 ; Select = {!!}
139 Φ : {lv : Nat} → lv ≡ Zero → Transtive lv 174 ; Replace = {!!}
140 T-suc : {lv : Nat} → lv ≡ Zero → Transtive {n} lv → Transtive lv 175 ; infinite = {!!}
141 ℵ : {lv : Nat} → Transtive {n} lv → Transtive (Suc lv) 176 ; isZF = {!!}
142 177 } where
143
144
145