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

comparison src/generic-filter.agda @ 1249:c57b8068f97c

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 Wed, 15 Mar 2023 12:59:55 +0900
parents b1d024385208
children 6c467705e6e4
comparison
equal deleted inserted replaced
1248:b1d024385208 1249:c57b8068f97c
60 ctl→ : ℕ → Ordinal 60 ctl→ : ℕ → Ordinal
61 ctl<M : (x : ℕ) → odef (ctl-M) (ctl→ x) 61 ctl<M : (x : ℕ) → odef (ctl-M) (ctl→ x)
62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → ℕ 62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → ℕ
63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x 63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x
64 TC : {x y : Ordinal} → odef ctl-M x → odef (* x) y → odef ctl-M y 64 TC : {x y : Ordinal} → odef ctl-M x → odef (* x) y → odef ctl-M y
65 is-model : (x : HOD) → ctl-M ∋ (x ∩ ctl-M) 65 is-model : (x : HOD) → & x o< & ctl-M → ctl-M ∋ (x ∩ ctl-M)
66 -- we have no otherway round 66 -- we have no otherway round
67 -- ctl-iso← : { x : ℕ } → ctl← (ctl→ x ) (ctl<M x) ≡ x 67 -- ctl-iso← : { x : ℕ } → ctl← (ctl→ x ) (ctl<M x) ≡ x
68 -- 68 --
69 -- almmost universe 69 -- almmost universe
70 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x 70 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
371 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 ) 371 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
372 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra 372 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra
373 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q )) 373 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
374 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))) 374 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
375 → (C : CountableModel ) 375 → (C : CountableModel )
376 → ctl-M C ∋ L
376 → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp ) 377 → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
377 → ¬ ( ctl-M C ∋ rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C )) 378 → ¬ ( ctl-M C ∋ rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C ))
378 lemma232 P L p0 LPP Lp0 CAP UNI NEG C NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj2 rgf∩D) (proj1 rgf∩D)) 379 lemma232 P L p0 LPP Lp0 CAP UNI NEG C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj2 rgf∩D) (proj1 rgf∩D))
379 ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where 380 ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
380 GF = genf ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C ) 381 PG = P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C
381 rgf = rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C ) 382 GF = genf PG
383 rgf = rgen PG
382 M = ctl-M C 384 M = ctl-M C
383 D : HOD 385 D : HOD
384 D = L ＼ rgf 386 D = L ＼ rgf
385 M∋DM : M ∋ (D ∩ M ) 387 M∋DM : M ∋ (D ∩ M )
386 M∋DM = is-model C D 388 M∋DM = is-model C D ?
387 D⊆PP : D ⊆ Power P 389 D⊆PP : D ⊆ Power P
388 D⊆PP {x} ⟪ Lx , ngx ⟫ = LPP Lx 390 D⊆PP {x} ⟪ Lx , ngx ⟫ = LPP Lx
389 ll01 : {q r : HOD } → (rgf ∋ q) ∧ (rgf ∋ r) → (q ⊆ rgf ) ∧ (r ⊆ rgf ) 391 -- ll01 : {q r : HOD } → (rgf ∋ q) ∧ (rgf ∋ r) → (q ⊆ (q ∪ r) ) ∧ (r ⊆ (q ∪ r) )
390 ll01 {q} {r} rgfpq = ⟪ ll02 , ? ⟫ where 392 -- ll01 {q} {r} rgfpq with gfilter2 PG rgfpq
391 ll02 : {x : Ordinal } → odef q x → odef rgf x 393 -- ... | record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } = ?
392 ll02 {x} qx = record { z = ? ; az = record { z = ? ; az = ? ; x=ψz = ? } ; x=ψz = ? } 394 -- ll02 : {x : Ordinal } → odef q x → odef rgf x
393 -- filter2 GF ? ? ? 395 -- ll02 {x} qx = record { z = ? ; az = record { z = ? ; az = ? ; x=ψz = ? } ; x=ψz = ? }
396 -- -- filter2 GF ? ? ?
394 -- with contra-position ? ? 397 -- with contra-position ? ?
395 -- ... | t = ? 398 -- ... | t = ?
396 DD : Dense {L} {P} LPP 399 DD : Dense {L} {P} LPP
397 Dense.dense DD = D 400 Dense.dense DD = D
398 Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx 401 Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx