beanandbean的回答
作为科普向的节目，毕导视频的节奏和流程都一向很好；不过可惜的是，哥德尔不完备性作为一个抽象性很强的数学话题，视频中对于不少细节的讨论都有所模糊/欠缺，这就使得整个论证虽然“看上去有点道理”，但是关于其中的实际步骤确实能让人挑出一些错漏或者得不到解答的疑问来。可以看到，本问题下已有的其他回答中，其实也是对视频内容提出疑惑的居多。因此，我们在这个回答里试图对毕导视频中的关于具体数学细节不妥之处做一个修订和补充，也希望能够同时解决一些其他回答中提出的问题。
1. 命题、代换与变量哥德尔数的确定性
首先，关于 
这个数的构造的基石是命题和将其中变元代换为值的过程。然而，在毕导的视频中对于“命题”的概念使用的过于宽泛，甚至涵盖了如 
〈11:18〉这种包含自由变元的形式；同时，对于变元的概念与地位又没有足够的强调，乃至于出现了 
中“ 
是一个未知的大数”〈17:32〉这样的说法，这会在不经意间传递出“无法证明哥德尔数是 的命题”是一个尚为完成的构造、我们会在未来某时指定 为某一个大数之类的想法，成为许多困惑的源泉。毕导的视频发布后，我们在知乎能看到这样一个回答：
如果有一台真理机器只能回答是或不是，能对人类社会作多大贡献？
这就是错误地认为了求出 这个数本身是一件很复杂乃至数学上不可能的任务，但实际上，“无法证明哥德尔数是 的命题”就是一个可以直接用公式语言写出的确定式子，从中求得哥德尔数 
乃至 是一个小学二年级的学生就可以通过重复的四则运算完成的事情。
那么，让我们回到开头，毕导所使用的看似非常符合直觉的“命题”概念到底出现了什么偏差呢？在严格的形式语言中，我们会将用给定的符号组合出的有意义序列划为“公式”和“命题”两类：“命题”指的是（在一个数学结构中）能够明确判定对错的式子，比如 
， 
，“对于任意自然数 
都有 
”等等；而“公式”除了包含命题，还额外允许命题中出现自由变元，也就是前面没有加“对于任意”或者“存在某个”这两种量词限定的变量字母。举例来说， 
就是一个公式，在严格的形式语言中，我们不能直接说它是正确的，而要说它“对于 的任意自然数赋值”都是正确的。这是因为一个类似的式子，比如 
，就可能对于某些赋值是正确的，而对于其他的赋值又是错误的；将它们划到命题的范畴以外，就可以让我们依然能安全地断言：任何一个命题要么是正确的，要么是错误的（而对表达式不能这么说）。
在这样的定义下，我们可以看到，不管是命题还是公式都可以按照毕导视频中介绍的规则被赋予一个哥德尔数，而“无法证明哥德尔数是 的命题”作为一个公式，它其中出现的 并不是什么尚待确定的大数，而就是硬生生被包含在式中的 这个字母。比起说 是某个命题/公式的哥德尔数，更接近严格论述的想法是把它看作一个由单个自变量 的函数，如果我们任取一个公式 
，求出它的哥德尔数 作为输入放进函数，这个函数就会还原出原本的表达式 ，然后把其中但凡（自由地）出现哥德尔数为 
的符号（也就是 这个字母）的地方都替换为 这个常量对应的符号，最后求出新公式的哥德尔数进行输出。
那么上面，在公式“无法证明哥德尔数是 的命题”中这个函数的出现方式我们可以类比于一个更简单的公式“ 
”：你不能说 
本身是一个数——它并没有确定任意给定的数值，而只是一个关于自变量 的函数，但是我们却可以将 理解为在赋值后变成“将赋给变元 的值平方后等于 
”这样一个命题的公式。同样地，公式“无法证明哥德尔数是 的命题”中的 并不指代着某一个确定的哥德尔数，但是我们计算出这个公式的哥德尔数 （回忆起我们刚才说过的：即使不是命题，仍然含有未被赋值的自由变元，依然可以求出确定的哥德尔数）后，再将 赋值给 ，就可以通过函数计算求出 这个（对应某个公式的）确定的数。更好的是，因为 作为一个哥德尔数，它对应的公式里面只有一个自由变元，也就是字母 ，于是执行了 
函数的代换规则后，得到的新公式中不再剩下任何的自由变元了——换句话说，我们发现 确实是一个命题的哥德尔数，也就可以开始判断其正确与否了。
2. sub(a, b, c) 是什么？
当然，上一节用 和 进行类比的方法可能听起来仍然有点抽象。毕竟，我们都能看到 可以用四则运算写成 
，但是哥德尔数的构造里可没有提过怎么计算其他某个任意函数的哥德尔数，而毕导的视频中也完全没有解释这部分内容——这确实情有可原，因为这确实是证明中比较繁琐的步骤。
简单来说，在形式逻辑系统中的习惯是通过类似隐函数的方式来使用函数。对于一个函数 
，我们想要找到一个包含这两个自由变元 
的公式 
，从而在每一次想要将 
这个式子作为计算结果来使用时——比如我们想说“ 有性质 
”——我们就改成说“存在某个数学对象 ，它满足 ，且有性质 ”，这就将这个式子改写成了可以用哥德尔数能够表示的逻辑符号写出的状态。当然，和隐函数带来的问题一样，对于每一个想要这样使用的公式 ，我们都要先证明它确实是一个函数，也就是说，对于任意的 ，都有且只有一个 能够满足 。不过这一步只需要在定义函数时一次性完成，之后再使用这个函数的时候都不必再有烦恼，因此之后就不做赘述了。
于是，在一个严格的哥德尔不完备性定理的证明中我们需要面对的任务就是把 
的函数写成类似隐函数的定义公式，且其中只用哥德尔数能够表示的四则运算和量词技巧。在此，我们对这个过程仅做一概述：如毕导视频中所说的，通过可除性判断我们可以对一个哥德尔数所表示的符号串中的内容进行判定〈14:04〉，于是这个代换过程只需要检查输入 
所表示的符号串中的每一位，如果第 
位上符号的哥德尔数（也就是 的质因子分解中第 个质数的幂次）不等于 
（或者我们已经处在某个“量词+ ”的前缀所作用的子公式范围之内，从而 所表示的变量不再是自由变元），那么只需要将这一位原样放进输出 
中即可；反之，第 位上符号的哥德尔数恰好就是 ，那么我们就在输出 的对应位置连续插入 
个符号 
以及一个 （所对应的哥德尔数），从而表示出 这个常量。关于这个过程的细节，还涉及如何使用有限元组表达函数递归的计算等等，如果要详细介绍可能另外制作一个半小时的视频也讲不完，但作为科普目的，我们只需要明确，通过反复地使用类似哥德尔数的编码方式来表示“一些元素排成的有限序列”，我们可以把任何类似一个计算机程序的方式写出的机械计算过程利用算术语言和量词表示成所需的隐函数形式。
这其中，要避免替换在量词作用范围内出现的变量字母是一件尤其复杂的事情。为了“公式”这个概念的定义的简便性，我们在形式逻辑系统中一般允许自由和受限变元重名，比如说“ 
都有 
显然在行为上是不同的变量：前者可以通过赋值指定一个确认的值，而后者总是会遍历论域中的所有数学对象；对应地，我们再进行形如 
的变量代换时，就会希望只将前一个 替换为常量 ，而不影响后一个不能被赋值的 。在现在许多关于哥德尔不完备性的讨论中，我们一般会采用一种偷懒的办法：与其让函数 
对哥德尔数 所对应公式中出现的变量字母一一进行辨认和修改，我们直接在 对应的公式前方加上“存在某个 
使得 
且”的前缀，其中 为哥德尔数为 的符号，然后输出带有前缀的新公式的哥德尔数即可。很容易验证，可以证明这种方法所得到的新公式和之前实际进行代换得到的公式是等价的。
不过，这两种方法的区别仅仅在于最终找到的用来表示函数 的具体公式上的区别。回到哥德尔不完备性定理的证明上，我们都是要将“无法证明哥德尔数是 的命题”这个公式按照前面所述的思路形式化成“存在某个 
满足 
且不存在任意 
使得 是一段证明的哥德尔数，而 是这段证明的结论的哥德尔数”，其中 处填入的是一段很复杂的、包含 和 这两个字母的公式。于是，我们就可以按照标准的计算规则求得这整个公式的哥德尔数 ，以及将上述公式中出现的字母 都替换为常量 得到的命题及其对应的哥德尔数 ——如我们强调了很多遍的，这些都会是只要遵循哥德尔数的定义就可以进行的完全机械的计算。
这一节的最后，我们提到在其他的回答中，有人困惑于“无法证明哥德尔数是 的命题”这个命题是怎么拥有在其表达中出现的哥德尔数 的：按照哥德尔数的计算规则，包含常量 
的公式的哥德尔数总是应该大于 ，所以看上去自指现象是不可能发生的。从本回答第1、2节的内容出发，我们能够做出的回答是：在这个命题中出现的 并不是作为常量而是作为函数表达式出现的（注意到，我们的出发点是“无法证明哥德尔数是 的命题”，而这个公式中 仍然是变量而非某个代入的实际数字，因此我们也不可能把 直接作为一个数字写进公式，这一点直接继承到了将 变换为 得到的结果中），而一个表达式显然能比其求出的值简单很多：举一个极端一点的例子，用来计算葛立恒数的函数 
只要用篇幅不长的一段描述就可以定义，我们估算这段描述的哥德尔数也不会超过最开始的几百、上千个质数（对应于其定义形式化后的符号串长度）各自取两位数次幂之后的乘积：这远小于葛立恒数 
的值，但是却可以让一个公式中出现葛立恒数这个常量。在这里，我们也是利用相似的结构实现了自指：在哥德尔数为 的命题中记录了一个常量 和一些计算规则，而将这些计算规则应用到常量 上会求得一个很大的数——恰好是这个命题自己的哥德尔数 。
3. 证明、前提与形式系统
比起公式和其中变量字母的地位，在毕导的视频中同样没有得到足够的重视、而且我们可以说是哥德尔不完备性定理的证明中更重要的一个组件是证明的前提。在毕导的证明过程中，他用来求出对应的哥德尔数 的关键公式被写作了“无法证明哥德尔数是 的命题”〈17:16〉；但是，如果你去查询绝大多数数学专业的、讲解哥德尔不完备性和相关问题的教材，其中这个公式都应该被写作“在皮亚诺算术中无法证明哥德尔数是 的命题”（或者类似的形式）。这就是整个视频中可能最为让人困惑的一点的来源：在这之后对于哥德尔第一不完备性定理的证明中，我们确实说明了哥德尔数为 的命题为真〈20:59〉，这难道不是证明了哥德尔数为 的命题吗？填补这个漏洞的答案就是：是的，我们确实证明了哥德尔数为 的命题，但是我们不是在皮亚诺算术中证明的。
在形式化的数理逻辑中，一个证明的出发点是有限多个前提公式（这是因为绝大多数的形式系统中证明本身必须是有限长度的），而判断一些公式是否组合成一个正确的证明的过程——也是我们关心的这个关键命题的重要组成部分——其中的一个核心步骤就是检查证明中的前提公式是否都在给定的公理集合中。而哥德尔第一不完备性定理中“为真但不可证”的说法，精确来说是在给定了一个公理集合，比如皮亚诺算术之后，我们构造出的这个新命题在原本的公理集合中不能够证明，但是如果我们在公理集合之外选择一些额外的假设，那我们还是能够证明这个新命题的。更进一步地，因为需要与前面在原本的公理中不可证明的结果自洽，所以我们自然也就知道了，新假设的这些性质在原本的公理体系中同样不能被证明。
那么，哥德尔数为 的命题为真的这个证明中，具体是哪个步骤使用了皮亚诺算术以外的假设呢？其实问题的所在，恰恰是“‘哥德尔数是 的命题’都可以证明了，那它当然是一个真命题”〈20:13〉这句乍一听非常符合直觉的断言。抽象来说，这个性质可以被写作“若存在某个 为形式系统 
中命题 的证明的哥德尔数，则命题 成立”，其中 是某个固定的命题而非一个表示哥德尔数的变元（这么做的原因详见第5节），我们一般将其称为形式系统 的可靠性（soundness）。很不幸的是，和一致性类似地，一个包含皮亚诺算术的一致系统也同样不能够证明自己的可靠性：精确来说，若 是一个包含皮亚诺算术的系统，假设 是一致的，那么一定能够找到一个命题 ，使得 不能证明“若存在某个 为形式系统 中命题 的证明的哥德尔数，则命题 成立”。如我们上一段所说的，要验证这一点，只需要取命题 为与哥德尔不完备性定理中同样的哥德尔数为 的命题，并且假设 可以证明其关于命题 的证明的可靠性，那么毕导视频中对于命题 的证明就真的成了前提 下的证明。通过哥德尔数将这个证明进行编码，我们一方面可以得到 证明了“存在某个数是形式系统 中命题 的证明的哥德尔数”，另一方面刚刚在前提 下证明的命题 又本身表示了“不存在某个数是形式系统 中命题 的证明的哥德尔数”，因此我们从 推出了矛盾，违背了 的一致性。
另外一方面，更符合直觉的看法可能是从模型论出发：在数理逻辑中，皮亚诺算术这样的形式系统被统一归类为一阶逻辑系统，而关于一阶逻辑有非常著名的勒文海姆–斯科伦定理：任何有无限模型的一阶形式系统均有论域为任意基数的无限模型。在皮亚诺算术中，这就是说可能存在包含自然数以及其他的一些数学对象的更大数学结构，其上也可以定义四则运算并满足皮亚诺算术的全部公理。现在，我们如果考虑某个性质 的一个实际证明，那么这个证明的哥德尔数按照计算规则求出来一定会是一个自然数；但是勒文海姆–斯科伦定理也保证了在那些包含额外对象的更大模型里，我们也可以找到一个不是自然数的对象，使得它满足我们使用一阶逻辑写出的“ 是某个证明的哥德尔数”的条件。换句话说，我们可能找到一个数学结构满足全部的皮亚诺公理，也满足“存在一个数是命题 的证明的哥德尔数”这个一阶命题，但是因为这个所谓的“哥德尔数”实际上不是自然数而没法真正找到与之对应的命题 的证明。这就是导致皮亚诺算术不能够推出一个证明的可靠性的异常情况。
因此，回过头来，毕导视频中说哥德尔数为 的命题为真但是不可证，其实精确来说是它在皮亚诺算术中不可证，但是在皮亚诺算术加上“皮亚诺算术可靠”的前提下是可证的。在现实中，我们愿意相信全体自然数构成的标准模型是皮亚诺算术的一个模型，这一承诺同时也保证了皮亚诺算术是一致的、皮亚诺算术是可靠的、皮亚诺算术加上“皮亚诺算术一致”的假设是一致的、皮亚诺算术加上“皮亚诺算术可靠”的假设是可靠的等等无限套娃下去的结论。因此，说皮亚诺算术加上“皮亚诺算术可靠”的前提下推出的一项结论为真没有任何的问题，但应该加以强调的是此处正确与否的推理中允许运用的上述各种套娃结论都不是皮亚诺算术这个系统本身的推论，与我们在哥德尔数中编码的、只允许使用皮亚诺算术中的公理作为前提的证明万万不可混为一谈。
4. 第一定理的正确前提
说到这里，如果你仔细观看了毕导的完整视频，又阅读了前一节的详细内容，一定会发现一个明显的偏差：据视频中的说法，哥德尔第一不完备性定理使用的额外前提是一致性〈23:02〉，但是我们在上一节中指出的是，这个证明实际使用了可靠性的前提。这一节中将展开解释，此处视频中的说法是不正确的，这也是我个人认为毕导的此部视频中存在的最大问题——如果说前面提出的几点尚属于在定义和证明细节上的遗漏，那么毕导对于第一定理证明的总结和这一总结在第二定理中的运用可以直接就认定是错误的，换句话说，该视频中根本就没有成功地给出第二定理的证明。
毕导的视频中，关于第一定理的证明依赖一致性这一点，可以追溯到其证明最后“如果你承认数学是一致的，那就不能有矛盾，故原假设不成立”〈20:53〉并由此推出哥德尔数为 的命题为真的一步。关于这一步的处理，有两个非常不专业的地方：首先，如我们在上一节中所说的，在这个证明的前序步骤中已经使用了“皮亚诺算术是可靠的”的假设，也就是说，我们讨论这几个“关于命题的命题”的前提语境早就已经从皮亚诺算术本身移到了皮亚诺算术加上“皮亚诺算术是可靠的”的情境中，如果硬要说和一致性有什么关系，也不应该是和皮亚诺算术的一致性产生关系。另一方面，这个证明中，我们所作的事情大致是假设某个命题 为假，然后从此出发推出了命题 为真，从而希望从这个过程得到 一定为真的结论：这个过程叫做排中律，我们只需要知道命题 要么为真要么为假，那么既然从两种情况中都可以推出 为真（其中前者是显然的），那么 当然必须为真。
事实上，在数理逻辑中，一个命题确实（证明）为真和不能（证明）为假相比，前者往往是比后者容易推导许多的结论，这里我们想要得出的是前者，但实际需要一致性的是后者。直观地来看，一致性所说的是某个系统不能推出矛盾，但是矛盾对于我们想要推导出一个命题来说不仅没有损害还有帮助：如毕导视频中就介绍过的，爆炸原理保证了从矛盾中可以推出任何结论〈4:45〉，因此一个系统如果推出了矛盾，那么当然就能够推出我们想要证明的命题，于是不管有没有一致性，我们都只要处理推不出矛盾的这一种情况就可以了。
所以说，毕导视频中对哥德尔第一不完备性定理的证明，实际上证明的是“假设皮亚诺算术是可靠的，那么可以推出哥德尔数为 的命题为真但不能在皮亚诺算术中证明”。如前一节中所说的，我们默认接受的“自然数是皮亚诺算术的一个模型”，也附带保证了皮亚诺算术的可靠性，因此如果以找到一个真但是不可证明的命题这一目标来看的话，视频中的过程姑且是正确的，同时，我们也额外知道了皮亚诺算术不能证明其中关于哥德尔数为 的命题的证明的可靠性。但是，要想用这个证明来直接验证哥德尔第二不完备性定理，也就是皮亚诺系统的一致性的不可证性，将会是完全不可能的，因为这个证明中根本就没有用到皮亚诺算术的一致性。
当然，视频中关于第二定理的证明思路依然是完全合理的，只不过要想沿着这一路线取得成果，我们需要实实在在地用皮亚诺算术的一致性而非可靠性作为前提证明第一定理。这当然是可行的，只是要比视频中采用的证明稍微复杂一点点：
我们还是从哥德尔数为
的命题为假出发，于是其反面为真，也就是（在皮亚诺算术中）可以证明哥德尔数为
我们将这个证明的哥德尔数写作
注意到，哥德尔数为
将前面两点结合起来，我们发现（在皮亚诺算术中）可以证明哥德尔数为
但是，我们假设了皮亚诺算术是一致的，也就是皮亚诺算术不能证明矛盾。因此，反证法告诉我们，前提是错的，哥德尔数为
仔细观察可以确认，这个新证明中确实没有用到形式系统的可靠性，反而显式的用到了系统的一致性。因此，这确实是我们可以用来完成第二定理的推导过程：假如皮亚诺算术是一致的，且证明了自己的一致性，则它就可以遵循上面的过程证明哥德尔数为 的命题，从而再次导出矛盾，违背一致性。因此，如果皮亚诺算术（或者任何一个包含皮亚诺算术的形式系统）是一致的，它就不能证明自己的一致性。
作为这一节的结尾，我们试图说明可靠性确实是比一致性更强的结论——如果不然，比如说假如这两个性质互相等价，那么我们此前做出的区分就都没有什么意义了，而毕导视频中使用可靠性来证明第一定理的过程还是可以用来说明算术系统一致性的不可证性。但可惜的是，这两者并不等价。首先，我们可以注意到一致性公理本身就是可靠性公理的一个实例：我们考虑对于一个矛盾命题的可靠性断言，它说的是“如果形式系统 中有矛盾命题的一个证明，那么矛盾命题成立”——通过排中律，这句话就等价于“如果形式系统 中没有矛盾命题的证明”，也就是形式系统 是一致的。但是反过来，即使假设了系统的一致性，我们依然不能推出其中的证明都是可靠的：精确来说，我们将证明，如果 是一个包含了皮亚诺算术的形式系统，假设 是可靠的，那么能够找到一个命题 ，使得即使假设了 以及“ 是一致的”的前提，依然不能证明“ 中存在一个 的证明”可以推出 成立。
首先，我们可以等价地将前提“ 是一致的”化为要证明的内容的条件，也就是要说明从前提 不能推出“若 是一致的且存在一个 的证明，则 成立”。现在，有趣的事情开始了：我们考虑公式“ 不一致或者其中不存在哥德尔数为 的命题的证明”，将其哥德尔数记作 ，并且考虑哥德尔数为 
的命题，也就恰好是“ 不一致或者其中不存在哥德尔数为 的命题的证明”这个命题。假设从前提 能够推出“若 是一致的且存在哥德尔数为 的命题的证明，则哥德尔数为 的命题成立”，那么将哥德尔数为 的命题的具体形式代入这个条件命题的后半部分，注意到这恰好是条件命题前半部分的否定，于是通过排中律，可以直接推出条件命题的前半部分不成立，也就是从前提 能够推出“ 不一致或者其中不存在哥德尔数为 的命题的证明”。但是，我们这就从 推出了哥德尔数为 的命题，于是求出这个证明的哥德尔数，我们就能够验证 可以证明“存在哥德尔数为 的命题的证明”；这意味着上述析取式的后半部分不能成立，也就只能是前半部分成立，即 推出“ 不一致”。最后，由于我们假设了 是可靠的，因此 真的不一致；但另一方面，在上一段中刚刚说明， 的可靠性蕴含了 的一致性，这就产生了矛盾。因此，根据反证法，前提不能成立，也就是从 不能够推出“若 是一致的且存在哥德尔数为 的命题的证明，则哥德尔数为 的命题成立”，即以 和“ 是一致的”作为前提也不能够保证 中证明的可靠性。
就此，我们说明了关于哥德尔第一不完备性定理的前提选择是一件微妙的事情，而在毕导的视频中，证明第一定理实际使用了皮亚诺算术的可靠性，这是比一致性更强的假设，从而试图从该证明推出“若皮亚诺算术证明了自己的一致性就会导致矛盾”是不能成立的做法。
5. 补充阅读：关于真值
作为对毕导视频的补充，在这个问题下有答主注意到了如果将自指构造使用在真值谓词上会直接导致的结果：
看了毕导的年更新视频sub(n,n,17)之后，你有何感想？
在许多数理逻辑资料上，这会是讲完哥德尔的对角线法构造（不是康托尔的那个），也就是毕导视频中的 之后，最先讨论的简单结论，甚至要排在哥德尔第一不完备性定理前面；不过这确实和不完备性结论的相关性不大，既然毕导的视频中没有出现，那么我就在这里简单介绍一下。
首先，这位答主指出的矛盾确实存在，被称作塔斯基不可定义定理。这一讨论的背景是，“证明”是一个纯粹句法学的概念，也就是说我判断一些公式构成的序列是不是一个正确的证明，只单纯地检查出现在开头的公式是否和某些公理一摸一样、出现在中间的公式和相邻的公式之间的关系是否符合例如肯定前件之类的基本推理规则等等性质，这只需要通过有限时间内进行的机械操作就可以得出结论。因此，类似于我们之前所讨论的表达 的公式，“ 是某个公理体系中的一个证明”是可以被人工地翻译成皮亚诺算术中某些包含量词的式子的（只要这个公理体系本身可以用一阶语言来定义）；但是对于一个命题是否为真这件事，进行检定往往需要检查无限多的自然数，并且如毕导视频后面说明的那样，是不能通过图灵机这样的递归过程进行判定的〈24:12〉。于是，塔斯基思考的这个问题，也就是“我到底能不能写出一个带有一个变元 的公式 
，使得 成立当且仅当 是某个命题的哥德尔数且这个命题也成立呢？”与找到表达“证明”这一概念的公式不同，这是一个非平凡的问题。
而塔斯基最后得出的结论是这样的 是不可能存在的，他的依据就是同样通过代换构造出的这个矛盾：假如这个公式 存在，那么就可以将否定式 
的哥德尔数记作 
，然后构造出哥德尔数为 
的命题。现在，这个命题的内容恰好是 
，也就是说哥德尔数为 的命题成立当且仅当 
不成立；由我们假设 应该拥有的性质， 不成立又当且仅当哥德尔数为 的命题成立。于是哥德尔数为 的命题既不能成立也不能不成立，由反证法可知只能是开头假设的公式 不存在。
所以，简单来说，就是如果 是一个变量（或者含有变量的表达式）而非常量，那么“哥德尔数为 的命题为真”这句话在我们现在接受的逻辑体系中表达不出来，这样悖论自然就不存在了。从另一更直观的角度，哥德尔不完备性定理其实也是在说，如果某个包含皮亚诺算术且描述自然数的形式体系可以用（一阶）语言表述，那么一定能在其中构造出一个不能证明也不能证伪的命题；但是，如果我们有一个公式能够用来检查关于自然数的全部命题正确与否，那么通过这个公式定义出的形式系统就应该能证明全部的真命题、证伪全部的假命题，这显然是不可能的。回过头来，这也解释了为什么我们在之前引入可靠性的概念的时候，需要十分繁琐地说可靠性公理是对于每一个确定的命题 构造出一条公理，或者说是以公理模式的形式给出：这就是在可靠性这个条件公式的后半部分，如果想要写成“则哥德尔数为 的命题成立”，其中 是一个变量符号，这将是无法在皮亚诺算术之类的形式系统中写出的。因此，我们只能退而求其次地将关于某一确定命题 的证明的可靠性写成“若存在某个 为形式系统 中命题 的证明的哥德尔数，则命题 成立”的形式。
