数学 (6-2)

(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 不一致）：

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。