数学

首先回答问题。令 K = BB(750)。其中 BB(n) 是忙海狸函数，即所有最终停机的 2 色 n 状态图灵机中运行步数的最大值。

根据忙海狸函数 BB(n) 的定义，我们显然地有 K 是一个有限大的自然数。而我们很容易证明，对于任意有限大的自然数 n， 0.333...3 (n 个 3) ＜ 0.333... (循环) = 1/3，于是 0.333...3 (K 个 3) ＜ 0.333... (循环) = 1/3 这个大小关系平凡地成立。

0. 首先限定一下讨论范围

涉及到实数，尤其是显式地讨论柯西列（无限小数）的情况，很难避免涉及到讨论二阶算术的细节，从而让问题变得复杂化。为了避免这些复杂的技术细节，我们不在 R 上讨论这个问题，从而本回答也基本不涉及问题中的 2、3 部分。后面我们会看到，涉及到 R 的部分的讨论对于这个问题来说并不是本质的。在本回答的第 4 部分，我们会非常简略地讨论一下 R 上的情形。

只在 Q 上讨论这个问题，则 0.333... (循环) 只是 1/3 的一种记法，此时它们实际指代的是同一个数学对象，从而不涉及任何“无穷逼近”之类只在 R 上有意义的语义，也就不用去考虑诸如它小数点后面到底是有标准自然数那么多位还是非标准自然数那么多位之类事实上无法在 ZFC 内部合法讨论的问题。而另一方面，0.333...3 (n 个 3) 是一个等比数列，用等比数列求和公式可以写出简单的表达式：

0.333...3 (n 个 3) = 3 * (10^(-1) + 10^(-2) + ... + 10^(-n)) = (1/3) * (1 - 10^(-n))

不难证明上式的求和对任意自然数 n 成立，结果一定是一个有理数且总是小于 1/3。这个结论在算术上是平凡的，整个过程都可以简单地在 ZFC 中完成。

重新收集一下我们的结果：

(1)：由忙海狸函数 BB(n) 的定义，我们显然地有 K = BB(750) 是一个有限大的自然数。

(2)：可以证明：「对任意自然数 n，0.333...3 (n 个 3) ＜ 1/3」。

联立 (1)：(2)，立即得到：0.333...3 (K 个 3) ＜ 1/3。

此时问题出现了：0.333...3 (K 个 3) 里的那个 K，也就是 BB(750)，这个东西它潜在地依赖于 ZFC 的一致性因而在 ZFC 中无法判定。题主的疑问自然就是——我们要如何判定一个在 ZFC 中无法判定的 K 的性质？

1. ZFC 能判定什么，不能判定什么

「BB(750) 在 ZFC 中无法判定」这个说法很常见，但细究起来是有问题的：它在一个很重要的地方进行了模糊处理，即「ZFC 无法判定的东西到底是什么」。

利用比如 Post's theorem，我们可以把图灵机的性质翻译成一阶逻辑语言从而在 ZFC 里面讨论。忙海狸函数也可以用这种方式在 ZFC 里面处理。即使我们忽略掉 ZFC 里有没有非标准自然数之类不能在 ZFC 内部讨论的部分，以下的命题也是 ZFC 中的定理：

(1')：有且仅有唯一的自然数 K，它满足【一个一阶语言的句子，这个句子在元语言中可以被解释为「K = BB(750)」】。

(1')：只不过是把上一节中用元语言描述的命题 (1)：翻译到 ZFC 上的版本。对于我们的讨论来说没有什么区别。为了避免啰嗦，后文中我们直接用【K = BB(750)】来替代“K 满足【一个一阶语言的句子，这个句子在元语言中可以被解释为「K = BB(750)」】”。注意：这里我们事实上并没有在讨论 ZFC 上的相等关系，当然也没有显式地构造出 BB(750) 具体的值。「K = BB(750)」是我们在元语言层面的解读，在 ZFC 内部，它应该被读作“K 满足某个特定的一阶语言句子”。

(1')：的具体证明在技术上比较复杂，不过重点主要在于如何为忙海狸函数选取一个合适的 ZFC 翻译，而这部分是纯粹机械的工作。一旦选定了合适的定义，证明满足条件的 ZFC 自然数一定唯一存在并没有什么实质性的困难。至于 (#2)，前面说过了，它只是一个平凡的算术上的结论，本身不需要什么特别的技术处理就可以在 ZFC 中被证明。由 (1')：+ (2)，ZFC：可以证明以下定理：

(3a)：有且仅有唯一的自然数 K，它满足【K = BB(750)】，且 0.333...3 (K 个 3) ＜ 1/3。

回到元语言中，我们显然可以合理地把上面的定理 (3a)：翻译为「ZFC 可以证明 0.333...3 (BB750 个 3) ＜ 0.333... (循环) = 1/3」。

其实到这里，问题应该已经很明确了：题主声称「如果一段程序告诉我们，0.33......3(BB750个3)＜0.33循环，说明这段程序求出了BB(750)的值」，这个说法显然是错误的。回顾一下本节的内容，实际上在 ZFC 中做证明的思路是“我们在 ZFC 中证明某个满足【某个特定的一阶语言句子】的自然数 K （唯一）存在，然后在元语言里把这个【特定的一阶语言句子】解释为「K = BB(750)」”。全过程里面事实上从未出现 BB(750) 的显式构造。从以上证明出发，除了判定一些在算术上平凡的性质（比如0.33......3(BB750个3)＜0.33循环）之外，对于求 BB(750) 的具体数值显然也没有任何帮助。

ZFC：是时候给愚蠢的直觉主义逻辑信奉者一点小小的排中律震撼了。

说白了，ZFC 用的又不是直觉主义逻辑，在 ZFC 里面做证明并不需要显式地给出具体构造。如果一个算术性质对所有自然数成立，那么它平凡地对 BB(750) 也同样成立，且这一点可以在 ZFC 内部得到证明（本质上是因为 (1') 是一个 ZFC 的内定理）。精妙地构造一个算术性质以使它看起来可以通过一个程序去构造性地判定，并不能强迫 ZFC 也同样用构造性的方法去判定它。

其实除了 K (【K = BB(750)】) 是一个自然数之外，ZFC 能判定的东西还要再稍微多一点点：比如说我们可以在 ZFC 里面证明 K ＞ 3, 3^3, G(64), etc. 换句话说，ZFC 可以证明 BB(750) 的一些下界。

另一方面，ZFC 不能证明 BB(750) 的任何上界。具体来说，对于元理论中每一个有限的自然数 D，以下的命题都不是 ZFC 中的定理（除非 ZFC 不一致）：

(4!)：有且仅有唯一的自然数 K，它满足【K = BB(750)】，且 D ＞ K。

上面的命题实际上就是蔡廷不完备性的一种形式。且我们立即可以得出这样的推论：对于元理论中每一个有限的自然数 D，【D = BB(750)】同样也都不是 ZFC 中的定理（除非 ZFC 不一致）。也即是说，就算可以通过某种特殊的方式获得 BB(750) 的真实值，我们也没法在 ZFC 里验证它。

重新收集一下我们的结果：

(a)ZFC 可以证明 BB(750) 是一个自然数：(1')：是 ZFC 的内定理。

(b)ZFC 可以判定 BB(750) 的一些平凡（比如对所有自然数成立）的算术性质。具体地，(3a)：是 ZFC 的内定理。

(c) 无论对 (a) 还是 (b)，ZFC 上的证明都是非构造性的。对 (a) 的证明并不能提供一个 BB(750) 的具体构造，同样，对 (b) 的证明也不蕴含题主想象中的那个“可以构造性地验证 BB(750) 到底等于多少”的程序。如果题主接受排中律，那么“非构造性的证明”应该不是什么难以想象的东西。而且你也不可能通过设计某种“看起来似乎应该可以被构造性地验证”的性质来强迫 ZFC 提供一个构造性的证明。

(d) 除了 (a) 和 (b) 之外，ZFC 还可以判定一些关于 BB(750) 的稍微不那么平凡的性质，例如 BB(750) 的一些稍微不那么平凡的下界。

(e) [除非 ZFC 不一致]BB(750) 的任何上界都不能在 ZFC 中被证明。特别地，借助神谕获得 BB(750) 的答案的人没有办法在 ZFC 中验证这个答案。

2. 神谕机

上一节中的 (e) 提到了神谕的概念。事实上，考虑到 BB(n) 是一个不可计算函数，在讨论它的一般性质的时候引入神谕是很容易想到的处理。此处我们直接假设题主拥有可以判定标准图灵机停机问题的神谕。这个神谕的构造也可以是非常简单粗暴的：比如给一台标准图灵机额外加装一卷记载了蔡廷常数精确值的纸带。

在上述神谕机的模型下，这个问题立刻就变得非常简单且直观：K = BB(750) 除了大到超越人智之外和任何其他有限大的自然数（比如TREE(750)）并没有什么本质区别。一旦真的把 K 具体写下来（比如说，展开成一个具体的有限长度的冯诺伊曼序数符号），在 ZFC 中证明用 K 构造出的有限小数小于 1/3 也没有什么难度。

(3b)：0.333...3 (K 个 3) ＜ 1/3，其中 K 是元语言中的某个特定自然数。〔在元语言中可以（依据神谕）见证 K = BB(750)〕

(3b)：显然也是 ZFC 的定理，此处的 K 是首先在元语言里面被钦定了一个固定的有限大的值，在 ZFC 中则应当被视为是一个被具体写下的自然数（有限冯诺依曼序数）符号。此时 (3b)：作为 ZFC 的定理成立是显然的。而 (3b)：后面六角括号里的内容仅仅是对那个 ZFC 中的具体的自然数符号在（包含神谕的）元语言层面的解读，对于限定在 ZFC 中的讨论来说实际是不存在的。在这个语境下，(3b)：也同样可以（从另一个方向上）被解释为「ZFC 可以证明 0.333...3 (BB750 个 3) ＜ 0.333... (循环) = 1/3」。

实际上 ZFC 真正不能见证的恰恰就是「 K = BB(750) 」这一步：（假设 ZFC 一致，）你没有办法写下一个在 ZFC 里面合法的证明来确认你依靠神谕机找到的那个 K 确实等于 BB(750)。

从上面的讨论中可以看出，(3a)：和 (3b)：说白了是从两个不同的方向进行旁敲侧击：(3a)：表明 ZFC 可以证明可以证明 ZFC 中【满足某个特定一阶语言句子】的自然数 K 一定唯一存在，并且那些对任意自然数都成立的性质（显然）也对 K 成立。至于这个 K 究竟等于多少（乃至于 K 在元语言里究竟是不是标准的），ZFC 是没法回答的。(3b)：说明那个在元语言里可以（通过神谕）被见证为 BB(750) 的「那个具体的自然数 K」，它在 ZFC 里也就是一个普通的自然数，从而那些对任意自然数都成立的性质（显然）也对 K 成立。至于只在元语言中才能见证的那个关系（「K = BB(750)」）在 ZFC 中是否成立，ZFC 当然也是没法回答的。

3. 世界线分歧 α：ZFC 是一致的吗？

前面所有的讨论都假设 ZFC 确实是一致的。根据忙海狸函数的定义我们很容易意识到，如果 ZFC 确实是一致的，那么那个用来枚举从 ZFC 的公理出发证明矛盾的 2 色 745 状态图灵机（不妨把它叫做「机器 A」）就永远不会停机，而永远不会停机的图灵机对忙海狸函数的函数值其实是没有贡献的。拥有神谕的题主大概率会发现 BB(750) 的函数值其实来自于某个增长率暴力到超越人智的快速增长函数（大数数学家狂喜），不仅不是什么不可捉摸的无穷大/非标准自然数，甚至跟那个「机器 A」压根就没什么关系。ZFC 的问题只不过是它没法证明某些图灵机（比如「机器 A」）不会停机，也无法判定那个最终生成了 BB(750) 函数值的图灵机所对应的增长率——这两个问题在大数数学领域都是稀松平常的事情，根本没有什么值得惊讶的。像 Laver Table 之类看起来人畜无害的玩意也一样可以搞出增长率（疑似）在 ZFC 里不可判定的函数。

最近（也就是今年，2024 年的事情）关于忙海狸函数的最新研究成果证明了 BB(5) = 47176870。其实 47176870 这个数字在 30 多年前（1989 年）就已经被算出来了。剩下的工作其实都是“怎么证明其他那些机器最终都不会停机”。某种意义上讲这也正是忙海狸函数“不可计算性”的一个体现：它的函数值事实上并不是被“算出来”的，而是被“证明出来”的。算出一个（在事后用上帝视角看来，或者说依靠“神谕”）正确的数字只对应于忙海狸函数复杂性中微不足道的部分，剩下更加不可名状的任务其实是「证明你的答案是对的」。这一条和上一节中的讨论也是一致的——忙海狸函数的函数值显而易见地是一个自然数（即 (1')：在 ZFC 中可证），除了可观测宇宙状态数太少写不下之类细枝末节的技术困难（笑）之外也没有什么根本性的阻碍阻止你在 ZFC 里面讨论「辣个（依据神谕）在数字上等于 BB(750) 的自然数」（展开成标准的冯诺伊曼序数符号的形式）。

如果题主能够意识到「47176870」这个数字并没有什么不可名状的魔力阻止我们（在任何算术系统中，无论它多么弱）去讨论「0.333...3 (BB5 个 3) ＜ 1/3」，那么「辣个（依据神谕）在数字上等于 BB(750) 的自然数」其实也一样。如果我们预先在元语言里把「BB(5)」展开成「47176870」，「0.333...3 (47176870 个 3) ＜ 1/3」就立即是一个显然的结论，与我们工作理论的强度无关。唯一的问题在于证明「BB(5) = 47176870」这件事本身并不平凡，而且如果选用的算术系统足够弱，这个结论有可能证明不出来。BB(750) 所面对的情况和 BB(5) 并没有真正本质的区别。如果我们预先在元语言里面把 BB(750) 展开成一个具体的自然数 K（当然，需要忽略掉可观测宇宙状态数太小写不下之类“细枝末节”的技术困难），「0.333...3 (K 个 3) ＜ 1/3」也同样是一个显然的结论，而且同样并不依赖于我们选取的工作理论的强度。只不过证明「K = BB(750)」确实是不平凡的：而且我们已经确认它超出了 ZFC 的能力范围。当然，即使如此，原则上也并不阻止我们在一个比 ZFC 更强的工作理论中尝试证明这个结论。在往 ZFC 中添加了合适的公理之后，我们可能可以得到一个足以判定 BB(750) 的一阶理论。

那如果 ZFC 其实是不一致的呢？

这是完全有可能发生的事情：事实上，公理化集合论这个事情本身就是因为我们发现朴素集合论是不一致的才被发展起来。更不消说，在大数数学领域常年充斥着各种不良定义的记号（其中有一些甚至是在已经明确证实不良定义的前提下仍被广泛使用），这其实就是在做“不一致的数学”。虽然经过长期数学实践的检验我们相信以 ZFC 为代表的公理化集合论是一致的，但这也完全有可能是我们搞错了。如果 ZFC 是不一致的，那么「机器 A」最终会停机，而且停机步数会依赖于从 ZFC 的公理出发证明矛盾的最短证明的长度。如果这个证明的长度非常长（我是说，「非常」长，你懂的），那么「机器 A」有可能会在忙海狸竞赛中取胜，从而决定 BB(750) 的具体值。

然而从另一个方面来说，考虑到我们在构造 ZFC 时，并没有试图去优化“证明矛盾的最短长度”这样一个目标。即使 ZFC 确实不一致，想要让从 ZFC 公理出发证明矛盾的最短证明恰好能长到足以赢得忙海狸竞赛，这个可能性其实也不见得就很高——更大的可能性是，如果 ZFC 确实不一致，那么见证矛盾的证明可以用不超过 10↑↑10 个符号写下来。在这种情况下，「机器 A」的停机步数会和真正的忙海狸冠军相差甚远。此时「ZFC 的一致性」和 BB(750) 之间的关系只能说是有一点，但不多。

由本节中的讨论，我们事实上可以得出这样的观察：「BB(750) 在 ZFC 中不可判定」这句话，其实它更多地是在陈述某种 ZFC 的性质，而不是在陈述有关 BB(750) （作为一个自然数）的性质。如果 ZFC 事实上是一致的，则「BB(750) 在 ZFC 中不可判定」这个命题（以及与之相关的那个「机器 A」）事实上和 BB(750) 作为一个自然数的具体值（以及相关的数论性质）完全无关——因为「机器 A」事实上并不会停机，因此根据定义，它对 BB(750) 的值从一开始就没有任何贡献。实际上 BB(750) 的函数值来自于其他（和 Con(ZFC) 完全无关的）计算过程。如果 ZFC 事实上不一致，BB(750) 也有很大的可能性并不和「机器 A」直接相关——这需要 ZFC 中最短的见证矛盾的证明的长度超过各种不可名状的大数才会发生。

而无论 ZFC 是否一致，我们都有足够的理由接受「0.333...3 (BB750 个 3) ＜ 1/3」为真：除非涉及无穷的数学并不真正存在（i.e., 事实上不存在一个「拥有合理强度的一致的一阶理论」可以作为我们的工作理论），或者我们拒绝经典逻辑（i.e., 禁止排中律，这会导致无法在不给出具体构造的前提下证明 BB(750) 是一个自然数），否则 (1‘)：和 (2)：总是成立（i.e., 总是可以找到合理的一致的工作理论使得它们是理论中的内定理），从而 (3a)：也总是（能够找到合理的一致的工作理论使其）成立。另一方面，除非忙海狸函数本身不良定义或者有穷数学本身不一致，否则 (3b)：必然始终成立（且不依赖于具体工作理论的选取）。因此，除非我们目前所工作的数学体系存在着一些根本（我是说，比 Con(ZFC) 可能不成立要更加根本）的问题，否则我们总是可以接受「0.333...3 (BB750 个 3) ＜ 1/3」为真，且这一点（在很大程度上）并不依赖 ZFC 或者某个特定的工作理论，也并不特别需要对「ZFC 到底是不是一致的」进行预设。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。