|
1458
|
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
|
|
1283
|
6 Sat May 13 10:51:35 JST 2023
|
|
|
7
|
|
|
8 use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
|
|
|
9 tranfinite induciton on well-founded set
|
|
|
10
|
|
423
|
11 Sat Aug 1 13:16:53 JST 2020
|
|
|
12
|
|
|
13 P Generic Filter
|
|
1458
|
14 as a ZF model ( -- this is no good )
|
|
|
15 define Definition for L ( -- this is no good )
|
|
423
|
16
|
|
187
|
17 Tue Jul 23 11:02:50 JST 2019
|
|
|
18
|
|
423
|
19 define cardinals ... done
|
|
1458
|
20
|
|
|
21 scheme on CH is no good in HOD
|
|
|
22
|
|
187
|
23 prove CH in OD→ZF
|
|
338
|
24 define Ultra filter ... done
|
|
187
|
25 define L M : ZF ZFSet = M is an OD
|
|
|
26 define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
|
|
|
27 prove ¬ CH on L N
|
|
|
28 prove no choice function on L N
|
|
|
29
|
|
148
|
30 Mon Jul 8 19:43:37 JST 2019
|
|
|
31
|
|
338
|
32 ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive ... fixed
|
|
148
|
33
|
|
|
34 remove ord-Ord and prove with some assuption in HOD.agda
|
|
|
35 union, power set, replace, inifinite
|
