Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison zf.agda @ 10:8022e14fce74
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 |