一、引论 哥德尔（Gōdel）不完全定理是二十世纪数学意义最深远的和惊人的成果之一。它发表于1931年，破灭了希尔伯特（Hilbert）形式主义的规划，推进了数理逻辑的发展，然而，即使到了今天，许多非逻辑学家对正确地评价哥德尔定理的意义，或理解它的基本内容，无疑还存在一些问题。
这种认识的不足，部分的原因在于：基础问题和“正在工作着的”数学家无关的想法还缠住人不放。我们暂且不顾这些，然而由于大部分对不完全性定理的说明都集中在它的证明的悖论性质上，带来的后果是定理的意义被淹没在错综复杂的技巧之中了，有些人甚至认为定理虽是珍品，但不可理解。
本文的目的是想从完全不同的角度来考察哥德尔定理，着重说明它的意义。按这种方法我们将概观一系列逻辑学中的重要成果，并且考察朝向一个杰出的未解决问题的进展。
二、逻辑背景 尽管哥德尔定理的影响已远为超出数论范围，我们还将把注意限制在原初的范围中，一开始，我们必须区别非逻辑学家熟悉的非形式的匹阿诺（Peano）公理和它在一阶数论（证哥德尔定理时采用的）中的逻辑的形式化。用兰道（Landau）的方法，我们把前者写成：
1. 零是自然数。
2. 每一自然数有唯一的自然数作为它的后继。
3. 零本身不是任何自然数的后继。
4. 有相同后继的自然数相同。
5. （归纳公理）任何包含零，并且包含属于它的每个数的后继的自然数集，包含一切自然数。
根据这些公理和算术运算的定义，按照非形式的逻辑规则（如兰道所作）可以导出初等算术的所有基本的定理。此外，众所周知，我们能证明两个满足上述所有公理的结构一定是同构的；但是、我们必须在本质上使用归纳公理，该公理作用于数的集而不是数本身。
在对公理形式化时，避免使用集合论的符号是合适的。简单地重述匹阿诺原来叙述的归纳公理是可能的：“任何性质、对零为真并且对某数为真时对它的后继也为真，那么对所有自然数为真。”
“适当的形式语言”可以用各种方式构造，不过在任何情况下，我们总把它理解为一阶语言。即：
注意，在一阶语言中，变元只允许被解释成它的变域是结构的元，决不能解释成这些元组成的集，也要注意，尽管从集合论观点看，函数可以被处理成一种特殊的关系，在形式逻辑中，函数和关系符号是有区别的，因为它们在语法上所起作用不同。
形式语言是表达数学理论精确公式的工具；它们的巨大的优点是允许在真和可证这些基础的数学概念之间作出区分。因此真的语义的确定是对于结构而言的：对语言中的变元符号给出结构中的特殊元作为指派，结构中的关系，函数和常项提供了解释原子公式的意义（从而真或假）的自然框架。而较为复杂的公式，需要通过按经典逻辑规则解释联结词和量词的意义，归纳地加以确定（一种精细的思想由塔斯基（Tarski）提出）。一个公式在结构Ц中是真的，如果对它的变元符号不管做怎样的特殊的指派，它都是真的；一个公式是逻辑的有效的，如果对于语言的每个结构它最真的。
为了定义证明的概念，我们首先要选出逻辑有效公式集的子集为逻辑公理，然后选出其它一组（或许是空的）公式作为固有的（或非逻辑的）公理。最后我们列出一组推演规则。因此，理论中的一个证明乃由一个有限的公式序列组成，其中每一公式或者是一公理，或者是应用推理规则于前面列出的公式的结果。证明的长度（行数）是序列中公式的数目。
三、形式化的局限性 完全性和不完全性。我们假定数学研究的目标是确定关于某些数学上是有趣的结构的真是什么，其次是a明，最后才是方法，特别地，用纯粹语义术语对真所作的形式定义，启示人们设想证明是可能省去的。对于联结词逻辑（命题逻辑），确实能够这样做到，真值表提供了判定一个任意的命题陈述的有效性的能行方法。但是，当引进量词和关系时，怎样去确定一个陈述在所有可能的解释之下是否成立，这是不清楚的：一阶逻辑中的一个基本成果（丘奇不可判定定理）说：不存在能行的程序（算法），能判定PA中一个任意公式是否逻辑有效；对于至少包含一个n元关系符号（对某个n≥2）的一阶语言，加上等号上述结论同样成立。
丘奇定理有着深远的含义，它证明了在构造算术的真时使用的证明是正确的，而在同时它也提出一个如何选取一足够的逻辑公理集的问题。对任意的适当的证明系统，一定可能识别公理（为大家知道的递归可公理化性的条件），如果逻辑公理被取作由所有逻辑有效公式组成，这将是不可能的，所以就有了问题：能否选取一个递归的逻辑公理集和有限的推理规则，从中，所有逻辑有效的公式都能作为定理而导出呢？
这个问题试验性的解答是由希尔伯特（Hilbert）和他的追随者在本世纪前几十年提出的，它们的奠基石是由哥德尔（Gōdel）在他的博士论文中提供的。他证明，能够在任意一阶理论中选取一分组簇，使得定理精确地对应于那些在相应于固有公理组的一切模型（即，结构可满足的）为真的公式。这个结果，即哥德尔完全性定理是哥德尔的另一定理的系理，该定理说：每个一致的一阶理论（没有矛盾的）有一模型。因为如果一公式在给定的理论中不可证，它的否定式可以一致地附加为一个新公理；因而对于要论证的理论的一个模型是原初理论的一个模型，在原初理论中谈及的公式是假的。（严格地说，哥德尔仅就可数多个符号的语言获得了他的结果；推广到不可数语言是由马尔采夫（Mal'cev）和另一些人作出的。）
完全性定理似乎维护了形式主义的期望，但是，和逻辑有效性相像，它也包含一个弱点：提到了一个公理组的所有模型。一个理论的所有模型这种说法是很不明显的。确实，非欧几何的发现成了数学史的转折点，它唤起了对公理系统存在非标准模型的认识。在集合论中现代一致性和独立性证明，基于同样的想法。
在用匹阿诺公理刻划自然数直至自同构的结构的特性的非形式证明中，非固有解仍可以出现在与数论不相干的地方。但是，完全性定理本身蕴涵了形式数论非同构模型的存在性，因为证明长度有限，一个理论是一致的，如果它的公理的每个有限子集是一致的。因此，根据完全性定理我们得到关于一阶理论的紧致性定理：一个一阶理论有一模型，如果它的每个有限子理论有模型，特别地，和PA相近的，一个新的常项符号c和相应于每个自然数n的
单单非标准模型的存在本身并没有破灭发现关于自然数为真的精确含义是什么的希望，由于同构是两个结构满足PA的同一句子集的充分条件而并非必要条件。PA的一切模型具有相同的一阶性质仍是可信的。但是在1931年，仅在完全性定理发现—年之后，哥德尔通过构造一个实例：PA的一个句子对自然数为真但在PA中不可证。这大为震惊了数学世界。因而，这个（第一）不完全性定理造成了：在形式数论的一切模型中为真的公式构成了这样一种自然数的真子集，区分自然数和非标准“顶替者”，不可能用给定的演绎系统中的形式证明的方法加以发现。
人们仍然可以问：是否有在数论中建立真的形式证明？悖论性地回答是肯定的。由于哥德尔不完全性定理的证明显示了一个公式的形式不可判定性通过非形式证明为真的可能性。（见§5）。但是，潜在的，用这种方法去发现数论意义下的真，只是最近才开始为人们所认识（一个激动人心的进步在J. B. Paris [18]）。此外，哥德尔的技巧得出：对PA的任意一个公式（在自然数中），并不存在判定它真或假的能行的程序。这个和丘奇定理的类似物与Presburger的肯定结果形成了尖锐的对照，他曾在二年前已证明：对于无乘法的算术，能行判定程序是存在的。
有理由期待，在PA中至少足以证明每一闭的，无量词的在自然数中为真的公式。事实上，每个真的闭存在公式是PA的一条定理。当我们考察全称公式时，麻烦就来临了。如果我们通过补上表示某个（原始）递归函数的新函数符号，再加上在PA中的这些函项的定义为公理，在扩充了的理论中，哥德尔的一个真的但不可证的句子的规范例子是一个
PA中证明全称句的主要工具是归纳簇，我们可以把它看作是理论的加强和减弱的原因，没有归纳，PA将被删削。此外，正如Ryll-Nardzewski使用了非标准模型证明的，他不存在有限归纳公理组能够代替完全归纳组。在一种意义上看，由于只存在可数多个公式，哪怕完全簇所含的公式也太少，但是要用到归纳的（非形式的）自然数的性质却是不可数的。这个基本冲突出现在非标准模型的存在和匹阿诺公理范畴性的非形式证明之间的矛盾之中。
因为它反过来可以得出：所得的ω - 逻辑对于研究标准自然数结构是一真正的传递思想的工具，这是在定理在PA中可证和公式在N中的真完全一致的意义之下。ω - 完全性定理的特殊情况可以陈述如下：
元定理：对自然数真但在（通常的）PA中不可证的任意公式，由于对无限多个“特殊情况”成立，它一定为真。
有理由怀疑：有某些PA中的全称句并非如此，它在N中成立只是通过吻合于无限多个内在的不同实例。值得注意的是ω - 完全性定理蕴涵了这样一种思想：这是仅有的对于的证明理论的不充分性的一个理由。
我们的论点：ω - 完全性定理，为理解哥德尔不完全性定理提供了最好的方法。下节将对之作详细的考察。
五、ω - 完全性和型的省略 ω - 完全性定理是由1931年哥德尔的文章中所采用的概念形成的，大约出现在25年以后。这个思想的发展历史涉及到一个有趣的值得大家批判地研究的主题，因而，重述它的发现，蛰伏，再发现，和应用是值得的。我们在这里对事件的过程作一概述。
罗塞尔的结果对令人窒息的ω - 概念是否有效是不清楚的；不管怎么说ω - 完全性定理的最早形式是由奥莱（Orey）在1956年，辛钦（Henkin）在1957年阐明的。一个“迅速”发展时期接踵而至，定理很快地重复出现在各种各样的外观之下，以致多种不同的被结合成了一种形式：
每个在数论语言中一致的，ω - 完全的理论有一个模型，它的论域精确地由解释常项符号n的元组成（一个所谓的ω - 模型）。
接下来的是平缓时期。伴随着模型论（当前逻辑学中最为活跃和最激励人的研究领域）的突飞猛进，定理经历了变化，成了省略型定理。后来，定理成了模型构造的重要工具。
六、证明长度 - 克来塞猜想和帕里的定理 前一节刻划的整个模型论的“酝酿时期”，在证明论方面也发生了一个平行的发展。在1936年，三篇重要的文章出现了，它们都以考察形式系统中证明的长度和复杂性为基础。罗塞尔改进不完全性定理的一篇已经提及。另外的是甘岑（Gentzen）关于算术一致性的证明，首次采用超限归纳法于推导的复杂性；和哥德尔本人写的简洁的很少引人注意的文章。后来简单地标以“论证明的长度”，它指出，通过对较高类型的系统（允许整数集，整数集的集等）考察，不仅可证新的定理，而且“缩短超长无限多有效证明成为可能了。”
只是到了1965年才被译成英文的，哥德尔的证明的长度的文章在计算机革命之前一直被忽视，当对计算的效力的关注导致M. 勃罗姆（Blwm）创造了计算复杂性理论时，哥德尔的证明缩短的成果才被重新重视，成了整个一类增速定理的先驱。克来塞和王浩的一些文章也研究了证明的缩短问题，他们考察了各种“长度≤n的证明”，包括至多n行的证明，所得的结果和哥德尔第二不完全性定理有关。
但在PA中，证明长度的界蕴涵在PA*中的译象证明长度相应的界是不清楚。帕里的定理我们说得较充分了，帕里的证明依赖较早的判定性结果。我们必须做最终的思考，数学文献已经含有用计算机论证极大数量状态而得到的证明的例子（最著名的是四色问题的最新解答），而数论史上关于不可解猜想的相似实例是众多的（费尔马大“定理”，哥特巴赫猜想等），它们通过各种方法被证明在许多特殊情况是成立的。这些著名猜想中的某些能否作为我们一直在讨论不可判定性现象的自然的实例呢？
（The American Mathematical Monthly，1980年11月）