第五章数学玄宇宙计划篇章 (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），接着再看更方便。