背景
我们都记得幼儿园时学到的哥德尔第一不完备性定理。这是一个给定形式系统F，构造一个句子G(F)，它是数学编码的 “这个句子在F中不可证明”。 如果F证明了G(F)，那么F既证明了F证明G(F)也证明了F不证明G(F)，所以F是不一致的（因此也是不可靠的）。同时，如果F证明了Not(G(F))，那么它“相信”有一个G(F)的证明。因此要么那个证明存在（在这种情况下根据前面的论点它会使F不一致），要么它不存在（在这种情况下F是不可靠的）。结论是，假设F足够强大以表达像G(F)这样的句子，它不能既是可靠的又是完备的（即它不能证明所有且仅是真实的算术陈述）。
好吧，但大多数人喜欢陈述哥德尔定理的方式比这更强：没有一个足够强大的形式系统F能既完备又一致。请注意，可靠性意味着一致性，但反之则不成立。（如果我相信月球上有一个巨大的紫色妖怪，那么大概我的信念是不可靠的，但它可能与我关于妖怪的各种其他信念完全一致。）
不幸的是，哥德尔的原始证明和计算机科学家最喜欢的替代证明实际上并没有给你关于完备性和一致性的更强陈述。当我在本科可计算性和复杂性课程中教授哥德尔时，这一直是个持久的问题。
哥德尔论证中的问题在哪里？它在于F证明Not(G(F))（即G(F)是可证明的），尽管实际上G(F)是真实的（即G(F)不可证明）。在这种情况下，F显然是不可靠的，但它可能不包含任何矛盾——基本上因为无论你看多长时间，你永远无法排除F（错误）相信G(F)是可证明的。实际上，F会是我喜欢称之为自我憎恨理论的东西：一种理论，比如F+Not(Con(F))，悲观地相信自己的不一致性，尽管事实上它是完全一致的。（相比之下，如果F傲慢地相信自己的一致性，那么根据第二不完备性定理，它不能是一致的！这里有某种教训……）
哥德尔自己解决这个问题的方法是引入一个称为ω-一致性的新概念，它介于一致性和可靠性之间。他然后展示了F不能既完备又ω-一致。（为什么哥德尔不直接谈论可靠性？因为与一致性或ω-一致性不同，可靠性是一个“元理论”概念，在F中无法形式化。因此，如果他使用了可靠性，那么第一不完备性定理甚至不能在F本身中陈述，更不用说证明了，这反过来会为他的第二不完备性定理的证明带来问题。）
无论如何，从本科课程的角度来看，担心的是，一旦你开始谈论“ω-一致性”，所有哥德尔的浪漫和自我参照魔法都会在技术细节的泥潭中消失。
所以我们肯定可以在这里点上i（或者更确切地说，在ö上加上变音符号），并证明更强、更干净的陈述，即F不能既完备又一致？
是的，我们可以——但要做到这一点，我们需要罗瑟定理：这是1936年对哥德尔定理的一种加强，在普通极客中远没有得到应有的广泛认识。在罗瑟的证明中，我们用一个新句子R(F)代替G(F)，它是以下内容的数学编码： “对于在F中的每个这个句子的证明，都有一个更短的反驳。”
如果F证明了R(F)，那么它也证明了存在一个比我们刚刚假设存在的R(F)证明更短的R(F)反驳。因此我们可以寻找那个反驳（因为只有有限多字符串需要检查），要么我们会找到它，要么不会——但无论哪种情况，我们都会揭示F是不一致的。同时，如果F证明了Not(R(F))，那么它证明了存在一个没有更短反驳的R(F)证明。所以特别地，它证明了存在一个不比我们刚刚假设存在的Not(R(F))证明更长的R(F)证明。但再一次，我们可以寻找那个证明（只有有限多字符串需要检查），要么我们会找到它，要么不会，无论哪种情况，F都会被揭示为不一致。
请注意罗瑟句子实现了什么：它在R(F)可证明和R(F)可反驳的情况之间创建了一种对称性，纠正了哥德尔原始论证中两种情况之间的不对称。
好吧，那么为什么我不在本科课程中教授罗瑟定理，而是教哥德尔定理呢？
我会告诉你为什么：因为当我向计算机科学家教授哥德尔时，我喜欢绕过如何形式化“在F中可证明性”概念的讨厌细节。（从现代计算机科学的角度来看，哥德尔编号是一种令人作呕的丑陋黑客！）
相反，我只是将哥德尔定理视为其概念上优先（尽管历史上稍后的）堂兄：图灵关于停机问题不可解性的定理的一个微不足道的推论。
对于那些从未见过这两个人类思想胜利之间联系的人来说：假设我们有一个既可靠又完备（且递归公理化，等等）的形式系统F，它足够强大以推理图灵机。然后我声称，使用这样的F，我们可以轻松解决停机问题。因为假设我们得到一个图灵机M，我们想知道它是否在空白磁带上停机。然后我们只需枚举F中的所有可能证明，直到我们找到M停机或M永远运行的证明。因为F是完备的，我们最终会找到一个或另一个，因为F是可靠的，证明的结论是真实的。因此我们会决定M是否停机。但由于我们已经知道（感谢图灵先生）停机问题是不可判定的，我们得出结论，F不可能存在。
“看妈，没有哥德尔编号！”
新发现
上述讨论引出了一个明显的问题： 是否也有一种仅使用图灵机的方法来证明罗瑟定理——类似于我们刚刚给出的“原始”不完备性定理的计算机科学家友好的证明？
我最初担心答案是否定的。因为罗瑟句子不仅比哥德尔句子更复杂，而且它本质上依赖于证明的排序——而在图灵机世界中，这样的排序对应什么并不清楚。
为什么这让我担心？因为这威胁到我的信念，即计算机程序“真的”是哥德尔定理的核心，无论任何传统主义哲学家或逻辑学家声称相反。如果即使是从哥德尔到罗瑟这一适度步骤也需要放弃可计算性视角，那么我对万能图灵机的信仰将受到动摇。
但不要害怕！几个月前，我发现了一种简短、简单、基于图灵机的方法来证明罗瑟定理。虽然这似乎太小了，不值得写成论文，但我以前从未见过它（请告诉我如果你有！），所以我想在这里分享一下。（更新：Makoto Kanazawa指出Kleene 1967年教科书中有一个基本类似的论证。所以，你可以把接下来的内容看作是Kleene的一种“普及版”。）
第一步是定义以下变体停机问题：
一致猜测问题
给定图灵机M的描述作为输入：
- 如果M在空白磁带上接受，则接受。
- 如果M在空白磁带上拒绝，则拒绝。
- 如果M在空白磁带上永远运行，则接受或拒绝，但无论如何都要停机！
通过修改（可以说甚至简化）图灵对停机问题的原始论证，很容易显示没有图灵机可以解决一致猜测问题。事实上，我把一致猜测问题不可解性放在上学期期中考试中，至少一半学生解决了。（该死！看来不能再用了。）
看出来了吗？没有？好吧，让P成为解决一致猜测问题的图灵机。那么我们可以轻松修改P生成一个新图灵机Q，它给定另一个图灵机M的描述⟨M⟩作为输入：
- 如果M(⟨M⟩)接受，则拒绝。
- 如果M(⟨M⟩)拒绝，则接受。
- 如果M(⟨M⟩)永远运行，则停机（接受或拒绝）。
现在在其自身描述⟨Q⟩上运行Q。如果Q(⟨Q⟩)接受，那么它拒绝；如果Q(⟨Q⟩)拒绝，那么它接受。因此唯一剩下的选项是Q(⟨Q⟩)永远运行，违反了第三个条件。
从一致猜测问题不可解性出发，我声称罗瑟定理随之而来。因为假设我们有一个既完备又一致（但不一定可靠！）且足够强大以谈论图灵机的形式系统F。那么使用F，我们可以解决一致猜测问题，如下所示。给定图灵机描述⟨M⟩作为输入，开始枚举关于“M在空白磁带上接受”的所有可能证明和反驳。一旦找到一个证明就接受，一旦找到一个反驳就拒绝。
因为F是完备的，你必须最终找到一个证明或反驳（因此停机，无论接受还是拒绝）。此外，因为F是一致的，如果M真的拒绝，那么F不能证明M接受，而如果M真的接受，那么F不能证明M不接受（因为无论哪种情况，都可以在有限时间内发现矛盾）。所以如果M接受你会接受，如果M拒绝你会拒绝。但这意味着你正在解决一致猜测问题！既然我们已经显示没有图灵机可以解决一致猜测问题，我们得出结论，F不可能存在。
QED：宇宙道德秩序恢复了，图灵机在人类思想基础上的崇高地位得到了重申。
（顺便说一句，你可能想知道哥德尔第二不完备性定理，即一致F不可能证明其自身的一致性，也能否以图灵机为中心的方法来证明。为了回答你的问题，答案是肯定的——更好的是，它甚至涉及Kolmogorov复杂度！参见例如Shira Kritchman和Ran Raz最近这篇漂亮论文。）
那么，哥德尔定理是否总会并且永远作为可计算性理论的重要部分被教授，而哥德尔编号会得到应得的退休？我看不出为什么不应该发生这种情况——但遗憾的是，我预测的一致性不足以暗示其元理论真相。
这篇文章发布在 Nerd Interest 分类下。