\begingroup

根据哥德尔不完备定理，不可能证明 ZFC 在 ZFC 内的一致性（如果它是一致的）。

众所周知，Busy Beaver 函数是不可计算的，并且执行（称之为 TM）BB(8000) 步可以证明 ZFC 是一致的。

在我看来，人们可以在 ZFC 中制定如下声明：

TM 状态 (BB(8000)) ≠停止

这个论点的谬误是什么？

很容易想象，许多多达 8000 个图灵机的非终止性证明都是 Collat​​z 式的，并且很难证明；而且绝对明显的是，没有凡人能够验证这样的假设。

但是，似乎可以在 ZFC 中陈述，并且计算TM 的状态 (BB(8000)) 只需要“仅仅”有限规则的有限枚举，这在理论上应该是可以接受的。或者，这个陈述在 ZFC 中是可以接受的，但“给定TM 的状态 (BB(8000)) ≠停机，ZFC 是一致的”这个蕴涵陈述在 ZFC 中是无法表达的？

\endgroup


最佳答案
1

\begingroup

这里的符号可能太紧凑了，所以很难看清发生了什么。BB （8000 ）​乙乙（8000）BB(8000)根据定义，是停止的最大步数800080008000-状态图灵机在停止前运行。这意味着如果你根据以下定义扩展这个陈述BB （8000 ）​乙乙（8000）BB(8000)，这涉及到在一组图灵机上写下量化，其中包括图灵机电视米电视米TM这个问题中，这个陈述直接等同于

TM 永远运行

这又相当于保守党​​FC）反对意见（是FC）\text{Con}(ZFC)。所以，到目前为止，这并不是什么大秘密：ZFC 当然有能力说明这一点。微妙之处就在这里：

而计算 TM (BB(8000)) 的状态“仅仅”需要有限规则的有限枚举

此时我们需要小心区分“BB （8000 ）​乙乙（8000）BB(8000)“。我相信你在这里想要的论点是：无论BB （8000 ）​乙乙（8000）BB(8000)是，它只是一些正整数nnn，并且对于任何正整数nnn，TM 在步骤的真实状态nnn是有限计算的结果，无论它有多大，ZFC 都应该不仅能够陈述，而且能够证明。

这是正确的。然而，这并不意味着ZFC 可以证明保守党​​FC）反对意见（是FC）\text{Con}(ZFC)这样，因为如果你替换“BB （8000 ）​乙乙（8000）BB(8000)“（我将其解释为对800080008000状态图灵机）具有真实值nnn的BB （8000 ）​乙乙（8000）BB(8000)，ZFC 无法证明这一点nnn真正的价值是BB （8000 ）​乙乙（8000）BB(8000)，这意味着 ZFC 无法证明电视米（名词）电视米（n）TM(n)有什么关系保守党​​FC）反对意见（是FC）\text{Con}(ZFC)！

所以这是相当微妙的。正如我在之前关于这个结果的问题中提到的那样人们必须仔细区分数字和数字描述，以避免在这里陷入完全混乱。

\endgroup

2

  • \begingroup
    在我的问题中，我本意是将“BB(8000)”表示为整数值，而不是语句。那么我是否可以将您的答案理解为“给定 TM 的状态 (BB(8000)) ≠ 停机，ZFC 是一致的”这一含义无法在 ZFC 中表达，因为 ZFC 可以表达“TM 的状态 (<BB(8000) 的值>)”和“TM 的状态 (<BB(8000) 的值>) ≠ 停机”，但不能表达“BB(8000) = <BB(8000) 的值>”？
    \endgroup


    – 


  • 1
    \begingroup
    @user22476690：它可以用 ZFC 表达，但 ZFC 无法证明它。是的，这就是我的意思，如果你再次说“表达”是指“证明”。
    \endgroup


    –