|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 module generic-filter {n : Level } (O : Ordinals {n}) where
|
|
|
4
|
|
|
5 import filter
|
|
|
6 open import zf
|
|
|
7 open import logic
|
|
|
8 -- open import partfunc {n} O
|
|
|
9 import OD
|
|
|
10
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Data.Empty
|
|
|
14 open import Relation.Binary
|
|
|
15 open import Relation.Binary.Core
|
|
|
16 open import Relation.Binary.PropositionalEquality
|
|
|
17 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
18 import BAlgbra
|
|
|
19
|
|
|
20 open BAlgbra O
|
|
|
21
|
|
|
22 open inOrdinal O
|
|
|
23 open OD O
|
|
|
24 open OD.OD
|
|
|
25 open ODAxiom odAxiom
|
|
|
26 import OrdUtil
|
|
|
27 import ODUtil
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
|
30 open Ordinals.IsNext isNext
|
|
|
31 open OrdUtil O
|
|
|
32 open ODUtil O
|
|
|
33
|
|
|
34
|
|
|
35 import ODC
|
|
|
36
|
|
|
37 open filter O
|
|
|
38
|
|
|
39 open _∧_
|
|
|
40 open _∨_
|
|
|
41 open Bool
|
|
|
42
|
|
|
43
|
|
|
44 open HOD
|
|
|
45
|
|
|
46 -------
|
|
|
47 -- the set of finite partial functions from ω to 2
|
|
|
48 --
|
|
|
49 --
|
|
|
50
|
|
|
51 open import Data.List hiding (filter)
|
|
|
52 open import Data.Maybe
|
|
|
53
|
|
|
54 import OPair
|
|
|
55 open OPair O
|
|
|
56
|
|
434
|
57 record CountableModel : Set (suc (suc n)) where
|
|
431
|
58 field
|
|
434
|
59 ctl-M : Ordinal
|
|
|
60 ctl→ : Nat → Ordinal
|
|
|
61 ctl← : (x : Ordinal )→ x o< ctl-M → Nat
|
|
|
62 is-Model : (x : Nat) → ctl→ x o< ctl-M
|
|
|
63 ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M) → ctl→ (ctl← x lt ) ≡ x
|
|
|
64 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (is-Model x) ≡ x
|
|
|
65
|
|
|
66 open CountableModel
|
|
431
|
67
|
|
|
68 ----
|
|
|
69 -- a(n) ∈ M
|
|
|
70 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q
|
|
|
71 --
|
|
434
|
72 PGHOD : (i : Nat) → (C : CountableModel) → (P : HOD) → (p : Ordinal) → HOD
|
|
431
|
73 PGHOD i C P p = record { od = record { def = λ x →
|
|
|
74 odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) }
|
|
|
75 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }
|
|
|
76
|
|
|
77 ---
|
|
433
|
78 -- p(n+1) = if (f n) then qn otherwise p(n)
|
|
431
|
79 --
|
|
433
|
80 next-p : (p : Ordinal) → (f : HOD → HOD) → Ordinal
|
|
|
81 next-p p f with is-o∅ ( & (f (* p)))
|
|
|
82 next-p p f | yes y = p
|
|
|
83 next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice
|
|
431
|
84
|
|
|
85 ---
|
|
434
|
86 -- search on p(n)
|
|
431
|
87 --
|
|
434
|
88 find-p : (C : CountableModel) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
|
|
431
|
89 find-p C P Zero x = x
|
|
433
|
90 find-p C P (Suc i) x = find-p C P i ( next-p x (λ p → PGHOD i C P (& p) ))
|
|
431
|
91
|
|
|
92 ---
|
|
|
93 -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
|
|
|
94 --
|
|
434
|
95 record PDN (C : CountableModel) (P : HOD ) (x : Ordinal) : Set n where
|
|
431
|
96 field
|
|
|
97 gr : Nat
|
|
|
98 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
|
|
|
99 x∈PP : odef (Power P) x
|
|
|
100
|
|
|
101 open PDN
|
|
|
102
|
|
|
103 ---
|
|
|
104 -- G as a HOD
|
|
|
105 --
|
|
434
|
106 PDHOD : (C : CountableModel) → (P : HOD ) → HOD
|
|
431
|
107 PDHOD C P = record { od = record { def = λ x → PDN C P x }
|
|
|
108 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) }
|
|
|
109
|
|
|
110 open PDN
|
|
|
111
|
|
|
112 ----
|
|
|
113 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
|
|
|
114 --
|
|
|
115 -- p 0 ≡ ∅
|
|
434
|
116 -- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) )
|
|
431
|
117 --- else p n
|
|
|
118
|
|
|
119 P∅ : {P : HOD} → odef (Power P) o∅
|
|
|
120 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
|
|
|
121 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
|
|
|
122 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
|
|
|
123 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
|
|
|
124 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
|
|
|
125
|
|
433
|
126 open _⊆_
|
|
|
127
|
|
434
|
128 P-GenericFilter : (C : CountableModel) → (P : HOD ) → GenericFilter P
|
|
431
|
129 P-GenericFilter C P = record {
|
|
434
|
130 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 }
|
|
431
|
131 ; generic = λ D → {!!}
|
|
|
132 } where
|
|
434
|
133 PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i C P x ⊆ Power P
|
|
|
134 PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
|
|
|
135 find-p-⊆P : (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y
|
|
|
136 find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso
|
|
431
|
137 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py))
|
|
434
|
138 find-p-⊆P (Suc i) x y Px Py with is-o∅ ( & (PGHOD i C P (& (* x))))
|
|
|
139 ... | yes y1 = find-p-⊆P i x y Px Py
|
|
|
140 ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where
|
|
|
141 fmin : HOD
|
|
|
142 fmin = ODC.minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
143 fmin∈PGHOD : PGHOD i C P (& (* x)) ∋ fmin
|
|
|
144 fmin∈PGHOD = ODC.x∋minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
145 pg-01 : Power P ∋ fmin
|
|
|
146 pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i C P k ∋ fmin ) &iso fmin∈PGHOD )
|
|
431
|
147 f⊆PL : PDHOD C P ⊆ Power P
|
|
|
148 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
|
|
434
|
149 find-p-⊆P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
|
|
|
150 f1 : {p q : HOD} → q ⊆ P → PDHOD C P ∋ p → p ⊆ q → PDHOD C P ∋ q
|
|
|
151 f1 {p} {q} q⊆P PD∋p p⊆q = {!!}
|
|
|
152 f2 : {p q : HOD} → PDHOD C P ∋ p → PDHOD C P ∋ q → PDHOD C P ∋ (p ∩ q)
|
|
|
153 f2 {p} {q} PD∋p PD∋q = {!!}
|
|
|
154
|
|
431
|
155
|
|
|
156
|
|
|
157 open GenericFilter
|
|
|
158 open Filter
|
|
|
159
|
|
|
160 record Incompatible (P : HOD ) : Set (suc (suc n)) where
|
|
|
161 field
|
|
434
|
162 q : {p : HOD } → Power P ∋ p → HOD
|
|
|
163 r : {p : HOD } → Power P ∋ p → HOD
|
|
|
164 incompatible : { p : HOD } → (P∋p : Power P ∋ p) → Power P ∋ q P∋p → Power P ∋ r P∋p
|
|
|
165 → ( p ⊆ q P∋p) ∧ ( p ⊆ r P∋p)
|
|
|
166 → ∀ ( s : HOD ) → Power P ∋ s → ¬ (( q P∋p ⊆ s ) ∧ ( r P∋p ⊆ s ))
|
|
431
|
167
|
|
434
|
168 lemma725 : (C : CountableModel) (P : HOD )
|
|
|
169 → Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter C P )))
|
|
431
|
170 lemma725 = {!!}
|
|
|
171
|
|
433
|
172 open import PFOD O
|
|
|
173
|
|
|
174 -- HODω2 : HOD
|
|
|
175 --
|
|
|
176 -- ω→2 : HOD
|
|
|
177 -- ω→2 = Power infinite
|
|
|
178
|
|
431
|
179 lemma725-1 : Incompatible HODω2
|
|
|
180 lemma725-1 = {!!}
|
|
|
181
|
|
434
|
182 lemma726 : (C : CountableModel) (P : HOD )
|
|
431
|
183 → Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
|
|
|
184 lemma726 = {!!}
|
|
|
185
|
|
|
186 --
|
|
|
187 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
|
|
|
188 --
|
|
|
189 -- W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) | { i ∈ Nat → p i ≠ i1 } is finite }
|
|
|
190 --
|
|
|
191
|
|
|
192
|
|
|
193
|
