1200
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
1242
|
2 import Level
|
431
|
3 open import Ordinals
|
1242
|
4 module generic-filter {n : Level.Level } (O : Ordinals {n}) where
|
431
|
5
|
|
6 import filter
|
|
7 open import zf
|
|
8 open import logic
|
|
9 -- open import partfunc {n} O
|
|
10 import OD
|
|
11
|
|
12 open import Relation.Nullary
|
|
13 open import Relation.Binary
|
|
14 open import Data.Empty
|
|
15 open import Relation.Binary
|
|
16 open import Relation.Binary.Core
|
|
17 open import Relation.Binary.PropositionalEquality
|
1242
|
18 open import Data.Nat
|
1124
|
19 import BAlgebra
|
431
|
20
|
1124
|
21 open BAlgebra O
|
431
|
22
|
|
23 open inOrdinal O
|
|
24 open OD O
|
|
25 open OD.OD
|
|
26 open ODAxiom odAxiom
|
|
27 import OrdUtil
|
|
28 import ODUtil
|
|
29 open Ordinals.Ordinals O
|
|
30 open Ordinals.IsOrdinals isOrdinal
|
|
31 open Ordinals.IsNext isNext
|
|
32 open OrdUtil O
|
|
33 open ODUtil O
|
|
34
|
|
35
|
|
36 import ODC
|
|
37
|
|
38 open filter O
|
|
39
|
|
40 open _∧_
|
|
41 open _∨_
|
|
42 open Bool
|
|
43
|
|
44
|
|
45 open HOD
|
|
46
|
|
47 -------
|
|
48 -- the set of finite partial functions from ω to 2
|
|
49 --
|
|
50 --
|
|
51
|
|
52 open import Data.List hiding (filter)
|
|
53 open import Data.Maybe
|
|
54
|
1218
|
55 open import ZProduct O
|
431
|
56
|
1242
|
57 record CountableModel : Set (Level.suc (Level.suc n)) where
|
431
|
58 field
|
461
|
59 ctl-M : HOD
|
1242
|
60 ctl→ : ℕ → Ordinal
|
|
61 ctl<M : (x : ℕ) → odef (ctl-M) (ctl→ x)
|
|
62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → ℕ
|
461
|
63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x
|
1174
|
64 -- we have no otherway round
|
1242
|
65 -- ctl-iso← : { x : ℕ } → ctl← (ctl→ x ) (ctl<M x) ≡ x
|
446
|
66 --
|
|
67 -- almmost universe
|
|
68 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
|
|
69 --
|
436
|
70
|
457
|
71 -- we expect P ∈ * ctl-M ∧ G ⊆ L ⊆ Power P , ¬ G ∈ * ctl-M,
|
434
|
72
|
|
73 open CountableModel
|
431
|
74
|
|
75 ----
|
|
76 -- a(n) ∈ M
|
1239
|
77 -- ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ p(n) ⊆ q
|
431
|
78 --
|
1242
|
79 PGHOD : (i : ℕ) (L : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
|
457
|
80 PGHOD i L C p = record { od = record { def = λ x →
|
1239
|
81 odef L x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) }
|
457
|
82 ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L (proj1 lt) }
|
431
|
83
|
|
84 ---
|
1239
|
85 -- p(n+1) = if ({q | q ∈ a(n) ∧ p(n) ⊆ q)} != ∅ then q otherwise p(n)
|
446
|
86 --
|
1242
|
87 find-p : (L : HOD ) (C : CountableModel ) (i : ℕ) → (x : Ordinal) → Ordinal
|
|
88 find-p L C zero x = x
|
|
89 find-p L C (suc i) x with is-o∅ ( & ( PGHOD i L C (find-p L C i x)) )
|
457
|
90 ... | yes y = find-p L C i x
|
|
91 ... | no not = & (ODC.minimal O ( PGHOD i L C (find-p L C i x)) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice
|
431
|
92
|
|
93 ---
|
1239
|
94 -- G = { r ∈ L ⊆ Power P | ∃ n → r ⊆ p(n) }
|
431
|
95 --
|
457
|
96 record PDN (L p : HOD ) (C : CountableModel ) (x : Ordinal) : Set n where
|
431
|
97 field
|
1242
|
98 gr : ℕ
|
1239
|
99 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p L C gr (& p))) y
|
457
|
100 x∈PP : odef L x
|
431
|
101
|
|
102 open PDN
|
|
103
|
|
104 ---
|
|
105 -- G as a HOD
|
|
106 --
|
457
|
107 PDHOD : (L p : HOD ) (C : CountableModel ) → HOD
|
|
108 PDHOD L p C = record { od = record { def = λ x → PDN L p C x }
|
|
109 ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L {y} (PDN.x∈PP lt) }
|
431
|
110
|
|
111 open PDN
|
|
112
|
|
113 ----
|
1242
|
114 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. ℕ → P → Set )
|
431
|
115 --
|
|
116 -- p 0 ≡ ∅
|
434
|
117 -- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) )
|
431
|
118 --- else p n
|
|
119
|
|
120 P∅ : {P : HOD} → odef (Power P) o∅
|
|
121 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
|
|
122 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
|
|
123 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
|
|
124 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
|
|
125 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
|
|
126
|
1242
|
127 gf05 : {a b : HOD} {x : Ordinal } → (odef (a ∪ b) x ) → ¬ odef a x → ¬ odef b x → ⊥
|
|
128 gf05 {a} {b} {x} (case1 ax) nax nbx = nax ax
|
|
129 gf05 {a} {b} {x} (case2 bx) nax nbx = nbx bx
|
|
130
|
|
131 gf02 : {P a b : HOD } → (P \ a) ∩ (P \ b) ≡ ( P \ (a ∪ b) )
|
|
132 gf02 {P} {a} {b} = ==→o≡ record { eq→ = gf03 ; eq← = gf04 }where
|
|
133 gf03 : {x : Ordinal} → odef ((P \ a) ∩ (P \ b)) x → odef (P \ (a ∪ b)) x
|
|
134 gf03 {x} ⟪ ⟪ Px , ¬ax ⟫ , ⟪ _ , ¬bx ⟫ ⟫ = ⟪ Px , (λ pab → gf05 {a} {b} {x} pab ¬ax ¬bx ) ⟫
|
|
135 gf04 : {x : Ordinal} → odef (P \ (a ∪ b)) x → odef ((P \ a) ∩ (P \ b)) x
|
|
136 gf04 {x} ⟪ Px , abx ⟫ = ⟪ ⟪ Px , (λ ax → abx (case1 ax) ) ⟫ , ⟪ Px , (λ bx → abx (case2 bx) ) ⟫ ⟫
|
|
137
|
446
|
138 open import Data.Nat.Properties
|
|
139 open import nat
|
433
|
140
|
1242
|
141 p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : ℕ} → (* (find-p L C n (& p))) ⊆ (* (find-p L C (suc n) (& p)))
|
1096
|
142 p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p))))
|
|
143 ... | yes y = refl-⊆ {* (find-p L C n (& p))}
|
1242
|
144 ... | no not = λ lt → proj2 (proj2 fmin∈PGHOD) _ lt where
|
447
|
145 fmin : HOD
|
457
|
146 fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
|
147 fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin
|
|
148 fmin∈PGHOD = ODC.x∋minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
438
|
149
|
1242
|
150 p-monotonic : (L p : HOD ) (C : CountableModel ) → {n m : ℕ} → n ≤ m → (* (find-p L C n (& p))) ⊆ (* (find-p L C m (& p)))
|
|
151 p-monotonic L p C {zero} {zero} n≤m = refl-⊆ {* (find-p L C zero (& p))}
|
|
152 p-monotonic L p C {zero} {suc m} z≤n lt = p-monotonic1 L p C {m} (p-monotonic L p C {zero} {m} z≤n lt )
|
|
153 p-monotonic L p C {suc n} {suc m} (s≤s n≤m) with <-cmp n m
|
|
154 ... | tri< a ¬b ¬c = λ lt → p-monotonic1 L p C {m} (p-monotonic L p C {suc n} {m} a lt)
|
1096
|
155 ... | tri≈ ¬a refl ¬c = λ x → x
|
446
|
156 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
|
438
|
157
|
1242
|
158 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (Level.suc n) where
|
1239
|
159 field
|
|
160 dense : HOD
|
|
161 d⊆P : dense ⊆ L
|
|
162 dense-f : {p : HOD} → L ∋ p → HOD
|
|
163 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
|
|
164 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p
|
|
165
|
1242
|
166 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
|
1239
|
167 field
|
|
168 genf : Filter {L} {P} LP
|
|
169 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Replace (Filter.filter genf) (λ x → P \ x )) ≡ od∅ )
|
|
170 rgen : HOD
|
|
171 rgen = Replace (Filter.filter genf) (λ x → P \ x )
|
|
172
|
1241
|
173 -- \-⊆
|
|
174
|
1243
|
175 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
|
|
176 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))
|
|
177 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P \ p)))
|
1241
|
178 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
|
1243
|
179 P-GenericFilter P L p0 L⊆PP Lp0 CAP NEG C = record {
|
1241
|
180 genf = record { filter = Replace (PDHOD L p0 C) (λ x → P \ x) ; f⊆L = gf01 ; filter1 = ? ; filter2 = ? }
|
1240
|
181 ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
|
431
|
182 } where
|
1241
|
183 GP = Replace (PDHOD L p0 C) (λ x → P \ x)
|
461
|
184 f⊆PL : PDHOD L p0 C ⊆ L
|
1096
|
185 f⊆PL lt = x∈PP lt
|
1241
|
186 gf01 : Replace (PDHOD L p0 C) (λ x → P \ x) ⊆ L
|
|
187 gf01 {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef L k) (sym x=ψz) ( NEG (subst (λ k → odef L k) (sym &iso) (f⊆PL az)) )
|
1242
|
188 gf141 : {xp xq : Ordinal } → (Pp : PDN L p0 C xp) (Pq : PDN L p0 C xq) → (* xp ∪ * xq) ⊆ P
|
|
189 gf141 Pp Pq {x} (case1 xpx) = L⊆PP (PDN.x∈PP Pp) _ xpx
|
|
190 gf141 Pp Pq {x} (case2 xqx) = L⊆PP (PDN.x∈PP Pq) _ xqx
|
|
191 gf121 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → p ∩ q ≡ P \ * (& (* (Replaced.z gp) ∪ * (Replaced.z gq)))
|
|
192 gf121 {p} {q} gp gq = begin
|
|
193 p ∩ q ≡⟨ cong₂ (λ j k → j ∩ k ) (sym *iso) (sym *iso) ⟩
|
|
194 (* (& p)) ∩ (* (& q)) ≡⟨ cong₂ (λ j k → ( * j ) ∩ ( * k)) (Replaced.x=ψz gp) (Replaced.x=ψz gq) ⟩
|
|
195 * (& (P \ (* xp ))) ∩ (* (& (P \ (* xq )))) ≡⟨ cong₂ (λ j k → j ∩ k ) *iso *iso ⟩
|
|
196 (P \ (* xp )) ∩ (P \ (* xq )) ≡⟨ gf02 {P} {* xp} {* xq} ⟩
|
|
197 P \ ((* xp) ∪ (* xq)) ≡⟨ cong (λ k → P \ k) (sym *iso) ⟩
|
|
198 P \ * (& (* xp ∪ * xq)) ∎ where
|
|
199 open ≡-Reasoning
|
|
200 xp = Replaced.z gp
|
|
201 xq = Replaced.z gq
|
|
202 gf131 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → P \ (p ∩ q) ≡ * (Replaced.z gp) ∪ * (Replaced.z gq)
|
|
203 gf131 {p} {q} gp gq = trans (cong (λ k → P \ k) (gf121 gp gq))
|
|
204 (trans ( L\Lx=x (subst (λ k → k ⊆ P) (sym *iso) (gf141 (Replaced.az gp) (Replaced.az gq))) ) *iso )
|
|
205
|
460
|
206 f1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → p ⊆ q → PDHOD L p0 C ∋ q
|
1239
|
207 f1 {p} {q} L∋q PD∋p p⊆q = ?
|
1241
|
208 f2 : {p q : HOD} → GP ∋ p → GP ∋ q → L ∋ (p ∩ q) → GP ∋ (p ∩ q)
|
|
209 f2 {p} {q} record { z = xp ; az = Pp ; x=ψz = peq }
|
|
210 record { z = xq ; az = Pq ; x=ψz = qeq } L∋pq with <-cmp (gr Pp) (gr Pq)
|
1242
|
211 ... | tri< a ¬b ¬c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq) } where
|
|
212 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
213 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
214 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
215 gf10 = record { gr = PDN.gr Pq ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
216 gf16 : gr Pp ≤ gr Pq
|
|
217 gf16 = <to≤ a
|
|
218 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pq) (& p0))) y
|
|
219 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
220 ... | case1 xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y xpy )
|
|
221 ... | case2 xqy = PDN.pn<gr Pq _ xqy
|
1243
|
222 ... | tri≈ ¬a eq ¬c = record { z = & (* xp ∩ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = gf22 } ; x=ψz = gf23 } where
|
|
223 gf22 : odef L (& (* xp ∩ * xq))
|
|
224 gf22 = CAP (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pp)) (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pq))
|
|
225 gf21 : (y : Ordinal) → odef (* (& (* xp ∩ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
226 gf21 y xpqy with subst (λ k → odef k y) *iso xpqy
|
|
227 ... | ⟪ xpy , xqy ⟫ = PDN.pn<gr Pp _ xpy
|
|
228 gf25 : odef L (& p)
|
|
229 gf25 = subst (λ k → odef L k ) (sym peq) ( NEG (subst (λ k → odef L k) (sym &iso) (PDN.x∈PP Pp) ))
|
|
230 gf27 : {x : Ordinal} → odef p x → odef (P \ * xp) x
|
|
231 gf27 {x} px = subst (λ k → odef k x) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) peq)) px
|
|
232 gf23 : & (p ∩ q) ≡ & (P \ * (& (* xp ∩ * xq))) -- != P \ (xp ∪ xq)
|
|
233 gf23 = cong (&) ( ==→o≡ record { eq→ = gf24 ; eq← = gf30 } ) where
|
|
234 gf24 : {x : Ordinal} → odef (p ∩ q) x → odef (P \ * (& (* xp ∩ * xq))) x
|
|
235 gf24 {x} ⟪ px , qx ⟫ = subst (λ k → odef (P \ k) x) (sym *iso) ⟪ L⊆PP gf25 _ (subst (λ k → odef k x) (sym *iso) px) , gf26 ⟫ where
|
|
236 gf26 : ¬ odef (* xp ∩ * xq) x
|
|
237 gf26 npx = proj2 (gf27 px) (proj1 npx)
|
|
238 gf30 : {x : Ordinal} → odef (P \ * (& (* xp ∩ * xq))) x → odef (p ∩ q) x
|
|
239 gf30 {x} pxp with subst (λ k → odef (P \ k) x) *iso pxp
|
|
240 ... | ⟪ Px , ¬xpqx ⟫ = ⟪ ? , gf28 ⟪ Px , (λ xqx → ¬xpqx ⟪ ? , xqx ⟫ ) ⟫ ⟫ where
|
|
241 gf28 : {x : Ordinal} → odef (P \ * xq) x → odef q x
|
|
242 gf28 {x} qx = subst (λ k → odef k x) (sym (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) qeq))) qx
|
|
243 pn : HOD
|
|
244 pn = * (find-p L C (gr Pp) (& p0))
|
|
245 qn : HOD
|
|
246 qn = * (find-p L C (gr Pq) (& p0))
|
|
247 gf20 : pn ≡ qn
|
|
248 gf20 = cong ( λ k → * (find-p L C k (& p0))) eq
|
|
249 gf19 : * xp ⊆ pn
|
|
250 gf19 = PDN.pn<gr Pp _
|
|
251 gf18 : PDN L p0 C xp → PDN L p0 C xq → Replaced (PDHOD L p0 C) (λ z → & (P \ * z)) (& (p ∩ q))
|
|
252 gf18 record { gr = gr₁ ; pn<gr = pn<gr₁ ; x∈PP = x∈PP₁ } record { gr = gr ; pn<gr = pn<gr ; x∈PP = x∈PP } = ?
|
|
253 -- record { z = xp ; az = Pp ; x=ψz = trans (cong (&) gf17) peq } where
|
1242
|
254 gf17 : p ∩ q ≡ p
|
|
255 gf17 = ==→o≡ record { eq→ = proj1 ; eq← = λ {y} px → ⟪ px , ? ⟫ }
|
1243
|
256 f4 : (y : Ordinal) → odef (* (find-p L C (gr Pp ) (& p0))) y → odef (p ∩ q) y
|
|
257 f4 y lt = ⟪ subst (λ k → odef k y) *iso ? , subst (λ k → odef k y) *iso (pn<gr ? ? lt) ⟫
|
1242
|
258 ... | tri> ¬a ¬b c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq ) } where
|
|
259 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
260 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
261 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
262 gf10 = record { gr = PDN.gr Pp ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
263 gf16 : gr Pq ≤ gr Pp
|
|
264 gf16 = <to≤ c
|
|
265 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
266 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
267 ... | case1 xpy = PDN.pn<gr Pp _ xpy
|
|
268 ... | case2 xqy = p-monotonic L p0 C gf16 (PDN.pn<gr Pq y xqy )
|
1240
|
269 gf00 : Replace (Replace (PDHOD L p0 C) (λ x → P \ x)) (_\_ P) ≡ PDHOD L p0 C
|
1242
|
270 gf00 = ==→o≡ record { eq→ = gf20 ; eq← = gf22 } where
|
|
271 gf20 : {x : Ordinal} → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P \ x₁)) (_\_ P)) x → PDN L p0 C x
|
|
272 gf20 {x} record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } =
|
|
273 subst (λ k → PDN L p0 C k ) (begin
|
|
274 z ≡⟨ sym &iso ⟩
|
|
275 & (* z) ≡⟨ cong (&) (sym (L\Lx=x gf21 )) ⟩
|
|
276 & (P \ ( P \ (* z) )) ≡⟨ cong (λ k → & ( P \ k)) (sym *iso) ⟩
|
|
277 & (P \ (* ( & (P \ (* z ))))) ≡⟨ cong (λ k → & (P \ (* k))) (sym x=ψz₁) ⟩
|
|
278 & (P \ (* z₁)) ≡⟨ sym x=ψz ⟩
|
|
279 x ∎ ) az where
|
|
280 open ≡-Reasoning
|
|
281 gf21 : {x : Ordinal } → odef (* z) x → odef P x
|
|
282 gf21 {x} lt = L⊆PP ( PDN.x∈PP az) _ lt
|
|
283 gf22 : {x : Ordinal} → PDN L p0 C x → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P \ x₁)) (_\_ P)) x
|
|
284 gf22 {x} pdx = record { z = _ ; az = record { z = _ ; az = pdx ; x=ψz = refl } ; x=ψz = ( begin
|
|
285 x ≡⟨ sym &iso ⟩
|
|
286 & (* x) ≡⟨ cong (&) (sym (L\Lx=x gf21 )) ⟩
|
|
287 & (P \ (P \ * x)) ≡⟨ cong (λ k → & ( P \ k)) (sym *iso) ⟩
|
|
288 & (P \ * (& (P \ * x))) ∎ ) } where
|
|
289 open ≡-Reasoning
|
|
290 gf21 : {z : Ordinal } → odef (* x) z → odef P z
|
|
291 gf21 {z} lt = L⊆PP ( PDN.x∈PP pdx ) z lt
|
1240
|
292 fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
|
1239
|
293 fdense D MD eq0 = ? where
|
448
|
294 open Dense
|
|
295
|
431
|
296 open GenericFilter
|
|
297 open Filter
|
|
298
|
1242
|
299 record NonAtomic (L a : HOD ) (L∋a : L ∋ a ) : Set (Level.suc (Level.suc n)) where
|
431
|
300 field
|
461
|
301 b : HOD
|
|
302 0<b : ¬ o∅ ≡ & b
|
|
303 b<a : b ⊆ a
|
431
|
304
|
461
|
305 lemma232 : (P L p : HOD ) (C : CountableModel )
|
1241
|
306 → (LP : L ⊆ Power P ) → (Lp0 : L ∋ p ) ( NEG : {p : HOD} → L ∋ p → L ∋ ( P \ p))
|
461
|
307 → ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq )
|
1243
|
308 → ¬ ( (ctl-M C) ∋ rgen ( P-GenericFilter P L p LP Lp0 ? NEG C ))
|
1241
|
309 lemma232 P L p C LP Lp0 NEG NA MG = {!!} where
|
1101
|
310 D : HOD -- P - G
|
|
311 D = ?
|
431
|
312
|
|
313 --
|
1174
|
314 -- P-Generic Filter defines a countable model D ⊂ C from P
|
|
315 --
|
|
316
|
|
317 --
|
|
318 -- in D, we have V ≠ L
|
|
319 --
|
|
320
|
|
321 --
|
431
|
322 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
|
|
323 --
|
436
|
324
|
1242
|
325 record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (Level.suc n) where
|
437
|
326 field
|
|
327 valx : HOD
|
436
|
328
|
437
|
329 record valS (ox oy oG : Ordinal) : Set n where
|
436
|
330 field
|
437
|
331 op : Ordinal
|
|
332 p∈G : odef (* oG) op
|
|
333 is-val : odef (* ox) ( & < * oy , * op > )
|
436
|
334
|
459
|
335 val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P}
|
1096
|
336 → (G : GenericFilter {L} {P} LP {!!} )
|
436
|
337 → HOD
|
437
|
338 val x G = TransFinite {λ x → HOD } ind (& x) where
|
|
339 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
|
439
|
340 ind x valy = record { od = record { def = λ y → valS x y (& (filter (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
|
437
|
341
|