連続体仮説の独立性は定理証明支援系で証明されているのに対してBorel予想の無矛盾性みたいな反復強制法が必要となるやつはまだされていないのって、やっぱり反復強制法は形式化するの大変なんかなと勝手に思っている。
CHの独立性だけだったら強制関係だけで割と簡単にいくけど反復強制はジェネリックフィルター取らずにやるのはしんどすぎるので…。
Embed Notice
HTML Code
Corresponding Notice
- Embed this notice
fujidig@mathtod.online's status on Wednesday, 14-Aug-2024 17:25:35 JSTfujidig