🔢 mathematics

Generalized Decidability via Brouwer Trees

本文在同伦类型论中引入了一个利用布劳尔序数（Brouwer ordinals）推广可判定性的框架，以建立 $\alpha$ -可判定命题的层级结构，并刻画了它们在逻辑运算与量词下的封闭性质，且所有结果均在 Cubical Agda 中进行了形式化。

原作者： Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

发布于 2026-07-10

📖 1 分钟阅读🧠 深度阅读

CC BY 4.0

原作者： Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

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

想象一下你是一名试图破解谜题的侦探。在计算机科学的世界里，我们通常将谜题分为三个桶：可判定（Decidable）（我们可以快速找到答案）、半可判定（Semidecidable）（如果答案是“是”，我们可以找到它；但如果答案是“否”，我们可能会永远等待下去）以及不可判定（Undecidable）（我们根本无法解决它）。

但如果有些谜题比其他的更“半可判定”呢？如果某些“是”的答案需要更长的时间才能找到，但仍然不会耗时到无穷大呢？

这正是 Tom de Jong、Nicolai Kraus、Aref Mohammadzadeh 和 Fredrik Nordvall Forsberg 在他们的新论文中所探索的内容。他们提出了一种衡量寻找“是”的答案究竟需要多长时间的方法，使用的是一种特殊的数字系统，叫做布劳尔树序数（Brouwer tree ordinals）。请记住，这些不是像 1, 2, 3 这样的普通数字，而是一个代表时间步长的神奇阶梯，它远远超越了无穷大。

时间的神奇阶梯

在他们的框架中，他们不只是说“它是可解的”。他们会说：“它是 $\alpha$ -可判定的”，其中 $\alpha$ 是他们神奇阶梯上的一个特定阶梯。

第 1 层（可判定）： 如果一个问题是 1-可判定的，这意味着你可以在有限的步骤内找到答案（或证明其不可能）。这就像检查一个数字是否为质数；你只需要向上计数，最终你就会确定。
第 $\omega + 1$ 层（半可判定）： 如果一个问题是 $(\omega + 1)$ -可判定的，这意味着如果答案是“是”，你将在 $\omega$ 步之内找到它。但 $\omega$ 不是一个普通的数字；它代表“永远计数下去”。所以，如果答案是“是”，你最终会找到它；但如果答案是“否”，你可能会不停地计数，永无止境。这就是经典的“半可判定”定义。

作者证明了这个新系统与旧系统完美契合。如果你有一个问题是“可判定的”，它就位于第 1 阶。如果它是“半可判定的”，它就位于 $\omega + 1$ 阶。但神奇之处在于，他们现在可以讨论介于两者之间、甚至更高阶梯的问题。

孪生素数之谜

为了展示这套方法如何运作，他们使用了一个著名的数学难题：孪生素数猜想（Twin Prime Conjecture）。这个问题问的是：“无论计数到多高，是否总能找到一对质数（比如 3 和 5，或者 11 和 13），它们之间的距离正好是 2？”

检查是否存在某一个特定的对子是很简单的（可判定的）。
检查在某个数字之上是否存在任何一对对子是半可判定的（你只需不断寻找；如果你找到了一个，你就停止）。
但大问题问的是，这是否对每一个数字都成立。

作者证明了这个特定的问题是 $\omega^2$ -可判定的。想象 $\omega$ 是单条无限长的线，而 $\omega^2$ 则像是拥有无数条这样的无限线堆叠在一起。这意味着，如果孪生素数猜想存在反例，你可以找到它，但可能需要经历一段相当于走过无数层无限线堆叠的时间跨度。

他们还研究了当你组合这些问题时会发生什么：

与（AND）： 如果你有两个 $\alpha$ -可判定的问题，它们的“与”（两者都必须为真）也是 $\alpha$ -可判定的。这就像检查两个盒子；如果你能在相同的时限内检查完两者，那就没问题。
或（OR）： 这比较复杂。如果两个问题的“或”（其中之一为真）要达到可判定，前提是时间限制必须足够小（具体来说，如果级别是类似 $\omega \cdot k + n$ 的形式）。如果时间限制变得太大，“或”可能会破坏他们系统的规则。

“选择”问题

这里是真正有趣的地方。作者发现，如果你想组合无限个“半可判定”的问题（比如检查每一个起始数字下的孪生素数猜想），你会撞上一堵墙。如果没有一个特殊的数学规则叫做可数选择（Countable Choice），你就无法证明组合后的结果仍然是半可判定的。

事实上，他们证明了如果你试图在没有该规则的情况下证明这一点，将会破坏其他基本的逻辑定律。因此，他们建议，为了让处理无限组合的数学运算能够顺利进行，你需要假设可数选择。

然而，他们也找到了一个变通方法！他们研究了另一种不同类型的“半可判定”，称为西尔宾斯基-半可判定（Sierpiński-semidecidable）。这是一种稍微弱一点的版本，它不需要依赖可数选择规则就能让你组合无限列表。这就像是另一种不同类型的手电筒，虽然光照范围不像原来的那么广，但它不需要电池（即不需要选择规则）就能点亮。

他们并未解决的问题

重要的是要了解这篇论文没有做的事情。作者非常明确：他们并没有解决孪生素数猜想。他们只是将其作为一个玩具示例，来展示他们这个新测量尺是如何工作的。

他们也承认，他们目前还不了解这个阶梯的完整形态。他们怀疑，如果你有一个处于阶梯 $\alpha$ 的问题和另一个处于阶梯 $\beta$ 的问题，且 $\alpha$ 低于 $\beta$ ，那么 $\alpha$ 上的问题也应该是 $\beta$ 可解的。但他们还没有证明这对阶梯上的每一个阶梯都成立。这目前是一个“猜想”（强有力的猜测），而不是一个事实。

底线总结

这篇论文提出了一种新的方式，用来讨论在数学和计算中寻找“是”的答案到底有多难。与其仅仅说“我们可以找到”或“我们找不到”，他们给了我们一把由无限步长组成的精确标尺。他们证明了这个标尺适用于我们已知的知识（可判定和半可判定），并用它来衡量像孪生素数猜想这样复杂的难题，发现其处于 $\omega^2$ 这个特定的、可测量的维度。

他们还表明，虽然这个标尺很强大，但它也有局限性：组合无限列表需要一个特定的假设（可数选择），除非你切换到另一种稍有不同的标尺（西尔宾斯基-半可判定）。

所有这一切都是在名为 Cubical Agda 的计算机程序中构建并经过检验的，该程序充当了一个超级严格的裁判，以确保他们逻辑中的每一步都是完美的。因此，尽管这些想法是全新的且令人兴奋，但其背后的数学逻辑是极其严密的。

技术摘要：通过 Brouwer 树实现的广义可判定性

问题陈述
在构造数学和合成可计算性理论中，将命题划分为“可判定的”、“半可判定的”或“不可判定的”标准分类往往过于粗糙。例如，虽然素数性的可判定性是显而易见的，但孪生素数猜想（即是否存在高于任何 $n$ 的孪生素数对）涉及一个由 $\omega$ 个半可判定子问题构成的结构。在经典数学中，这可能被视为极限的极限，但构造性框架需要一种更精确的方式来衡量寻找证据的“持续时间”或复杂度。现有的序数概念（如句法性的 Cantor 范式或语义上的良基关系）无法提供合适的层级结构：句法方法使所有比较都变得可判定（从而导致层级坍缩），而语义方法则往往无法使比较变得半可判定。本文旨在解决建立一个能够实现更精细的可判定性区分的框架的需求，特别是为了刻画那些需要经由超限步骤才能验证的命题。

方法论
作者在 同伦类型论 (HoTT) 的框架内开展工作，利用 Brouwer 树序数 ( $\text{Brw}$ ) 作为其层级的基础。这些序数是通过一个包含零、后继以及严格递增序列极限构造器的 商归纳归纳类型 (QIIT) 来定义的。至关重要的是，极限构造器仅接受严格递增的序列，这确保了有限性是可判定的，同时保留了理论的构造性质。

核心定义引入了 $\alpha$ -可判定性：一个命题 $P$ 是 $\alpha$ -可判定的，如果存在一个序数 $y$ ，使得 $P \leftrightarrow (\alpha \leq y)$ 。该定义推广了现有概念：

$1 $-可判定性（或$ \omega$-可判定性）对应于标准的可判定性。
$(\omega + 1)$ -可判定性（等价于 $\omega \cdot 2$ -可判定性）对应于半可判定性。

作者在 Cubical Agda 中形式化了所有结果，利用了其对 QIIT 的原生支持和单价性（univalence）。他们采用了特定技术来处理在 QIIT 上定义函数的复杂性，例如先在点构造器上定义关系，随后再提取函数，以避免在处理路径构造器时出现组合爆炸。

主要贡献与结果

可判定性层级：
- 本文确立了 $\alpha$ -可判定性是可判定性和半可判定性的推广。
- 研究表明，对于任何序数 $\alpha$ ， $(\alpha+1)$ -可判定性等价于 $(\alpha+\omega)$ -可判定性。因此，该层级可以有效地由极限序数（非后继序数）进行索引。
- 作者证明，如果 $P$ 是 $\alpha$ -可判定的且 $Q$ 是 $\alpha$ -可判定的，那么 $P \land Q$ 也是 $\alpha$ -可判定的。这依赖于为非后继序数构造一个二元最小值函数，而如果不隐含有限性原则 (LPO)，在任意序数上通常无法实现这一点。
析取与最大值：
- 虽然合取在同一层级是封闭的，但二元析取对于任意 $\alpha$ 并非封闭。然而，作者证明了 $(\omega \cdot k + n)$ -可判定的命题在二元析取下是封闭的。这需要相对于形如 $\omega \cdot k$ 的序数构造一个二元最大值函数。
- 作者证明，非后继序数的全局二元最大值的存在意味着 LPO，这是一个构造性的禁忌。
可数量词与族：
- 可数交 (Countable Meets)： 对于一个半可判定命题族 $P: \mathbb{N} \to \text{Prop}$ ，可数交 $\forall i. P(i)$ 被证明是 $\omega^2$ -可判定的。这一结果被应用于孪生素数猜想，将其刻画为 $\omega^2$ -可判定。
- 可数并 (Countable Joins)： 半可判定命题的可数并 $\exists i. P(i)$ 被证明是 $(\omega \cdot 3)$ -可判定的。
- 量词交替： 本文分析了具有交替量词的公式。对于一个满足 $P(n, m) \to P(n, m+1)$ 的族 $P(n, m)$ ，命题 $\exists m. \forall n. P(n, m)$ 被证明是 $(\omega^2 + \omega)$ -可判定的。这为寻找孪生素数猜想反例的搜索过程提供了一个精确的序数界限。
与选择原则的关系：
- 作者研究了可数选择 (AC) 的影响。假设 AC，半可判定命题的可数并变为半可判定（即 $(\omega \cdot 3)$ -可判定坍缩为 $(\omega \cdot 2)$ -可判定）。
- 然而，即使在有 AC 的情况下， $\omega^2$ -可判定的命题也不会坍缩为半可判定，除非马尔可夫原理蕴含 LPO。
- 本文引入了 Sierpiński-半可判定性（基于 Sierpiński 类型，即自由的 $\omega$ -完备偏序集）作为另一种半可判定性的概念，它在不假设可数选择的情况下对可数并也是封闭的。研究表明，Sierpiński-半可判定性弱于标准的半可判定性。

意义与主张
作者将这项工作定位为广义可判定性理论的第一步。他们声称提供了一个框架，在该框架下，算法的“持续时间”（在构造性的、抽象的意义上）可以通过序数算术进行精确的指定和证明。

论文谦虚地指出，它并未解决诸如孪生素数猜想之类的开放问题；相反，它提供了一种描述此类问题复杂度的形式化语言。它强调，可判定性层级尚未被完全理解，特别指出是否对于所有 $\alpha \leq \beta$ ， $\alpha$ -可判定性都蕴含 $\beta$ -可判定性仍是一个开放问题（尽管已提供了部分结果）。此外，是否 Brouwer 树序数是该理论的最优序数概念，或者其他的序数构造能否产生不同且可能更丰富的层级，也是留待研究的问题。

所有结果均在 Cubical Agda 中进行了严密的程序化实现，确保了证明的构造性质以及序数及其属性定义的计算可靠性。