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

comparison src/generic-filter.agda @ 438:50949196aa88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
⊆-reduction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 25 Feb 2022 14:46:43 +0900
parents 2b5d2072e1af
children fdcbf23ba2f9
comparison
equal deleted inserted replaced
437:2b5d2072e1af 438:50949196aa88
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 65 ctl-P∈M : Power P ∈ * ctl-M
66 66
67 -- we expect ¬ G ∈ * ctl-M, so ¬ P ∈ * ctl-M 67 -- we expect ¬ G ∈ * ctl-M, so ¬ P ∈ * ctl-M
68 68
69 open CountableModel 69 open CountableModel
70 70
125 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt )) 125 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
126 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y 126 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
127 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
128 128
129 open _⊆_ 129 open _⊆_
130
131 find-an :{P p : HOD} → (C : CountableModel P ) → odef (Power P) (& p) → Nat
132 find-an = ?
133
134 found-an :{P p : HOD} → (C : CountableModel P ) → (pw : odef (Power P) (& p)) → * (ctl→ C (find-an C pw)) =h= p
135 found-an = ?
136
137 record ⊆-reduce ( p : HOD ) : Set (suc n) where
138 field
139 next : HOD
140 is-small : next ⊆ p ∧ ( ¬ ( next =h= p ))
141
142 ⊆-induction : { ψ : (x : HOD) → Set (suc n) }
143 → (p : HOD) → ψ p
144 → (next : (x : HOD) → ψ x → ⊆-reduce x )
145 → (ind : (x : HOD) → (m : ψ x) → ψ ( ⊆-reduce.next (next x m )) )
146 → ψ od∅
147 ⊆-induction = ?
148
130 149
131 P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P 150 P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
132 P-GenericFilter P p0 C = record { 151 P-GenericFilter P p0 C = record {
133 genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 } 152 genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 }
134 ; generic = λ D → {!!} 153 ; generic = λ D → {!!}
150 f⊆PL : PDHOD P p0 C ⊆ Power P 169 f⊆PL : PDHOD P p0 C ⊆ Power P
151 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → 170 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
152 find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) } 171 find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
153 f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q 172 f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
154 f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = {!!} ; pn<gr = {!!} ; x∈PP = {!!} } where 173 f1 {p} {q} q⊆P PD∋p p⊆q = record { gr = {!!} ; pn<gr = {!!} ; x∈PP = {!!} } where
155 -- ¬ p ⊆ a n ⊆ p m 174 -- reduction : {ψ : (x : HOD) → x =h= od∅ → P x} →
156 -- a(n) ∈ M, ¬ (∃ q ∈ a(n) ∧ p(n) ⊆ q ) ∨ (∃ q ∈ a(n) ∧ p(n) ⊆ q ) 175 -- q ∈ a(∃ n) ⊆ P → ( p n ⊆ q → PDHOD P p0 C ∋ q )
176 -- ∨ (¬ (p n ⊆ q) → induction on (p n - q)
157 PDNp : {!!} -- PD⊆⊆N P C (& p) 177 PDNp : {!!} -- PD⊆⊆N P C (& p)
158 PDNp = PD∋p 178 PDNp = PD∋p
159 f02 : {x : Ordinal} → odef q x → odef P x 179 f02 : {x : Ordinal} → odef q x → odef P x
160 f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) ) 180 f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) )
161 f03 : {x : Ordinal} → odef p x → odef q x 181 f03 : {x : Ordinal} → odef p x → odef q x