希尔伯特计划 program in the foundations of mathematics (Richard Zach)

首次发布于 2003 年 7 月 31 日星期四；实质性修订于 2023 年 9 月 29 日星期五

在 1920 年代初期，德国数学家大卫·希尔伯特（1862-1943）提出了一个关于古典数学基础的新提议，后来被称为希尔伯特计划。该计划要求以公理形式对所有数学进行形式化，同时证明这种数学的公理化是一致的。一致性证明本身应仅使用希尔伯特所称的“有限”方法来进行。有限推理的特殊认识论特征随后为古典数学提供了所需的理由。尽管希尔伯特仅在 1921 年以这种形式提出了他的计划，但其各个方面根植于他自约 1900 年以来的基础工作，当时他首次指出了直接给出分析一致性证明的必要性。该计划的工作在 1920 年代取得了显著进展，得益于逻辑学家如保罗·伯奈斯、威廉·阿克曼、约翰·冯·诺伊曼和雅克·埃尔布兰等人的贡献。它也对库尔特·哥德尔产生了很大影响，哥德尔关于不完备定理的工作是受到希尔伯特计划的启发。哥德尔的工作通常被认为表明希尔伯特计划无法实施。尽管如此，它仍然是数学哲学中一个有影响力的立场，并且从 1930 年代格哈德·根岑的工作开始，所谓的相对化希尔伯特计划的研究对证明论的发展至关重要。

1. 希尔伯特计划的历史发展

1.1 基础研究的早期工作

希尔伯特计划中关于数学基础的工作源于他在 1890 年代关于几何的研究，最终体现在他具有影响力的教材《几何基础》（1899 年）中（参见 19 世纪几何）。希尔伯特认为，严谨发展任何科学学科的正确方式需要采用公理化方法。通过提供一个公理化的处理，理论将独立于任何直觉的需要而发展，并且将有助于分析基本概念和公理之间的逻辑关系。对于希尔伯特来说，调查公理的独立性和尤其是一致性对于公理化处理至关重要。对于几何的公理，可以通过在实平面中提供系统的解释来证明一致性，因此，几何的一致性被简化为分析的一致性。当然，分析的基础本身需要一个公理化和一致性证明。希尔伯特在（1900b）中提供了这样的公理化，但很快就清楚地意识到，分析的一致性面临着重大困难，特别是因为在戴德金的工作中提供分析基础的偏爱方式依赖于类似于导致集合论悖论和弗雷格算术基础中的罗素悖论的可疑假设。

希尔伯特计划因此意识到，需要一种直接的分析一致性证明，即不基于对另一理论的归约。他在 1900 年国际数学家大会上的演讲中将寻找这样一个证明作为他的 23 个数学问题中的第二个问题，并在他的海德堡演讲中提出了这样一个证明的草图。几个因素延迟了希尔伯特基础计划的进一步发展。其中一个也许是庞加莱（1906 年）对希尔伯特所描绘的一致性证明中归纳法的恶性循环使用的批评。希尔伯特还意识到，公理化研究需要一个完善的逻辑形式主义。当时，他依赖于基于代数传统，特别是 Schröder 的工作的逻辑概念，这并不特别适合作为数学公理化的形式主义。（有关希尔伯特计划早期发展，请参阅 Peckhaus 1990。）

1.2 《数学原理》的影响

罗素和怀特海德的《数学原理》的出版为重新攻击基础问题提供了必要的逻辑基础。从 1914 年开始，希尔伯特的学生海因里希·贝曼和其他人研究了《数学原理》的体系（有关贝曼在希尔伯特学派中的作用，请参见曼科苏 1999 年的著作）。希尔伯特本人于 1917 年重新开始研究基础问题。1917 年 9 月，他在瑞士数学学会发表了题为《公理化思维》的演讲（1918a）。这是自 1905 年以来他在数学基础领域发表的第一篇文章。在演讲中，他再次强调了公理系统的一致性证明的要求：“公理理论的主要要求必须更进一步 [不仅仅是避免已知的悖论]，即要表明在每个知识领域内，基于基础公理系统的矛盾绝对不可能。”他将算术（以及集合论）的一致性证明再次提出为主要的未解问题。在这两种情况下，似乎没有比逻辑本身更基本的东西可以将一致性归结为。希尔伯特当时认为，罗素在《数学原理》中的工作基本上已经解决了这个问题。然而，其他公理学的基本问题仍未解决，包括“每个数学问题的可决定性”问题，这也可以追溯到希尔伯特 1900 年的演讲。

这些公理学中未解决的问题导致希尔伯特在接下来的几年里致力于逻辑工作。1917 年，保罗·伯奈斯作为他在哥廷根的助手加入了他。在 1917 年至 1921 年的一系列课程中，希尔伯特在伯奈斯和贝曼的协助下，对形式逻辑做出了重大贡献。特别是 1917 年的课程（希尔伯特，1918b），其中包含了对一阶逻辑的复杂发展，并构成了希尔伯特和阿克曼的教科书《理论逻辑原理》（1928 年）的基础（参见 Ewald 和 Sieg 2013 年，Sieg 1999 年，以及 Zach 1999 年，2003 年）。

1.3 有限主义和一致性证明的追求

然而，在接下来的几年里，希尔伯特开始反对罗素对算术一致性问题的逻辑主义解决方案。与此同时，布劳威尔的直觉主义数学开始流行起来。特别是，希尔伯特的前学生赫尔曼·韦伊尔转向直觉主义。韦伊尔的论文《数学中的新基础危机》（1921 年）在 1921 年夏天的汉堡三次讲座中得到了希尔伯特的回应（1922b）。在这里，希尔伯特提出了自己关于解决数学基础问题的方案。这个方案融合了希尔伯特关于直接一致性证明的想法，他对公理系统的构想，以及罗素在数学公理化工作中的技术发展，以及他和他的合作者进行的进一步发展。新的地方在于希尔伯特希望赋予他的一致性项目哲学上的重要性，以回应布劳威尔和韦伊尔的批评：有限观点。

根据希尔伯特，数学中有一个特权部分，即内容性初等数论，它仅依赖于“纯粹直观的具体符号基础”。而操作抽象概念被认为是“不足和不确定的”，存在一个领域

超逻辑的离散对象，它们在所有思维之前作为直接经验直观存在。如果逻辑推理要确切，那么这些对象必须能够在所有部分完全被审视，它们的呈现、它们的差异、它们的继承（就像对象本身一样）必须对我们立即、直观地存在，作为不能被归约为其他东西的东西。（希尔伯特 1922b，202；这段话几乎一字不差地重复在希尔伯特 1926，376，希尔伯特 1928，464 和希尔伯特 1931b，267 中）

对于希尔伯特来说，这些对象是符号。内容性数论的领域包括有限数字符号，即，笔画序列。它们没有意义，即，它们不代表抽象对象，但可以进行操作（例如，连接）和比较。对它们的性质和关系的了解是直观的，并且不经由逻辑推理进行中介。希尔伯特认为，以这种方式发展的内容性数论是安全的：简单地因为内容性数论的命题中没有逻辑结构，所以不会出现矛盾。

用符号进行直观内容操作构成了希尔伯特计划的基础。正如内容数论使用笔画序列一样，元数学使用符号序列（公式、证明）。公式和证明可以在语法上进行操作，公式和证明的性质和关系同样基于一种无逻辑的直观能力，这种能力确保了通过这种语法操作得出的关于公式和证明的知识的确定性。然而，数学本身使用抽象概念，例如量词、集合、函数，并使用基于数学归纳法或排中律等原则的逻辑推理。这些“概念形成”和推理方式曾受到布劳威尔等人的批评，理由是它们假定了给定的无限整体，或者涉及不可预言的定义（这被批评者认为是恶性循环）。希尔伯特的目标是证明它们的使用是合理的。为此，他指出它们可以在公理系统中形式化（例如普林西皮亚的公理系统或希尔伯特自己开发的系统），数学命题和证明因此变成了根据严格限定的推导规则从公理中推导出的公式和推导。希尔伯特认为，数学“成为可证明公式的清单。”通过这种方式，数学的证明受到元数学、内容性调查的影响。希尔伯特计划的目标是提供一个内容性的、元数学的证明，证明不存在矛盾的推导，即不存在公式 A 及其否定 ¬A 的形式推导。

这个计划的目标草图是由希尔伯特及其合作者在接下来的 10 年内详细阐述的。在概念方面，希尔伯特（1928 年）、希尔伯特（1923 年）、希尔伯特（1926 年）和伯奈斯（1928b 年）、伯奈斯（1922 年）、伯奈斯（1930 年）详细阐述了有限立场和一致性证明的策略；其中，希尔伯特的文章《论无穷》（1926 年）提供了最详细的有限立场阐述。除了希尔伯特和伯奈斯，还有许多其他人参与了该计划的技术工作。在哥廷根的讲座中（希尔伯特和伯奈斯，1923 年；希尔伯特，1922a 年），希尔伯特和伯奈斯将 ε-演算作为他们关于算术和分析公理系统的最终形式主义。希尔伯特还提出了他所谓的 ε-替换方法来给出一致性证明的方法。阿克曼（1924 年）试图将希尔伯特的思想扩展到一个分析系统中。然而，该证明是错误的（参见 Zach 2003）。约翰·冯·诺伊曼当时正在哥廷根访问，他在 1925 年为 ε 形式主义系统提供了一个经过修正的一致性证明（发表于 1927 年）。在冯·诺伊曼的工作基础上，阿克曼设计了一种新的 ε-替换程序，并将其传达给了伯奈斯（参见伯奈斯 1928b 年）。在 1928 年博洛尼亚国际数学家大会上的演讲《数学基础问题》中（1929 年），希尔伯特乐观地声称，阿克曼和冯·诺伊曼的工作已经确立了数论的一致性，并且分析的证明已经由阿克曼“在只剩下证明一个纯粹算术的基本有限性定理的任务”的程度上完成。

1.4 哥德尔不完备性定理的影响

哥德尔的不完备性定理表明希尔伯特计划的乐观是不合理的。1930 年 9 月，库尔特·哥德尔在康斯堡的一次会议上宣布了他的第一个不完备性定理。在场的冯·诺伊曼立即意识到哥德尔的结果对希尔伯特计划的重要性。会议结束后不久，他写信给哥德尔，告诉他发现了哥德尔结果的一个推论。哥德尔已经独立发现了相同的结果：第二不完备性定理，宣称普林西皮亚系统不能证明普林西皮亚系统的一致性的形式化（假设它是的）。直到那时为止，一直相信在一致性证明中使用的所有有限推理方法都可以在普林西皮亚中形式化。因此，如果普林西皮亚的一致性可以通过阿克曼证明中使用的方法证明，那么应该可以在普林西皮亚中形式化这个证明；但第二不完备性定理指出这是不可能的。伯奈斯在 1931 年 1 月研究了哥德尔的论文后立即意识到哥德尔结果的重要性，写信给哥德尔说（在有限推理可以在普林西皮亚中形式化的假设下）不完备性定理表明普林西皮亚的有限一致性证明是不可能的。不久之后，冯·诺伊曼表明阿克曼的一致性证明存在缺陷，并提供了所提出的 ε-替换程序的反例（参见 Zach 2003）。

在 1936 年，Gentzen 发表了一篇关于一阶 Peano 算术（PA）一致性证明的文章。正如 Gödel 所表明的那样，Gentzen 的证明使用了在 PA 本身中无法形式化的方法，即沿着序数 ε0 的超限归纳。Gentzen 的工作标志着后 Gödel 证明论和相对希尔伯特计划工作的开始。Gentzen 传统中的证明论根据有必要证明它们的一致性的有限观点的扩展来分析公理系统。通常，系统的一致性强度是通过系统的证明论序数来衡量的，即足以证明一致性的超限归纳的序数。在 PA 的情况下，该序数是 ε0。（有关进一步讨论，请参阅有关证明论和证明论发展的条目。）

2. 有限观点

希尔伯特数学哲学的基石，以及他从 1922 年开始的基础思想的实质性新方面，包括他所称的有限观点。这种方法论观点包括将数学思想限制在那些“在所有思想之前作为直接经验直观存在”的对象上，以及对这些对象进行的操作和推理方法，这些操作和方法不需要引入抽象概念，特别是不需要借助于完成的无限整体。

在理解希尔伯特计划的有限立场时，存在几个基本且相关的问题：

有限推理的对象是什么？
有限意义命题是什么？
什么是有限可接受的建构和推理方法？

2.1 有限对象和有限主义认识论

希尔伯特在一段著名的段落中刻画了有限推理的领域，在希尔伯特 20 世纪 20 年代更多的哲学论文中大致以相同的表述出现（1931b; 1922b; 1928; 1926）：

作为逻辑推理和逻辑操作的使用条件，我们的表象能力必须已经给予某些东西，即某些超逻辑的具体对象，这些对象在所有思维之前作为直观经验直接存在。如果逻辑推理要可靠，就必须能够完全审视这些对象的所有部分，它们的出现、彼此之间的差异以及它们相继发生或连接的事实，与对象一起，作为直观给出的东西，既不能被归纳为其他任何东西，也不需要被归纳。这是我认为对数学以及一般所有科学思维、理解和交流都必不可少的基本哲学立场。（希尔伯特计划，1926 年，376 页）

对于希尔伯特来说，这些对象就是符号。对于内容性数论领域，所讨论的符号是数字如

1, 11, 111, 11111

如何确切地理解希尔伯特对数字的看法是一个难以回答的问题。它们不是物理对象（例如纸上的实际笔画），因为必须始终有可能通过添加另一个笔画来扩展数字（正如希尔伯特在《论无穷》（1926）中所辩论的，物理宇宙是否无限是值得怀疑的）。根据希尔伯特（1922b，202），它们的“形状可以被我们普遍和确定地认识到—独立于空间和时间，独立于符号产生的特殊条件，独立于成品中微不足道的差异”。它们不是心智建构，因为它们的属性是客观的，然而它们的存在取决于它们的直觉建构（参见伯奈斯 1923，226）。无论如何清楚的是，它们在逻辑上是原始的，即它们既不是概念（如弗雷格的数字）也不是集合。这里重要的不是它们的形而上学地位（抽象与具体在这些术语当前意义上的对立），而是它们不参与逻辑关系，例如，它们不能被断言为任何事物。在伯奈斯对有限主义的最成熟阐述中（希尔伯特和伯奈斯，1939；伯奈斯，1930），有限主义的对象被描述为通过重复过程递归生成的形式对象；笔画符号然后是这些形式对象的具体表示。

希尔伯特计划认为有限主义对象的认识论地位同样困难。为了为无穷数学提供一个稳固的基础，对有限对象的访问必须是直接和确定的。希尔伯特的哲学背景大体上是康德式的，伯奈斯也是如此，他与哥廷根的伦纳德·纳尔逊周围的新康德学派有密切联系。希尔伯特对有限主义的描述经常涉及康德式直觉，以及有限主义对象作为直觉给出的对象。事实上，在康德的认识论中，直接性是直觉知识的一个定义特征。问题是，这种直觉是何种类型？Mancosu（1998b）在这方面指出了一个转变。他认为，虽然希尔伯特早期论文中涉及的直觉是一种感性直觉，但在后来的著作中（例如，伯奈斯 1928a），它被确定为康德式纯直觉的一种形式。然而，大约在同一时间，希尔伯特（1928，469）仍然将直觉的类型确定为感性的。在（1931b，266-267）中，希尔伯特将有限思维模式视为先验知识的另一个来源，除了纯直觉（例如，空间）和理性之外，声称他“认识并表征了伴随经验和逻辑的第三种知识来源”。伯奈斯和希尔伯特都以广义康德术语证明有限知识（但并没有提供超验演绎），将有限推理描述为支撑所有数学，甚至科学思维的推理，没有这种推理，这种思维将是不可能的。（有关有限主义认识论，请参见 Kitcher 1976 和 Parsons 1998，有关希尔伯特符号理论的历史和哲学背景，请参见 Patton 2014，有关与德国哲学家阿洛伊斯·穆勒的后续辩论，请参见 Eder（即将出版）。）

2.2 有限意义命题和有限推理

关于有限数的最基本判断是关于相等和不等的。此外，有限观点允许对有限对象进行操作。这里最基本的是连接。数 11 和 111 的连接被表达为“2+3”，而数 11 与 111 连接的陈述结果与 111 与 11 连接的数相同，即“2+3=3+2”。在实际的证明理论实践中，以及明确地在（希尔伯特和伯奈斯，1934 年；伯奈斯，1930 年）中，这些基本操作被推广为由递归定义的操作，典型地是原始递归，例如乘法和指数运算（有关指数运算的哲学困难，请参见帕森斯 1998 年，以及 2007 年关于直觉数学和有限主义的广泛讨论）。同样，有限判断可能不仅涉及相等或不等，还可能涉及基本可判定的属性，例如“是素数”。只要这种属性的特征函数本身是有限的，这在有限意义上是可以接受的：例如，如果一个数是素数，则将其转换为 1 的操作，否则为 11，可以通过原始递归来定义，因此是有限的。这样的有限命题可以通过传统的逻辑操作符合、析取、否定，以及有界量词来组合。（希尔伯特，1926 年）举了一个命题的例子，“在 p+1 和 p!+1 之间存在一个素数”，其中 p 是一个特定的大素数。这个陈述在有限意义上是可以接受的，因为它“仅仅用来缩写这个命题”，即 p+1 或 p+2 或 p+3 或…或 p!+1 是一个素数。

表达一般关于数字的事实的问题有那些表述，比如，对于任何给定的数字 n，1+n=n+1。这是有问题的，因为正如希尔伯特所说，“从有限主义的观点来看，它无法被否定”（1926 年，378 页）。他的意思是，对于存在一个数字 n 使得 1+n≠n+1 的矛盾命题在有限意义上是没有意义的。“毕竟，人不能尝试所有的数字”（1928 年，470 页）。出于同样的原因，有限一般命题不应被理解为无限连词，而是“仅仅作为一个假设性判断，当给定一个数字时就会断言某事”（同上）。尽管从这个意义上讲它们是有问题的，一般的有限陈述对于希尔伯特的证明理论非常重要，因为形式系统 S 的一致性陈述具有这样的一般形式：对于任何给定的公式序列 P，P 在 S 中不是导出矛盾的。

2.3 有限操作和有限证明

对于有限主义和希尔伯特的证明理论的理解而言，关键性的重要性在于有限主义观点应该允许哪些操作和哪些证明原则。从希尔伯特的证明理论的要求来看，很明显需要一个一般性答案，即，不应该期望给定一个数学形式系统（甚至是一个单独的公式序列）就能“看到”它是一致的（或者它不能是一个真正的不一致的推导），就像我们可以看到 11+111=111+11 一样。一致性证明所需的是一个操作，它可以将一个形式推导转换为特殊形式的推导，再加上证明这种操作确实做到了这一点，以及特殊类型的证明不能是不一致的证明。要算作有限一致性证明，操作本身必须从有限主义观点可接受，并且所需的证明必须仅使用有限主义可接受的原则。

希尔伯特计划从有限主义的角度没有给出哪些操作和证明方法是可以接受的一般性说明，而只是他接受为有限的内容有限数论中的操作和推理方法的例子。希尔伯特（1922b）明确接受了内容归纳在其应用于假设的一般性有限性陈述中。他（1923, 1139）说直觉思维“包括对有限现存的整体的递归和直觉归纳”，并在 1928 年的一个例子中使用了指数运算。伯奈斯（1930）解释了如何将指数运算理解为对数字的有限操作。希尔伯特和伯奈斯（1934）给出了有关有限内容数论的唯一一般性说明；根据这一说明，由原始递归定义的操作和使用归纳的证明在有限意义上是可以接受的。所有这些方法都可以在一个称为原始递归算术（PRA）的系统中形式化，该系统允许通过原始递归和对无量词自由公式的归纳来定义函数（同上）。然而，希尔伯特和伯奈斯从未声称只有原始递归操作才算是有限的，并且事实上，他们在 1923 年就已经在明显有限的一致性证明中使用了一些非原始递归方法（参见 Tait 2002 和 Zach 2003）。

更有趣的概念问题是哪些操作应被视为有限的。由于希尔伯特在有限观点的内容上并不十分清晰，因此在建立对有限操作和证明的限制时存在一定的余地，这些限制必须满足认识论等方面的分析。希尔伯特将有限数论的对象描述为“直观给定的”，“在所有部分中可调查的”，并表示它们具有基本属性必须“在我们这里直观存在”。伯奈斯（1922 年，216 页）建议在有限数学中，只有“原始直观认知”起作用，并在 1930 年关于有限主义的“直观证据观点”中使用了这个术语。对于有限主义的这种描述，特别强调了帕森斯（1998 年）的观点，他认为根据这种理解，可以被视为有限的只有那些可以使用有界递归从加法和乘法定义的算术运算。特别是，根据他的观点，指数运算和一般的原始递归在有限意义上是不可接受的。

将有限主义与原始递归推理相一致的论点得到了（Tait 1981; 另见 2002 年，2005b 年，2019 年）的有力辩护。与 Parsons 相反，Tait 拒绝将直觉中的可表达性视为有限性的标志；相反，他认为有限推理是“所有关于数字的非平凡数学推理所预设的一种最小推理”，并将有限运算和证明方法分析为隐含在数字作为有限序列形式的概念中的那些。希尔伯特（1931b，267）支持对有限性推理的分析，认为有限推理是逻辑和数学，事实上是任何科学思维的先决条件。由于有限推理是所有关于数字的非平凡推理所预设的数学的一部分，因此，Tait 认为，在笛卡尔意义上，“不容置疑”，这种不容置疑性是有限推理所需提供的唯一内容，以实现希尔伯特为之设想的数学的认识论基础。

另一个有趣的有限证明分析，然而，没有提供详细的哲学理据，是由 Kreisel（1960）提出的。该分析得出的结论是，只有那些可以被证明在一阶算术 PA 中是全的函数才是有限的。它基于证明论概念的反射原理；有关更多详细信息，请参阅 Zach（2006），以及有关分析，请参阅 Dean（2015）。Kreisel（1970，第 3.5 节）通过专注于“可视化”的内容提供了另一种分析。结果是相同的：有限可证性最终证明与 PA 中的可证性相一致。

泰特的技术分析表明，有限函数恰好是原始递归函数，有限数论真理恰好是可在原始递归算术理论 PRA 中证明的真理。强调这一分析并非从有限主义观点内部进行。由于“函数”和“证明”的一般概念本身并非有限，有限主义者无法理解泰特的论点，即 PRA 中可证明的一切都是有限真理。据泰特称，对有限可证性的适当分析不应假定有限主义本身可以接触到这种非有限概念。克赖塞尔的方法以及一些依赖于反射原理或 ω-规则的对泰特的批评违背了这一要求（参见泰特 2002 年，2005b 年）。另一方面，可以主张 PRA 是过于强大的理论，无法算作关于数字的“所有非平凡数学推理所预设的”形式化：存在与原始递归函数类别较小相关的较弱但非平凡理论，如 PV 和 EA，分别与多项式时间和 Kalmar-初等函数相关（参见 Avigad 2003 年关于在 EA 中可以进行多少数学）。使用与泰特相同思路的分析，Ganea（2010 年）得出了与之对应的 Kalmar-初等函数类。另请参阅 Incurvati（2019 年）以进一步分析不同有限主义概念。

3. 形式主义、还原主义和工具主义

Weyl（1925 年）是对希尔伯特在 1922 年和 1923 年提出的建议的一种调和反应，尽管其中包含了一些重要的批评。魏尔将希尔伯特的项目描述为用毫无意义的公式游戏取代内容性数学。他指出，希尔伯特想要“确保的不是真理，而是分析的一致性”，并提出了一个批评，这与弗雷格早期的批评相呼应：我们为什么要将数学形式系统的一致性视为相信其所编码的前形式数学的真理的理由？希尔伯特的毫无意义的公式清单难道不只是“分析的无血色幽灵”吗？魏尔提出了一个解决方案：

如果数学要继续成为一个严肃的文化关注点，那么希尔伯特的公式游戏必须被赋予某种意义，我只看到一种可能性，即将其（包括其超穷分量）赋予独立的智力意义。在理论物理学中，我们面前有一个伟大的例子，这是一种完全不同性质的知识，与表达直觉中所给内容的普通或现象知识完全不同。在这种情况下，每个判断都有其自己的意义，完全可以在直觉中实现，但对于理论物理学的陈述来说情况却并非如此。在这种情况下，如果与经验相对立，那么问题实际上是整个系统。（魏尔，1925 年，140）

类比物理学是惊人的，人们可以在希尔伯特自己的著作中找到类似的想法——也许希尔伯特受到了魏尔的影响。尽管希尔伯特最初的提议专注于一致性，但在希尔伯特的思想中可以看到朝着一种在当时科学哲学中非常普遍的一般还原主义项目的发展（正如 1983 年吉亚昆托所指出的）。在 20 世纪 20 年代的下半叶，希尔伯特用保守性计划取代了一致性计划：形式化数学应该类比于理论物理学。理论部分的最终理由在于它在“真实”数学上的保守性：每当理论上的“理想”数学证明了一个“真实”命题时，该命题也在直觉上是真实的。这证明了超限数学的使用：它不仅在内部一致，而且只证明真实的直觉命题（实际上是所有的，因为直觉数学的形式化是所有数学的一部分）。

1926 年，希尔伯特引入了实际和理想公式之间的区别。这种区别在 1922 年并不存在，只在 1923 年略有暗示。在后者中，希尔伯特首先提出了一个关于无限定量的数论的形式系统，他说：“我们以这种方式获得的可证公式都具有有限性的特征”（1139）。然后，添加了超限公理（即，定量词）以简化和完善理论（1144）。在这里，他首次将理想元素的方法与之类比：“在我的证明理论中，超限公理和公式被附加到有限公理中，就像在复变量理论中，虚构元素被附加到实数中一样，在几何学中，理想构造被附加到实际中一样”（同上）。当希尔伯特在 1926 年明确引入理想命题的概念时，以及在 1928 年首次提到除了理想之外还有实际命题时，他非常清楚，理论的实际部分仅由可判定的、无变量的公式组成。它们应该是“直接可验证的”——类似于从自然法则推导出的命题，可以通过实验进行检验（1928 年，475）。该计划的新图景是：经典数学将被形式化为一个系统，其中包括所有直接可验证（通过计算）的内容有限数论命题的形式化。一致性证明应该表明，所有可以通过理想方法证明的实际命题都是真实的，即可以通过有限计算直接验证。（实际证明，如 ε-替换，一直是这种类型的：提供消除实际陈述的证明中的超限元素的有限程序，特别是 0=1 的证明。) 实际上，希尔伯特看到更强的东西是真实的公式的一致性证明不仅建立了理想方法可证明的真实公式的真理，而且如果相应的自由变量公式可由理想方法推导，则它还产生了有限证明的有限一般命题（1928 年，474 页）。

除了保守性，希尔伯特还建议对该理论进行进一步限制：简单性，证明的简洁性，“思想的经济性”和数学生产力。无限逻辑的形式系统并非是任意的：“这个公式游戏是根据某些明确的规则进行的，其中表达了我们思维的技术。[…] 我的证明理论的基本思想无非是描述我们理解的活动，根据我们的思维实际进行的规则制定协议”（希尔伯特 1928 年，475 页）。当魏尔（1928 年）最终摆脱直觉主义时，他强调了希尔伯特证明理论的这一动机：不是将数学变成一个毫无意义的符号游戏，而是将其转变为一门将科学（数学）实践编码化的理论科学（有关魏尔与直觉主义和希尔伯特形式主义的关系，请参见 Mancosu 和 Ryckman 2002 年以及 Kish Bar-On 2021 年）。

因此，希尔伯特的形式主义相当复杂：它避免了两个关键的反对意见：（1）如果系统的公式是无意义的，那么系统中的可导性如何产生任何信仰？（2）为什么接受 PA 系统而不接受任何其他一致的系统？这两个反对意见都是从弗雷格那里熟悉的；对于（2），此外，希尔伯特有一个接受的自然标准：我们在系统选择上受到简单性，多产性，一致性以及数学家实际做什么的考虑的限制；魏尔还会补充说，理论的最终测试将是其在物理学中的实用性。

大多数研究希尔伯特的数学哲学的哲学家都将他解读为一位工具主义者（包括 Kitcher 1976，Resnik 1980，Giaquinto 1983，Sieg 1990，特别是 Detlefsen 1986），因为他们认为希尔伯特解释理想命题“本身没有意义”（希尔伯特，1926 年，381 页）是在声称经典数学只是一种工具，而无穷数学的陈述没有真值。在这种程度上，这必须被理解为一种方法论工具主义：证明论计划的成功执行将表明人们可以假装数学是毫无意义的。因此，与物理学的类比并非如此：无穷命题没有意义，就像涉及理论术语的命题没有意义一样，而是：无穷命题不需要直接直观意义，就像人们不必直接看到电子就能对其进行理论化。Hallett（1990 年）考虑到希尔伯特所处的 19 世纪数学背景以及希尔伯特整个职业生涯的已发表和未发表的来源（特别是希尔伯特 1992 年，对理想元素方法最广泛的讨论）得出以下结论：

[希尔伯特对哲学问题的处理] 并非意味着对存在和真理等问题持一种工具主义者的不可知论态度。相反，它旨在提供对这些问题的一种非怀疑的积极解决方案，一种用认知可及的术语表达的解决方案。而且，似乎，这个解决方案对数学理论和物理理论都适用。一旦新概念或“理想元素”或新的理论术语被接受，那么它们存在的方式就像任何理论实体存在的方式一样。（Hallett，1990 年，239 页）

4. 希尔伯特计划和哥德尔的不完备性定理

关于哥德尔不完备性定理对希尔伯特计划的影响存在一些争论，以及是第一还是第二不完备性定理给予了致命一击。毫无疑问，直接参与这些发展的人士认为这些定理确实产生了决定性影响。哥德尔在 1930 年 10 月发表的一篇摘要中宣布了第二不完备性定理：像普林斯顿、策梅洛-弗雷克尔集合论或阿克曼和冯·诺伊曼研究的系统等系统的一致性证明是不可能的，因为这些系统无法用这些方法来表述。在他的论文的完整版本中，哥德尔（1931 年）留下了这样的可能性，即可能存在一些有限方法，这些方法无法在这些系统中形式化，但可以产生所需的一致性证明。伯奈斯在 1931 年 1 月写给哥德尔的一封信中也表达了同样的看法：“如果像冯·诺伊曼那样，认为任何有限考虑都可以在系统 P 内形式化——就像你一样，我认为这一点还没有确定——那么就会得出这样的结论：P 的一致性的有限证明是不可能的”（哥德尔，2003a，87）。

哥德尔的定理如何影响希尔伯特计划？通过对符号序列（公式、证明）进行仔细的（“哥德尔”）编码，哥德尔表明在包含足够数量的算术的理论 T 中，可以产生一个公式 Pr(x,y)，其中“说”x 是（代码为）y 的证明。具体来说，如果 ┌0=1┐ 是公式 0=1 的编码，则 ConT=∀x¬Pr(x,┌0=1┐)可以被理解为“说”T 是一致的（没有任何数字是 T 中 0=1 的推导的代码）。第二不完备性定理（G2）表明，在关于 T 和编码装置的某些假设下，T 无法证明 ConT。现在假设存在一个有限一致性证明 T。在这种证明中使用的方法可能可以在 T 中形式化。（“可形式化”意味着，粗略地说，如果证明使用对推导的有限操作 f，将任何推导 D 转换为简单形式的推导 f(D)；那么存在一个公式 F(x,y)，使得对于所有推导 D，T⊢F(┌D┐,┌f(D)┐)。）T 的一致性将以一般假设的形式被有限地表达，即如果 D 是任何给定的符号序列，则 D 不是 T 中公式 0=1 的推导。这个命题的形式化是公式 ¬Pr(x,┌0=1┐)，其中变量 x 是自由的。如果存在 T 一致性的有限证明，其形式化将产生 T 中的一个推导 ¬PrT(x,┌0=1┐)，从中可以通过对 x 进行简单的普遍化在 T 中推导出 ConT。然而，G2 排除了在 T 中对 ConT 的推导。

如上所述，最初哥德尔和伯奈斯认为，对于 PA 的一致性证明的困难可以通过采用一些方法来克服，尽管这些方法在 PA 中无法形式化，但仍然是有限的。这些方法是否符合有限主义的原始概念或构成原始有限主义观点的延伸是一个有争议的问题。考虑的新方法包括希尔伯特提出的 ω-规则的有限版本。然而，可以公平地说，大约在 1934 年之后，几乎普遍认为在哥德尔的结果之前被接受为有限的证明方法都可以在 PA 中形式化。已经提出并在广泛的有限主义基础上辩护了原始有限主义立场的延伸，例如，根岑（1936）在他对 PA 的一致性证明中为使用直到 ε0 的超限归纳进行了“无可争议”的辩护，武内（1987）提出了另一种辩护。哥德尔（1958）提出了有限主义立场的另一个延伸；上面提到的克莱塞尔的工作可以看作是另一种试图在保留希尔伯特原始概念精神的同时延伸有限主义的尝试。

一个不同的尝试是由 Detlefsen（1986 年；2001 年；1979 年）提出的，以绕过希尔伯特计划的哥德尔第二定理。Detlefsen 提出了几条辩护线索，其中之一类似于刚刚描述的：认为 ω-规则的一个版本在有限范围内是可以接受的，尽管不能形式化（但请参阅 Ignjatovic 1994）。Detlefsen 反对对哥德尔第二定理的常见解释的另一个论点集中在形式化的概念上：哥德尔的公式 ConT 对“T 是一致的”进行的特定形式化不可证明并不意味着就不能有其他在 T 中可证明的公式，这些公式同样有权被称为“T 的一致性的形式化”。这些依赖于与标准形式化的可证性谓词 PrT 不同的谓词的不同形式化。已知，每当可证性谓词遵守某些一般推导条件时，形式化的一致性陈述是不可证明的。Detlefsen 认为这些条件对于一个谓词被视为真正的可证性谓词并不是必要的，实际上存在一些可证性谓词违反可证性条件，并导致在相应理论中可证明的一致性公式。然而，这些依赖于非标准的可证性概念，这些概念可能不会被希尔伯特接受（另请参阅 Resnik 1974 年，Auerbach 1992 年和 Steiner 1991 年）。

Smorynski（1977）认为，第一个不完备性定理已经击败了希尔伯特计划。希尔伯特的目标不仅仅是要表明形式化数学是一致的，而且要以一种特定的方式来表明理想数学永远不会得出与实际数学不符的结论。因此，要成功，理想数学必须在实际部分上保守：无论何时，形式化的理想数学证明一个实际公式 P，P 本身（或者它所表达的有限命题）必须是有限可证的。对于 Smorynski 来说，实际公式不仅包括数值相等和它们的组合，还包括带有自由变量但没有无界量词的一般公式。

现在，哥德尔的第一个不完备性定理（G1）陈述了对于任何足够强大、一致的形式理论 S，都存在一个真实但在 S 中不可导出的句子 GS。根据 Smorynski 的定义，GS 是一个真实句子。现在考虑一个形式化理想数学及其子理论 S 的理论 T，后者形式化了实际数学。S 满足 G1 的条件，因此 S 不推导 GS。然而，T 作为数学的全部形式化（包括证明 GS 为真所需的内容）确实推导 GS。因此，我们有一个在理想数学中可证的真实陈述，在实际数学中却不可证。

Detlefsen（1986，附录；另见 1990）也为希尔伯特计划辩护。Detlefsen 认为，“希尔伯特式”工具主义通过否认理想数学必须在实际部分上保守来摆脱 G1 的论据；唯一需要的是真实性。希尔伯特式工具主义只要求理想理论不证明与实际理论冲突的任何内容；并不要求它只证明实际理论也证明的真实陈述。

弗兰克斯（2009）提供了对希尔伯特计划的相关辩护和重新评估，麦卡锡（2016）提出了哥德尔本人对一致性和 G2 可证性的另类方法。克里普克（即将出版）展示了希尔伯特自己对一致性证明的方法如何自然地导致了哥德尔的不完备性。桑托斯等人（即将出版）在阿尔泰莫夫（2020）的工作基础上进行了拓展，认为“部分有限主义”可以提供与 G2 兼容的一致性证明，并与希尔伯特本人在哥德尔之后的观点一致。另请参阅 Schirn 和 Niebergall（2001）以及 Schirn（2019）的相关提议。Zach（2004）提供了关于希尔伯特计划中保守性和一致性问题的历史细节。另请参阅有关哥德尔和哥德尔不完备定理的条目，以及程（2021）进行进一步讨论哥德尔的定理和一致性证明。

5. 修订后的希尔伯特计划

即使无法给出算术的有限一致性证明，寻找一致性证明的问题仍具有价值：这些证明中使用的方法，尽管必须超越希尔伯特对有限主义最初的理解，但可能为算术和更强大的理论的建设性内容提供真正的见解。哥德尔的结果表明，数学的所有绝对一致性证明是不可能的；因此，哥德尔之后的证明理论工作集中在相对结果上，即相对于给出一致性证明的系统，以及相对于使用的证明方法。

在这个意义上，简化证明理论遵循了两个传统：第一个传统主要由跟随 Gentzen 和 Schütte 的证明理论家进行，他们追求所谓的序数分析计划，以 Gentzen 关于 PA 的第一个一致性证明为例，该证明通过 ε0 的归纳进行。ε0 是某种超限（尽管可数）序数，然而，在这里使用的“ε0 的归纳”并不是一个真正的超限程序。序数分析不涉及无限序数，而是涉及序数符号系统，这些系统本身可以在非常弱（基本上是有限的）系统中形式化。如果给出了系统 T 的序数分析，则：（a）可以产生一个序数符号系统，模拟小于某个序数 αT 的序数，以便（b）可以有限地证明归纳原理的形式化 TI(αT)暗示了 T 的一致性（即，S⊢TI(αT)→ConT），以及（c）T 证明了对于所有 β<αT 的 β 都有 TI(β)（S 是形式化有限元数学的理论，通常是 T 的一个弱子理论）。为了具有任何基础意义，还需要对达到 αT 的超限归纳给出一个建设性的论证。如上所述，Gentzen 和 Takeuti 已经为 PA 的证明论序数 ε0 完成了这一点，但对于更强的理论来说，这变得更加困难，并且在哲学上的意义也逐渐变得值得怀疑。请参阅有关证明理论的条目，了解 Gentzen 的一致性证明概况，Mancosu 等人 2021 年的易懂教材介绍，以及 Thomas-Bolduc 和 Darnell 2022 年关于 Takeuti 的良序证明。

希尔伯特计划在证明论术语中的哲学上更令人满意的延续被 Kreisel（1983 年；1968 年）和 Feferman（Feferman，1988 年；Feferman，1993a）提出。这项工作从对希尔伯特计划更广泛的概念出发，试图通过有限手段来证明理想数学的合理性。在这种概念中，希尔伯特的证明理论的目的是要表明，至少在某一类真命题方面，理想数学并不超越实数学。希尔伯特所设想的有限一致性证明将实现这一点：如果理想数学证明了一个真命题，那么这个命题已经可以通过实数学（即有限的）方法证明。在某种意义上，这将理想数学简化为实数学。将理论 T 在证明论上归约到理论 S 表明，至少在某一类命题方面，如果 T 证明了一个命题，那么 S 也能证明它，并且这一事实的证明本身是有限的。希尔伯特的证明论计划可以被看作是在寻找将所有数学归约到有限数学的证明论归约；在一个相对化的计划中，人们寻找将比所有古典数学更弱的理论归约到通常比有限数学更强的理论。证明论者已经获得了许多这样的结果，包括将那些在表面上需要大量理想数学来证明的理论（例如分析的子系统）归约到有限系统。Feferman（1993b 年）利用了这些结果与其他结果相结合，表明大多数，如果不是全部，科学应用数学可以在这些归约可用的系统中进行，以反驳数学哲学中的不可或缺性论证。目前，这种证明论归约的哲学意义正在进行辩论（Hofweber，2000 年；Feferman，2000 年）。

由 Friedman 和 Simpson 等人开发的所谓逆向数学计划，是希尔伯特计划的另一个延续。面对哥德尔的结果表明并非所有经典数学都可以归结为有限性，他们试图回答一个问题：经典数学中有多少可以这样归结？逆向数学试图通过研究哪些经典数学定理可以在可归结为有限性数学的弱分析子系统中被证明来精确回答这个问题（在前一段讨论的意义上）。一个典型的结果是，泛函分析的 Hahn-Banach 定理可以在一个名为 WKL0（“弱 König 引理”）的理论中被证明；WKL0 对于 Π02 句子（即形如 ∀x∃yA(x,y)的句子）是保守的（有关概述，请参见 Simpson 1988，有关技术处理，请参见 Simpson 1999）。

Bibliography

An extended version of the first revision of this entry can be found in Zach (2006).

Ackermann, Wilhelm, 1924, “Begründung des ‘tertium non datur’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit,” Mathematische Annalen, 93: 1–36.
Artemov, Sergei, 2020, “The provability of consistency,” arXiv:1902.07404.
Auerbach, David, 1992, “How to say things with formalisms,” in Proof, Logic, and Formalization, Michael Detlefsen, ed., London: Routledge, 77–93.
Avigad, Jeremy, 2003, “Number theory and elementary arithmetic,” Philosophia Mathematica, 11: 257–284.
Bernays, Paul, 1922, “Über Hilberts Gedanken zur Grundlegung der Arithmetik,” Jahresbericht der Deutschen Mathematiker-Vereinigung, 31: 10–19. English translation in Mancosu (1998a, 215–222).
–––, 1923, “Erwiderung auf die Note von Herrn Aloys Müller: Über Zahlen als Zeichen,” Mathematische Annalen, 90: 159–63. English translation in Mancosu (1998a, 223–226).
–––, 1928a, “Über Nelsons Stellungnahme in der Philosophie der Mathematik,” Die Naturwissenschaften, 16: 142–45.
–––, 1928b,, “Zusatz zu Hilberts Vortrag über ‘Die Grundlagen der Mathematik,’” Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 88–92. English translation in: van Heijenoort (1967, 485–489).
–––, 1930, “Die Philosophie der Mathematik und die Hilbertsche Beweistheorie,” Blätter für deutsche Philosophie, 4: 326–67. Reprinted in Bernays (1976, 17–61). English translation in Mancosu (1998a, 234–265).
–––, 1976, Abhandlungen zur Philosophie der Mathematik, Darmstadt: Wissenschaftliche Buchgesellschaft.
Cheng, Yong, 2021, “Current Research on Gödel’s Incompleteness Theorems,” Bulletin of Symbolic Logic, 27(2): 113–67.
Dean, Walter, 2015, “Arithmetical reflection and the provability of soundness,” Philosophia Mathematica, 23: 31–64, doi:10.1093/philmat/nku026
Detlefsen, Michael, 1979, “On interpreting Gödel’s second theorem,” Journal of Philosophical Logic, 8: 297–313. Reprinted with a postscript in Shanker (1988, 131–154).
–––, 1986, Hilbert’s Program, Dordrecht: Reidel.
–––, 1990, “On an alleged refutation of Hilbert’s program using Gödel’s first incompleteness theorem,” Journal of Philosophical Logic, 19: 343–377.
–––, 2001, “What does Gödel’s second theorem say?,” Philosophia Mathematica, 9: 37–71.
Eder, Günther, forthcoming, “The Bernays-Müller debate,” HOPOS: The Journal of the International Society for the History of Philosophy of Science.
Ewald, William Bragg (ed.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, vol. 2, Oxford: Oxford University Press.
Ewald, William Bragg and Wilfried Sieg (eds.), 2013, David Hilbert’s Lectures on the Foundations of Arithmetic and Logic 1917–1933, Berlin and Heidelberg: Springer.
Feferman, Solomon, 1988, “Hilbert’s Program relativized: Proof-theoretical and foundational reductions,” Journal of Symbolic Logic, 53(2): 364–284.
–––, 1993a, “What rests on what? The proof-theoretic analysis of mathematics,” in Philosophy of Mathematics. Proceedings of the Fifteenth International Wittgenstein-Symposium, Part 1, Johannes Czermak, ed., Vienna: Hölder-Pichler-Tempsky, 147–171. Reprinted in Feferman (1998, Ch. 10, 187–208).
–––, 1993b, “Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics,” PSA 1992, 2: 442–455. Reprinted in Feferman (1998, Ch. 14, 284–298). [Preprint available online].
–––, 1998, In the Light of Logic, Oxford: Oxford University Press.
–––, 2000, “Does reductive proof theory have a viable rationale?.” Erkenntnis, 53: 63–96.
Franks, Curtis, 2009, The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited, Cambridge: Cambridge University Press.
Ganea, Mihai, 2010, “Two (or three) notions of finitism,” Review of Symbolic Logic, 3: 119–144.
Gentzen, Gerhard, 1936,, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen, 112: 493–565. English translation in Gentzen (1969, 132–213).
–––, 1969, The Collected Papers of Gerhard Gentzen, Amsterdam: North-Holland.
Giaquinto, Marcus, 1983, “Hilbert’s philosophy of mathematics,” British Journal for Philosophy of Science, 34: 119–132.
Gödel, Kurt, 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik und Physik, 38: 173–198. Reprinted and translated in Gödel (1986, 144–195).
–––, 1958, “Über eine bisher noch nicht benütze Erweiterung des finiten standpunktes,” Dialectica, 280–287. Reprinted and translated in Gödel (1990, 217–251).
–––, 1986, Collected Works, vol. 1, Oxford: Oxford University Press.
–––, 1990, Collected Works, vol. 2, Oxford: Oxford University Press.
–––, 2003, Collected Works, vol. 4, Oxford: Oxford University Press.
Hallett, Michael, 1990, “Physicalism, reductionism and Hilbert,” in Physicalism in Mathematics, Andrew D. Irvine, ed., Dordrecht: Reidel, 183–257.
Hilbert, David, 1899, “Grundlagen der Geometrie,” in Festschrift zur Feier der Enthüllung des Gauss-Weber-Denkmals in Göttingen, Leipzig: Teubner, 1–92, 1st ed.
–––, 1900a, “Mathematische Probleme,” Nachrichten von der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-Phys. Klasse, 253–297. Lecture given at the International Congress of Mathematicians, Paris, 1900. Partial English translation in Ewald (1996, 1096–1105).
–––, 1900b, “Über den Zahlbegriff,” Jahresbericht der Deutschen Mathematiker-Vereinigung, 8: 180-184. English translation in Ewald (1996, 1089–1096).
–––, 1905, “Über die Grundlagen der Logik und der Arithmetik,” in Verhandlungen des dritten Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904, A. Krazer, ed., Leipzig: Teubner, 174–85. English translation in van Heijenoort (1967, 129–138).
–––, 1918a, “Axiomatisches Denken,” Mathematische Annalen, 78: 405–15. Lecture given at the Swiss Society of Mathematicians, 11 September 1917. Reprinted in Hilbert (1935, 146–156). English translation in Ewald (1996, 1105–1115).
–––, 1918b, “Prinzipien der Mathematik,” Lecture notes by Paul Bernays. Winter-Semester 1917/18. Typescript. Bibliothek, Mathematisches Institut, Universität Göttingen. Edited in Ewald and Sieg (2013, 59–221)..
–––, 1922a, “Grundlagen der Mathematik,” Vorlesung, Winter-Semester 1921/22. Lecture notes by Paul Bernays. Typescript. Bibliothek, Mathematisches Institut, Universität Göttingen. Edited in Ewald and Sieg (2013, 431–527).
–––, 1922b, “Neubegründung der Mathematik: Erste Mitteilung,” Abhandlungen aus dem Seminar der Hamburgischen Universität, 1: 157–177. Series of talks given at the University of Hamburg, July 25–27, 1921. Reprinted with notes by Bernays in Hilbert (1935, 157–177). English translation in Mancosu (1998a, 198–214) and Ewald (1996, 1115–1134).
–––, 1923, “Die logischen Grundlagen der Mathematik,” Mathematische Annalen, 88: 151–165. Lecture given at the Deutsche Naturforscher-Gesellschaft, September 1922. Reprinted in Hilbert (1935, 178–191). English translation in Ewald (1996, 1134–1148).
–––, 1926, “Über das Unendliche,” Mathematische Annalen, 95: 161–190. Lecture given Münster, 4 June 1925. English translation in van Heijenoort (1967, 367–392).
–––, 1928, “Die Grundlagen der Mathematik,” Abhandlungen aus dem Seminar der Hamburgischen Universität, 6: 65–85. Reprinted in Ewald and Sieg (2013, 917–942). English translation in van Heijenoort (1967, 464–479).
–––, 1929, “Probleme der Grundlegung der Mathematik,” Mathematische Annalen, 102: 1–9. Lecture given at the International Congress of Mathematicians, 3 September 1928. Reprinted in Ewald and Sieg (2013, 954–966). English translation in Mancosu (1998a, 227–233).
–––, 1931a, “Beweis des Tertium non datur,” Nachrichten der Gesellschaft der Wissenschaften zu Göttingen. Math.-phys. Klasse, 120-125. Reprinted in Ewald and Sieg (2013, 967–982).
–––, 1931b, “Die Grundlegung der elementaren Zahlenlehre,” Mathematische Annalen, 104: 485–494. Reprinted in Hilbert (1935, 192–195) and Ewald and Sieg (2013, 983–990). English translation in Ewald (1996, 1148–1157).
–––, 1935, Gesammelte Abhandlungen, vol. 3, Berlin: Springer.
–––, 1992, Natur und mathematisches Erkennen, Basel: Birkhäuser. Vorlesungen, 1919–20.
Hilbert, David and Ackermann, Wilhelm, 1928, Grundzüge der theoretischen Logik, Berlin: Springer.
Hilbert, David and Bernays, Paul, 1923, “Logische Grundlagen der Mathematik,” Vorlesung, Winter-Semester 1922-23. Lecture notes by Paul Bernays, with handwritten notes by Hilbert. Hilbert-Nachlaß, Niedersächsische Staats- und Universitätsbibliothek, Cod. Ms. Hilbert 567.
–––, 1934, Grundlagen der Mathematik, vol. 1, Berlin: Springer.
–––, 1939, Grundlagen der Mathematik, vol. 2, Berlin: Springer.
Hofweber, Thomas, 2000, “Proof-theoretic reduction as a philosopher’s tool,” Erkenntnis, 53: 127–146.
Ignjatovic, Aleksandar, 1994, “Hilbert’s program and the omega rule,” Journal of Symbolic Logic, 59: 322–343.
Incurvati, Luca, 2019, “On the concept of finitism,” Synthese, 192: 2413–2436.
Kish-Bar-On, Kati, 2021, “Towards a New Philosophical Perspective on Hermann Weyl’s Turn to Intuitionism,” Science in Context, 34: 51–68.
Kitcher, Philip, 1976, “Hilbert’s epistemology,” Philosophy of Science, 43: 99–115.
Kreisel, Georg, 1960, “Ordinal logics and the characterization of informal notions of proof,” in Proceedings of the International Congress of Mathematicians. Edinburgh, 14–21 August 1958, J. A. Todd, ed., Cambridge: Cambridge University Press, 289–299.
–––, 1968, “A survey of proof theory,” Journal of Symbolic Logic, 33: 321–388.
–––, 1970, “Principles of proof and ordinals implicit in given concepts,” in Intuitionism and Proof Theory, A. Kino, J. Myhill, and R. E. Veseley, eds., Amsterdam: North-Holland.
–––, 1983, “Hilbert’s programme,” in Philosophy of Mathematics, Paul Benacerraf and Hilary Putnam, eds., Cambridge: Cambridge University Press, 207–238, 2nd ed.
Kripke, Saul A., forthcoming, “The Collapse of the Hilbert Program: A Variation on the Gödelian Theme,” Bulletin of Symbolic Logic.
Mancosu, Paolo (ed.), 1998a, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.
Mancosu, Paolo, 1998b, “Hilbert and Bernays on Metamathematics,” in (Mancosu, 1998a), 149–188. Reprinted in Mancosu (2010).
–––, 1999, “Between Russell and Hilbert: Behmann on the foundations of mathematics,” Bulletin of Symbolic Logic, 5(3): 303–330. Reprinted in Mancosu (2010).
–––, 2010, The Adventure of Reason: Interplay Between Philosophy of Mathematics and Mathematical Logic, 1900–1940, Oxford: Oxford University Press.
Mancosu, Paolo, Sergio Galvan, and Richard Zach, 2021, An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs. Oxford: Oxford University Press.
Mancosu, Paolo and Ryckman, Thomas, 2002, “Mathematics and phenomenology: The correspondence between O. Becker and H. Weyl,” Philosophia Mathematica, 10: 130–202. Reprinted in Mancosu (2010).
McCarthy, T., 2016, “Gödel’s third incompleteness theorem,” Dialectica 70: 87–112.
Parsons, Charles, 1998, “Finitism and intuitive knowledge,” in The Philosophy of Mathematics Today, Matthias Schirn, ed., Oxford: Oxford University Press, 249–270.
–––, 2007, Mathematical Thought and its Objects, Cambridge: Cambridge University Press.
Patton, Lydia, 2014, “Hilbert’s objectivity,” Historia Mathematica, 41(2): 188–203.
Peckhaus, Volker, 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoeck und Ruprecht.
Poincaré, Henri, 1906, “Les mathématiques et la logique,” Revue de métaphysique et de morale, 14: 294–317. English translation in Ewald (1996, 1038–1052).
Resnik, Michael D., 1974, “On the philosophical significance of consistency proofs,” Journal of Philosophical Logic, 3: 133–47.
–––, 1980, Frege and the Philosophy of Mathematics, Ithaca: Cornell University Press.
Santos, Paulo Guilherme, Wilfried Sieg, and Reinhard Kahle, forthcoming, “A New Perspective on Completeness and Finitist Consistency,” Journal of Logic and Computation.
Schirn, Matthias, 2019, “The finite and the infinite: On Hilbert’s formalist approach before and after Gödel’s incompleteness theorems,” Logique et Analyse, 245: 1–34.
Schirn, Matthias, and Karl-Georg Niebergall, 2001, “Extensions of the finitist point of view,” History and Philosophy of Logic, 22(3): 135–61.
Shanker, Stuart G., 1988, Gödel’s Theorem in Focus, London: Routledge.
Sieg, Wilfried, 1990, “Reflections on Hilbert’s program,” in Acting and Reflecting, Wilfried Sieg, ed., Dordrecht: Kluwer, 171–82. Reprinted in Sieg (2013).
–––, 1999, “Hilbert’s programs: 1917–1922,” Bulletin of Symbolic Logic, 5(1): 1–44. Reprinted in Sieg (2013).
–––, 2013, Hilbert’s Programs and Beyond, New York: Oxford University Press.
Simpson, Stephen G., 1988, “Partial realizations of Hilbert’s program,” Journal of Symbolic Logic, 53(2): 349–363.
–––, 1999, Subsystems of Second Order Arithmetic, Berlin: Springer.
Smorynski, Craig, 1977, “The incompleteness theorems,” in Handbook of Mathematical Logic, Jon Barwise, ed., Amsterdam: North-Holland, 821–865.
Steiner, Mark, 1975, Mathematical Knowledge, Ithaca: Cornell University Press.
–––, 1991, “Review of Hilbert’s Program: An Essay on Mathematical Instrumentalism (Detlefsen, 1986),” Journal of Philosophy, 88(6): 331–336.
Tait, W. W., 1981, “Finitism,” Journal of Philosophy, 78: 524–546. Reprinted in Tait (2005a, 21–42).
–––, 2002, “Remarks on finitism,” in Reflections on the Foundations of Mathematics. Essays in Honor of Solomon Feferman, Wilfried Sieg, Richard Sommer, and Carolyn Talcott, eds., Association for Symbolic Logic, LNL 15. Reprinted in Tait (2005a, 43–53). [Preprint available online]
–––, 2005a, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History, New York: Oxford University Press.
–––, 2005b, “Appendix to Chapters 1 and 2,” in Tait (2005a, 54–60).
–––, 2019, “What Hilbert and Bernays meant by ‘finitism,’” in Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, Gabriele M. Mras, Paul Weingartner, and Bernhard Ritter (eds.), Berlin: De Gruyter, 249–62.
Takeuti, Gaisi, 1987, Proof Theory (Studies in Logic: 81), Amsterdam: North-Holland, 2nd edition.
Thomas-Bolduc, Aaron, and Eamon Darnell, 2022, “Takeuti’s well-ordering proof: An accessible recontruction,” The Australasian Journal of Logic, 19(1): 1–31.
van Heijenoort, Jean (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic, 1897–1931, Cambridge, Mass.: Harvard University Press.
von Neumann, Johann, 1927, “Zur Hilbertschen Beweistheorie,” Mathematische Zeitschrift, 26: 1–46.
Weyl, Hermann, 1921, “Über die neue Grundlagenkrise der Mathematik,” Mathematische Zeitschrift, 10: 37–79. Reprinted in Weyl (1968, 143–180). English translation in Mancosu (1998a, 86–118).
–––, 1925, “Die heutige Erkenntnislage in der Mathematik,” Symposion, 1: 1–23. Reprinted in: Weyl (1968, 511–42). English translation in: Mancosu (1998a, 123–42).
–––, 1928, “Diskussionsbemerkungen zu dem zweiten Hilbertschen Vortrag über die Grundlagen der Mathematik,” Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 86–88. English translation in van Heijenoort (1967, 480–484).
–––, 1968, Gesammelte Abhandlungen, vol. 1, Berlin: Springer Verlag.
Zach, Richard, 1999, “Completeness before Post: Bernays, Hilbert, and the development of propositional logic,” Bulletin of Symbolic Logic, 5(3): 331–366.
–––, 2003, “The practice of finitism. Epsilon calculus and consistency proofs in Hilbert’s Program,” Synthese, 137: 211–259.
–––, 2004, “Hilbert’s ‘Verunglückter Beweis,’ the first epsilon theorem, and consistency proofs,” History and Philosophy of Logic, 25: 79–94.
–––, 2006, “Hilbert’s program then and now,” in: Dale Jacquette, ed., Philosophy of Logic. Handbook of the Philosophy of Science, vol. 5. Amsterdam: Elsevier, 411–447.

Academic Tools

Other Internet Resources

[Please contact the author with suggestions.]

上一页*与弗雷格的争议——见戈特洛布·弗雷格：弗雷格-希尔伯特争论 controversy with Frege — see Frege, Gottlob: controversy with Hilbert 下一页*希庇亚斯——见智者 Hippias — see Sophists, The

最后更新于12小时前