💻 computer science

Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

本文分析了 coq-paradoxes 库中机械化的四个悖论，以阐明它们如何共同界定 Rocq 内核的必要设计边界——特别是关于非 predicativity、大消除和宇宙约束——通过说明系统为维护一致性而必须拒绝某些构造的确切原因。

原作者： Bernardo Alonso

发布于 2026-05-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Bernardo Alonso

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你有一位非常严格、极其聪明的机器人建筑师，名叫Rocq。它的工作是构建逻辑结构（数学证明），并保证这些结构是安全且一致的。它绝不会崩溃，绝不会撒谎，也绝不会产生矛盾。

但你如何知道这位机器人是否正确地完成了它的工作呢？你不仅仅是观察它如何构建；你试图欺骗它。你试图向它提供一份蓝图，这份蓝图看起来应该能行得通，但实际上包含了一个隐藏的陷阱，会导致整座建筑崩塌。

本文介绍的是一个名为coq-paradoxes的特殊“陷阱蓝图”库。它包含了四个具体的尝试，旨在破坏机器人的逻辑。本文认为，这些不仅仅是谜题或奇闻异事；它们实际上是机器人倒写的“安全手册”。它们精确地展示了机器人的规则是如何划定边界以防止灾难发生的。

以下是这四个陷阱及其所揭示的教训的分解，使用了简单的类比：

1. 布拉利 - 福尔蒂陷阱（The Burali-Forti Trap）： “包含自身的盒子”

陷阱： 想象一个图书馆，其中每一本书都有一个标签，描述其自身的内容。该悖论试图创建一个“总目录”，列出图书馆中的每一本书，包括“总目录”本身。
问题： 如果目录是一本书，它必须将自己列入目录。但如果它将自己列入目录，它就会改变图书馆的规模，进而改变目录，再进而改变图书馆……这是一个打破规模规则的循环。
教训： 机器人（Rocq）有一条关于**宇宙层级（Universe Hierarchy）**的规则。它规定：“一个盒子不能位于一个与它自身大小相同的盒子内部。”机器人拒绝构建“总目录”，因为数学表明“内层盒子”必须比“外层盒子”小。这个陷阱证明，机器人正在正确地执行严格的规模限制，以防止无限循环。

2. 迪亚科内斯库陷阱（The Diaconescu Trap）： “魔法硬币翻转器”

陷阱： 想象你有一台机器，可以从任何一组平局选项中选出一个“获胜者”（例如从一群同卵双胞胎中选出一名代表）。该悖论声称：“如果你给我这台机器，我就能迫使它告诉我任何是/否问题的答案（例如‘天空是蓝色的吗？’），而无需真正知道答案。”
问题： 在一个构造性系统（你必须构建答案，而不仅仅是猜测）中，拥有一台能从平局中选出获胜者的机器过于强大。它暗中迫使系统接受“要么 A 为真，要么 A 为假”适用于一切事物，包括那些我们尚无法证明的事物。
教训： 机器人有一条关于**大消除（Large Elimination）**的规则。它规定：“你可以从一组数字中选出一个获胜者，但你不能利用这一点来神奇地决定一个哲学真理。”这个陷阱表明，如果机器人允许这种“魔法选择”，它将意外地破坏系统区分“已知事物”和“未知事物”的能力。

3. 雷诺兹陷阱（The Reynolds Trap）： “无法存在的字典”

陷阱： 想象试图创建一本字典，其中每一个可能的定义都是字典中的一个单词。该悖论试图构建一个“通用字典”，将每一个可能的句子映射到一个单词。
问题： 这就像试图将整张世界地图压缩到一枚邮票上。数学证明，如果你试图将所有可能的逻辑陈述压缩成单一类型的对象，就会产生矛盾（类似于你无法列出所有可能的列表）。
教训： 机器人有一条关于**非直谓性（Impredicativity）**的规则（允许定义引用其所属的整个集合）。机器人允许这种机制用于“命题”（简单的真/假陈述），但在其他地方划定了严格的界限。这个陷阱表明，如果机器人允许这种针对复杂类型的“通用字典”，整个系统将崩溃。

4. 赫肯斯陷阱（The Hurkens Trap）： “自指镜子”

陷阱： 这是最复杂的一个。想象一面镜子，它反射出倒影，倒影又反射出倒影，永无止境。该悖论试图构建一个系统，在其中你可以观察一个“小”对象（例如布尔值真/假），并用它来定义一个“大”对象（例如整个类型宇宙），然后再用那个大对象来定义那个小对象。
问题： 这是一个“自指循环”，它以创造逻辑悖论的方式结合了观察大事物和小事物的能力。这就像一条蛇在吞食自己的尾巴，但尾巴是由蛇自己的身体构成的。
教训： 机器人有一条关于**集合中的非直谓性（Impredicativity in Set）**的规则。它规定：“你可以对简单的真/假陈述进行自指，但你不能将这种自指与庞大、复杂的类型混合在一起。”这个陷阱证明，如果机器人允许这种混合，系统将无法保持一致性。

全局视角：为何这很重要

本文认为，我们不应将这四个文件视为“失败的数学”。相反，我们应该将它们视为机器人成功的证据。

负面规范： 将这些文件想象成通缉犯的海报。通缉犯是“不一致性”。海报并没有展示通缉犯本人；它展示了通缉犯恰好会出现的确切条件。
边界： 机器人（Rocq）在沙地上画了三条看不见的线：
1. 规模限制： 你不能将一个盒子放入一个与它自身大小相同的盒子中。
2. 选择限制： 你不能利用一个简单的选择来强制得出一个复杂的真理。
3. 反射限制： 你不能将简单的自指与复杂的类型混合在一起。

每当用户试图构建跨越这些界限之一的结构时，机器人就会阻止他们。这四个文件证明了机器人正在做它被设计要做的事情：拒绝构建任何最终会倒塌的东西。

简而言之，本文指出：“我们试图用这四个巧妙的技巧来破坏系统。系统说了‘不’。这个‘不’是系统最重要的部分，因为它让一切保持安全。”

技术摘要：四个悖论与一个证明助手

问题陈述
本文探讨了归纳构造演算（CIC）的基础边界，CIC 是 Rocq 证明助手（前身为 Coq）所基于的类型理论。尽管 CIC 的一致性已得到充分确立，但那些防止不一致性的具体设计决策——特别是关于非直谓性、层级约束和大消除（large elimination）的决策——往往被视为抽象的工程约束。随 Rocq 分发的 coq-paradoxes 库包含了四个形式化推导出的 False（Burali-Forti、Diaconescu、Reynolds 和 Hurkens），它们依赖于被 Rocq 内核拒绝的假设。核心问题在于，不仅要将这些推导视为历史奇闻或孤立的不一致案例，更要将其解读为一种“负面规范”，精确界定内核必须划定界限以维持可靠性的具体位置。

方法论
本文采用对 coq-paradoxes 库源代码的细致研读，具体分析四个文件：BuraliForti.v、diaconescu.v、Reynolds.v 和 Hurkens_Set.v。方法论包括：

解构共享机制：分析 Logics.v 以理解被多个悖论使用的可访问性谓词（ACC）和良基性基础设施。
追踪推导过程：跟随每个文件中的逻辑步骤，识别导致矛盾的具体假设（例如，关系的通用类型、选择公理，或从 Prop 到单个命题的注入）。
映射至内核拒绝机制：将形式化中的矛盾点与 Rocq 内核中的具体机制（层级算术、消除规则或非直谓性检查）相关联，该机制阻止了该构造的编译。
综合设计决策：汇总发现，提取出 governing 内核行为的三个统一边界条件。

主要贡献与结果

本文分析了四个具体的悖论，展示了如果某些设计选择被更改，每个悖论如何揭示类型理论中的独特漏洞：

Burali-Forti 悖论（BuraliForti.v）：
- 机制：假设存在一个关系的通用类型 $A_0$ 和一个注入 $i_0$ ，将关系映射到 $A_0$ 的元素。这使得能够构造一个“所有序数的序数”（ $\Omega$ ），并将其嵌入自身。
- 内核拒绝：该悖论依赖于将 $A_0$ 实例化为自身。Rocq 内核强制执行严格的层级分层（ $Type_j < Type_i$ ），以防止一个类型包含其自身的图像。该构造触发了“层级不一致”错误，因为内部类型所需的层级必须至少与外部类型一样大，从而违反了内核的累积约束。
- 结果：确立了层级约束的必要性，以防止导致不动点矛盾的自我引用类型定义。
Diaconescu 悖论（diaconescu.v）：
- 机制：使用基于命题 $P$ 定义的 bool 上的等价关系上的类型化选择公理（Tchoice）。选择函数 $f: bool \to bool$ 通过比较 $f(\text{true})$ 和 $f(\text{false})$ 来决定 $P$ 。
- 内核拒绝：该论证从 Prop 中的存在性证明中提取了一个计算决策（Set 中的函数）。这构成了从 Prop 到 Set 的“大消除”。
- 结果：证明了允许在 Set 中使用选择公理（或从 Prop 到 Set 的大消除）会将排中律（LEM）强加给构造性系统。内核限制大消除，以防止将经典逻辑引入计算层。
Reynolds 悖论（Reynolds.v）：
- 机制：重述了 Reynolds 关于 System F 没有集合论模型的结果。它假设存在一个注入 $I: Prop \to Heyt$ （其中 $Heyt $是单个命题），并为函子$ \Phi$ 构造了一个预初始代数（Church 编码）。利用 Lawvere 的不动点定理，它推导出了否定的不动点，进而导致 False。
- 内核拒绝：该构造依赖于 Prop 的非直谓性（在 Prop 内对所有命题进行量化）。然而，该悖论需要从一个命题到单个命题的注入，内核基于层级理由在逻辑矛盾发生之前就拒绝了这一点。
- 结果：突显了**Prop 中非直谓性**的作用。虽然 Prop 是非直谓的，但内核阻止了那些会使康托尔对角线论证导致命题宇宙坍缩的特定结构注入。
Hurkens 悖论（Hurkens_Set.v）：
- 机制：对 Hurkens 简化 Girard 悖论的改编。它假设 Prop 和 bool 之间存在一个收缩（通过双重否定），并利用 Set 的非直谓性（如果启用）结合大消除，构造一个导致 False 的自我引用良基关系。
- 内核拒绝：该悖论需要**Set 中的非直谓性和大消除**（从命题内容中提取布尔值）。默认的 Rocq 内核保持 Set 为直谓的，并限制从 Prop 的大消除。
- 结果：表明 Set 中非直谓性与大消除的组合与经典逻辑（LEM）不一致。内核决定保持 Set 直谓并限制消除，是这一安全机制。

意义与主张

本文认为，coq-paradoxes 包充当了 Rocq 内核的负面规范。该包不仅仅是列举不一致性，而是通过失败的示例提供了内核可靠性的形式化证明。

三个边界条件：本文将四个悖论综合为内核执行的三个具体设计决策：
1. 层级分层：防止类型以创建不动点的方式对自身进行量化（Burali-Forti）。
2. 非直谓性的定位：将非直谓性量化限制在 Prop（以及在特定条件下可选的 Set），防止 Reynolds 和 Hurkens 矛盾。
3. 大消除的纪律：限制从命题证明中提取计算内容（如 bool 或 Set 中的函数），防止 Diaconescu 和 Hurkens 矛盾。
元数学角色：本文声称该包是写在它所记录的系统内部的独特元数学作品。它不为应用证明定理，而是证明特定假设的不可满足性。内核的“拒绝”被证明是统一政策（层级算术、消除规则）的结果，而非临时修补。
结论：其意义在于证明 Rocq 内核拒绝编译这些构造并非随意，而是维持 CIC 一致性所必需的精确结构机制。该包验证了内核的设计决策是出于“正确的理由”做出的，有效地从外向内划定了系统的边界。