贡献者： 待更新
本文根据 CC-BY-SA 协议转载翻译自维基百科相关文章。
哥德尔的不完全性定理是数学逻辑中的两个定理，涉及形式公理化理论中可证明性的极限。这些结果由库尔特·哥德尔在 1931 年发布，在数学逻辑和数学哲学中都具有重要意义。这些定理被广泛地，但并非普遍地解释为，证明了希尔伯特寻找一个完整且一致的公理集合来描述所有数学的计划是不可能实现的。
第一个不完全性定理声明，任何一个一致的公理系统，只要其定理可以通过有效程序（即算法）列出，都无法证明关于自然数算术的所有真理。对于任何这样的形式系统，总会存在一些关于自然数的陈述，这些陈述是正确的，但在该系统内无法证明。
第二个不完全性定理，是第一个定理的扩展，表明该系统无法证明自身的一致性。
通过使用对角线论证，哥德尔的不完全性定理是首批关于形式系统局限性的紧密相关定理之一。随后，塔尔斯基提出了真理的形式不可定义性定理，丘奇证明了希尔伯特的判定问题是不可解的，图灵的定理表明不存在可以解决停机问题的算法。
不完全性定理适用于那些足够复杂的形式系统，这些系统能够表达自然数的基本算术，并且是一致的且具有有效的公理化。特别是在一阶逻辑的背景下，形式系统也被称为形式理论。一般来说，形式系统是一个推理工具，由一组特定的公理以及符号操作规则（或推理规则）组成，这些规则允许从公理推导出新的定理。一个这样的系统的例子是一阶皮亚诺算术系统，这是一个所有变量都指代自然数的系统。在其他系统中，如集合论，只有一些形式系统中的句子表达关于自然数的陈述。不完全性定理涉及的是这些系统内的形式可证明性，而不是 “非正式意义上的可证明性”。
形式系统可能具有几个属性，包括完整性、一致性和有效公理化的存在。不完全性定理表明，包含足够算术内容的系统无法同时具备这三种属性。
如果一个形式系统的定理集合是递归可枚举的，则该系统被称为有效公理化（也称为有效生成）。这意味着存在一个计算机程序，理论上可以枚举该系统的所有定理，而不会列出任何非定理的陈述。有效生成的理论的例子包括皮亚诺算术和泽梅洛–弗兰克尔集合论（ZFC）。\(^\text{[1]}\)
被称为真算术的理论包括在皮亚诺算术语言中关于标准整数的所有真陈述。该理论是一致且完整的，并包含足够的算术内容。然而，它没有递归可枚举的公理集合，因此不满足不完全性定理的假设。
一组公理是（语法上或否定上）完整的，如果对于公理语言中的任何陈述，该陈述或其否定可以从这些公理中证明出来。\(^\text{[2]}\) 这是与哥德尔的第一个不完全性定理相关的概念。它不应与语义完整性混淆，语义完整性意味着该公理集合能证明给定语言中的所有语义重言式。在他的完整性定理中（不应与这里描述的不完全性定理混淆），哥德尔证明了一阶逻辑在语义上是完整的。但它不是语法完整的，因为在一阶逻辑的语言中，有些句子既不能从逻辑的公理中证明，也不能反驳。
在一个数学系统中，像希尔伯特这样的思想家认为，找到这样一种公理化方法，使得可以通过证明其否定来证明或反驳每个数学公式，迟早只是时间问题。
一个形式系统可能是有意设计为语法不完整的，正如逻辑通常那样。或者它可能是不完整的，仅仅是因为并没有发现或包含所有必要的公理。例如，没有平行公设的欧几里得几何是不完整的，因为语言中的一些陈述（例如平行公设本身）不能从其余的公理中证明出来。同样，稠密线性序的理论是不完整的，但在添加一个额外的公理，即在序列中没有端点的公理后，它变得完整。连续统假设是 ZFC 语言中的一个陈述，在 ZFC 中无法证明，因此 ZFC 不是完整的。在这种情况下，没有显而易见的候选公理能够解决这个问题。
一阶皮亚诺算术的理论似乎是一致的。假设这确实是正确的，请注意它有一个无限但递归可枚举的公理集合，并且可以编码足够的算术内容以符合不完全性定理的假设。因此，根据第一个不完全性定理，皮亚诺算术不是完整的。该定理给出了一个算术陈述的明确示例，该陈述在皮亚诺算术中既不能被证明，也不能被反驳。此外，这个陈述在通常模型中为真。此外，没有有效公理化的一致扩展皮亚诺算术能够是完整的。
一组公理是（简单地说）一致的，如果没有任何陈述既能从公理中证明，又能证明其否定，否则该公理集合是不一致的。也就是说，一个一致的公理系统是没有矛盾的。
皮亚诺算术可以从 ZFC 中证明其一致性，但不能从自身内部证明。类似地，ZFC 不能从自身内部证明其一致性，但 ZFC + “存在一个不可接近的基数” 证明了 ZFC 是一致的，因为如果 \( \kappa \) 是最小的这样的基数，那么 \( V_\kappa \) 位于冯·诺伊曼宇宙内部是 ZFC 的一个模型，而一个理论是一致的，当且仅当它有一个模型。
如果将皮亚诺算术语言中的所有陈述都作为公理，那么这个理论是完整的，具有递归可枚举的公理集合，并且可以描述加法和乘法。然而，它不是一致的。
不一致理论的其他例子来自于集合论中，当假设无限制的理解公理 schema 时所产生的悖论。
不完全性定理仅适用于能够证明关于自然数的足够多事实的形式系统。一个足够的集合是罗宾逊算术 Q 的定理集合。一些系统，如皮亚诺算术，可以直接表达关于自然数的陈述。其他系统，如 ZFC 集合论，能够将关于自然数的陈述翻译成它们的语言。这两种选项都适用于不完全性定理。
给定特征的代数封闭域的理论是完整的、一致的，并且具有一个无限但递归可枚举的公理集合。然而，无法将整数编码到这个理论中，而且该理论不能描述整数的算术。一个类似的例子是实闭域的理论，它本质上等同于塔尔斯基的欧几里得几何公理。所以欧几里得几何本身（在塔尔斯基的表述中）是一个完整、一致、有效公理化的理论的例子。
普雷斯堡算术系统由一组自然数的公理组成，仅包含加法运算（乘法被省略）。普雷斯堡算术是完整的、一致的、递归可枚举的，能够编码加法但不能编码自然数的乘法，这表明对于哥德尔的定理，理论不仅需要编码加法，还需要编码乘法。
丹·威拉德（Dan Willard，2001 年）研究了一些弱的算术系统家族，这些系统允许足够的算术作为关系来形式化哥德尔编号，但不够强大以使乘法成为一个函数，因此无法证明第二不完全性定理；也就是说，这些系统是一致的，并且能够证明它们自身的一致性（见自验证理论）。
在选择一组公理时，其中一个目标是能够证明尽可能多的正确结果，而不证明任何错误的结果。例如，我们可以想象一组正确的公理，它们允许我们证明关于自然数的每一个正确的算术命题（Smith 2007，第 2 页）。在标准的一阶逻辑系统中，一个不一致的公理集合将证明它语言中的每个命题（这有时被称为爆炸原理），因此它自动是完整的。然而，一个既完整又一致的公理集合证明的是一组最大的非矛盾定理。
在前面几节中用皮亚诺算术、ZFC 和 ZFC + "存在一个不可接近的基数"所展示的模式通常无法打破。这里，ZFC + "存在一个不可接近的基数"无法从自身证明一致性。它也不是完整的，如连续统假设所示，这在 ZFC + "存在一个不可接近的基数"中是无法解决的。\(^\text{[3]}\)
第一个不完全性定理表明，在可以表达基本算术的形式系统中，永远不可能创建一个完整且一致的有限公理列表：每次添加一个额外的、一致的陈述作为公理时，仍然存在其他正确的陈述，即使在有了新公理的情况下也无法证明。如果添加的一个公理使得系统完整，那么它的代价就是使系统变得不一致。甚至不可能有一个无限的公理列表是完整、一致且有效公理化的。
哥德尔的第一个不完全性定理首次出现在哥德尔 1931 年论文《关于《数学原理》及相关系统中的形式不可判定命题 I》的 “定理 VI” 中。定理的假设在随后的时间里被 J. 巴克利·罗斯尔（1936 年）通过使用罗斯尔技巧改进。结合罗斯尔的改进，得出的定理可以用以下英语表述，其中 “形式系统” 包括假设系统是有效生成的。
第一个不完全性定理：“任何一致的形式系统 \( F \)，只要该系统能够进行一定量的基本算术运算，都是不完整的；即在 \( F \) 的语言中存在一些命题，这些命题在 \( F \) 中既无法证明也无法反驳。”（Raatikainen 2020）
定理所提到的不可证明命题 \( G_F \) 通常被称为系统 \( F \) 的 “哥德尔句子”。证明构造了一个特定的哥德尔句子 \( G_F \) 用于系统 \( F \)，但在系统语言中有无限多的命题具有相同的特性，例如哥德尔句子与任何逻辑有效命题的合取。
每个有效生成的系统都有自己的哥德尔句子。可以定义一个更大的系统 \( F' \)，它包含整个 \( F \) 以及 \( G_F \) 作为额外的公理。这样不会得到一个完整的系统，因为哥德尔定理也适用于 \( F' \)，因此 \( F' \) 也不能是完整的。在这种情况下，\( G_F \) 确实是 \( F' \) 中的一个定理，因为它是一个公理。由于 \( G_F \) 仅说明它在 \( F \) 中不可证明，因此它在 \( F' \) 中可证明并不产生矛盾。然而，由于不完全性定理适用于 \( F' \)，会有一个新的哥德尔命题 \( G_{F'} \) 对应于 \( F' \)，从而表明 \( F' \) 也是不完整的。\( G_{F'} \) 将与 \( G_F \) 不同，因为 \( G_{F'} \) 将指向 \( F' \)，而不是 \( F \)。
哥德尔句子的设计是间接地自指。该句子声明，当使用特定的步骤序列构造另一个句子时，该构造的句子在系统 \( F \) 中不可证明。然而，这些步骤的序列是如此安排，以至于构造出的句子实际上就是 \( GF \) 本身。通过这种方式，哥德尔句子 \( GF \) 间接地声明它在 \( F \) 中不可证明。\(^\text{[4]}\)
为了证明第一个不完全性定理，哥德尔展示了系统内可证明性的概念可以完全用算术函数来表示，这些算术函数作用于系统句子的哥德尔编号。因此，系统不仅可以证明有关数字的某些事实，还可以间接证明关于其自身陈述的事实，前提是它是有效生成的。关于系统内句子的可证明性的问题被表示为关于数字本身的算术性质的问题，如果系统是完整的，这些问题是可以决定的。
因此，尽管哥德尔句子间接地指向系统 \( F \) 的句子，但当它被作为算术陈述来解读时，哥德尔句子仅直接指向自然数。它断言没有自然数具有某个特定的属性，这个属性由一个原始递归关系给出（Smith 2007，第 141 页）。因此，哥德尔句子可以用算术语言以简单的语法形式写出。特别地，它可以表示为算术语言中的一个公式，该公式由若干个前导的全称量词后跟无量词体（这些公式属于算术层级中的 \( \Pi_1^0 \) 级别）。通过 MRDP 定理，哥德尔句子可以被重写为一个声明，即当将整数代入其变量时，特定的多变量整数系数的多项式永远不会取零值（Franzén 2005，第 71 页）。
第一个不完全性定理表明，适当形式理论 \( F \) 哥德尔句子 \( G_F \) 在 \( F \) 中是不可证明的。因为当它被解释为关于算术的陈述时，这种不可证明性正是该句子（间接）所断言的内容，因此哥德尔句子实际上是真的（Smoryński 1977，第 825 页；另见 Franzén 2005，第 28-33 页）。因此，哥德尔句子 \( G_F \) 通常被称为 “真实但不可证明”（Raatikainen 2020）。然而，由于哥德尔句子无法正式指定其预期的解释，句子 \( G_F \) 的真值只能通过来自系统外部的元分析来得出。通常，这种元分析可以在一个被称为原始递归算术的弱形式系统中进行，该系统证明了命题 \( \text{Con}(F) \rightarrow G_F \)，其中 \( \text{Con}(F) \) 是一个典型的陈述，断言 \( F \) 的一致性（Smoryński 1977，第 840 页；Kikuchi & Tanaka 1994，第 403 页）。
尽管一致理论的哥德尔句子作为关于算术预期解释的陈述是正确的，但哥德尔句子在一些非标准算术模型中是错误的，这是哥德尔完整性定理的一个结果（Franzén 2005，第 135 页）。该定理表明，当一个句子独立于一个理论时，该理论将具有既包含句子为真的模型，也包含句子为假的模型。如前所述，系统 \( F \) 的哥德尔句子是一个算术陈述，声称不存在具有某个特定属性的数字。不完全性定理表明，这个断言将独立于系统 \( F \)，而哥德尔句子的真值来自于没有任何标准自然数具有所讨论的属性这一事实。任何使哥德尔句子为假的模型必须包含某个元素，该元素在该模型中满足该属性。这样的模型必须是 “非标准的”——它必须包含一些不对应于任何标准自然数的元素（Raatikainen 2020，Franzén 2005，第 135 页）。
哥德尔在其论文《关于《数学原理》及相关系统中的形式不可判定命题 I》的引言部分中特别提到了理查德悖论和说谎者悖论，作为他语法不完全性结果的语义类比。说谎者悖论是 “这个句子是假的” 这句话。对这个说谎者句子的分析表明，它既不能为真（因为如果它为真，如它所断言的那样，它是假的），也不能为假（因为如果它为假，那么它就为真）。哥德尔句子 \( G \) 对于系统 \( F \) 做出了类似于说谎者句子的断言，但将 “真” 替换为 “可证明”：\( G \) 说 “\( G \) 在系统 \( F \) 中不可证明”。对 \( G \) 的真值和可证明性的分析是对说谎者句子真值分析的形式化版本。
在哥德尔句子中，不能将 “不可证明” 替换为 “假”，因为谓词 “\( Q \) 是一个假公式的哥德尔编号” 不能表示为算术公式。这个结果被称为塔尔斯基的不可定义性定理，它是由哥德尔在研究不完全性定理的证明时独立发现的，并且塔尔斯基也独立发现了这一定理。
与哥德尔 1931 年论文中陈述的定理相比，许多当代的不完全性定理表述在两个方面更加普遍。这些广义的表述被措辞为适用于更广泛的系统类别，并且被措辞为包含较弱的一致性假设。
哥德尔证明了《数学原理》系统的不完全性，这是一个特定的算术系统，但可以为任何具有一定表达能力的有效系统给出类似的证明。哥德尔在他的论文引言中提到这一事实，但为了具体性将证明限制在一个系统中。在现代的不完全性定理表述中，通常将有效性和表达能力条件作为不完全性定理的假设陈述，因此它不再局限于任何特定的形式系统。在 1931 年哥德尔发表其结果时，表述这些条件所需的术语尚未发展出来。
哥德尔原始的不完全性定理的陈述和证明要求假设系统不仅是一致的，而且是 \( \omega \)-一致的。如果一个系统不是 \( \omega \)-不一致的，则它是 \( \omega \)-一致的；而如果存在一个谓词 \( P \)，使得对于每个特定的自然数 \( m \)，系统证明 \( \neg P(m) \)，但同时系统也证明存在一个自然数 \( n \) 使得 \( P(n) \) 成立，则该系统是 \( \omega \)-不一致的。也就是说，系统说存在一个具有属性 \( P \) 的数字，但否认它具有任何具体的值。系统的 \( \omega \)-一致性意味着它的一致性，但一致性并不意味着 \( \omega \)-一致性。J. 巴克利·罗斯尔（1936 年）通过找到一种证明的变式（罗斯尔技巧）加强了不完全性定理，这种变式只要求系统是一致的，而不是 \( \omega \)-一致的。这主要具有技术性意义，因为所有关于算术的真实形式理论（其公理是关于自然数的所有真实命题）都是 \( \omega \)-一致的，因此原始表述的哥德尔定理适用于这些理论。现在，假设系统仅一致，而非 \( \omega \)-一致的更强版本的不完全性定理通常被称为哥德尔不完全性定理，也叫做哥德尔–罗斯尔定理。
对于每个包含基本算术的形式系统 \( F \)，可以规范地定义一个公式 \( \text{Cons}(F) \)，表达 \( F \) 的一致性。这个公式表达了 “不存在一个自然数，编码了在系统 \( F \) 中的形式推导，其结论是一个语法上的矛盾” 的属性。语法上的矛盾通常被认为是 “0=1”，在这种情况下，\( \text{Cons}(F) \) 表示 “没有自然数编码从 \( F \) 的公理推导出‘0=1’”。
哥德尔的第二个不完全性定理表明，在一般假设下，这个规范的一致性陈述 \( \text{Cons}(F) \) 在 \( F \) 中是无法被证明的。该定理首次出现在哥德尔 1931 年的论文《关于《数学原理》及相关系统中的形式不可判定命题 I》的 “定理 XI” 中。在以下表述中，“形式化系统” 一词还包括假设 \( F \) 是有效公理化的。这个定理声明，对于任何一个一致的系统 \( F \)，如果该系统能够进行一定量的基本算术运算，则 \( F \) 的一致性不能在 \( F \) 本身中得到证明。\(^\text{[5]}\) 这个定理比第一个不完全性定理更强，因为第一个不完全性定理中构造的陈述并没有直接表达系统的一致性。第二个不完全性定理的证明是通过在系统 \( F \) 本身中形式化第一个不完全性定理的证明得到的。
在第二个不完全性定理中，有一个技术性的微妙之处，涉及如何在 \( F \) 的语言中将一致性表达为一个公式。表达系统一致性的方法有很多种，并不是所有方法都能得出相同的结果。第二个不完全性定理中的公式 \( \text{Cons}(F) \) 是一致性的一个特定表达。
一致性声明的其他形式化可能在 \( F \) 中是不等价的，其中一些甚至可能是可证明的。例如，一阶皮亚诺算术（PA）可以证明 “PA 的最大一致子集是一致的”。但是，因为 PA 是一致的，PA 的最大一致子集实际上就是 PA，因此在这个意义上，PA “证明了它自己是一致的”。但 PA 无法证明的是，PA 的最大一致子集实际上就是整个 PA。（这里所说的 “PA 的最大一致子集” 是指在某个特定有效枚举下，PA 公理的最大一致初始段。）
第二个不完全性定理的标准证明假设可证明性谓词 \( Prov_{A}(P) \) 满足希尔伯特–伯奈斯可证明性条件。设 \( \#(P) \) 代表公式 \( P \) 的哥德尔编号，可证明性条件如下：
有些系统，如罗宾逊算术，足够强大，能够满足第一个不完全性定理的假设，但并不证明希尔伯特–伯奈斯条件。然而，皮亚诺算术足够强大，能够验证这些条件，所有比皮亚诺算术更强的理论也能满足这些条件。
哥德尔的第二个不完全性定理还意味着，满足上述技术条件的系统 \( F_1 \) 不能证明任何系统 \( F_2 \) 的一致性，尤其是 \( F_2 \) 证明了 \( F_1 \) 的一致性。这是因为这样的系统 \( F_1 \) 可以证明，如果 \( F_2 \) 证明 \( F_1 \) 的一致性，那么 \( F_1 \) 实际上是一致的。关于 \( F_1 \) 一致性的声明具有 “对于所有数字 \( n \)，\( n \) 具有可判定的属性，即不是 \( F_1 \) 中矛盾证明的代码” 这样的形式。如果 \( F_1 \) 确实不一致，那么 \( F_2 \) 会证明对于某个 \( n \)，\( n \) 是 \( F_1 \) 中矛盾的代码。但如果 \( F_2 \) 也证明 \( F_1 \) 是一致的（即不存在这样的 \( n \)），那么它本身就会不一致。这一推理可以在 \( F_1 \) 中形式化，证明如果 \( F_2 \) 一致，那么 \( F_1 \) 也一致。由于根据第二个不完全性定理，\( F_1 \) 并不能证明自己的统一性，因此它也不能证明 \( F_2 \) 的一致性。
这个第二个不完全性定理的推论表明，举例来说，无法通过任何可以在皮亚诺算术（PA）中形式化的有限方法来证明皮亚诺算术的一致性。举例来说，广泛接受的原始递归算术（PRA）系统被认为是有限数学的准确形式化，它在 PA 中是可证明一致的。因此，PRA 不能证明 PA 的一致性。这个事实通常被认为意味着希尔伯特的计划无法执行，希尔伯特的计划旨在通过给出一个有限的证明来证明 “理想”（无穷）数学原则在 “真实”（有限）数学命题证明中的一致性，进而证明理想原则的一致性。\(^\text{[6]}\)
如果一个系统 \( F \) 证明了自己的一致性，这不会提供任何有趣的信息。因为不一致的理论可以证明一切，包括它们的一致性。因此，在 \( F \) 中进行的一致性证明不会为我们提供关于 \( F \) 是否一致的任何线索；通过这样的证明，关于 \( F \) 一致性的任何疑问都不会得到解决。一致性证明的兴趣在于能够在某个在某种意义上比 \( F \) 本身更少存疑的系统 \( F' \) 中证明系统 \( F \) 的一致性，例如，\( F' \) 比 \( F \) 弱。对于许多自然发生的理论 \( F \) 和 \( F' \)，例如 \( F = \) 泽梅洛–弗兰克尔集合论和 \( F' = \) 原始递归算术，\( F' \) 的一致性可以在 \( F \) 中证明，因此根据第二个不完全性定理的推论，\( F' \) 无法证明 \( F \) 的一致性。
第二个不完全性定理并没有完全排除在不同的公理系统中证明一致性的可能性。例如，格哈德·根岑在一个包含断言序数 \( \varepsilon_0 \) 是良基的公理的不同系统中证明了皮亚诺算术的一致性；见根岑的一致性证明。根岑的定理促使了证明理论中序数分析的发展。
在数学和计算机科学中，"不可判定"一词有两种不同的含义。第一种含义是与哥德尔定理相关的证明理论含义，即一个命题在指定的推理系统中既不能被证明也不能被反驳。第二种含义（在此不讨论）与可计算性理论相关，适用于决策问题，而不是命题。决策问题是一个可数无限集，每个问题都需要一个 “是” 或 “否” 的回答。如果没有可计算的函数能正确回答问题集中的每个问题，则称该问题是不可判定的（见不可判定问题）。
由于"不可判定"一词有这两层含义，"独立"一词有时被用来代替"不可判定"以表示"既不能被证明也不能被反驳"的含义。
在特定推理系统中，命题的不可判定性本身并没有解决该命题的真值是否明确定义，或是否可以通过其他方式确定的问题。不可判定性仅意味着所考虑的特定推理系统不能证明命题的真或假。是否存在所谓的 “绝对不可判定” 命题，其真值永远无法得知或定义不明确，是数学哲学中的一个争议点。
哥德尔和保罗·科恩的联合工作提供了两个具体的不可判定命题（第一层含义的不可判定性）：连续统假设在 ZFC（集合论的标准公理化）中既不能被证明也不能被反驳，选择公理在 ZF（即 ZFC 公理中去除选择公理后的部分）中既不能被证明也不能被反驳。这些结果并不需要不完全性定理。哥德尔在 1940 年证明，这两个命题都不能在 ZF 或 ZFC 集合论中被反驳。在 1960 年代，科恩证明了这两个命题也不能从 ZF 中得到证明，且连续统假设不能从 ZFC 中得到证明。
谢拉（Shelah，1974 年）证明了群论中的怀特海德问题在标准集合论中是不可判定的（第一层含义的不可判定性）。\(^\text{[7]}\)
格雷戈里·蔡廷在算法信息理论中产生了不可判定命题，并在该领域证明了另一个不完全性定理。蔡廷的不完全性定理声明，对于任何能够表示足够算术的系统，存在一个上界 \( c \)，使得在该系统中无法证明某个特定数字具有大于 \( c \) 的科尔莫戈洛夫复杂性。虽然哥德尔定理与说谎者悖论相关，蔡廷的结果则与贝瑞悖论相关。
这些是哥德尔 “真实但不可判定” 命题的自然数学等价物。它们可以在一个更大的系统中得到证明，该系统通常被接受为有效的推理形式，但在像皮亚诺算术这样的更有限的系统中是不可判定的。
1977 年，巴黎和哈林顿证明了巴黎–哈林顿原理，一个无限拉姆齐定理的版本，在（一阶）皮亚诺算术中是不可判定的，但可以在更强大的二阶算术系统中证明。基尔比（Kirby）和巴黎后来证明了古德斯坦定理，一个关于自然数序列的命题，比巴黎–哈林顿原理要简单一些，它也在皮亚诺算术中是不可判定的。
克鲁斯卡尔树定理，该定理在计算机科学中有应用，也是从皮亚诺算术中不可判定的，但可以在集合论中证明。事实上，克鲁斯卡尔树定理（或其有限形式）在一个更强的系统 ATR0 中也是不可判定的，该系统编码了基于一种叫做预测主义的数学哲学所接受的原则。\(^\text{[8]}\) 相关但更一般的图小定理（2003 年）对计算复杂性理论有重要影响。
不完全性定理与递归理论中的若干关于不可判定集合的结果密切相关。
克利尼（Kleene，1943 年）通过使用可计算性理论的基本结果，给出了哥德尔不完全性定理的证明。其中一个结果表明停机问题是不可判定的：没有任何计算机程序可以正确地判断，给定任意程序 \( P \) 作为输入，是否当使用特定的输入运行时，程序 \( P \) 最终会停机。克利尼证明了，如果存在一个具有某些一致性特性的完整有效算术系统，那么它将迫使停机问题可判定，这是一个矛盾。\(^\text{[9]}\) 这种证明方法也由肖恩菲尔德（Shoenfield，1967 年）、查尔斯沃思（Charlesworth，1981 年）和霍普克罗夫特与乌尔曼（Hopcroft & Ullman，1979 年）提出过。\(^\text{[10]}\)
Franzén（2005 年）解释了如何利用马季亚谢维奇（Matiyasevich）对希尔伯特第十问题的解决方案来证明哥德尔的第一个不完全性定理。\(^\text{[11]}\) 马季亚谢维奇证明了，没有一个算法可以在给定一个多变量整数系数的多项式 \( p(x_1, x_2, ..., x_k) \) 时，判断方程 \( p = 0 \) 是否有整数解。由于具有整数系数的多项式和整数本身可以直接在算术语言中表达，如果一个多变量整数多项式方程 \( p = 0 \) 在整数中确实有解，那么任何足够强大的算术系统 \( T \) 都能证明这一点。而且，假设系统 \( T \) 是 \( \omega \)-一致的，在这种情况下，当整数中没有解时，它永远不会证明一个特定的多项式方程有解。因此，如果 \( T \) 是完整且 \( \omega \)-一致的，那么就可以通过简单地枚举 \( T \) 的证明来算法性地确定一个多项式方程是否有解，直到发现 “\( p \) 有解” 或 “\( p \) 无解”，这与马季亚谢维奇定理相矛盾。因此，可以得出结论，\( T \) 不能是 \( \omega \)-一致且完整的。此外，对于每个一致的有效生成系统 \( T \)，可以有效生成一个多变量多项式 \( p \)，使得方程 \( p = 0 \) 在整数上没有解，但缺乏解的事实不能在 \( T \) 中证明。\(^\text{[12]}\)
Smoryński（1977 年）展示了如何利用递归不可分集合的存在来证明第一个不完全性定理。这种证明通常会扩展，表明像皮亚诺算术这样的系统在本质上是不可判定的。\(^\text{[13]}\)
蔡廷的不完全性定理提供了一种不同的方法来生成独立句子，基于科尔莫戈洛夫复杂性。与克利尼提出的证明类似，蔡廷的定理只适用于具有额外属性的理论，即所有公理在自然数的标准模型中都为真。哥德尔的不完全性定理的不同之处在于，它适用于一致的理论，这些理论尽管在标准模型中包含虚假的陈述；这些理论被称为 \( \omega \)-不一致的。
该证明通过反证法分为三个关键部分。首先，选择一个符合提出标准的形式系统：
上述证明的一个主要问题是，乍一看，构造一个命题 \( p \) 来等价于 “\( p \) 不能被证明” 似乎必须让 \( p \) 包含对 \( p \) 的引用，这可能很容易导致无限递归。哥德尔的技术是展示命题可以与数字相匹配（通常称为语法的算术化），使得 “证明一个命题” 可以替换为 “测试一个数字是否具有某种属性”。这允许构造一个自指公式，从而避免任何定义的无限递归。这一技术后来被艾伦·图灵在他的《决策问题》研究中使用。
简单来说，可以设计一种方法，使得系统中可以表述的每个公式或命题都能得到一个唯一的数字，称为其哥德尔数，以便能够在公式和哥德尔数之间进行机械转换。所涉及的数字可能非常长（按位数计），但这并不是障碍；关键是这些数字可以被构造出来。一个简单的例子是，如何将英语存储为每个字母的数字序列，然后将其组合成一个更大的数字：
原则上，证明一个命题为真或为假可以被证明等同于证明与该命题匹配的数字是否具有某种属性。因为形式系统足够强大，能够支持关于数字的一般推理，它也能够支持关于代表公式和命题的数字的推理。关键是，由于该系统能够支持关于数字属性的推理，这些结果等同于对其等价命题的可证明性进行推理。
已经证明，在原则上，通过分析代表命题的数字的属性，系统可以间接地对可证明性做出陈述，现在可以展示如何构造一个实际执行这一过程的命题。
包含恰好一个自由变量 \( x \) 的公式 \( F(x) \) 称为命题形式或类符号。一旦将 \( x \) 替换为一个特定的数字，命题形式就变成了一个正式的命题，然后它要么在系统中是可证明的，要么不是。对于某些公式，可以证明对于每个自然数 \( n \)，\( F(n) \) 只有在它能够被证明时才为真（原始证明中的要求更弱，但对于证明概要来说，这样就足够了）。特别地，这对于每个有限自然数之间的具体算术操作都成立，例如 “\( 2 \times 3 = 6 \)”。
命题形式本身不是命题，因此不能被证明或反驳。但每个命题形式 \( F(x) \) 都可以分配一个哥德尔数，记作 \( G(F) \)。在命题形式 \( F(x) \) 中使用的自由变量的选择与分配哥德尔数 \( G(F) \) 无关。
可证明性的概念本身也可以通过哥德尔数进行编码，方法如下：由于证明是遵循某些规则的命题列表，因此可以定义证明的哥德尔数。现在，对于每个命题 \( p \)，可以询问一个数字 \( x \) 是否是其证明的哥德尔数。命题 \( p \) 的哥德尔数与 \( x \)（其证明的潜在哥德尔数）之间的关系是两个数字之间的算术关系。因此，有一个命题形式 \( \text{Bew}(y) \)，使用这个算术关系来陈述存在一个 \( y \) 的证明的哥德尔数： \[ \text{Bew}(y) = \exists x \left( y \text{ 是一个公式的哥德尔数，并且 } x \text{ 是由 y 编码的公式的证明的哥德尔数} \right)~ \] "Bew" 是德语单词 “beweisbar”（可证明）的缩写；这个名称最初由哥德尔用来表示刚才描述的可证明性公式。请注意，“Bew(y)” 只是一个缩写，表示原始语言中非常长的公式；"Bew" 本身并不被认为是该语言的一部分。
公式 \( \text{Bew}(y) \) 的一个重要特点是，如果命题 \( p \) 在系统中是可证明的，那么 \( \text{Bew}(G(p)) \) 也是可证明的。这是因为任何对 \( p \) 的证明都会有一个对应的哥德尔数，而这个哥德尔数的存在使得 \( \text{Bew}(G(p)) \) 得以满足。
证明的下一步是获得一个间接地表述其自身不可证明性的命题。虽然哥德尔直接构造了这个命题，但至少存在一个这样的命题，这一点可以通过对角化引理得到，后者表示，对于任何足够强大的形式系统和任何命题形式 \( F \)，存在一个命题 \( p \)，使得系统证明： \[ p \leftrightarrow F(G(p))~ \] 通过让 \( F \) 是 \( \text{Bew}(x) \) 的否定，我们得到定理： \[ p \leftrightarrow \neg \text{Bew}(G(p))~ \] 由此定义的命题 \( p \) 大致表述为：它自身的哥德尔数是一个不可证明公式的哥德尔数。
命题 \( p \) 并不字面上等于 \( \neg \text{Bew}(G(p)) \)；相反，\( p \) 表示，如果执行某种计算，得到的哥德尔数将是不可证明命题的哥德尔数。但当执行这个计算时，结果的哥德尔数最终是 \( p \) 本身的哥德尔数。这类似于下面这句英文：
“当它自己被引号包围时，是不可证明的。”
这句话并没有直接指代自己，但当进行声明的转换时，原句被作为结果得到，因此这句话间接地表述了它自身不可证明性。对角化引理的证明采用了类似的方法。
现在，假设公理系统是 \( \omega \)-一致的，并让 \( p \) 是上一部分中得到的命题。
如果 \( p \) 可证明，那么 \( \text{Bew}(G(p)) \) 将是可证明的，如上所述。但 \( p \) 断言 \( \text{Bew}(G(p)) \) 的否定。因此，系统将是不一致的，证明了一个命题及其否定。这个矛盾表明，\( p \) 不能是可证明的。
如果 \( p \) 的否定是可证明的，那么 \( \text{Bew}(G(p)) \) 将是可证明的（因为 \( p \) 是构造为与 \( \text{Bew}(G(p)) \) 的否定等价）。然而，对于每个特定的数字 \( x \)，\( x \) 不能是 \( p \) 证明的哥德尔数，因为 \( p \) 是不可证明的（根据前一段的推理）。因此，一方面，系统证明存在一个具有某种属性的数字（即它是 \( p \) 证明的哥德尔数），但另一方面，对于每个特定的数字 \( x \)，我们可以证明它没有这个属性。在 \( \omega \)-一致的系统中这是不可能的。因此，\( p \) 的否定是不可证明的。
因此，命题 \( p \) 在我们的公理系统中是不可判定的：它在系统内既不能被证明，也不能被反驳。
事实上，证明 \( p \) 不是可证明的只需要假设系统是一致的。证明 \( p \) 的否定不是可证明的则需要更强的假设，即 \( \omega \)-一致性。因此，如果 \( p \) 是为某个特定系统构造的：
如果试图 “添加缺失的公理” 以避免系统的不完全性，那么必须将 \( p \) 或 “不是 \( p \)” 添加为公理。但这样一来，“作为一个命题证明的哥德尔数” 的定义就发生了变化，这意味着公式 \( \text{Bew}(x) \) 现在不同。因此，当我们将对角化引理应用于这个新的 \( \text{Bew} \) 时，我们得到一个新的命题 \( p \)，它与之前的不同，如果新系统是 \( \omega \)-一致的，那么它将在新系统中是不可判定的。
布洛斯（Boolos，1989 年）概述了一个使用贝瑞悖论而非说谎者悖论来构造真实但不可证明公式的第一不完全性定理的替代证明。一个类似的证明方法是由索尔·克里普基独立发现的。\(^\text{[14]}\) 布洛斯的证明通过为任何可计算可枚举的算术真命题集合 \( S \) 构造另一个真实但不包含在 \( S \) 中的命题来进行。这给出了第一不完全性定理的一个推论。根据布洛斯的说法，这个证明之所以有趣，是因为它为算术的有效一致理论的不完全性提供了一种 “不同的理由”。\(^\text{[15]}\)
不完全性定理是相对少数几条非平凡定理中的一部分，这些定理已被转化为形式化的定理，并可以通过证明助手软件完全验证。哥德尔的不完全性定理的原始证明，像大多数数学证明一样，是用自然语言编写的，旨在供人类读者阅读。
使用 Nqthm（Shankar 1994）于 1986 年，Russell O'Connor（2003 年）使用 Rocq（之前称为 Coq）（O'Connor 2005），以及 John Harrison（2009 年）使用 HOL Light（Harrison 2009）宣布了第一不完全性定理版本的计算机验证证明。Lawrence Paulson（2013 年）使用 Isabelle（Paulson 2014）宣布了两条不完全性定理的计算机验证证明。
证明第二不完全性定理的主要难点是要证明，在第一不完全性定理的证明中使用的关于可证明性的各种事实，可以通过一个形式化的可证明性谓词 \( P \) 在系统 \( S \) 中进行形式化。一旦完成这一步，第二不完全性定理就可以通过在系统 \( S \) 内形式化整个第一不完全性定理的证明来得到。
令 \( p \) 表示上述构造的不可判定命题，并假设为了获得矛盾，系统 \( S \) 的一致性可以从系统 \( S \) 本身内部证明。这等同于证明命题 “系统 \( S \) 是一致的”。现在考虑命题 \( c \)，其中 \( c = \) “如果系统 \( S \) 是一致的，那么 \( p \) 不能被证明”。命题 \( c \) 的证明可以在系统 \( S \) 中形式化，因此命题 \( c \)，“\( p \) 不能被证明”（或同义地，“不是 \( P(p) \)”）可以在系统 \( S \) 中被证明。
接下来观察，如果我们能证明系统 \( S \) 是一致的（即 \( c \) 假设中的命题），那么我们就证明了 \( p \) 不能被证明。但这与第一不完全性定理相矛盾，因为根据第一不完全性定理，这个命题（即 “\( p \) 不能被证明”）是我们构造出来的不可证明命题。请注意，这就是为什么我们需要在系统 \( S \) 中形式化第一不完全性定理的原因：为了证明第二不完全性定理，我们通过与第一不完全性定理的矛盾来得到结论，而这只有通过在 \( S \) 中证明定理成立才能做到。因此，我们不能证明系统 \( S \) 是一致的。于是第二不完全性定理的命题得以成立。
不完全性定理影响了数学哲学，特别是形式主义的版本，形式主义使用单一的形式逻辑系统来定义其原则。
不完全性定理有时被认为对戈特洛布·弗雷格和伯特兰·罗素提出的逻辑主义计划产生了严重后果，该计划旨在通过逻辑来定义自然数。\(^\text{[16]}\) 博布·海尔和克里斯平·赖特认为，这并不是逻辑主义的一个问题，因为不完全性定理对一阶逻辑和算术的适用是相同的。他们认为，只有那些认为自然数应通过一阶逻辑定义的人，才会面临这个问题。
许多逻辑学家认为，哥德尔的不完全性定理对大卫·希尔伯特的第二问题打击致命，该问题要求为数学提供一个有限性的相容性证明。特别是第二不完全性定理，常常被视为使这个问题变得不可能。然而，并非所有数学家都同意这种分析，希尔伯特第二问题的地位尚未确定（见 “关于问题地位的现代观点”）。
包括哲学家 J. R. Lucas 和物理学家 Roger Penrose 在内的多位作者探讨了哥德尔的不完全性定理是否以及如何影响人类智慧。大部分讨论集中在人的思维是否等同于图灵机，或者根据丘奇–图灵假设，是否等同于任何有限的机器。如果是这样，并且如果机器是一致的，那么哥德尔的不完全性定理将适用于它。
普特南（Putnam，1960 年）建议，虽然哥德尔的定理不能应用于人类，因为人类会犯错误，因此是非一致的，但它可以应用于人类的科学或数学能力。假设它是一致的，要么其一致性无法证明，要么它无法被图灵机表示。\(^\text{[17]}\)
Wigderson（2010 年）提出，数学 “可知性” 的概念应基于计算复杂性，而不是逻辑可判定性。他写道：“当可知性以现代标准进行解释时，即通过计算复杂性，哥德尔现象仍然与我们息息相关。”\(^\text{[18]}\)
道格拉斯·霍夫施塔特在他的书《哥德尔、艾舍尔、巴赫》和《我是一个奇异循环》中，引用了哥德尔的定理作为他所称之为 “奇异循环” 的例子，奇异循环是一种存在于公理化形式系统中的层级自我指涉结构。他认为，这正是产生意识的结构——即人类大脑中 “自我” 感觉的来源。虽然哥德尔定理中的自我指涉来自哥德尔句子在《数学原理》这一形式系统内断言其不可证明性，但人类大脑中的自我指涉则来自于大脑如何将刺激抽象化并分类为 “符号”，即响应概念的神经元组，在这一过程中，实际上也是一个形式系统，最终产生出代表进行感知的实体概念的符号。霍夫施塔特认为，在一个足够复杂的形式系统中，奇异循环可以引发一种 “向下” 或 “颠倒” 的因果关系，这是一种常规因果关系层级被颠倒的情况。在哥德尔定理的情况下，这种现象简短地表现为以下几种情况：
仅仅通过知道公式的含义，就可以推断出其真伪，而无需像传统方法那样从公理出发，依照条理 “向上” 推导。这不仅是特殊的；它是令人震惊的。通常情况下，人们不能仅仅看一个数学猜想的内容，就凭借该陈述本身来推断其是否为真或为假。\(^\text{[19]}\)
在意识的情况下，这一 “向下因果关系” 在霍夫施塔特看来，表现为不可言喻的人类本能，即我们大脑的因果关系存在于欲望、概念、个性、思想和观念的高级层面，而不是在神经元之间或甚至是基本粒子之间的低级交互层面，尽管根据物理学，后者似乎拥有因果力量。
因此，我们正常的人类感知世界的方式具有一种奇特的颠倒感：我们天生倾向于感知 “大事物” 而非 “小事物”，即使微观世界似乎才是驱动现实的真正引擎所在。\(^\text{[19]}\)
尽管哥德尔的定理通常是在经典逻辑的背景下进行研究的，但它们在旁一致逻辑和固有矛盾命题（即二义命题）的研究中也有一定作用。Priest（1984，2006）认为，将哥德尔定理中的形式证明概念替换为通常的非正式证明概念，可以用来证明朴素数学是一致的，并将此作为对二义论的证据。\(^\text{[20]}\) 这种不一致的原因是语言中包含了一个针对系统的真值谓词。\(^\text{[21]}\)Shapiro（2002）对哥德尔定理在二义论中的应用给出了更为混合的评价。\(^\text{[22]}\)
有时在支持超越数学和逻辑的论点时，会引用或类比不完全性定理。多位作者对这种扩展和解释作出了负面评论，包括 Franzén（2005）、Raatikainen（2005）、Sokal & Bricmont（1999）；以及 Stangroom & Benson（2006）。\(^\text{[23]}\) 例如，Sokal & Bricmont（1999）和 Stangroom & Benson（2006）引用了 Rebecca Goldstein 对哥德尔所宣称的柏拉图主义与他的一些观点被用作反现实主义的对比的评论。Sokal & Bricmont（1999）批评了 Régis Debray 在社会学背景下引用该定理；Debray 则为这种用法辩护为隐喻（同上）。\(^\text{[24]}\)
在哥德尔于 1929 年以其博士论文发表完完整性定理的证明后，他转向了作为他的资格论文的第二个问题。他最初的目标是为希尔伯特的第二问题获得一个肯定的解决方案。\(^\text{[25]}\) 当时，类似于第二阶算术的自然数和实数理论被称为 “分析”，而仅涉及自然数的理论被称为 “算术”。
哥德尔并不是唯一在解决一致性问题的人。阿克曼在 1925 年发表了一个有缺陷的分析一致性证明，其中他尝试使用希尔伯特最初提出的ε-替代法。那年晚些时候，冯·诺依曼能够纠正没有归纳公理的算术系统的证明。到 1928 年，阿克曼向伯尔奈斯传达了一个修改后的证明；这个修改后的证明使得希尔伯特在 1929 年宣布他相信算术的一致性已被证明，并且分析的一致性证明可能很快也会随之而来。在不完全性定理发表后，证明阿克曼的修改证明必定是错误的，冯·诺依曼提出了一个具体的例子，证明了其主要技术是站不住脚的。\(^\text{[26]}\)
在他的研究过程中，哥德尔发现，尽管一句话宣称其虚假性会导致悖论，但一句话如果宣称其不可证明性则不会产生悖论。特别是，哥德尔意识到现在称为塔尔斯基的不可定义定理的结果，尽管他从未发表过这一结果。哥德尔于 1930 年 8 月 26 日向卡尔纳普、费格尔和瓦伊斯曼宣布了他的第一不完全性定理；他们四人将在接下来的一周参加在哥尼斯堡召开的第二届精确科学认识论会议，这次会议是一个重要的会议。
1930 年的哥尼斯堡会议是三大学术社团的联合会议，许多当时的主要逻辑学家参加了会议。卡尔纳普、海廷和冯·诺依曼分别就逻辑主义、直觉主义和形式主义的数学哲学发表了一个小时的演讲。\(^\text{[27]}\) 会议还包括希尔伯特的退休演讲，因为他将离开哥廷根大学的职位。希尔伯特在演讲中表达了他相信所有数学问题都可以解决的观点。他在演讲结束时说：
“对于数学家来说，没有‘我们不知道’，在我看来，对于自然科学也完全没有。……[没有人]能够找到一个无法解决的问题，原因在于，依我看，根本没有无法解决的问题。与愚蠢的‘我们不知道’相反，我们的信条是：我们必须知道。我们一定会知道！”
这次演讲很快成为了希尔伯特对数学的信仰总结（他的最后六句话 “Wir müssen wissen. Wir werden wissen!” 成为了希尔伯特 1943 年墓志铭的文字）。尽管哥德尔很可能出席了希尔伯特的演讲，但两人从未面对面见过面。\(^\text{[28]}\)
哥德尔在会议的第三天的圆桌讨论环节上宣布了他的第一不完全性定理。这个宣布除了引起冯·诺依曼的关注外，几乎没有引起其他注意，冯·诺依曼将哥德尔拉到一旁进行交谈。之后的同年，冯·诺依曼独立地在得知第一不完全性定理的基础上，获得了第二不完全性定理的证明，并在 1930 年 11 月 20 日的信中向哥德尔宣布了这一结果。\(^\text{[29]}\) 哥德尔则独立得出了第二不完全性定理，并将其包含在他提交的稿件中，该稿件于 1930 年 11 月 17 日被《数学月刊》接收。
哥德尔的论文于 1931 年在《数学月刊》上发表，题为《Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I》（《关于《数学原理》和相关系统中的形式上不可判定命题 I》）。正如标题所暗示的那样，哥德尔原计划在下一个卷期发表这篇论文的第二部分；第一篇论文的迅速接受是他改变计划的原因之一。\(^\text{[30]}\)
哥德尔于 1933 年至 1934 年在普林斯顿举办了一系列关于他不完全性定理的讲座，听众包括丘奇、克利尼和罗瑟。到那时，哥德尔已经意识到，他的定理所需的关键属性是系统必须是有效的（当时使用 “广义递归” 这一术语）。罗瑟于 1936 年证明了，如果适当改变哥德尔句子，那么ω-一致性假设（哥德尔原始证明中不可或缺的部分）可以被简单的一致性所替代。这些发展使不完全性定理基本上形成了现代形式。
1936 年，根岑发布了第一阶算术的一致性证明。希尔伯特接受了这一证明作为 “有限性证明”，尽管（正如哥德尔的定理已经展示的那样）它不能在被证明一致的算术系统内形式化。
不完全性定理对希尔伯特计划的影响很快被意识到。伯尔奈斯在《数学基础》第二卷（1939 年）中包括了不完全性定理的完整证明，并补充了阿克曼关于 \(\varepsilon\)-替代法和根岑算术一致性证明的额外结果。这是第二不完全性定理的第一次完整出版证明。
芬斯勒 芬斯勒（1926 年）使用了理查德悖论的一个版本，构造了一个在他所发展的特定非正式框架中既为假又无法证明的表达式。\(^\text{[31]}\) 在证明不完全性定理时，哥德尔并不知晓这篇论文（《哥德尔文集》第四卷，第 9 页）。芬斯勒于 1931 年写信给哥德尔，告知他这篇论文，芬斯勒认为这篇论文对不完全性定理有优先权。芬斯勒的方法并未依赖于形式化的可证明性，并且与哥德尔的工作只有表面的相似性。\(^\text{[32]}\) 哥德尔读了这篇论文，但发现其有深刻的缺陷，他在给芬斯勒的回复中指出了缺乏形式化的问题。\(^\text{[33]}\) 芬斯勒继续为他的数学哲学辩护，主张避开形式化，并在其余的职业生涯中坚持这一立场。
采尔梅罗 1931 年 9 月，恩斯特·采尔梅罗写信给哥德尔，宣布他认为哥德尔的论证中存在一个 “根本的缺陷”。\(^\text{[34]}\)10 月，哥德尔回复了一封 10 页的信，指出采尔梅罗错误地假设系统中的真理概念是可在该系统中定义的；根据塔尔斯基的不可定义性定理，通常情况下这是不成立的。\(^\text{[35]}\) 然而，采尔梅罗并没有退让，并在印刷出版物中发布了他的批评，包含了 “一段相当尖刻的批评，针对这位年轻的竞争者”。\(^\text{[36]}\) 哥德尔认为继续追究此事没有意义，卡尔纳普也同意这一看法。\(^\text{[37]}\) 采尔梅罗随后的大部分工作与比一阶逻辑更强的逻辑有关，他希望通过这些工作来展示数学理论的一致性和范畴性。
维特根斯坦
路德维希·维特根斯坦在他的 1953 年《数学基础的注释》中写了几段关于不完全性定理的文字，其中尤其有一段有时被称为 “臭名昭著的段落”，在这段文字中，他似乎混淆了 “真理” 和 “可证明性” 在罗素体系中的概念。哥德尔在维也纳学派的时期曾是该学派的成员，而在这一时期，维特根斯坦的早期理想语言哲学和《逻辑哲学论》主导了该学派的思想。关于维特根斯坦是否误解了不完全性定理，或者只是表达不清，存在一些争议。哥德尔的遗稿中表达了维特根斯坦误解了他的思想的观点。
许多评论者认为维特根斯坦误解了哥德尔，尽管 Floyd 和 Putnam（2000 年）以及 Priest（2004 年）提供了文本解读，认为大多数评论误解了维特根斯坦。\(^\text{[38]}\) 在维特根斯坦的评论发布后，伯纳伊斯、达米特和克雷塞尔分别写了关于维特根斯坦的评论，所有评论都非常负面。\(^\text{[39]}\) 这种一致的批评使得维特根斯坦关于不完全性定理的评论对逻辑学界的影响微乎其微。1972 年，哥德尔表示：“维特根斯坦失去理智了吗？他是认真的吗？他故意说出显而易见的无意义话语”，并写信给卡尔·门格尔，表示维特根斯坦的评论显示出他对不完全性定理的误解，写道：
“从你引用的段落中可以清楚地看出，维特根斯坦并没有理解[第一不完全性定理]（或者假装没有理解它）。他把它解释为一种逻辑悖论，而实际上它正好相反，即它是一个数学定理，属于数学中一个完全无争议的部分（有限数论或组合数学）。”\(^\text{[40]}\)
自从维特根斯坦的遗稿在 2000 年出版以来，哲学界发表了一系列论文，试图评估当初对维特根斯坦评论的批评是否合理。Floyd 和 Putnam（2000 年）认为，维特根斯坦对不完全性定理的理解比之前假设的更为完整。他们特别关注对ω不一致系统的哥德尔句子的解读，认为它说 “我不可证明”，因为该系统没有任何模型，其中的可证明性谓词与实际的可证明性相对应。Rodych（2003 年）认为，他们对维特根斯坦的解读在历史上并不成立。Berto（2009 年）探讨了维特根斯坦的著作与对称一致逻辑理论之间的关系。\(^\text{[41]}\)
以下翻译版本在所使用的词汇和排版上并不完全一致。排版问题尤其重要，因为 Gödel 特别强调 “那些在通常意义上已定义的元数学概念……”（van Heijenoort 1967，第 595 页）。共有三种翻译版本。第一版中，John Dawson 表示：“Meltzer 的翻译存在严重缺陷，并且在《符号逻辑杂志》上收到了毁灭性的评论；Gödel 也抱怨 Braithwaite 的评论（Dawson 1997，第 216 页）。” 他接着说，“幸运的是，Meltzer 的翻译很快被 Elliott Mendelson 为 Martin Davis 的文集《不可判定的命题》准备的更好版本所取代……他发现翻译‘没有他期望的那么好’……[但由于时间限制，他]同意了它的出版”（同上）。（Dawson 在脚注中指出，“他会后悔当时的同意，因为出版的版本在排版上很粗糙，并且有大量印刷错误”（同上））。Dawson 表示：“Gödel 偏爱的翻译版本是 Jean van Heijenoort 的版本”（同上）。对于认真的学生，还有一个版本是由 Stephen Kleene 和 J. B. Rosser 在 1934 年春季 Gödel 在高级研究院的讲座中记录的讲义笔记（参见 Davis 1965 年评论，第 39 页及从第 41 页开始）；该版本的标题是《关于形式数学系统中的不可判定命题》。按出版顺序：
友情链接： 超理论坛 | ©小时科技 保留一切权利