希爾伯特計劃（）是由德國數學家大卫·希尔伯特在1920年代提出的一個數學計畫，旨在为数学基础危机提供解决方案。当时，早期澄清数学基础的尝试被发现存在悖论和不一致之处。作为解决方案，希尔伯特主张将所有现有理论建立在一个有限且的公理集之上，并证明这些公理具有一致性。他提出，像实分析这样的更复杂系统的一致性，可以通过更简单的系统来证明。最终，整个数学的一致性可以归结为基本算术的一致性。
1931年发表的哥德爾不完備定理指出，希爾伯特計劃在数学的关键领域是无法实现的。在第一定理中，哥德尔证明：任何具备可计算公理集且能够表达算术的一致系统，都不可能是完备的——总可以构造出一个命题，该命题可被证明为真，却无法从系统的形式规则中推导出来。在第二定理中，他进一步指出，这样的系统无法证明自身的一致性，因此当然不能用来确证任何更强系统的一致性。这驳斥了希尔伯特的假设，即一个有限主义系统可用于证明自身的一致性，并进而证明其他所有理论。
希尔伯特计划的陈述
这个计划的主要目标，是为全部的数学提供一个安全的理论基础。具体地，这个基础应该包括：
- 所有数学的形式化。意思是，所有数学应该用一种统一的严格形式语言，并且按照一套严格的规则来使用。
- 完备性。我们必须证明以下命题：在形式化之后，数学里所有的真命题都可以被证明（根据上述规则）。
- 一致性。我们必须证明：运用这一套形式化和它的规则，不可能推导出矛盾。
- 保守性。我们需要证明：如果某个关于“实际物”的结论用到了“假想物”（如不可数集合）来证明，那么不用“假想物”的话我们依然可以证明同样的结论。
- 确定性。应该有一个算法，来确定每一个形式化的命题是真命题还是假命题。
哥德尔不完备定理
库尔特·哥德尔表明，希尔伯特计划的大部分目标都是无法实现的——至少在最直接的解释下是如此。哥德尔第二不完备定理指出，任何足够强大、能够编码整数加法与乘法的一致理论，都无法证明自身的一致性。这对希尔伯特计划构成了挑战：
*不可能在一个形式系统中将所有数学真命题都形式化，因为任何这样的形式化尝试都必定会遗漏某些真的数学命题。即便是皮亚诺算术，基于可计算枚举的公理集，也不存在任何完备且一致的扩张。
*像皮亚诺算术这样的理论甚至无法证明自身的一致性，因此它的一个受限的“有限主义”子集当然更不能证明诸如集合论等更强理论的一致性。
*在皮亚诺算术的任何一致扩张中，都不存在能够判定其中语句真值（或可证明性）的算法。严格来说，这一对判定问题的否定解出现在哥德尔定理发表几年之后，因为当时算法的概念尚未得到精确界定。
后哥德尔时代的希尔伯特计划
当前数理逻辑中的许多研究方向，例如证明论和逆数学，都可以视为希尔伯特原初计划的自然延续。通过略微调整其目标，该计划的大部分内容仍可得以保留（Zach 2005），并且在以下修改下，其中的一部分已成功完成：
*尽管不可能形式化所有数学，但基本上所有人们实际使用的数学都是可以形式化的。特别是策梅洛-弗兰克尔集合论，结合一阶逻辑，为当今几乎所有的数学提供了一种令人满意且被普遍接受的形式化体系。
*尽管对于至少能表达皮亚诺算术（或更一般地，具有可计算公理集）的系统无法证明其完备性，但对于许多其他有趣的系统，仍可以证明其某种形式的完备性。一个已经证明具有完备性的非平凡理论的例子是：给定特征的代数闭域理论。
*关于强理论是否存在有限主义一致性证明的问题，答案难以确定，这主要是因为“有限主义证明”本身尚无公认的定义。证明论领域的大多数数学家认为有限主义数学被包含在皮亚诺算术之中；若如此，则对于足够强的理论，不可能给出有限主义证明。另一方面，哥德尔本人曾建议，可以使用无法在皮亚诺算术中形式化的有限主义方法来给出有限主义一致性证明，因此他似乎对有限主义方法允许的范围持更为宽松的看法。几年后，根岑给出了。该证明中唯一明显不属于有限主义的部分是某一到序数ε0的超限归纳法。如果将这一超限归纳法接受为有限主义方法，那么就可以断言存在皮亚诺算术一致性的有限主义证明。更强大的子集，已被竹内外史等人给出了一致性证明；至于这些证明究竟在多大程度上属于有限主义或构造主义，人们仍然可以继续争论。（通过这些方法证明一致性的理论相当强，并且包含了大多数“普通”数学。）
*尽管皮亚诺算术中不存在用于判定语句真假的算法，但许多有趣且非平凡的理论已经找到了这样的算法。例如，塔斯基发现了一种能够判定解析几何中任何语句真假的算法（更精确地说，他证明了实闭域理论是可判定的）。根据，该算法可以被视为判定欧氏几何中任何语句真假的算法。这一点意义重大，因为很少有人会认为欧氏几何是一种平凡的理论。
參見
*希爾伯特第二問題
*哥德尔不完备定理
参考资料
G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen 112:493–565. Translated as 'The consistency of arithmetic', in The collected papers of Gerhard Gentzen*, M. E. Szabo (ed.), 1969.
D. Hilbert. 'Die Grundlegung der elementaren Zahlenlehre'. Mathematische Annalen 104:485–94. Translated by W. Ewald as 'The Grounding of Elementary Number Theory', pp. 266–273 in Mancosu (ed., 1998) From Brouwer to Hilbert: The debate on the foundations of mathematics in the 1920s*, Oxford University Press. New York.
S.G. Simpson, 1988. [https://www.personal.psu.edu/t20/papers/hilbert-jsl-1988.pdf Partial realizations of Hilbert's program (pdf)]. Journal of Symbolic Logic* 53:349–363.
R. Zach, 2006. Hilbert's Program Then and Now. Philosophy of Logic* 5:411–447, [https://arxiv.org/abs/math/0508572 arXiv:math/0508572] [math.LO].
外部連結
*
评论 (0)