Loading AI tools
在数理逻辑中，哥德尔不完备定理是库尔特·哥德尔于1931年证明并发表的两条定理。第一条定理指出：
 | 本条目存在以下问题，请协助改善本条目或在讨论页针对议题发表看法。
|
这是形式逻辑中的定理，容易被错误表述。有许多命题听起来很像是哥德尔不完备定理，但事实上并不是。具体实例见对哥德尔定理的误解。
把第一条定理的证明过程在体系内部形式化后，哥德尔证明了第二条定理。该定理指出：
哥德尔不完备定理破坏了希尔伯特计划的哲学企图。大卫·希尔伯特提出，像实分析那样较为复杂的体系的相容性，可以用较为简单的体系中的手段来证明。最终，全部数学的相容性都可以归结为基本算术的相容性。但哥德尔的第二条定理证明了基本算术的相容性不能在自身内部证明，因此当然就不能用来证明比它更强的系统的相容性了。
不完备性定理适用于足够复杂，可以表示自然数算术的形式系统，而这种形式系统是自洽的，可以被公理化的。这些概念的详细含义会在后面给出。尤其是在一阶逻辑的语境中，形式系统也被称为"形式定理"。一般地，一个形式系统被定义为含有一组特定公理集合以及符号变换规则(或者是推导规则)的演绎工具。这样的一个形式系统的例子是一阶算术系统，在这个系统中，所有变量都代表为自然数。而在其他系统中，例如集合论，只有部分属于形式系统的表述才表示了自然数算术。不完备性理论是关于这些形式系统中的形式可证明性，而不是关于非形式意义上的"可证明性"。
形式系统可能具有的性质如下，完备性、一致性和有效公理化的存在性。不完备性定理则表明任何蕴含皮亚诺算术公理的形式系统不能同时具有这三个性质。
如果形式系统中的定理集是递归可列举的集合(Franzén 2004, p. 112)，那么该形式系统是"有效公理化的"(也被称为“生成定理的有效性”)。
这意味着，在原则上计算机程序能够列举出系统中所有的定理，而不列出任何非定理的陈述。皮亚诺公理和策梅洛-弗兰克尔集合论 (ZFC) 都是有效生成定理的例子。
现在被称为真算术的理论不仅有皮亚诺算术中关于整数的正确陈述，而且是自洽和完备的，并有足够的运算公理。但是它的定理集不是递归可列举的集合，因此也不满足不完备定理的假设。
- 只要证明了初等算数理论Π是不完全的，采用相同的方法就可以证明任何包含Π的形式理论都是不完全的
- 证明Π的不完全性的关键是在于构造出初等算数语言Ľ中的一个含义为真的语句Α，证明如果Α能被证明则将推出矛盾
- 包含初等算数理论的意义是它包含所有正整数（无穷元素）。而命题和证明都可以被映射到正整数。另一方面，它还支持归纳集，即及由一些初始元素及新元素构成的集合，而新元素都是由初始元素归纳（运算）而得的。形式理论由公理及定理构成，定理可以看作是公理及已知定理的归纳，因而形式理论本身可以表示成以某些正整数为初始元素的某种归纳集。这使得可证性变为算术命题
- 所构造的语句Α类似于“说谎者悖论”（即“这句话在说谎”），但Α是“本语句不可证”。对这一形式化的Α如果假设Α可证将推出矛盾，但假设Α不可证却不能推出矛盾，所以Α不是一个悖论。而Α的含义是它不可证，而它又被证明是不可证的，因此Α是个不可证的真命题
- Ľ不完全，那么包含Ľ的Π不完全，那么包含Π的形式系统不完全。得证。
哥德尔巧妙地利用了命题的“真值为真”和“含义为真”的区别，从而构造出了含义为真而真值不可证的命题，又避免了悖论的陷阱。形式逻辑系统的命题本身是没有含义的。命题只有真值而没有含义。公理命题的真值为真。其它命题的真值为真当且仅当该命题可以被证明，为假当且仅当该命题的非可以被证明。当形式逻辑系统被实际应用时，系统中的符号都被映射到实际概念上，从而有了语义。这种映射叫做一个模型。有了模型，命题就有了含义（语义）。例如，在ZF公理化集合论中，系统中的对象（object）被影射到“集合”这一概念，∈被映射到“属于”这一概念就是模型的一个例子。而ZF公理化系统本身即使没有模型也可以成立。如果换一个模型，形式系统没变，只是它不再是集合论了。当然，ZF公理化系统是为了集合论量身打造的，很适合于集合论。如果换一个模型，很难找到可理解的语义。但这说明了“真值为真”和“含义为真”是有区别的。
在大多数情况下，命题的“真值为真”和“含义为真”是一致的。例如，设A为一命题,则命题A↔¬A的含义是“本命题A为假”，这时A的真值为真和含义为真是一致的，结果形成了否定循环而构成了悖论。而逻辑系统不能含有悖论，所以这样的A应该是构造不出来的。哥德尔定理证明的巧妙之处就在于将悖论的“为假”改为了“为不可证”使得真值为真和含义为真成为不一致（含义为真是不可证，而真值为真或假都是可证），因而产生了自我否定又避免了循环的效果，也就避免了悖论。
理解了这一点，就可以理解哥德尔定理不是说存在真值为真又不可证这种自相矛盾的悖论命题（实际上应该构造不出来），而是存在含义为真但不可证（即真值不可知）的命题。哥德尔定理也不只是说存在既不可证真，也不可证伪的命题，这样的命题有很多，哥德尔定理的重要之处在于它还说了该不可证的命题是含义为真的。
哥德尔定理是一阶逻辑的定理，故最终只能在这个框架内理解。在形式逻辑中，数学命题及其证明皆以一种符号语言描述，只要检查每一个证明的有效性，便可从一组公理开始无可辩驳地证明一条定理。理论上，这样的证明可以在电脑上检查，事实上这样的有效性检查程序也已经有了。
为了这个过程得以进行，需确定手头有什么样的公理。可以从一组有限的公理集开始，例如欧几里得几何。或者更一般地，由一个可以允许无穷的公理列表开始，只要能机械地判断给定的命题是否是一条公理就行。在计算机科学里面，这被称为公理的递归集。尽管无穷的公理列表听起来有些奇怪，实际上自然数的通常理论中(被称为皮亚诺公理)就是如此。
哥德尔的第一条不完备定理表明任何一个允许定义自然数的体系必定是不完备的：它包含了不能在此体系内以一阶谓词逻辑形式证明的命题，并且该命题的否命题也不能在该体系内以一阶谓词逻辑的形式证明。
存在不完备的体系这一事实本身并不使人感到特别惊讶。例如，在欧几里得几何中，如果把平行公设去掉，就得到一个不完备的体系。不完备的体系可能只意味着尚未找出所有必须的公理而已。
但哥德尔揭示的是在多数情况下，例如在数论或者实分析中，永远不能找出公理的完整集合。换句话说，每一次将一个命题作为公理加入，将总有另一个命题出现在所能形式证明的范围之外。
如果加入无穷条公理（例如，所有真命题）到公理列表中，确保所有命题都可证明为真或假，但得到的公理列表将不再是递归集。给出任意一条命题，将没有机械的方法判定它是否是系统的一条公理。如果给出一个证明，一般来说也无法检查它是否正确。
在计算机科学的语言中，哥德尔定理有另一种表述方式。在一阶逻辑中，定理是递归可枚举的：即可以编写一个可以枚举出其所有有效证明的程序。同时可以考虑是否可以将结论加强为递归的：可以编写一个在有限时间内判定命题真假的程序吗？然而根据哥德尔定理，答案是一般来说不能。
哥德尔和保罗·寇恩得出的一些结果结合起来给出了不确定命题（既不能证明也不能否证的命题）的一个实际例子：选择公理和连续统假设都是集合论的标准公理系统内的不确定命题。
在1973年，同调代数中的怀特海问题被证明是集合论中的不确定命题。
1977年，Paris和Harrington证明了组合论中的一个命题，拉姆赛理论的某个版本，在皮阿诺公理给出的算术公理系统中是不确定的，但可以在集合论的一个更大体系中证明为真。
在计算机科学中用到的Kruskal的树问题，也是在皮亚诺公理中不确定而在集合论中可证明的。
古德斯坦定理是一个关于自然数的相对简单的命题，它在皮亚诺算术中是不确定的。
古格里·钱顿（Gregory Chaitin）在算法信息论中构造了一个不确定命题，即“Chaitin随机数Ω的第n个字节是否为0”这样的命题在ZFC内是不可判定的。
以下列出的误解都是针对第一条定理而产生的。
不完备性的结论影响了数学哲学以及形式化主义（使用形式符号描述原理）中的一些观点。第一定理可以被解释为：“不存在一个万能的公理系统，使得其既能够证明一切数学真理，又能证伪任何谬误。”
以下对第二定理的另一种说法甚至更令人不安：
如果一个（强度足以证明基本算术公理的）公理系统可以用来证明它自身的相容性，那么它是不相容的。
于是，为了确立系统S的相容性，就要构建另一个系统T，但是T中的证明并不是完全可信的，除非不使用S就能确立T的相容性。举个例子，自然数上的皮亚诺公理的相容性可以在集合论中证明，但不能单独在自然数理论范围内证明。这对大卫·希尔伯特的著名的未解决的23个数学问题中的第二个给出了一个否定回答。
理论上，哥德尔理论仍留下了一线希望：也许可以给出一个算法判定一个给定的命题是否是不确定的，让数学家可以忽略掉这些不确定的命题。然而，对可判定性问题的否定回答表明不存在这样的算法。
值得注意的是，符合哥德尔不完备定理的系统，必须要蕴涵皮亚诺算术公理以承载对第一不完备定理证明过程的编码。基本上，这就要求系统能将一些基本操作例如加法和乘法形式化，例如在鲁宾逊算术Q中那样。有一些更弱的公理系统是相容而且完备的，例如Presburger算术，它包括所有的一阶逻辑的真命题和关于加法的真命题。
公理系统可能含有无穷条公理（例如皮亚诺算术就是这样），但要哥德尔定理生效，必须存在检验证明是否正确的有效算法。例如，可以将关于自然数的所有在标准模型中为真的一阶语句组成一个集合。这个公理系统是完备的；哥德尔定理之所以无效，是因为不存在决定任何一条语句是否正确的有效算法。从另一方面说，这个算法的不存在正是哥德尔定理的直接结果。
另一个哥德尔定理不适用的特殊情况是：将关于自然数的所有语句首先按长度然后按字典顺序排序，并从皮亚诺公理集开始，一个一个遍历列表，如果发现一条语句既不能证明又不能否证，就将它作为公理加入。这样得到的系统是完备的，兼容的，并且是足够强大的，但不是递归可枚举的。
哥德尔本人只证明了以上定理的一个较弱版本；以上定理的第一个证明是罗素（Russel）于1936年给出的。
基本上，第一定理的证明是通过在形式公理系统中构造如下命题
- 𝑝 = “此命题是不可证明的”
来完成的。这样，它可以看成是说谎者悖论的一个现代变种。
如果公理系统是相容的，哥德尔证明了𝑝（及其否定）不能在系统内证明。因此p是真命题（p声称它不可证明，而它确实不能），尽管其证明不能在系统内形式化。请注意将𝑝作为公理加入系统并不能解决问题：扩大了的系统中会有另一个哥德尔语句出现。
罗杰·彭罗斯声称“可被机械地证明的”和“对人类来说看起来是真的”的这一区别，表明了人类智能在本质上不同于机械过程。这一观点未被普遍接受，因为正如马文·闵斯基所指出的，人类智能有犯错误和理解不相容和谬误句子的能力。但马文·闵斯基透露说库尔特·哥德尔私下告诉他，他相信人类有一种到达真理的直觉方法，但因为跟计算机式的方法不同，人类可以知道为真的事情并不受他的定理限制。[2]
对以上认为该定理揭示了人类具有超出形式逻辑之能力的这种观点，也可以作如下评论：p无法被证明，也无法被证伪，因为无法知道系统是否是相容的。因此实际上在此公理系统可证明范围以外的真命题不在考虑范围之内。于是可以说明一个命题：
- 要么𝑝在系统内部无法证明，要么该系统是不相容的。
这样的命题之前已经在系统内部被证明。实际上，这样的证明可以如下给出。
要充实对证明要点的描述，主要的问题在于：为了构造相当于“𝑝是不可证明的”这样的命题𝑝，𝑝就必须包含有自身的引用，而这很容易陷入无穷循环。而哥德尔为了避开无穷循环而产生的方法，后来被艾伦·图灵用于解决可判定性问题。
首先，每个公式，或者说可形式化的命题都可以被赋予一个数，称为哥德尔数。例如，假设形式系统有100个符号，用0至99对这些符号进行编码，这样，一个命题的公式就是一个位数为公式长度的100进制的整数，同一个公式可以有多种不同的写法，因此可以对应多个数，但每一个数要么不对应任何公式，要么只对应唯一的一个公式，可能有多个数对应同一个公式。因为系统包含所有正整数，因此也就涵盖了所有的公式。而一个证明可以表示为一个有穷的命题序列，例如将推理过程表示为命题序列。用同样的原理也可以将一个证明过程表示为一个正整数。当然，表示一个命题的正整数和表示一个证明的正整数具有不同的含义，因此不能混在一起。
像𝐹(𝑥)这样的公式含有一个自由变量𝑥，它们称为命题形式。一旦𝑥被一个特定的数代替，它就成为一个真正的，可证的特定命题。于是它要么是在系统中可证明的，要么可证伪。例如若𝐹(𝑥)定义为：𝑥是偶数，那当设𝑥=2时𝐹(𝑥)是可证明的，而𝑥=3时𝐹(𝑥)是可证伪。由于𝐹(𝑥)不是命题，因此不能被证明也不能被否证。但每一个命题形式𝐹(𝑥)都有一个哥德尔数，可用𝑮(𝐹)表示。自由变量𝑥的选取𝑮(𝐹)无关。
通过小心地分析系统的公理和推理规则，可以写下一个命题形式𝑃(𝑥)，它表示𝑥是系统中一个可以证明的命题的哥德尔数。形式描述如下：如果𝑥是一个可证明命题对应的哥德尔数，𝑃(𝑥)就可被证明，而其否定~𝑃(𝑥)则不能。（尽管这作为一个证明要点来说已经足够，但在技术上却不太严格。请参见哥德尔和罗素的有关论文，关键字是“omega-consistency”。）
现在，重点来了：一个命题形式𝐹(𝑥)称为不可自证的，当且仅当把命题形式𝐹的哥德尔数𝑮(𝐹)代入𝐹中所得的命题𝐹(𝑮(𝐹))是不可证明的。这个定义可以形式化，于是可以构造一个命题形式𝑆𝑈(𝑧)，表示𝑧是某个不可自证命题形式的哥德尔数。𝑆𝑈(𝑧)的形式描述如下：
- 对某个命题形式𝐹(𝑥)有𝑧 = 𝑮(𝐹)，而且设𝑦=𝑮(𝐹(𝑧))，则有~𝑃(𝑦)成立。
则所需语句𝑝可定义为：
- 𝑝 = 𝑆𝑈(𝑮(𝑆𝑈))
直观上，当提及𝑝是否为真的时候，可以利用𝑝的定义将𝑝展开为“不可自证这个特性本身是不可自证的吗？”这个命题形似理发师悖论，即“若一个理发师只替那些不替自己理发的人理发：他替自己理发吗？”
现在如果公理系统相容，则下列论证成立：
如果𝑝是可证明的，于是𝑆𝑈(𝑮(𝑆𝑈))为真，根据𝑆𝑈的定义，𝑧 = 𝑮(𝑆𝑈)就是某个不可自证命题形式的哥德尔数。于是𝑆𝑈就是不可自证的，根据不可自证的定义，𝑆𝑈(𝑮(𝑆𝑈))是不可证明的。这一矛盾说明𝑝是不可证明的。
如果𝑝是可证伪的，则根据𝑆𝑈的定义，𝑧 = 𝑮(𝑆𝑈)就不是不可自证命题形式的哥德尔数。这意味着𝑆𝑈不是不可自证的。根据不可自证的定义，可知𝑆𝑈(𝑮(𝑆𝑈))是可以证明的，推出矛盾。这说明𝑝的否定也是不可证明的。
因此，𝑝既不可在系统内证明也不可在系统内否证。
令𝑝是如上构造的不确定命题，且假定系统的相容性可以在系统内部证明。上述证明说明，如果系统是相容的，则𝑝是不可自证的。这个证明过程可以在系统内部形式化，因此命题“𝑝是不可证明的”或者“~𝑃(𝑝)”可以在系统内证明。
但是最后一个命题就等价于𝑝自己（而且这种等价性可以在系统内部证明），从而𝑝就可以在系统内证明。这一矛盾说明系统是不相容的。
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
