希尔伯特梦后百年

作者：张寅生

一、希尔伯特纲要 

    希尔伯特于1917年在苏黎世数学学会提出了数学公理化的主张。1922年。希尔伯特在汉堡的数学会议上提出了所谓的希尔伯特纲要。纲要的要点是：

   数学可以完全形式化；
   所以数学知识均可由有穷的公理系统的推到出来；
   证明系统应该实现不矛盾性（一致性、相容性）；
   系统内的命题可以被判定出真假。  

  ----这是一个美好的梦想。

   但是广为流传的说法是，1931年哥德尔《论〈数学原理〉及其相关系统的形式不可判定命题（I）》（汉语译文见张寅生著《证明方法与理论》，国防工业出版社，2015年）彻底击碎了希尔伯特之梦，因为哥德尔宣称任何一个相容性的证明系统，必然存在该系统不可证明或证伪的命题，即所谓的哥德尔第一不完备性定理。

现在，他身后的梦随风飘逝了吗？

在希尔伯特的墓碑上以铭文留给我们一句遗言：我们必须知道，我们必将知道！

现在，我们需要知道这个梦想的真实结局。

二、哥德尔之后实现希尔伯特之梦的两个方向

假如哥德尔第一不完备性定理成立，那么，希尔伯特纲要是否不可能实现呢？

细想一下，至少可以通过两条道路实现希尔伯特纲要!

第一条道路，可以通过建立公理集合论限制悖论的产生。因为证明哥德尔不完备性定理的哥德尔语句（如“此句不可证”）是悖论，可以通过消除悖论的方法得以解决。虽然解悖方法可以有多种，但是集合论公理系统是针对数学对象及其命题构建的，专门适用于数学证明。

第二条道路，在公理集合论的前提下，构造不同的证明系统，以此逐渐逼近希尔伯特梦想的目标。

这两条道路走下来，到今天差不多已近百年，应该说，极大地实现了希尔伯特的梦想，至少在理论和实践上证实了希尔伯特梦想是可实现的-----尽管需要剔除悖论。哥德尔第一不完备性定理提出时希尔伯特还活着，他略微退让了一下，以躲过哥德尔第一不完备性定理之类的难题------毕竟还有无数的数学命题不是哥德尔语句！

三、公理集合论的进化谱系

ZFC是第一个公理集合论，它几乎被当作公理集合论的标准。它是早于哥德尔不完备性理论之前（Z，1908，F，1922）提出的。Z代表策梅洛（Ernest Zermelo），F代表弗兰克（Abraham A Fraenkel）,C代表选择公理，这是斯克伦（Thoralf Skolem）在1922 补充的。截至当前，已有5个五个集合论公理系统，其概况如下，详情见《证明方法与理论》第13章：相容性理论（引自《蒯因文集第3卷》，涂纪亮、陈波主编，人民大学出版社，2007）

五个集合论公理系统一览

策梅洛（ZFC）：（1908-1922）

幂集公理，对集公理，分离公理，并集公理，外延公理，无穷公理，附加（除选择公理），替换公理，基础公理。

现代类型论（塔斯基、哥德尔，1931年起）：

概括公理，外延公理，附加（除选择公理），无穷公理。 

新基础（NF）：（蒯因，1937）

概括公理，外延公理。

数理逻辑（ML，蒯因，1940）：

概括公理，集合性分层的，外延公理。

冯·诺依曼-贝尔奈斯（von Neumann–Bernays–Gödel SetTheory，NBG，1925-1954）：

概括公理，幂集、对集、并集公理，外延公理，无穷公理，替换公理，基础公理；概括公理；替换公理。

这5个五个集合论公理系统能够完全克服至少哥德尔语句类型的悖论吗？可以。但是“杀伤力”仍然过大。虽然禁止了哥德尔语句进入证明系统，但是这些集合论公理没有一个标准甄别合理的“自引用”与悖论之间的界限。即使能够甄别，悖论有多种，尚没有彻底的悖论解决方案。因此，到目前为止，数学的证明系统仍有“孤岛”，证明系统不得不绕开它们。

四、哥德尔体系结构

根据哥德尔第二不完备性定理，一个证明系统的理论是否一致（不矛盾），不能在本系统中得以证明，而需在更强的证明系统中得以证明。设T₁和T₂ 分别是两个证明系统的理论（公理或定理）。那么，根据哥德尔第二不完备性定理，“T₁是一致的”如果在T₂ 中得证，…就说T₂强于T₁，写作T₁ ＜T₂。这样，如果构建了一个T的升序列T₁ ＜T₂＜……就构造了一个一致性强度不同的证明系统，这个系统可称之为哥德尔体系结构。事实上，经过若干年的努力，一个算术哥德尔体系结构已经构建起立了。

进一步的研究表明，算术公理系统除具有良序特征（即算术哥德尔体系结构的特征）外，一个证明系统对于所证命题的确定性也是显而易见的。令t表示为一个给定的数学定理，S_t 是证明t的最弱的二阶算术子系统，下列现象是可观察到的：

给定t，常常可以确定S_t（即所谓逆推）；即t® (S_t⊢t) ，且不存在S⊂S_t使得(S⊢t)。换言之，如果证明系统S_t足够小，那么更小的证明系统S就证明不出来t了。因此可以确定一个大小正好，恰好能证明t的证明系统S_t。这也是逆推数学的主要目标之一和核心思想之一。

关于“算术”概念需要明确一下。在数理逻辑之中，“算术的”是指命题不包含量词约束的。虽然算术公理系统很多都陈述有量词约束的命题，如一阶命题的,通常f是不含量词的；在这个意义上，"x$yf(x,y)是关于算术命题f的命题，仍视为算术命题。这样算术命题就完全等同于数学命题了。因此，数理逻辑学中的“算术的”在研究范围上看大致可以等同于（描述算术的数理逻辑语言所描述的）数学领域，除非有特别约定。

哥德尔体系结构目前构造了83个算术公理体系。由数学家Stephen. G.Simpson建于1997年的数学基础论坛（Foundation of Mathematics,FOM）是关于数学基础的论坛，目前由数学家Matin Davis主审。FOM授权我发布的当前的哥德尔体系结构目前构造了83个算术公理体系。详见《证明方法与理论》附录1，由我加了注释和解释。其弱于PA（皮亚诺算术公理系统），也就是由弱至强的前8个算术公理系统如下：

(1) PFA:Peano Functional Arithmetic:the system that removes induction from PA without adding exponentiation.  

(2) EFA: Exponential Function Arithmetic.

(3) SEFA:Superexponential FunctionArithmetic.  

(4) PRA:Primitive RecursiveArithmetic.

(5) RCA₀:Recursive ComprehensionAxiom,subscript，“0”indicates restrict induction.

(6) IΣ₂:Induction ofΣ₂,the subscript “2” indicates one occurance of $-" for the variable in a Skolem prenex form of the

induction formulas f:$z₁"z₂f (z₁,z₂).

(7) IΣ₃.:The same asIΣ₂with exception $z₁"z₂$z₃f (z₁,z_2,,z₃).

(8) PA:Peano Arithmetic.

五、结论

考虑到上述的算术公理系统远远超出了自然数结构，不但包括了传统的算术，还扩展到了超穷算术、高阶逻辑运算、图灵计算，计算对象除超穷数，还扩展到了拓扑点集，总之极大地扩展了公理系统。因此应该说，希尔伯特的梦想，除了少量的悖论孤岛命题结构之外（这在希尔伯特生前已经做了让步），已经基本实现了。