希尔伯特计划

D．希尔伯特在20世纪20年代初提出的一个证明数学理论的协调性、保卫古典数学的计划。

在19世纪末20世纪初，在康托尔集合论中发现了几个悖论，引发了第三次数学危机。为解决集合论悖论，E．策尔梅洛建立了集合论的公理系统，B．罗素创立了逻辑类型论，而以L．E．J．布劳维尔为代表的直觉主义者则从他们的直觉主义数学观出发重建数学。公理集合论和逻辑类型论，排除了已知的悖论，但并不能保证在系统中不会出现新的悖论，系统的协调性仍旧是一个待解决的问题。而按照直觉主义重建数学，就要排斥康托尔集合论和像排中律这样的逻辑规律，否定古典数学中的大量的非构造性定义和纯存在性证明，从而摈弃大部分古典数学成果。希尔伯特认为，直觉主义者采取的是错误的途径。他认为古典数学是“我们最有价值的宝藏”，康托尔集合论是数学精神最值得惊叹的花朵，是人类纯理智活动的一个最高成就，排中律是普遍有效的规律，禁止数学家使用排中律就如禁止天文学家使用望远镜。希尔伯特的立场是通过证明数学的协调性来保卫古典数学。证明一个理论的协调性的经典方法是给该理论构造一个模型。例如，在1899年，希尔伯特就在实数理论中为欧氏几何构造了一个模型。这是一种相对协调性证明，即把一个理论的协调性化归为另一理论的协调性。现在要彻底解决数学的协调性问题，就不能再用相对的证明方法。就集合论来说，集合论的协调性不可能化归于其它数学理论，同时希尔伯特认为在物理世界中找不到集合论的模型，因而要求给出直接的证明。于是希尔伯特提出了他的著名的协调性证明计划。

希尔伯特的证明计划分两步。第一步是把全部数学——事实上，主要考虑的是算术、分析和集合论，连同所用的逻辑推理规则，完全形式化，构成一个形式系统。一个数学理论的基本概念由形式系统中某些符号来表示，而公理则由符号的有穷序列来表示。构成形式系统的只是一些具体对象，即有穷多个符号，符号的有穷序列，以及若干条符号变换规则。并且，形式系统的构造满足能行性要求。例如，能够机械地检查，一给定的符号序列的序列是不是最后那个符号序列的一个证明。形式系统中的符号、规则等等都是一些无意义的对象，系统中的推导只是对具体的符号对象的操作，而完全不涉及符号的意义。能够把数学理论完全形式化，则是有赖于那时已经存在的逻辑形式系统，和算术、集合论等的公理化。第二步是证明，在这样的形式系统中，永远不可能导致矛盾，或者说，证明系统的形式协调性，即在系统中不存在一个公式(符号的有穷序列)A，A及其否定都是在系统中可(形式)证明的(或者，证明某个公式，比如，1=0在系统中是不可证的。)如果证明了形式系统是协调的，那么也就证明了原来那个有内容的数学理论是协调的。形式系统的协调性的证明，是在称为元理论的另一个有内容的理论中进行的。协调性的证明应当具有这样初等的性质，它的可靠性是无可怀疑的。因此，希尔伯特对元理论作了非常严格的要求，只能使用有穷主义方法，满足有穷主义性，从而可以在直觉上保证它是协调的。

在实现希尔伯特的计划努力中，W．阿克曼在1924年证明了，对归纳公理加上小的限制后的初等数论是协调的。按照希尔伯特的看法，只需要若干即将出现的纯粹算术的初等引理就能证明分析的协调性。但是，K．哥德尔1930年得到的不完全性结果表明，希尔伯特计划是实现不了的。按照王浩的说法，有穷主义方法“这个不明确的概念的最可能的解释是，它们大约相当于原始递归算术(自然没有量词)的一个弱的扩张。”因此满足有穷主义性要求的理论，可以在一阶皮亚诺算术PA之中表示。而哥德尔证明，一个包含PA的理论的协调性，是不能在该理论自身中证明的。根据哥德尔这个不完全性结果，有穷主义方法甚至对证明一阶皮亚诺算术的协调性也是不够的。因此必须放宽对元理论的要求，允许使用比有穷主义方法更强的方法。在放宽对元理论的有穷主义性要求之后，哥德尔，G．根岑等人用不同方法证明了初等数论的协调性。

但是，希尔伯特最初设计的计划虽然行不通，不能实现，这个计划的提出仍然具有重要的意义，对数学和逻辑的发展都有重大的影响。其中最直接的结果就是证明论这个数理逻辑分支的形成和发展。