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

comparison Todo @ 1458:171c3f3cdc6b

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 Sat, 26 Aug 2023 08:37:08 +0900
parents f4dac8be0a01
children e8c166541c86
comparison
equal deleted inserted replaced
1457:79cf38cc667b 1458:171c3f3cdc6b
1 Sun Jul 9 09:42:20 JST 2023
2
3 Assume countable dense OD in Ordinal as L
4 if Power ω ∩ L is cardinal, ω c< (Power ω ∩ L) c< Power ω
5
1 Sat May 13 10:51:35 JST 2023 6 Sat May 13 10:51:35 JST 2023
2 7
3 use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter 8 use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
4 tranfinite induciton on well-founded set 9 tranfinite induciton on well-founded set
5 10
6 Sat Aug 1 13:16:53 JST 2020 11 Sat Aug 1 13:16:53 JST 2020
7 12
8 P Generic Filter 13 P Generic Filter
9 as a ZF model 14 as a ZF model ( -- this is no good )
10 define Definition for L 15 define Definition for L ( -- this is no good )
11 16
12 Tue Jul 23 11:02:50 JST 2019 17 Tue Jul 23 11:02:50 JST 2019
13 18
14 define cardinals ... done 19 define cardinals ... done
20
21 scheme on CH is no good in HOD
22
15 prove CH in OD→ZF 23 prove CH in OD→ZF
16 define Ultra filter ... done 24 define Ultra filter ... done
17 define L M : ZF ZFSet = M is an OD 25 define L M : ZF ZFSet = M is an OD
18 define L N : ZF ZFSet = N = G M (G is a generic fitler on M ) 26 define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
19 prove ¬ CH on L N 27 prove ¬ CH on L N