哥德尔不完备定理

哥德尔不完备定理是逻辑学中的两个结果，讨论能够表达初等算术的形式系统所具有的局限。库尔特·哥德尔于1931年发表了这两个定理，证明足够强、一致且有效公理化的理论无法判定其语言中的每一个语句，并且在适当条件下无法证明自身的一致性。这些定理严格限定的是形式可推导性的范围，而不是断言数学存在矛盾，或数学推理普遍不可靠。(doi.org)

历史背景

这两个定理源于对数学基础的研究，尤其是与大卫·希尔伯特相关的希尔伯特纲领。该纲领的目标包括将数学形式化，并通过有穷主义推理确立数学形式理论的一致性。哥德尔的结果为这一计划划定了根本性的界限：任何涵盖足够多算术内容的一致、有效公理化理论，都无法解决所有算术问题；而且，一致性证明并不总能在所要论证的理论内部完成。这些限制推动数学基础研究转向考察具体理论的强度与局限。(ic.openlogicproject.org)

哥德尔在《论〈数学原理〉及相关系统中形式上不可判定的命题Ⅰ》一文中提出了这些结果。该文发表于《数学与物理月刊》第38卷，第173—198页，给出了第一定理的证明，并概述了第二定理。(doi.org)

条件与术语

形式理论规定一种语言、一组公理以及支配形式证明的规则。如果一个理论不会同时证明某个语句及其否定，就称其为一致的。在这里所讨论的句法意义上，如果对于每一个语句，理论都能证明该语句或其否定，就称其为完备的。一个既不能被证明、也不能被反驳的语句，独立于该理论。(ic.openlogicproject.org)

有效公理化是指公理可以由某个算法枚举出来；公理不必只有有限条。足够的算术强度是指理论能够表示对形式推理进行编码所需的初等数值运算与关系。第一定理的一个标准基准是罗宾逊算术，通常记作 $Q$ 。一阶皮亚诺公理所构成的皮亚诺算术还包含归纳公理模式，是这两个定理均适用的一个核心例子。(web.mit.edu)

这些前提条件至关重要。普雷斯伯格算术是只含加法、不含乘法的自然数理论，它既完备又可判定。相反，所有在标准自然数中为真的语句所组成的集合是完备的，却无法有效公理化。这两个例子都不与不完备定理矛盾。(people.csail.mit.edu)

第一不完备定理

在标准的哥德尔—罗瑟形式下，第一定理表述为：

任何一致、有效公理化且扩展了罗宾逊算术的理论，都包含一个既不能被该理论证明、也不能被该理论反驳的语句。

哥德尔最初的论证使用了更强的ω-一致性假设，以确立所构造语句的否定也不可证明。这一条件排除了如下情形：理论一方面证明某个自然数具有某种性质，另一方面又对每一个具体数码证明它不具有该性质。J. 巴克利·罗瑟修改了这一构造，使得仅凭通常的一致性就足以推出不完备性。(web.mit.edu)

“不可证明”始终是相对于特定的公理和推理规则而言的。一个独立语句在添加新公理后可能变得可证明。然而，只要一个一致的扩展理论仍然有效公理化且足够强，它本身就仍然是不完备的；增加公理并不能得到一个能够判定全部算术问题的最终有效理论。(math.berkeley.edu)

算术化与自指

证明的核心技术是哥德尔编码：为符号、公式和证明赋予自然数编码。这样，对表达式的操作就可以用数值运算来表示。这将有关句法的问题——例如某个已编码的序列是否构成证明——转化为有关自然数的问题。这种编码并不要求表达式在字面上包含自身的文本。(web.mit.edu)

对角引理可以构造一个语句 $G_T$ ，使其满足

T\vdash G_T\leftrightarrow \neg\operatorname{Prov}_T(\ulcorner G_T\urcorner),

其中， $\operatorname{Prov}_T(x)$ 表示在 $T$ 中的可证明性， $\ulcorner G_T\urcorner$ 则表示该语句的数值编码。非正式地说， $G_T$ 断言它自身在这个特定理论中不可证明。如果 $T$ 证明了它，那么该理论也能确立存在一个对它的证明，这就与该语句所断言的内容相矛盾。(web.mit.edu)

对于标准构造，一致性意味着 $G_T$ 在标准自然数中为真，却在 $T$ 中不可证明。认识到它为真，依赖的是在理论外部对其一致性进行推理，而不是在 $T$ 内部给出证明。(math.berkeley.edu)

第二不完备定理

一种标准表述是：任何一致、有效公理化且扩展了皮亚诺算术的理论，都不能证明以常规算术方式表达的自身一致性陈述：

T\nvdash\operatorname{Con}(T), \qquad \operatorname{Con}(T)= \neg\operatorname{Prov}_T(\ulcorner0=1\urcorner).

这里，一致性被表达为不存在一个经过编码的矛盾证明。这一表述依赖于可证明性的标准表示方式以及相关的可推导性条件；它并不无差别地适用于每一个在非正式意义上被描述为“断言一致性”的语句。(ocw.mit.edu)

其证明将第一定理中的足够多推理形式化，从而在 $T$ 内部确立 $\operatorname{Con}(T)$ 蕴含 $G_T$ 。因此，如果存在内部的一致性证明，就会得到不可能存在的 $G_T$ 的证明。不过，较强的理论仍可能证明较弱理论的一致性。这一定理排除的是某种特定的内部论证，而不是所有数学上的一致性证明。(ocw.mit.edu)

完备性、模型与计算

不完备性并不与哥德尔关于一阶逻辑的完备性定理冲突。逻辑的完备性涉及能否推导出在公理的所有模型中都由这些公理所蕴含的每一个语句。相比之下，不完备的理论包含一些语句，它们的真假在该理论公理的不同模型之间有所不同。因此，在预期的自然数结构中为真，与在所有模型中都是逻辑后承，是两回事。(ic.openlogicproject.org)

这些结果还将证明论与可计算性联系起来。停机问题所涉及的不可判定性，提供了通向算术不完备性的另一条路径：一个有效、可靠且完备的算术理论，将使算法能够判定某些计算问题，而实际上不存在任何算法可以普遍判定这些问题。检验一个具体的有限证明，与判定每一个可能的数学问题，始终是不同的任务。(math.berkeley.edu)