我们现在来简短地讲一下数学证明是怎样形式化的。我已经说过，某些公式起了数学的形式构造的基石的作用。被称为“公理”、数学证明的本身则是一个可以为直觉接受的图形。它是由按照下面的演绎格式（schema）构成的

[这种格式称为“假言推理”（modus ponens）。下文也由中译者作了一些修改。——中译者注] 横线的上方称为前提（premise）, 下面则是结论（conclusion）。这里的前提和结论都用花体字母 \(\mathfrak {S}\) 和 \(\mathfrak {T}\) 来

表示、并不是因为它们有特殊的意义，它们都只不过是一些命题，不过有不同的来源：它们可能是公理、也可能是公理中的命题被其他命题代入了（substituted）、还可能是前面的演绎过程的最后一个公式、也可能是这个演绎过程中还含有某个公式、而它又被另一个公式代入了。一个公式如果是一个证明过程（即一串假言推理）的最后一个公式、就说此公式是可证明的（provable）。

这个程序还指导我们在创立证明论（即关于这种证明的数学和逻辑学理论）时中选择哪些命题作为公理。尽管还有一定程度的任意性，在选择公理时、还是可以分出某些性质上不同的、属于某一组的公理.。在几何学中我们就是这样做的。下面就是这种分组的例子：

1. 蕴涵公理

1. \(Α \to  ( Β \to  Α ).\) （就是添加一个假设）

2. \( ( B \to C ) \to \{ ( A \to B ) \to   (A \to  C ) \}\) （就是除去一个命题）

Ⅱ否定公理

1. \(\{ A\to (B\& \sim B ) \}\to \sim A.\}\) （就是矛盾律。）

2. \(\sim  \sim A \to  A.\) （就是双重否定律。）

Ⅰ和Ⅱ两组公理只不过就是命题演算的公理。

Ⅲ超穷公理

1. \(a A (a)\to A (b ).\)(由普遍成立可以推断到特例，也叫亚里斯多德公理)

2. \(\sim  (a ) A (a ) \to  (\exists a ) \sim  A (a ). \) （如果一个谓词不能普遍成立。则一定有反例）.

3. \(\sim  (\exists a )\text {\;A\;} (a ) \to  (a ) \sim  A (a ).\) (如果一个命题没有特例。则它对一切 \( ( a )\) 均不真。)

数学和逻辑学发展到了这个时刻，我们发现了一个非常值得注意的事实，就是所有这些超穷公理都可以从单一一个公理导出，这个公理的要点就是所谓选择公理（axiom of choice）、是数学文献中最具争议的公理：

\( ( i^{'} )\quad A (a ) \to  A (\varepsilon A ).\)

这里的 \(\varepsilon\) 就是所谓的超穷逻辑选择函数。

再往下还要加上一些特殊的数学公理，它们就是：

Ⅳ恒等公理

1. \(a =  a.\)

2. \(a =  b \to \{ A (b ) \}.\)

最后还有

Ⅴ自然数的公理 [就是皮亚诺公理。——中译者注]

1. \(a+1\neq0.\)

2. 完全归纳法公理

现在我们已经准备好了完成证明论的创立，构造出可证明公式的系统，也就是建立起整个数学。当我们为了这个成就而感到一般的欢乐、特别是由于我们自己毫不费力就找到了已经发展完善的、必不可少的工具、即逻辑运算、而感到特殊的欢乐之际，决不要忘记对于我们的工作有一个本质的条件。有一个与理想元素方法相关的、然而是绝对必要的条件。这个条件就是相容性（consistency）的证明: 如果想要用理想元素方法来扩展一个领域是合法的、就必须要求这个扩展不会在老的、较窄的领域中带来矛盾，或者换句话说，就是在把理想元素除去以后所余下的关系、在老领域中恒为适用（valid）的。

相容性问题在目前的状况下很容易处理。它显然地可以归结为：用我们的公理、以及设定下来的规则、不会得到 \(1 \neq  1\) 作为一个证明的最后一个式子，也就是说 \(1 \neq  1\) 是一个不可证明的公式。这项任务既属于直觉处理的领域，也像在例如在实地构造的数论中证明 \(\sqrt {2}\) 的无理性一样——就是证明不可能找到两个数值符号 \(a\) 和 \(b\)、使之适合关系式 \(a^{2} =  2 b^{2}\) ，也就是无法找到两个具有某种性质的数值符号。类似于此，我们会义不容辞地去证明不可能找到某一类的证明。一个形式化的证明、和一个数值符号一样，是一个具体而可以看见的对象。我们可以完全地描述它们。进一步说，上述公式所必须的性质、即它可以读作 \(1 \neq  1\)、也是这个证明的可以具体地确定的性质。因为我们可以在事实上证明不可能找到一个以此公式为最后一个公式，我们也就论证了引入理想命题的合理性。

使我们惊喜的是，在这个时候我们也同时解决了长久以来就困扰着数学家的问题，就是证明算术公理的相容性。因为，只要我们在应用公理方法，证明其相容性的问题就产生了。肯定地说，在选择、理解、和应用规则和公理时，我们不愿意单纯地依赖盲目的信念。在几何和物理学理论中，相容性的证明是通过把它化约为算术公理的相容性来实现的。但是我们显然不能用这个方法来证明算术公理自身的相容性。我们的基于引入理想元素的方法来建立的证明理论正是帮助了我们实现这个和关键性的一步，这一步就成了简称公理学的学说拱门的必要的基石。我们已经经历了两次的事情——一次是在处理无穷小演算时遇到过悖论、第二次是在处理集合论时遇到过悖论——就不会再出现第三次了，以后也在不会出现了。

我们在这里概述其要点的证明论不仅能为数学的基础提供坚实可靠的基础，而且我相信也为处理基本的数学问题提供了一个一般的方法、而数学家们迄今未能掌握这个方法。

在一定的意义上说，数学已经成了一个仲裁法庭、一个决定基本问题的最高法庭——裁决的具体的基础是每个人都会同意的，而每一个命题都在其掌控之下。

新近的“直觉主义”（intuitionism）——虽然可能还是比较温和的——在我看来，必须要现在这先庭上得到执照。

可以这样来掌握的这类基本问题的一个例子、是下面的论题：每一个数学问题都是可以解决的。我们都相信确实如此。事实上，吸引我们去破解一个数学问题的主要引力是我们总听到来自我们内心的一个呼喊：问题就在这里，去找出它的答案吧；您只要去想，就一定能找到，因为在数学中没有ignorabimus（不可知的东西）⁸我的证明论并没有给出解决每一个数学问题的一般方法，——这种方法电荷不可能有的。然而，证明每一个数学问题都是可解的是一个相容的假设、这件事完全属于我的理论的范围之中。⁹

现在我要吹响最后一个进军的号角了。一个新理论的试纸就是它解决一些问题的能力，而这些问题虽然人们久已知道，但这个理论本来并非公开地设计来解决它们的。“凭着他们的果子、就可以认出他们来。”[这句格言语出新约圣经马太福音第 7 章，这里的译文就是引自中文圣经和合本的。——中译者注]. 这句格言对于一个理论也是适用的。我在前面已经指出，当康托发现他的第一批超穷数是这个问题就已经出现、即这种超穷的计数方法能否用于这样一些集合、而他从其他来源就已经知道、这些集合在通常意义下是不可数的。一个区间里的点就明显地画出了这类集合。这个问题——即一个区间内的点、也就是实数能不能用前文中给出的表中的那些数来计数——就是著名的连续统假设。康托提出了这个问题，但是没有能够解决它。虽然有些数学家以为、通过否定这个问题的存在就可以处理掉这个问题。但是下面的说明就可以指出他们是大错特错了。连续统问题与其他问题的区分在于它的独特性和内在的美。此外它比之其他问题还有一个优点，就是它把两种品质结合起来了：一方面是它的解决需要新的方法，因为老方法都失败了；另一方面，由于它将会提供的结果的最大的重要性。

我所发展的理论给出了连续统问题的一种解决办法。每一个数学问题都是可解的、证明每一个数学问题都是可解的这一点、正是这种解决办法的第一步、也是最重要的一步…….¹⁰

总结起来，现在回到我们的主要论点、并且从我们的全部关于无穷的思想作出一些结论。我们主要的结果是：在现实世界中并不存在无穷。它即不在自然界中存在，也不能为理性思维提供合法性的基础——它是存在与思维之间的一个奇妙的和谐。与弗雷格和戴德金早前的努力做一个对照，我们相信，某些直觉概念和洞察力对于科学知识是必须的、而仅有逻辑是不够的。只有用有穷主义才能使对于无穷的运作称为确定的。

那么，给无穷留下来能够起的作用是什么呢？就是起一个观念的作用——这里我们是按照康德的用语来理解观念的，它是关于理性的一种看法、它超越了一切经验、而使具体性成为一个整体——在我们建立的这个理论的框架下，我们可以毫不犹豫地相信这个看法。

最后，我要感谢贝奈斯（ Paul Isaac Bernays ，1888–1977，瑞士数学家，[在数理逻辑上有重要贡献.——中译者注]）在本文写作时对于我在技术和编辑两方面的睿智的合作和有价值的帮助，特别是在连续统定理的证明上。

2019 年 5 月 22 日译毕

1. [本文的脚注分为几种情况：有原注，即在Mathematische Annalen上发表时就有的，凡此我们都注明为原注；有由英译者 E.Putnam 和 Gerald J. Massey 写的，我们都注明为英译者注；有由主编 Paul Benacerraf 和 Hilary Putnam 写的，我们都注明为编者注；最后还有由中译者写的，我们都注明为中译者注。原书在这里有原注：感谢Mathematische Annalen的出版者 Springer Verlag 允许文集采用和翻译本文。还要提醒一下，为了阅读的方便，我们把有些注释放在正文中间，但是仍均注明是谁的注解。——中译者注]↩

2. [“谁也不能把我们驱逐出康托为我们建立的天堂”这句常被引用的话原来人们总认为希尔伯特是在歌颂集合论，其实是讲的为了摆脱悖论仍然要研究康托的著作中有用的成分。实际上希尔伯特正是在哺育、强化、使用这些成分的过程中才有了我们即将讨论的超穷数理论、有了有穷主义的思想和实践，正是这一些构成了康托为我们建立的天堂。这句话源出于此。——中译者注]↩

3. 本文中我们都把德文字“inhaltlich”翻译成“material”或“materially”[中文译文则用了“实地”二字。——中译者注]，这种译法是为了说明是与传统上讲的实际与内容和逻辑形式有别。——英译者注。↩

4. [在这里我们第一次遇见了有穷主义（finitary theory, or finitism）这样的提法，那么什么是有穷主义呢？这里似乎缺少了“明确的”定义。这不是偶然的、无关紧要的小事。我们可以说这个脚注之前的一大段话正是对于有穷主义的解释。这一点希尔伯特和贝奈斯合写的《数学基础》第二卷，Grundlagen der Mathematik, Bd. 2, 1939 (此书实际上是贝奈斯写的) 更是明确地说：他们并没有明确地给出 finitistic 和非 finitistic 的界限何在，书中说：“我们并没有把 finitistic 一词作为具有尖锐的界限的用语，而只是作为对于一种方法论的指导原则的描述，[这种描述并没有——这几个字是中译者加的] 使得我们可以把某种概念的形成和推理的方式看成是确定地 finitistic 的，而把另一些看成是确定地非 finitistic 的。这个指导原则并没有给出精确的界限使得符合其要求的就算是 finitistic 的、反之则算是非 finitistic 的。(Hilbert and Bernays 1939, 347–48).”——中译者注]

   ]↩

5. [语出新约圣经哥林多前书第 13 章（这里的译文来自中文圣经的和合本），意为只能在天国中适用、而常人不可能遵守的语言或法令。——中译者注]↩

6. [这里指的当然包含了克隆尼克的名言：上帝创造了整数，其余都是人造的。所以如当然也是人造的，所以是不存在的。同样，克隆尼克也只承认有穷的演绎，而非有穷的演绎也是不存在、无意义的。——中译者注 ]↩

7. 希尔伯特原文“非”的符号是“—”，鉴于在通常的文献中多使用“”这里也改了。——英译者注。[“与”更常用的符号是“”，此外常用的还有表示“当且仅当”；表示“存在唯一一个”；“非”更常用来表示。——中译者注 ]↩

8. 这是一个拉丁字，而更常见的是一句拉丁格言：Ignoramus etignorabimus。Ignoramus 本意是“无知者”、或“我们不知道”，在法律上也会用到这个字，不过这里是一本 17 世纪喜剧的标题。后来德国生理学家 Emil Heinrichdu Bois-Reymond， 1818–1896 把它用于表述科学哲学的不可知论，以为在科学上有许多“我们不知道、也永远不可能知道”的事情。希尔伯特反对这种看法，并且针锋相对地提出自己的非常著名的口号Wir müssen wissen. Wir werden wissen. （英文的标准译法是We must know. We will know.）这个提法见于希尔伯特 1930 年在 Königsberg 的退休演说中，后来成了他的墓志铭。

   ↩

9. [这个问题称为逻辑学的判定问题（decision problem）、或完全性问题，是逻辑学的一个基本问题。——中译者注 ]↩

10. 希尔伯特的原文在此概述了他打算采用的解决连续统问题的方法。这个打算虽然不是没有意义的、但是从来没有实行过。所以现在略去这一部分。——编者注。[关于略去的部分读者可以参看 Jean van Heijenourt, ed.From Frege to Gὂdel, A Source Book in Mathematical Logic, 1879-1931,Harvard Univ. Press Cambridge, 1967. Pp 367-92——中译者注]↩