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

comparison src/generic-filter.agda @ 436:87b5303ceeb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 22 Feb 2022 22:08:44 +0900
parents b18ca68d115a
children 2b5d2072e1af
comparison
equal deleted inserted replaced
435:b18ca68d115a 436:87b5303ceeb5
52 open import Data.Maybe 52 open import Data.Maybe
53 53
54 import OPair 54 import OPair
55 open OPair O 55 open OPair O
56 56
57 record CountableModel : Set (suc (suc n)) where 57 record CountableModel (P : HOD) : Set (suc (suc n)) where
58 field 58 field
59 ctl-M : Ordinal 59 ctl-M : Ordinal
60 ctl→ : Nat → Ordinal 60 ctl→ : Nat → Ordinal
61 ctl← : (x : Ordinal )→ x o< ctl-M → Nat 61 ctl← : (x : Ordinal )→ x o< ctl-M → Nat
62 is-Model : (x : Nat) → ctl→ x o< ctl-M 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 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 64 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (is-Model x) ≡ x
65 ctl-P⊆M : Power P ⊆ * ctl-M
66
67 -- we expect ¬ G ∈ * ctl-M, so ¬ P ∈ * ctl-M
65 68
66 open CountableModel 69 open CountableModel
67 70
68 ---- 71 ----
69 -- a(n) ∈ M 72 -- a(n) ∈ M
70 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q 73 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q
71 -- 74 --
72 PGHOD : (i : Nat) → (C : CountableModel) → (P : HOD) → (p : Ordinal) → HOD 75 PGHOD : (i : Nat) (P : HOD) (C : CountableModel P) → (p : Ordinal) → HOD
73 PGHOD i C P p = record { od = record { def = λ x → 76 PGHOD i P C p = record { od = record { def = λ x →
74 odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } 77 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) } 78 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }
76 79
77 --- 80 ---
78 -- p(n+1) = if (f n) then qn otherwise p(n) 81 -- p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
79 -- 82 --
80 next-p : (p : Ordinal) → (f : HOD → HOD) → Ordinal 83 next-p : (p : Ordinal) → (f : HOD → HOD) → Ordinal
81 next-p p f with is-o∅ ( & (f (* p))) 84 next-p p f with is-o∅ ( & (f (* p)))
82 next-p p f | yes y = p 85 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 86 next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice
84 87
85 --- 88 ---
86 -- search on p(n) 89 -- search on p(n)
87 -- 90 --
88 find-p : (C : CountableModel) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal 91 find-p : (P : HOD ) (C : CountableModel P) (i : Nat) → (x : Ordinal) → Ordinal
89 find-p C P Zero x = x 92 find-p P C Zero x = x
90 find-p C P (Suc i) x = find-p C P i ( next-p x (λ p → PGHOD i C P (& p) )) 93 find-p P C (Suc i) x = find-p P C i ( next-p x (λ p → PGHOD i P C (& p) ))
91 94
92 --- 95 ---
93 -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) } 96 -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
94 -- 97 --
95 record PDN (C : CountableModel) (P : HOD ) (x : Ordinal) : Set n where 98 record PDN (P p : HOD ) (C : CountableModel P) (x : Ordinal) : Set n where
96 field 99 field
97 gr : Nat 100 gr : Nat
98 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y 101 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p P C gr (& p))) y
99 x∈PP : odef (Power P) x 102 x∈PP : odef (Power P) x
100 103
101 open PDN 104 open PDN
102 105
103 --- 106 ---
104 -- G as a HOD 107 -- G as a HOD
105 -- 108 --
106 PDHOD : (C : CountableModel) → (P : HOD ) → HOD 109 PDHOD : (P p : HOD ) (C : CountableModel P ) → HOD
107 PDHOD C P = record { od = record { def = λ x → PDN C P x } 110 PDHOD P p C = record { od = record { def = λ x → PDN P p C x }
108 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) } 111 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) }
109 112
110 open PDN 113 open PDN
111 114
112 ---- 115 ----
123 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y 126 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
124 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt 127 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
125 128
126 open _⊆_ 129 open _⊆_
127 130
128 P-GenericFilter : (C : CountableModel) → (P : HOD ) → GenericFilter P 131 P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
129 P-GenericFilter C P = record { 132 P-GenericFilter P p0 C = record {
130 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 } 133 genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 }
131 ; generic = λ D → {!!} 134 ; generic = λ D → {!!}
132 } where 135 } where
133 PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i C P x ⊆ Power P 136 PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i P C x ⊆ Power P
134 PGHOD∈PL i x = record { incl = λ {x} p → proj1 p } 137 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 138 find-p-⊆P : (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p P C i x)) y → odef P y
136 find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso 139 find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso
137 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py)) 140 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py))
138 find-p-⊆P (Suc i) x y Px Py with is-o∅ ( & (PGHOD i C P (& (* x)))) 141 find-p-⊆P (Suc i) x y Px Py with is-o∅ ( & (PGHOD i P C (& (* x))))
139 ... | yes y1 = find-p-⊆P i x y Px Py 142 ... | yes y1 = find-p-⊆P i x y Px Py
140 ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where 143 ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where
141 fmin : HOD 144 fmin : HOD
142 fmin = ODC.minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq)) 145 fmin = ODC.minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
143 fmin∈PGHOD : PGHOD i C P (& (* x)) ∋ fmin 146 fmin∈PGHOD : PGHOD i P C (& (* x)) ∋ fmin
144 fmin∈PGHOD = ODC.x∋minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq)) 147 fmin∈PGHOD = ODC.x∋minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
145 pg-01 : Power P ∋ fmin 148 pg-01 : Power P ∋ fmin
146 pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i C P k ∋ fmin ) &iso fmin∈PGHOD ) 149 pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i P C k ∋ fmin ) &iso fmin∈PGHOD )
147 f⊆PL : PDHOD C P ⊆ Power P 150 f⊆PL : PDHOD P p0 C ⊆ Power P
148 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → 151 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
149 find-p-⊆P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) } 152 find-p-⊆P (gr lt) {!!} (& y) {!!} (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 153 f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
151 f1 {p} {q} q⊆P PD∋p p⊆q = f01 (& p) (& q) (⊆→o≤ f02) PD∋p (⊆→o≤ f03) where 154 f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = {!!} ; pn<gr = {!!} ; x∈PP = {!!} } where
155 -- ¬ p ⊆ a n ⊆ p m
156 -- a(n) ∈ M, ¬ (∃ q ∈ a(n) ∧ p(n) ⊆ q ) ∨ (∃ q ∈ a(n) ∧ p(n) ⊆ q )
157 PDNp : {!!} -- PD⊆⊆N P C (& p)
158 PDNp = PD∋p
152 f02 : {x : Ordinal} → odef q x → odef P x 159 f02 : {x : Ordinal} → odef q x → odef P x
153 f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) ) 160 f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) )
154 f03 : {x : Ordinal} → odef p x → odef q x 161 f03 : {x : Ordinal} → odef p x → odef q x
155 f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) ) 162 f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) )
156 f04 : (ip : Ordinal) → PDN C P ip → (x : Ordinal) → ((y : Ordinal) → y o< x → ip o< osuc y → PDN C P y) → ip o< osuc x → PDN C P x 163 next1 : Ordinal
157 f04 ip PD x prev lt with trio< ip (osuc x) 164 next1 = {!!} -- find-p P C (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) P C (& p₁)))
158 ... | tri≈ ¬a b ¬c = {!!} 165 f05 : next1 o< ctl-M C
159 ... | tri> ¬a ¬b c = ⊥-elim ( o<> c lt ) 166 f05 = {!!}
160 ... | tri< a ¬b ¬c with osuc-≡< a 167 f06 : odef (Power P) (& q)
161 ... | case1 ip=x = {!!} 168 f06 = {!!}
162 ... | case2 ip<x = record { gr = ctl← C (find-p C P (PDN.gr PD) ( next-p x (λ p → PGHOD (PDN.gr PD) C P (& p)))) f05 169 f07 : (y : Ordinal) → odef (* (& q)) y → odef (* {!!} ) y
163 ; pn<gr = f07 ; x∈PP = f06 } where 170 f07 = {!!}
164 next1 : Ordinal 171 f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
165 next1 = find-p C P (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) C P (& p₁)))
166 f05 : next1 o< ctl-M C
167 f05 = {!!}
168 f06 : odef (Power P) x
169 f06 = {!!}
170 f07 : (y : Ordinal) → odef (* x) y → odef (* (find-p C P (ctl← C next1 f05) o∅)) y
171 f07 = {!!}
172 f01 : (ip iq : Ordinal) → iq o< osuc (& P) → PDN C P ip → ip o< osuc iq → PDN C P iq
173 f01 ip iq q<P PD = TransFinite0 {λ x → ip o< osuc x → PDN C P x } (f04 ip PD ) iq
174 f2 : {p q : HOD} → PDHOD C P ∋ p → PDHOD C P ∋ q → PDHOD C P ∋ (p ∩ q)
175 f2 {p} {q} PD∋p PD∋q = {!!} 172 f2 {p} {q} PD∋p PD∋q = {!!}
176 173
177 174
178 175
179 open GenericFilter 176 open GenericFilter
185 r : {p : HOD } → Power P ∋ p → HOD 182 r : {p : HOD } → Power P ∋ p → HOD
186 incompatible : { p : HOD } → (P∋p : Power P ∋ p) → Power P ∋ q P∋p → Power P ∋ r P∋p 183 incompatible : { p : HOD } → (P∋p : Power P ∋ p) → Power P ∋ q P∋p → Power P ∋ r P∋p
187 → ( p ⊆ q P∋p) ∧ ( p ⊆ r P∋p) 184 → ( p ⊆ q P∋p) ∧ ( p ⊆ r P∋p)
188 → ∀ ( s : HOD ) → Power P ∋ s → ¬ (( q P∋p ⊆ s ) ∧ ( r P∋p ⊆ s )) 185 → ∀ ( s : HOD ) → Power P ∋ s → ¬ (( q P∋p ⊆ s ) ∧ ( r P∋p ⊆ s ))
189 186
190 lemma725 : (C : CountableModel) (P : HOD ) 187 lemma725 : (P p : HOD ) (C : CountableModel P)
191 → Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter C P ))) 188 → * (ctl-M C) ∋ Power P
189 → Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p C )))
192 lemma725 = {!!} 190 lemma725 = {!!}
193 191
194 open import PFOD O 192 open import PFOD O
195 193
196 -- HODω2 : HOD 194 -- HODω2 : HOD
199 -- ω→2 = Power infinite 197 -- ω→2 = Power infinite
200 198
201 lemma725-1 : Incompatible HODω2 199 lemma725-1 : Incompatible HODω2
202 lemma725-1 = {!!} 200 lemma725-1 = {!!}
203 201
204 lemma726 : (C : CountableModel) (P : HOD ) 202 lemma726 : (C : CountableModel HODω2)
205 → Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2 203 → Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p C )))) =h= ω→2
206 lemma726 = {!!} 204 lemma726 = {!!}
207 205
208 -- 206 --
209 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } 207 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
210 -- 208 --
209
210
211 record valR (x y P : HOD) (G : GenericFilter P) : Set (suc n) where
212 field
213 p : HOD
214 p∈G : filter (genf G) ∋ p
215 is-val : x ∋ < y , p >
216
217 val : (x : HOD) (P : HOD )
218 → (G : GenericFilter P)
219 → HOD
220 val x P G = record { od = record { odef = ε-induction { λ y → (z : Ordinal) → odef y (& z) → {!!} } (λ {z} Prev → {!!} ) }
221 ; odmax = {!!} ; <odmax = {!!} }
222
223 --
211 -- W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) | { i ∈ Nat → p i ≠ i1 } is finite } 224 -- W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) | { i ∈ Nat → p i ≠ i1 } is finite }
212 -- 225 --
213 226
214 227
215 228