第五章数学玄宇宙计划篇章 (9-8)
反思的反思(本节和玄宇宙计划无关)
2024/01/31： Proof Assistants Stack Exchange 上的回答宣称
presheaves ... is the computational interpretation of intuitionistic forcing, so you can use it e.g. to negate CH.[11]
预层...是直觉主义力迫的计算解释，所以你可以用它来(构建) ¬CH (的计算解释).
此人是Coq的核心开发者之一。如果此话属实，那么几乎所有的，除了高等力迫公理（也就是所谓的无穷组合学）之外的一切集合论成果都能移植到类型论上并且拥有计算解释。
• 对于外模型：这至少包括了苏斯林假设 SH，马丁公理 MAκ ， 但不包括 PFA，马丁最大化 MM，
• 对于内模型：包括了终极L，L(R)，...， L[U]，没有Woodin基数的核心模型K，... 但不是所有带有(弱)覆盖引理的内模型/核心模型都可以，有不少构造都需要一个比 ZFC 强得多的预延展系统。
• 所有其他弱于ZFC + Mahlo, [公式] - 反射, [公式] - 反射, ... 的一致性结果
这可以说是一个美妙到无法令人相信的图景。
版本修改
2024/01/31：处理了一些理解错误的注释，改进格式，加入了对反思的反思。
2014/02/15：改进翻译和格式，添加一些对全知原理的补充。
参考
1. [SD Friedman, 2018] Explaining Maximality Through the Hyperuniverse Programme
2. 这里说的就是Woodin的终极-L
3. 翻译者的评论：如果只讨论「对集合论之外的数学产生了重大影响」，那我就要提议模态逻辑，构造主义类型论作为候选者了。集合论的影响力远不能和后两者比较。
4. [寇亮，2020] 反映原理作为大基数内在辩护的不可行性
5. [寇亮，2020] 反映原理作为大基数内在辩护的不可行性
6. [SD Friedman, 2018] Explaining Maximality Through the Hyperuniverse Programme
7. 即便允许V 、Ord 这样的对象是完成的对象，可以使用，但让人难以理解的是“Ord + 1”、“ V_Ord 之外”这样的概念。毕竟，除了它们没有良好的定义之外，我们还很难想象 V 之外的所谓“类似集合的对象”是什么样。[寇亮，2020]
8. 类似于力迫法的发明路程，一个同时接受柏拉图主义和高度完成主义的人也会遇到类似的问题。[杨睿之, 2016] 作为哲学的数理逻辑，P124
9. -3-319-62935-3
数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。
