【摘 要】基于当前文献中对数学深度的研究，我们没有一个判断给定数学定理是否深刻的被广泛接受的一般标准。不完全性定理被广泛认为是逻辑领域“深刻”的数学定理。本文将不完全性定理作为研究数学定理的深度的一个案例。本文研究如下两个关于不完全性定理的深度的问题：刻画不完全性定理的深度的标准是什么，如何基于这些标准论证不完全性定理的深度。基于文献中最新研究成果，我们提出三个刻画不完全性定理的深度的标准：成果的影响力、结论的丰富性、理论的统一性； 并基于这三个标准论证不完全性定理的深度。

【关键词】不完全性定理、数学深度、不完全性的限度、内涵性问题

 

一、导论

在评价同行的研究成果时，我们常使用“深刻”这个词形容成果的“深度”。本文对“深度”的讨论限定于数学定理。对于何谓“深刻的数学定理”，学界有不同的看法。即使人们对某一定理是否深刻达成共识，人们对此定理“为何深刻”的理由仍可能有不同的看法。文献中关于数学定理的深度的哲学讨论中，人们讨论得最多的四个问题是：（1）对给定的定理，对其是否深刻学界是否达成共识？（2）深刻的数学定理是否具有某些共同特征？（3）“深度”和其他一些概念间的区别：如丰富性、重要性、难度、基础性、解释力、优美性等。（4）数学深度是数学定理内在的客观特征还是与我们的兴趣和能力紧密相关的？对“数学深度”这一概念，我们没有精确的定义，目前也没有一个判断给定数学定理是否深刻的被广泛接受的一般标准。被认为深刻的数学定理可能具有不同的特征，不同的定理可能有刻画它们的深度的不同标准。虽然我们很难给出一个判定任意给定的定理是否深刻的一般标准，一个自然的问题是：对于被学界公认为“深刻”的单个数学定理，我们能否找到刻画此定理的深度的一些标准，并基于这些标准论证此定理的深度。

 

哥德尔是20世纪最伟大的逻辑学家，他最重要的成果是于1931年发表的不完全性定理。不完全性定理是20世纪最重要深刻的发现之一，是现代逻辑发展史上重要的里程牌，它对逻辑学、哲学、数学、理论计算机科学等领域的发展产生了广泛、深刻而持久的影响，极大的改变了1931年之后数学基础研究的面貌。不完全性定理被广泛认为是逻辑领域“深刻”的数学定理。本文的目标不是给出一个判断数学定理是否深刻的一般标准。相反，本文的策略是将不完全性定理作为研究数学定理的深度的一个案例，希望通过对此案例的深入分析，加深我们对“数学深度”这一概念的理解。本文集中于研究这样两个关于不完全性定理的深度的方法论问题：刻画不完全性定理的深度的标准是什么，如何基于这些标准论证不完全性定理的深度。基于文献中的最新研究成果，我们提出三个刻画不完全性定理的深度的标准：成果的影响力、结论的丰富性、理论的统一性；并基于这些标准论证不完全性定理的深度。在哥德尔不完全性定理发表90周年之际，我们以此文纪念哥德尔这一伟大的学术成果，并以尽量非形式的语言向国内同行介绍哥德尔之后国际学界关于不完全性定理研究的新进展。

 

二、不完全性定理

本节我们简要介绍不完全性定理的内容及其证明的主要思想。我们先解释若干文中用到的概念。一个形式理论包括如下基本构件：形式语言、公理、推演规则。形式理论的形式语言包括符号表和公式的形成规则。 符号表包括逻辑符号与非逻辑符号。有限个符号构成符号串。公式是一类根据形成规则递归定义的“有意义”的符号串。公理是一类特殊的公式（包括逻辑公理和非逻辑公理），是此理论中演绎推理的出发点。推演规则告诉我们如何由给定的一些公式推出其他公式。 给定理论   及   语言中的公式  ，我们可定义何谓“  在理论   中是可证的”(记为T├A)： 存在一个有限的公式序列，使得此序列的最后一个公式是   ，对此序列中的任意公式   ，   或者是理论   的公理，或者是由此序列中公式   前面的公式使用某种推演规则而得到的。皮亚诺算术PA，罗宾逊（Robinson）算术Q和理论R是不完全性研究中三个重要的形式理论。 

算术化是数理逻辑中的一种重要方法。它的思想是给形式理论的符号表编码，建立符号和自然数间的一一对应。因有限的自然数序列可被单个自然数编码，我们可建立符号串和自然数间的一一对应。这样符号串上的关系和运算就可转换为自然数上的关系和运算。通过算术化，任何公式或公式序列都可被一个自然数编码（称为哥德尔编码）。

我们称理论  是递归可公理化的，若  公理的哥德尔编码集是递归集（直观的说，存在一个能行的算法使得任给理论   语言中的公式   ，此算法可判定   是否是   的公理)。我们称理论   是一致的，若不存在公式   使得   和   都在   中可证。我们称理论   是完全的，若对理论   语言中的任意公式   ，或者   在   中可证，或者   在   中可证。我们称   是   的不可判定命题，若   和   都是在   中不可证的。因此，理论T是不完全的当且仅当存在T中的不可判定命题。下文中，若未作特殊说明，我们假设理论   是Q的递归可公理化的一致扩充。我们用[n]表示自然数   在   的语言中所对应的项。给定T语言中的公式ϕ，我们用[ϕ]表示ϕ的哥德尔编码在T的语言中所对应的项。

哥德尔在证明不完全性定理时使用的是罗素-怀特海《数学原理》中的形式系统P，其是基于戴德金-皮亚诺算术公理及自然数序列的简单类型理论。哥德尔1931年发表的第一不完全性定理的原始形式是：对任何由形式系统P基础上增加一递归的公理集而形成的具有与P相同语言的形式理论   ，若   是   -一致的，则   是不完全的。哥德尔没有发表第二不完全性定理的证明细节，而只是宣告了这一结果：我们无法在系统P内证明系统P的一致性。不完全性定理的原始表述受囿于很复杂的系统P及其语言，后人的研究极大的改进了此定理的表述形式。下面是现代版本的哥德尔不完全性定理：

第一不完全性定理 令   为Q的递归可公理化的扩充。若   是   -一致的，则   是不完全的。

第二不完全性定理 令   为Q的递归可公理化的扩充。若   是一致的，则“   的一致性”在   中不可证。

哥德尔第一不完全性定理证明的三个主要思想是：算术化、可表示性、自指构造。假设理论   是Q的递归可公理化的扩充。通过算术化，我们可以建立   的语言中的表达式和自然数间的一一对应。在此对应下，我们可将关于理论   的系统性质的命题转换成关于自然数的命题。哥德尔证明了：所有的递归关系都是在Q中可表示的。因此，关于理论   的系统性质的递归关系是在Q中可表示的，从而在Q中有对应的表示公式。这样，我们可以在Q内“谈论”理论   的系统性质，这是算术化思想的本质。

下面，我们给出现代版本哥德尔不完全性定理的证明概要。通过算术化，我们可定义表达理论   内演绎证明的自然数集上的关系。例如，我们可定义自然数集上的如下二元关系：   成立当且仅当   是编码为   的公式在   中的一个证明的编码。 我们可以证明，关系   是递归的。因递归关系都在Q中可表示，令   是   在Q中的表示公式。由证明谓词   我们可定义可证谓词   。最后，哥德尔构造了语句G（称为哥德尔语句），其断定自身在   中不可证。哥德尔证明了：若   是一致的，则G在   中不可证；若   是   -一致的，则   也在   中不可证。 因此，则若   是   -一致的，则   是不完全的。

由可证谓词我们可定义一致性命题   ；   是一算术语句，其含义是形如0=1的矛盾式在T中不可证。 如上构造的可证谓词   称为标准可证谓词。我们称由标准可证谓词   构造的语句   为典范一致性命题。本文中，若未作特别说明，我们假定是用   来表达理论   的一致性。由标准可证谓词   的性质，我们在中可证明G是等价于   。由此，我们得到第二不完全性定理：若   是一致的，则   在   中不可证。

哥德尔第一不完全性定理的证明假设   是   -一致的。罗瑟（Rosser）1936年改进了哥德尔的结果。罗瑟的证明仅假设理论   是一致的，而“一致”是比“   -一致”更弱的条件。

罗瑟第一不完全性定理 若   是Q的递归可公理化的一致扩充，则   是不完全的。

我们强调哥德尔和罗瑟的第一不完全性定理间的区别。下文中，我们用G1表示罗瑟第一不完全性定理，G2表示第二不完全性定理。下面，我们分别基于成果的影响力、结论的丰富性和理论的统一性这三个标准论证不完全性定理的深度。 不完全性定理满足这三个标准的数学证据有很多，限于篇幅，本文我们将只讨论关于这三个标准的最重要的数学证据。

 

三、成果的影响力

本节中，基于哥德尔之后人们对不完全性定理的研究成果，我们分析不完全性定理对数学基础、哲学、经典数学及理论计算机科学的影响。事实上，深入分析不完全性定理对这里任何一个领域的影响都需要专著的篇幅。 这里我们不可能讨论不完全性定理对这些领域各个方面的影响，而只能概述不完全性定理对这些领域的影响的主要方面。

不完全性定理对数学基础的影响主要体现在如下五个方面。第一，不完全性定理揭示了在逻辑和数学中普遍存在的不完全性现象。 不完全性定理告诉我们任何包含足够算术信息（如Q）的递归可公理化的一致理论都存在不可判定命题（即“遗漏”一些算术真理）。哥德尔构造的不可判定命题是纯粹的逻辑构造，没有自然的数学含义。在这个意义上，我们可以说哥德尔的证明揭示了PA的逻辑不完全性。 在哥德尔之后，一个重要的问题是：PA是否也是数学上不完全的？是否存在具有实在数学含义的不可判定的算术命题（如数论、组合中的命题）？在哥德尔之后，人们在经典数学中发现了很多具有实在数学含义的在PA中不可判定的算术命题。这些发现揭示了比一阶算术更强的形式理论（如高阶算术和公理集合论ZFC）的数学上的不完全性。例如，哥德尔和柯恩证明了连续统假设是独立于ZFC的。事实上，人们在很多数学领域中（如分析、代数、拓扑、数理逻辑等）发现了大量具有实在数学含义的在ZFC中不可判定的数学命题。

第二，不完全性定理在一定意义上揭示了形式化方法（或形式理论）的本质局限性。形式化方法是一种在逻辑与数学中广泛使用的方法。 不完全性定理揭示了包含Q的递归可公理化的一致理论的证明能力的限度。不管理论   有多强，只要   是递归可公理化的一致理论且包含足够的算术信息（如Q），总存在理论   中的不可判定命题。 若命题   在理论   中是不可判定的，我们总可找到比理论   更强的递归可公理化的一致理论   使得命题   在   中可证。然而，不完全性定理告诉我们，虽然理论   中的不可判定命题   在理论   中可证，但是理论   仍然存在不可判定命题。因此，不管我们怎么增强理论   ，只要   包含足够的算术信息，它的任意递归可公理化的一致扩充都存在不可判定命题。Q是很弱的算术理论，因此我们可以说不完全性定理揭示了大多数形式理论的证明的限度。

第三，不完全性定理揭示了“真”和“可证”这两个概念间的本质区别。在不完全性定理之前，人们普遍认为一个数学命题为真和其可证是相同的概念。特别的，一算术命题为真是指其在算术的标准模型下为真，一算术命题可证是指其在PA中可证。不完全性定理揭示了“可证”和“为真”这两个概念间的本质区别：在PA中可证的算术命题都为真，但存在在PA中不可判定的算术真命题。

第四，不完全性定理否定了怀特海-罗素的一种强版本的逻辑原子主义纲领：数学可以还原为逻辑。强版本的逻辑原子主义纲领包含两个基本观点：数学语言可还原为逻辑语言，数学定理可还原为逻辑证明。 这种强版本的逻辑原子主义纲领期望建构一种形式系统使得在其中可以形式化全部数学理论，且可证明所有的数学真命题，从而表明数学可还原为逻辑。G1直接否定了这种强版本的原子主义纲领：不存在一种形式理论在其中可以证明所有的数学真理。

第五，不完全性定理对希尔伯特纲领的发展产生了深刻的影响。希尔伯特纲领的一个主要目标是用有限性方法证明数学理论的一致性。人们常认为G2直接否定了希尔伯特纲领。 然而，学者们对此有不同的看法。对于“有限性方法”这个概念，我们没有精确的定义；对于何谓“有限性方法”，人们有不同的看法。若“用有限性方法证明算术的一致性”是指算术的一致性在PA中可证，那么在这种意义上，我们可以说G2直接否定了希尔伯特纲领的这个目标。若我们将可数序数长度的超穷归纳法也视为“有限性方法”，则根岑（Genzen）的结果表明，我们可在某种比PA稍强的理论中使用有限性方法证明PA的一致性。因此，G2并非完全否定了希尔伯特纲领，而是表明了希尔伯特纲领应用范围的限度（其全局的实现是不可能的）。在不完全性定理之后，希尔伯特纲领得到了很好的局部实现。关于希尔伯特纲领的后续发展及其对数理逻辑（特别是证明论）和数学哲学的影响，文献中有大量的讨论。

下面我们讨论不完全性定理对经典数学的影响。不完全性定理是原创性的数学成果。一种流行的看法是：不完全性定理的证明使用的是纯逻辑的方法，与经典数学没有什么关联。在不完全性定理的证明中，哥德尔语句是纯粹的逻辑构造，没有实在的数学含义，其表达的不是关于自然数的算术性质，而是关于算术形式理论自身的性质。在哥德尔之后，一个自然的问题是： 我们能否找到具有实在数学含义的不可判定的算术命题？我们称由具有实在数学含义的不可判定命题所揭示的不完全性现象为具体不完全性。事实上，具体不完全性在数学中是普遍存在的。在哥德尔之后，人们发现了很多在PA中不可判定的具有实在数学含义的算术语句。这些语句的构造没有使用算术化方法和可证谓词，但比哥德尔语句更复杂：哥德尔语句在PA中是等价于典范一致性命题   ；而这些语句在   中也是不可判定的。

哈维-弗里德曼（Harvey Friedman）是具体不完全性研究的国际知名专家。他的工作将具体不完全性的研究从一阶算术扩充到高阶算术和集合论。在他的关于具体不完全性的专著“布尔关系理论与不完全性（Boolean Relation Theory and Incompleteness）”中，他发现了很多在高阶算术的不同层级中不可证的关于算术和分析的数学定理的例子。

和其他数学定理不同的是，不完全性定理的影响力并非仅限于数学家和逻辑学家的圈子，它在哲学中也有广泛的影响。自其发表以来，不完全性定理引发了与其相关的一些哲学问题的广泛而持久的讨论：如人类智能与机器智能的本质及其区别，机器智能的限度等。限于篇幅，本文无法讨论哥德尔的哲学思想及其对发现不完全性定理的影响。这里我们重点讨论两个与不完全性定理紧密相关的哲学论题：反机械主义论题和哥德尔析取论题。

现有文献中有不少关于不完全性定理对“人类心智是否可机械化”这一哲学问题的影响的讨论。反机械主义论题认为人类心智是不可机械化的。单独个体的心智能力是很有限的，这里我们不是考虑单独个体的心智能力，而是考虑理想化的人类心智本质上可以做什么。人类心智包括很多维度，这里我们仅考虑人类心智的数学输出：即人类心智所能认识的数学真理。图灵提出了一种计算模型：图灵机，并通过此模型给出“可机械化”概念一种精确的数学刻画。反机械主义论题可更精确的表述为：人类心智的数学输出超越任何图灵机的数学输出。这里，我们不讨论“人类心智是否可机械化”这个一般的哲学问题，而仅讨论不完全性定理与反机械主义论题间的关联。对G1的一种流行解释是：G1蕴涵反机械主义论题。文献中有不少基于不完全性定理的支持反机械主义论题的论证，其中最著名的是卢卡斯（Lucas）论证和彭罗斯（Penrose）论证。卢卡斯论证在文献中被广泛的批评。彭罗斯提出一个比卢卡斯论证更复杂精细的支持反机械主义论题的论证。彭罗斯论证是文献中被广泛讨论、仔细分析的支持反机械主义论题的最复杂、最有前景的一个论证。文献中最新研究表明，认为G1蕴涵反机械主义论题的论证是源于对不完全性定理的某些误解。现今绝大多数哲学家和逻辑学家认为卢卡斯论证和彭罗斯论证及其变体都不是令人信服的。然而，人们在对卢卡斯论证和彭罗斯论证的错误根源的认识上存在分歧。克拉耶夫斯基（Krajewski）在最近的文章中详细讨论了基于不完全性定理的反机械主义论证的历史，仔细分析了卢卡斯论证和彭罗斯论证的问题所在，并得出“G1并非蕴涵反机械主义论题”的结论。

哥德尔本人并不认为不完全性定理蕴涵反机械主义论题，尽管他相信人类心智是不可机械化的，且可认识所有的数学真理。哥德尔相信，与图灵机相比，人类心智的独特之处在于它能提出新公理，建构新的数学理论。基于他的理性乐观主义，哥德尔相信人类心智能够认识所有的算术真理。然而，哥德尔承认，他既不能给出“人类心智不可机械化”的令人信服的论证，也不能给出“不存在绝对不可判定命题”的令人信服的论证。哥德尔认为，从不完全性定理他至多可得出如下一个更弱的结论（称为哥德尔析取论题(GD)）：若人类心智是可机械化的，则存在绝对不可判定命题（即人类心智无法认识的数学命题）。在哥德尔看来，GD是可由不完全性定理推导出来的有哲学意义的数学定理。

科尔纳（Koellner）对GD的分析是现有文献中对此论题的最全面精确的分析。 科尔纳认为，要精确的讨论GD并证明不完全性定理蕴涵GD，首先得在恰当的形式理论中形式化GD。科尔纳构造了理论DTK，在DTK中形式化GD，并证明了如下结果：（1）GD在DTK中可证；（2）卢卡斯论证和彭罗斯论证在DTK中都不成立；（3）GD的两个析取支命题“人类心智不可机械化”和“存在绝对不可判定命题”在DTK中对应的形式化命题在DTK中都不可证。

最后，我们简要讨论不完全性定理对理论计算机科学的影响。理论计算机科学研究计算的能力和限度。不完全性定理的证明中包含若干可计算性理论的重要想法。哥德尔在证明不完全性定理中使用的原始递归函数和算术化方法是理论计算机科学研究中两种很重要的工具。 原始递归函数概念是在哥德尔之后发展起来的递归论这一数理逻辑分支的基础概念和理论基石之一。算术化方法的思想是用自然数来给形式理论的一些语法对象如项、公式、证明等编码。 算术化方法在理论计算机科学研究中是种很关键且有用的技术。在理论计算机科学中，否定性结果构成一种很重要和独特的传统。不完全性定理是否定性结果的一个范例。在不完全性定理之后，人们发现了很多逻辑中的重要否定性结果，如塔斯基真不可定义定理、连续统假设独立性定理等。在理论计算机科学中，否定性结果的一个典型例子是图灵停机问题不可判定性定理。图灵停机问题和不完全性定理也有紧密的关联。更多关于不完全性定理对理论计算机科学的影响的讨论，参见研究文集“哥德尔与数学基础：真的视野”。

 

四、结论的丰富性

本节我们从结论的丰富性的标准论证不完全性定理的深度。本文中，定理结论的丰富性是指此定理及其证明可派生出的肯定性或否定性结果的多样性。 我们从如下三个方面论证不完全性定理的结论丰富性：不完全性定理的不同证明，不完全性定理的可推广性（在何种程度上不完全性定理可被推广），不完全性定理成立的限度（在何种情形下不完全性定理不成立）。

不完全性定理结论的丰富性的第一个标志是证明方法的多样性。哥德尔之后，人们发现了很多不完全性定理的不同证明。我们称G1的证明是构造性的，若存在一个能行的算法将不可判定命题显式地构造出来。G1的非构造性证明仅断定不可判定命题的存在，但没有能行地将此不可判定命题显式地构造出来。我们称G1的证明具有罗瑟特征，若它的证明仅需假设   是一致的，而不需假设更强的结论（如   是   -一致的）。

我们可依据如下特征对文献中的不完全性定理的不同证明进行分类：使用证明论方法、使用递归论方法、使用模型论方法、使用算术化方法，使用对角线引理、使用逻辑悖论、使用构造性证明、具有罗瑟特征、使用柯尔莫哥洛夫（Kolmogorov）复杂性、构造有实在数学含义的不可判定命题。不完全性定理的一种证明可能具有若干以上特征。以上这些特征都不是证明不完全性定理的必要条件： 我们既可找到具有这些特征的不完全性定理证明的例子，也可找到不具有这些特征的不完全性定理证明的例子。 哥德尔第一不完全性定理的证明具有如下特征：使用了算术化等证明论方法，没有直接使用对角化引理、证明是构造性的、不具有罗瑟特征、哥德尔语句类似于说谎者悖论中的说谎者语句，哥德尔语句没有实在的数学内容。不完全性定理的这些不同的证明方法揭示了不同领域间的关联：证明论、递归论、逻辑悖论、模型论、柯尔莫哥洛夫复杂性、数论等。

不完全性定理结论的丰富性的第二个标志是它具有多种推广形式。G1和G2都既可推广到PA的扩充理论也可推广到PA的子理论。不完全性定理这些丰富的推广形式揭示了不完全性定理的解释力量和广泛的可应用性。这里我们简要给出G1的两类推广形式的例子。

第一，G1也可推广到一些非递归可公理化但算术可定义的一致理论。G1告诉我们，PA的任意递归可公理化的一致扩充都是不完全的。但在一定条件下，这一结论可推广到PA的一些非递归可公理化但算术可定义的扩充理论。

第二，通过解释的概念，G1可推广到很多具有不同语言的一致理论。我们可定义G1对一致理论   成立当且仅当对任意递归可公理化的一致理论   ，若   在   中可解释，则   是不完全的。我们知道G1对PA成立。我们可证明G1对很多解释度比PA弱的理论也成立。例如，G1对Q和R都成立。理论R在解释度意义上比Q弱，人们常认为理论R是使得G1成立的在解释度意义上的最弱理论。事实上，G1对很多在解释度意义上比理论R弱的理论也成立。

G2也有多种推广形式，这里我们仅举两个典型例子。首先，我们可通过解释的概念推广G2。一个经典的结论是：不存在递归可公理化的一致理论   使得   在   中可解释。由此可得，对任意递归可公理化的一致理论   ，若Q在   中可解释，则G2对   成立（即   在   中不可证）。 其次，洛布（Löb）定理是G2的一种重要推广形式：对Q的任意递归可公理化的一致扩充理论   ，对任意标准可证谓词   和公式   ，若“ϕ在T中可证蕴涵ϕ”在T中可证，则ϕ在T中可证。由此可得，G2对   成立。

最后，我们讨论关于不完全性定理的否定性结果：不完全性定理成立的限度。对不完全性定理成立的范围的研究揭示了不完全性定理可应用性的限度，极大的更新了我们对不完全性定理可应用范围的理解，提供了论证不完全性定理的结论丰富性的数学新证据。

我们先讨论G1成立的限度。首先，很多一致的理论是完全的。其次，一算术理论是否完全与理论的语言有关。在语言   中，PA是不完全的。但在语言   和   中分别存在递归可公理化的完全的算术理论。关于G1是否成立与理论的语言的关系，我们作如下几点说明：第一，包含足够的关于算术的信息对于证明G1是必要的。例如，欧几里得几何不是关于算术而是关于点、线、面的理论，塔斯基证明了欧几里得几何是完全的。第二，包含关于算术的乘法信息对于证明G1是必要的。若一理论只包含关于算术的加法信息而不包含关于算术的乘法信息，其可能是完全的。例如：普雷斯堡(Presburger)算术是关于算术的加法的理论，但其是完全的。

我们知道，G1对Q的某些算术可定义的一致扩充成立。但并非Q的所有算术可定义的一致扩充都是不完全的。我们已知很多使得G1成立的在解释度意义上比R弱的理论。当前的一个前沿问题是：是否存在使得G1成立的解释度意义上的极小理论。

下面我们讨论G2成立的限度。无论数学或哲学上，G2与G1是本质上不同的。它们的区别在于：对于G1，要证明一理论是不完全的，仅需证明存在一不可判定命题即可，我们并不关心此命题的内容（此命题并不必须是关于此理论的系统性质）。而对于G2，我们要证明   的一致性在   中不可证，就需恰当的形式化“   的一致性”这个概念。因此，对于G2，我们需关心如何在   中表达   的一致性。我们称G2对理论   成立，若“   的一致性”在   中不可证。然而，这个定义是模糊的。G2对理论   是否成立取决于我们如何在   中形式化“   的一致性”。我们称这一现象为G2的内涵性问题。在我们可不使用算术化和可证谓词等纯逻辑方法来构造有实在数学含义的不可判定命题的意义上，我们可以说G1是外延性的。然而，G2是内涵性的，与G1有本质的区别。如我们下面将讨论的，G2对理论  是否成立取决于很多因素。现有文献中有不少关于G2的内涵性问题的讨论。

我们称公式   是理论   公理集的表示公式，若对任意的自然数   , PA├ϕ([n])当且仅当   是   的某一公理的编码。若未作特殊说明，下文中我们作如下假设：（1）理论   是Q的递归可公理化的一致扩充；（2）我们使用典范一致性命题Con(T)表达理论T的一致性；（3）我们默认使用哥德尔编码法；（4）我们使用的可证谓词是标准可证谓词；（5）理论   公理集的表示公式是   公式。

基于文献中关于不完全性的研究，下面我们说明G2对理论   是否成立取决于如下因素：(1) 理论   的选择；(2) 表达一致性的方式；(3) 可证谓词的选择；(4) 编码方法的选择；(5) 理论   公理集的表示公式的复杂性。

对这些因素作两点说明：第一，这些因素间不是完全相互独立的，但它们强调的侧重点有所不同。例如，给定一种表达一致性的模式，选择不同的可证谓词也导致不同的表达一致性的方式。但(2)强调的是表达一致性的整体方式，而不是具体可证谓词的选择。而(3)强调的是具体可证谓词的选择。第二，当我们讨论G2是否成立是如何取决于某种因素时，我们是假定其他的因素以我们如上假设的方式保持不变，而仅讨论此种因素的变动是如何影响G2是否成立的。以因素(2)为例，当我们说G2对理论   是否成立取决于表达一致性的方式时，我们是说：假设   是Q的递归可公理化的一致扩充，使用的是标准可证谓词和哥德尔编码法且   公理集的表示公式是   公式，不同于典范一致性命题的表达一致性的方式可能会导致G2不成立。

下面我们简要讨论G2是否成立是如何取决于以上五个因素。第一，G2对理论   是否成立取决于理论   的选择。若理论   并非包含足够多的关于算术的信息，则G2可能不成立：即   的一致性在   中可证。例如，威拉德（Willard）研究G2对理论   不成立的边界情形，并构造了一些算术理论，它们不能证明后续函数是全函数，但可证明自身的一致性。

第二，G2对理论   是否成立取决于表达一致性的方法。何谓一个理论的一致性命题？不同学者有不同的看法。在研究文献中，我们常用理论   语言中的算术语句表达   的一致性。然而，仍存在不同于典范一致性命题的表达一致性的方法使得G2不成立：即在这种表达方式下，其对应的一致性命题在理论   中可证。

第三，G2对理论   是否成立取决于可证谓词的选择。维瑟（Visser）论证道，一致性命题不是一个绝对的概念，而是与可证谓词的选择有关。我们知道G2对标准可证谓词成立，即理论   的典范一致性命题在   中不可证。然而，对于非标准可证谓词，G2可能不成立。一种重要的非标准可证谓词是罗瑟可证谓词，其是罗瑟在证明G1时引入的。我们可证明，用罗瑟可证谓词表达的一致性命题在理论   中可证。

第四，G2对理论   是否成立取决于编码方法的选择。格拉布迈尔定义了一类可接受的编码方法，并证明了G2对这类可接受的编码方法是成立的；然而，格拉布迈尔指出，若一种编码方法是不可接受的，则G2可能不成立。

最后，G2对理论   是否成立取决于理论   公理集的算术复杂性。给定理论   公理集的表示公式，我们可定义其对应的可证谓词和一致性命题。 我们已知，若理论   公理集的表示公式是   公式，则其对应的一致性命题在   中不可证。若理论   的公理集具有不同复杂性的表示公式，则在此种表示公式下，G2可能不成立，即其对应的一致性命题可能在   中可证。例如，费弗曼构造了理论   公理集的一个复杂性为   的表示公式，使得其对应的一致性命题在   中可证，即G2不成立。

 

五、理论的统一性

下面，我们从理论的统一性的标准论证不完全性定理的深度。理论的统一性是指建立起的不同领域理论间的关联。下面我们从如下方面说明不完全性定理的理论统一性：经典数学与元数学（证明论）间的关联；不完全性与不可判定性理论间的关联；不完全性与逻辑悖论间的关联；不完全性与可证性逻辑间的关联；不完全性与真的形式理论间的关联。

哥德尔不完全性定理的证明使用了数学和逻辑的方法。例如，在哥德尔的证明中，他使用了如中国剩余定理和素数唯一表示定理之类的数论方法，及如算术化、可表示性、自指构造之类的元数学方法。前面我们指出，在哥德尔之后，人们发现了很多具有实在数学含义的在PA中不可判定的算术命题。 之前的讨论强调通过纯逻辑方法构造的不可判定命题与具有实在数学内容的不可判定命题间的区别。我们知道，哥德尔语句的构造使用了算术化方法，而具有实在数学内容的不可判定命题如佩尔斯-哈灵顿（Pairs-Harrington）语句的构造没有使用算术化方法。但一个有趣、令人惊讶的事实是，前面我们给出的具有实在数学内容的不可判定命题实际上是等价于某种可通过算术化方法来表示的元数学命题。这一事实揭示了经典数学中的具有实在数学含义的不可判定命题与元数学的算术命题间的关联。

最后，我们简要的讨论不完全性定理与不可判定性理论、逻辑悖论、可证性逻辑及真的形式理论间的关联。哥德尔的工作和可计算性理论及不可判定性理论间有紧密的关联。哥德尔的证明中包含了一些可计算性理论中一些重要思想的萌芽：如算术化方法、原始递归函数等。算术化方法和递归函数在递归论的发展中扮演了重要的角色。我们称理论   是实质不可判定的，若   的递归可公理化的一致扩充都是不可判定的。我们称理论   是实质不完全的，若   的递归可公理化的一致扩充都是不完全的。我们可证明，理论   是实质不可判定的当且仅当   是实质不完全的。这表明，完全性/不完全性与可判定性/不可判定性之间是紧密关联的。我们可通过停机问题的不可判定性证明G1和G2。这些都表明了不完全性定理和不可判定性理论间的紧密关系。

当前关于不完全性定理的研究揭示了不完全性定理是与逻辑悖论紧密相关的。哥德尔指出：“任何认识论上的悖论都可用来构造一个不可判定命题”。哥德尔语句使用的是“证明”概念，而说谎者悖论中的说谎者语句使用的是语义“真”概念。哥德尔语句可看作一种形式化版本的说谎者语句（用“可证”概念取代“真”概念）。除了说谎者悖论，还有很多其他的逻辑悖论可通过恰当的形式化被用来证明不完全性定理：如贝瑞（Berry）悖论，格林灵-纳尔逊（Grelling-Nelson）悖论，意外考试悖论，亚布洛（Yablo）悖论等。这些研究证实了哥德尔如上关于不完全性与逻辑悖论间的关联的观点。

作为对角化引理的应用，不完全性定理的一个重要的结论是塔斯基真不可定义定理。令算术可证集是所有在PA中可证的算术语句组成的集合，算术真语句集是所有在算术的标准模型中为真的算术语句组成的集合。不完全性定理揭示了算术可证集是算术真语句集的真子集。由塔斯基真不可定义定理，算术真语句集在算术的标准模型中是不可定义的。算术可证集在算术的标准模型中是可定义的，但不是递归集。维瑟由塔斯基真不可定义定理给出G2的一个非自指性证明。这些研究揭示了不完全性定理与塔斯基真不可定义定理间的关联。

可证性逻辑是研究不完全性及算术的元数学的一种重要且有用的工具。历史上，可证性逻辑的起源与不完全性定理紧密相关，如亨金（Henkin）问题，可导性条件，洛布定理。在这种意义上，我们可以说不完全性定理是连接一阶算术和模态逻辑的一种桥梁。 算术解释的概念为我们提供了一种建立可证性逻辑和算术的元数学的关联的重要工具。令人惊讶的是，可证性逻辑GL和GLS的索洛维（Solovay）算术完全性定理刻画了算术可证集和算术真语句集间的区别。令   是Q的   -可靠的递归可公理化的扩充。GL的索洛维算术完全性定理告诉我们：对任意的模态公式   ，   在GL中可证当且仅当对任意的算术解释   在PA中可证。GLS的索洛维算术完全性定理告诉我们：对任意的模态公式   ，   在GLS中可证当且仅当对任意的算术解释   在算术的标准模型中为真。

我们知道不完全性定理（特别是G2）的证明取决于可证谓词的性质。可证性逻辑是关于可证谓词的性质的逻辑。不同的可证谓词可能对应不同的可证性逻辑。基于不同可证性谓词的可证性逻辑揭示了不同可证性谓词的性质。 可证性逻辑给我们提供了一种理解不完全性的新视角和重要的工具。

 

六、对本文分析的一些讨论

基于上文对不完全性定理的深度的分析，本节我们进一步讨论与数学定理的深度相关的一些问题。

第一，基于现有文献，我们没有一个判断数学定理是否深刻的一般标准。我们对“深刻”一词没有精确的定义，“数学深度”是个模糊的概念。一个自然的问题是：本文提出的分析论证不完全性定理的深度的三个标准是否也可看作判断数学定理是否深刻的一般标准呢？成果的影响力、结论的丰富性和理论的统一性，这三个特征中的任何单个的特征都不是判断一个数学定理是否深刻的充分条件。例如，有影响力的成果未必被公认为是深刻的；结论丰富的定理也未必被公认为是深刻的。关于成果的影响力、结论的丰富性和理论的统一性是否是判断一个数学定理是否深刻的必要条件，文献中是有争议的。本人倾向于认为这些特征都是判断一个数学定理是否深刻的必要条件。一个深刻的数学定理应具有这些特征，尽管人们在论证数学定理具有这些特征时可能使用不同的数学证据。一个支持这种观点的证据是：到目前为止，我们还没有发现一个不具有这些特征的数学定理被公认为是深刻的。另一个自然的问题是：虽然单个特征不是判断数学定理是否深刻的充分条件，成果的影响力、结论的丰富性和理论的统一性这三个特征的合取是否判断一个数学定理是否深刻的充分条件？对此，我们是不清楚的，虽然我们认为对于分析论证不完全性定理的深度而言，这三个特征已经足够。即使定理的深度仅可由成果的影响力、结论的丰富性和理论的统一性来刻画，我们可以比较具有这些特征的不同定理的深度吗？在本人看来，很难有一个统一的方法去比较不同数学定理的深度，虽然我们有可能比较两个十分相近的定理的深度。我们提出的三个标准（成果的影响力、结论的丰富性、理论的统一性）是定性而非定量的。关于影响力的大小、结论丰富性的程度及理论统一性的程度，我们无法有精确的界定。即使不同的定理都具有成果的影响力、结论的丰富性和理论的统一性这些特征，我们对这些特征的分析论证及其使用的证据也是不同的。因此，我们很难提出一个比较不同数学定理的深度的一般方法。

第二，定理的深度不是定理内在的本质特征，而是关于这个定理的研究实践的特征。数学定理的某些特征是定理内在的客观特征，如结论的语法复杂性、定理的逻辑强度等。但数学定理的深度刻画的是主体对数学定理的认知评价。因此，定理深度的评估与人们对定理的认知理解水平有关。在这种意义上，我们可以说定理的深度不是定理与生俱来的内在特征，而是在对此定理的研究实践中学术共同体对此定理达成共识的学术评价。

第三，定理的深度具有历史性和时间性。人们之前认为深刻的定理随着时间的推移可能不再被认为是深刻的。例如，在古希腊时代，人们认为“正方形的对角线的长度不是有理数”是个深刻的定理，然而，在今天这个定理被认为证明太简单而不再被认为是深刻的。一个定理的深度被广泛接受和认同通常是几代学者对此定理研究的结果。一个定理刚发表时人们可能并未充分意识到此定理的深刻涵义从而不被广泛认为是深刻的，然而其在后续研究实践中可能被广泛认为是深刻的。以不完全性定理为例，在哥德尔之后通过对不完全性定理的深入研究，人们才逐步全面的认识到不完全性定理成果的影响力、结论的丰富性和理论的统一性。哥德尔发表不完全性定理时可能他自己都没意识或预想到不完全性定理会对数学基础、哲学、经典数学和理论计算性科学产生如此重要、广泛和持久的影响；不完全性定理会有如此多的不同证明和推广形式，揭示出如此多的不同领域间的关联统一性，第二不完全性定理是否成立会取决于这么多的因素。在今天，不完全性定理的证明是本科高年级逻辑教材中的标准内容。哥德尔之后关于不完全性的一些研究在技术上比哥德尔的证明更加复杂（如关于具体不完全性的研究）。哥德尔之后人们对不完全性定理的研究已极大的更新和深化了我们对不完全性的理解，人们对不完全性定理理解的深度和广度已超过了哥德尔时代对此定理的理解。因此，若不完全性定理的深度仅与哥德尔的初始证明有关，而与哥德尔之后对此定理的研究实践无关，则我们可能不再认为不完全性定理是深刻的。最后，一个定理成果的影响力、结论的丰富性及理论的统一性都取决于对此定理的研究实践的发展水平。然而，研究实践是没有限度的；随着研究的深入，人们会发现关于不完全性定理成果的影响力、结论的丰富性及理论的统一性的更多的数学证据。

第四，对数学定理的深度的评价不应仅基于个体的兴趣和认知水平。因不同的个体对数学定理的深度可能有不同的判断。对同一个定理，有些人可能认为它是深刻有趣的，而其他人却可能不这样认为。对数学基础感兴趣的数学家更容易认为不完全性定理是深刻的；而对数学基础没有兴趣的数学家可能不认为不完全性定理是深刻的。虽然个体对一个数学定理是否深刻可能有不同的看法，但对一个学术共同体而言，对定理的深度的认识是可能达成共识的，从而可能是客观的。数学定理的深度应由定理所在领域的学术共同体来评价，而不是由所有的学术共同体来评价。例如，不完全性定理的深度不应由拓扑学家来评价，而应主要由数理逻辑学家来评价。本文中对不完全性定理成果的影响力、结论的丰富性和理论的统一性的分析都是基于研究文献中对不完全性定理研究的数学证据，而不是基于个人的偏好和兴趣，尽管我们对文献中关于不完全性定理的研究成果的知识是有限的，且因限于篇幅本文给出的数学证据也是有限的。从这个意义上，我们可以说本文对不完全性定理的深度的分析论证是客观的。

下面我们描述一个判定给定的数学定理是否深刻的实际程序。 给定某领域   中的数学定理   ，   是否深刻可由领域   中国际上最顶尖的专家组成的学术委员会来判定：学术委员会可先确定判定此定理   是否深刻的达成共识的标准（如本文提出的影响力、丰富性和统一性标准），再根据这些标准集体判定定理   是否深刻。

关于数学定理的深度，有很多问题值得后续研究：如刻画数学定理的深度的一般标准，比较不同定理的深度的方法及其可行性，数学定理的深度的客观性，数学定理的深度和其他对象（如证明、论文、项目、哲学命题等）的深度之间的区别、纯逻辑定理的深度与纯数学定理的深度的区别等。本文探讨的是不完全性定理的数学深度，至于不完全性定理是否有哲学深度及（若有的话）它的哲学深度表现在哪些方面，这些有待进一步研究。

本文中，我们将不完全性定理作为研究数学定理的深度的一个案例。我们研究刻画不完全性定理的深度的标准，及基于这些标准如何论证不完全性定理的深度。基于文献中最新研究成果，我们提出刻画不完全性定理的深度的三个标准：成果的影响力、结论的丰富性及理论的统一性，并论证了不完全性定理满足这三个标准。希望本文对不完全性定理的深度的分析，能提供我们分析“数学深度”的新视角。

 

作者简介：程勇，金沙集团1862cc成色教授。主要研究领域为数学基础、数理逻辑、数学哲学，特别研究两个核心概念：不完全性和大无穷。

文章来源：《哲学分析》, Vol.12, No.6, 2021年12月。因排版需要，此文符号略有改动且省略了原文的所有注释。