数学并不总是从一开始就严谨。历史上，无论是伯特兰悖论，还是围绕无穷小量的争论，都曾暴露出定义模糊带来的不确定性。为回应这些问题，数学逐步走向形式化表达。

作者：silverxz
审核： $\Delta\delta Delta$

引言：先问「是什么」

无论是学习数学还是解决数学问题，“先问「是什么」”都是很自然的想法。

比如刚开始学习集合的高中生，首先需要知道集合是什么，哪怕只是朴素地说一句“集合就是把一些对象放在一起构成的整体”。只有先知道它是什么，才能继续回答关于集合的其他问题，或继续学习之后的映射等概念。

到了学习复数的时候，也得先知道“复数就是形如 $x+iy$ 的东西，其中 $x,y$ 是实数”。紧接着再问， $i$ 是什么？这里的加号意味着什么？如此追问，直到“复数是什么”这个问题被回答清楚，才能进行后续的复数模长等的学习。如果不把「是什么」回答清楚，学生将始终云里雾里，自然也就无法继续学习下去。

不过，到底怎样才算是 “把「是什么」回答清楚 ” 呢？一般来说，这个问题似乎不需要回答：人类自己有思维能力和理解能力，自己懂了，那就算是回答清楚了；而自己究竟懂没懂，自己当然知道……真的是这样吗？

很遗憾，不完全是。像自然数、实数、简单的概率和“随机”这样的概念，它们和生活联系紧密，属于常识概念。很多人会觉得自己已经弄得很清楚了，但这有时是幻觉。我们考虑法国数学家伯特兰 (Joseph Bertrand, 1822-1900) 提出的经典概率悖论：

给定一个半径为 $r$ 的圆，随机选取圆中的一条弦。问：这条弦的长度比圆的内接等边三角形的边长（为 $\sqrt 3 r$ ）更长的概率是多少？

圆周上的两个点确定一条弦。出于旋转对称性，我们不妨先固定弦的一端为圆上的任意一点，再随机选取另一端，这样就得到了一条随机的弦，如图 1a。我们以固定的弦端点为顶点，作内接等边三角形（图中灰色三角形），可以发现：当随机的弦在顶点对应的角的内部时（图中红色的弦），其长度大于内接等边三角形的边；在角的外部时（图中蓝色的弦），其长度小于内接等边三角形的边。

因此，若要使取到的弦比内接等边三角形的边更长，则需要取到角内部的红色的弦。而若我们在圆周上等概率随机地取端点，由几何概型，得到红色的弦的概率就是顶角所对的圆弧（图中红褐色的圆弧）占整个圆周长的比例，即 $1/3$ 。我们略去了随机到同一个点，让弦退化成圆周上一点的这种边界退化情况，这不影响概率。

但是，我们不止有这一种随机的方法。对于一条给定的弦（除了直径），恰有一条半径垂直于这条弦，交于一点；反过来，给定半径和半径上一点，也可以过这一点作垂直于半径的直线，与圆相交，确定一条弦。因此，出于旋转对称性，我们任取一条半径，随机取半径上一点，如上所述作与半径垂直的弦，如图 1b。同样，图中红色的弦比内接等边三角形的灰色底边更长，蓝色的弦则更短。若我们等概率随机地取交点，则容易看出，得到红色的更长的弦的概率是 $1/2$ 。同样由于弦取到直径的情况是一种边界的特殊情况，我们忽略其概率，是合理的。

我们还有第三种方法，和上一方法类似：弦（除了直径）的中点唯一确定了弦，因此我们只需随机取圆内部一点作为中点即可，如图 1c。容易看出，若中点取在红色小圆（即内接等边三角形的内切圆）的内部，则可以得到比内接等边三角形的边更长的弦，反之则更短。那么随机取点落在红色小圆的概率是多少呢？如我们熟知的几何概型，为红色小圆与整个圆的面积之比， $1/4$ 。

一个简明的随机取弦的问题，竟然可以利用三种不同方法给出三个不同的概率，这就是伯特兰悖论。

从今天的视角来看，人们对「等概率随机」的朴素直觉大致可以总结为 无差别原则 ：具有相同地位的情况应该是等概率的、平等的。而伯特兰悖论的核心诘难就在于，它给出的三种方法都没有违背无差别原则。没有哪种方法显然不随机，却又给出了截然不同的结果，如果计算没有出错，那就一定是我们对随机的理解出了问题。到底哪种方法才是真正的随机，或者——随机是什么？

于是我们发现，就算是我们自以为已经搞清楚的常识概念，还是会有悖论冒出来，让我们不得不重新追问“那到底指的是什么”。类似的事情在数学史上反复发生：对「是什么」的回答往往不是一次性的，而是反复的“回答、出现问题、重新回答”的过程。最典型的例子当属微积分，尤其是对其中的无穷小量、极限、连续性「是什么」的解释。我们将在下一节简要介绍这段历史，若读者了解一定的微积分知识则更好，不过单就了解历史而言，没有微积分知识也不会有明显妨碍。

无穷小量的发展简史

经典微积分由牛顿 (Isaac Newton, 1643-1727) 和莱布尼茨 (Gottfried Leibniz, 1646-1716) 创立。莱布尼茨认为 [4, p.187]，无穷小量 $\mathrm{d}x$ 是一种比任何可以给出 (assignable) 的量都小的量，且本身无法给出 (inassignable)。这里的“可以给出”大约说的就是像 $1, 0.3, \sqrt 2$ 这样能写出来的实数，那个时代还没有“正实数集”的概念和想法，莱布尼茨自然也就只能这样表述。

当然，莱布尼茨对无穷小量的认识要比这几句话深刻、清楚得多。他还说，无穷小量是一种“不可比量”。所谓可比，指的是欧几里得 (Euclid) 几何原本第五卷第 4 定义（今称阿基米德公理）所定义的可比性。而不可比量，也就是违反了可比性的量 [4, p.201]。直观地讲，它的意思是同一个无穷小量反复相加，加任意有限多次得到的结果也不会比任何正数更大。他对无穷小的阶也有清楚的认识，制定了相对明确的无穷小运算及比较的规则，比如我们计算中常做的忽略高阶无穷小 [5, p.33]。

此外，莱布尼茨对无穷小量的地位也有明确看法：他认为无穷小量是一个虚构的量 (fictions)，不需要对应于实际存在的量，只是可以有助于分析问题 [5, pp.54-55]。

以上的内容大致构成了莱布尼茨对无穷小量「是什么」的回答。至于他对连续和连续性的理解则更粗糙而直觉化 (注 1)，只出于一种朴素的哲学信念：“自然不会跳跃” (natura non facit saltus [nature does not make jumps])。限于篇幅，我们略去更深入的讨论。总之从这样的信念出发，他认为从有限情况外推到无限情况的微积分操作能够成立。

坦白来说，莱布尼茨的观点在他的时代确实够用了。他没有遇到也不会遇到伯特兰悖论那样的东西，自然也没有动机给出更严密的定义。但在牛顿和莱布尼茨去世后不久，贝克莱 (George Berkeley, 1685-1743) 于 1734 年发表著作《分析学家》(The Analyst)，对经典微积分中的无穷小量予以抨击：无穷小量一方面作为非零的量存在于分母中，另一方面又像 $0$ 一样在最后被忽略掉，说不清楚。我们很难说这样的抨击在多大程度上化为了动力，但无论如何，人们此后开始尝试更清楚地回答无穷小量「是什么」的问题，希望它能像珠玉在前的欧氏几何一样清晰严谨。

其中，对现代微积分的理论基础影响最大的一支 (注 2) 是从 18 世纪到 19 世纪初的一系列法国数学家：从达朗贝尔 (Jean Le Rond d’Alembert, 1717-1783)，到拉格朗日 (Joseph Lagrange, 1736-1813)，到拉克鲁瓦 (Sylvestre Lacroix, 1765-1843)，再到柯西 (Augustin Cauchy, 1789-1857)……在柯西 1821 年发表的教材 Cours d’analyse 中，无穷小量已经被定义为一个极限为 $0$ 的“变化量” (quantité variable)，换言之，这是一个逼近的过程而不是一个确定的数。不过，柯西在实际使用中对无穷小量和它的极限值的区分不甚明显，可以说他对无穷小量的地位的实际态度颇为模糊暧昧 (注 3)。

随后，德语世界的数学家接手，包括了从波西米亚数学家波尔查诺 (Bernard Bolzano, 1781-1848) 到德国的几位数学家魏尔斯特拉斯 (Karl Weierstrass, 1815-1897)，戴德金 (Richard Dedekind, 1831-1916)，康托 (Georg Cantor, 1845-1918)等人。现在一般认为是魏尔斯特拉斯奠定了现代标准分析的基础，他明确提出了极限和连续性的 $\varepsilon-\delta$ 形式的定义，无穷小量也基于此定义，和我们现在学到的东西已经基本一致了。随着后续戴德金和康托对集合论以及实数理论的进一步完善，跨越两百年，无穷小量「是什么」的问题终于得到了令大部分人基本满意的回答。

形式化数学

数学家们花了两百年，大小数次迭代，才算是把无穷小量「是什么」的问题回答清楚。倘若每个概念都这么折腾两百年，那可真是件麻烦事。有没有什么一劳永逸的解决方法，让我们能把这个问题一次性回答好呢？有没有什么标准能判断我们的回答是否足够好呢？

19世纪末到20世纪初的数学家们尝试做这件事。弗雷格 (Gottlob Frege, 1848-1925) 和皮亚诺 (Giuseppe Peano, 1858-1932) 等人奠定了数理逻辑的基础，我们今天用到的许多逻辑符号如集合元素的属于 $\in$ ，集合的交 $\cap$ 与并 $\cup$ ，以及存在量词 $\exists$ 就来自于皮亚诺[6]；弗雷格也有一套自己的记号，但是有点怪，所以没有沿用下来。

借由逻辑符号，我们就可以更简洁精准地讲数学。对比魏尔斯特拉斯风格的连续性定义(注 4)，函数 $f$ 在点 $x$ 处连续当且仅当如下命题成立：

可以确定一个与 $0$ 不同的、可以任意小但有限的 $\delta$ ，使 $|f(x+h)-f(x)| < \varepsilon$ 对所有满足 $|h| <\delta$ 的 $h$ 成立，其中 $\varepsilon$ 表示一个任意小的给定的量。

今天，这一命题已经转写成由逻辑符号组成的如下式子

$\forall \varepsilon > 0\ \exists \delta > 0\ \forall h \in \mathbb{R} \ \big( |h| < \delta \to |f(x+h) - f(x)| < \varepsilon\big).$

考虑到读者可能并不完全清楚这些逻辑符号的意思，我们稍微解释一下它们在命题中的意思，并举一些简单的例子。

$\forall$ 的意思是“对任意”。 $\forall x\ (P(x))$ 的意思就是，对于任意的 $x$ ， $x$ 都满足性质 $P$ . 一个简单的例子是， $\forall n\in \mathbb{N}\ (n^2 \geq n)$ 的意思是，对任意的自然数 $n$ ，都有 $n^2 \geq n$ 成立。容易看出，这是一个真命题。

$\exists$ 的意思是“存在”。与 $\forall$ 类似， $\exists x\ (P(x))$ 的意思就是存在一个 $x$ 满足性质 $P$ . 而 $\exists n\in \mathbb{N}\ (n^2 < n)$ 的意思就是，存在自然数 $n$ 使 $n^2 < n$ 成立。容易看出，这是一个假命题，而且是 $\forall n\in \mathbb{N}\ (n^2 \geq n)$ 这一命题的否定。

$\to$ 的意思是“实质蕴涵”。具体来说， $P\to Q$ 的意思是，若 $P$ 成立，那么 $Q$ 成立。 $\forall x \in \mathbb{R}\ (x^2=1\to x=1)$ 就是一个假命题，因为 $x$ 可以取 $-1$ 使它不成立。而 $\forall x \in \mathbb{R}\ (x=1 \to x^2=1)$ 显然是一个真命题。

其他符号如加减运算、比较大小、取绝对值就不再解释。现在我们回过头来，看看那个定义连续性的一串逻辑符号究竟是什么意思。翻译过来也就是：对任意的大于 $0$ 的数 $\varepsilon$ 都存在一个大于 $0$ 的数 $\delta$ ，使对任意的实数 $h$ 而言，只要 $|h| < \delta$ ，就有 $|f(x+h)-f(x)| < \varepsilon$ 成立。

把它和之前魏尔斯特拉斯风格的连续性定义对比一下，你觉得它们一样吗？

它们想表达的意思肯定是一样的。但是魏尔斯特拉斯风格的定义明显有一些模糊，且容易导致歧义：到底是先确定 $\delta$ 再给定 $\varepsilon$ ，还是先给定 $\varepsilon$ 再确定 $\delta$ ？它想要表达的是后者，叙述顺序上却把 $\varepsilon$ 放到最后，这就要读者仔细辨意，努力领会了。与之相比，逻辑符号的表述就不会出现这种问题。 $\exists \delta > 0$ 是被前面的 $\forall \varepsilon > 0$ “统辖”的，唯一的解读方式就是先给定 $\varepsilon$ ，再确定 $\delta$ .

这就是逻辑符号的一个重要优点，可以避免自然语言（即我们说的这些汉语、英语等语言）潜在的模糊或歧义，或者说，可以强迫你把其中的模糊和歧义一一澄清。另一方面，虽然我们通常不会真的用纯逻辑符号写证明，但了解这些逻辑符号也会有助于我们减少自然语言使用中的歧义，因为我们会在脑袋里有意或无意地“校验”它能否翻译成纯逻辑符号的语言。

我们再举一个关于自然语言歧义的经典例子，它来自另一位重要的逻辑学家与数学家罗素 (Bertrand Russell, 1872-1970)。考虑以下命题[7]：现任法国国王不是秃头 (the present King of France is not bald)。要是有那么一个法国国王，事情倒还好办，问题在于彼时 (1905年) 的法兰西第三共和国是共和制而非君主制，其国家元首是选举产生的总统而非国王。换言之，“现任法国国王”并不存在。

于是，这一自然语言写就的命题的真假就会引起争论。有人会说，这是对国王的描述，而国王不存在，因此是假命题。有人会说，难道你能说一个不存在的国王的确是秃头吗？既然不能，那么“不是秃头”就是真命题(注 5)。还有人说，若国王不存在，则这个命题没有意义，不能讨论真假。

但若写成逻辑公式的形式(注 6)，那就清楚多了，因为它强迫你澄清其中的歧义。设 $K(x)$ 表示「 $x$ 是现任法国国王」，而 $B(x)$ 表示「 $x$ 是秃头」。若我们将前述命题翻译为

$\neg \exists x\bigl(K(x) \land \forall y(K(y)\rightarrow y=x) \land B(x)\bigr)$

即（这里 $\land$ 的意思是“且”， $\neg$ 是对后面的否定）不存在一个满足如下条件的 $x$ ： $x$ 是现任法国国王，且若 $y$ 也是现任法国国王则 $y=x$ （保证现任法国国王至多只有一个），且 $x$ 是秃头。如此一来，的确不存在这样的 $x$ ，因此该逻辑公式为真。

而我们若采取另一种翻译方式

$\exists x\bigl(K(x) \land \forall y(K(y)\rightarrow y=x) \land \neg B(x)\bigr)$

即，存在一个满足如下条件的 $x$ ： $x$ 是现任法国国王，且若 $y$ 也是现任法国国王则 $y=x$ ，且 $x$ 不是秃头。按这种翻译方式，由于不存在现任法国国王，还是不存在这样的 $x$ ，因此该逻辑公式为假。

看起来，两种翻译方式得到了真假各异的逻辑公式，这不是更混乱了吗？但这并不是逻辑公式的问题，而是那个自然语言写就的命题中原本就存在的歧义导致的。逻辑公式要求你把歧义说清楚：否定 $\neg$ 到底加在内层还是外层，是不是秃头，还是 不存在 $x$ 。说清楚以后，命题的真假性就是显然的了(注 7)。

总而言之，将自然语言写就的内容澄清为逻辑公式确有益处。在今天的数学学习和研究中，一般也不会把所有自然语言都拿掉，变成全是逻辑符号的天书。但遇到争议或模糊不清之处时，我们总是可以（也理应确保可以）把它具体写成逻辑公式来予以澄清。

但是，到现在为止，我们只是在用逻辑符号来翻译、澄清自然语言，它只是在帮我们把我们原来就想说的话讲清楚。我们还是在按自然语言思考，按现实世界的情形思考，考虑现实中有没有那么一个国王。这已经很有用了，但有一些数学家在考虑更激进大胆的事：我们能否先不管逻辑公式在现实中的语义，将其视为纯粹的符号做逻辑推理？

这样说着可能有点难懂，我们举个例子。考虑经典的三段论：

大前提：所有人都会死；
小前提：所有希腊人都是人；
结论：所有希腊人都会死。

这样的论证完全可以抽象成：

大前提：所有具有性质 $M$ 的 $x$ 都有性质 $P$ ；
小前提：所有具有性质 $S$ 的 $x$ 都有性质 $M$ ；
结论：所有具有性质 $S$ 的 $x$ 都有性质 $P$ 。

若使用同名的谓词，即，设 $M(x)$ 表示 $x$ 是否具有性质 $M$ ， $P(x),S(x)$ 同理，那么上述三段论可以翻译成以下的逻辑公式

$\big(\left(\forall x (M(x)\to P(x))\right) \land \left(\forall x (S(x)\to M(x))\right)\big) \to \forall x (S(x)\to P(x))$

若读者阅读这样的式子尚有困难，也没关系，只需领会到：三段论本质上是一种一般、通用的推理模式，它并不依赖于其中的性质 $M,P,S$ 具体是什么，因此我们可以抛开语义去做纯粹的符号推导。而此时数学家们要做的事情比这更一般化。

这项工作中最有代表性的数学家无疑是希尔伯特 (David Hilbert, 1862-1943)，他是那个时代最有影响力的大数学家之一。从生卒年份中也可以看出，他与皮亚诺和罗素大致是同一时代的人。可以说是生逢其时，数理逻辑刚刚得以发展，他正好能借助这些工具构建他想要的“形式系统”(注 8)。

形式系统(注 9)将给定一个符号表，比如表示命题变量的 $p, q, \dots$ 和表示逻辑的 $\to, \land, \lor, \dots$ 。在形式系统中，所有能谈论的东西都只是符号表中的符号满足一定规则的排列组合（如 $p\to q$ ），我们只能基于这种规则下定义，即 形式化定义 ；而所有允许的推理方式也只是形式系统给定的一些摆弄符号的方式（就类似于上面的三段论）。你只能从形式系统事先给定的一些默认为真的公理出发，且只能使用它给定的推理方式一步一步推导来证明其他结论，此即 形式化证明 。这样描述和发展的数学就叫 形式化数学 。

这意味着，你不能在形式系统中使用描述性的自然语言下定义，不能说“连续就是可以一笔不间断地画出来”这样的话；你也不能在形式系统中借助物理意义或者现实经验来推导，不能像伽利略那样用称重的方式测量摆线下面积，也不能用量角器来猜答案，因为这些内容没有被纳入形式系统允许的推理规则中。这些限制换来的好处就是，你给出的每一个形式化定义都是清晰的，无需再进一步补充，也没有再补充的余地；形式化证明也是一样，人们可以按照它每一步使用的推理方式机械地检验它。

当然，别人仍然可以追问“你为什么要这样定义”，“你为什么要把函数的连续性定义成这样而不是那样”，这是你仍然需要澄清的；但是无论你选择给出什么样的形式化定义，这一定义本身已经清楚。这与之前的情况已经大不一样了。之前我们需要反复地追问「是什么」，因为我们的自然语言定义往往说不清「是什么」，这正是我们在前面的伯特兰悖论和无穷小量发展中遇到的问题；而现在，在形式系统中，既然概念已经清晰，那么「是什么」不再需要追问，只需要问「为什么是这个？」

一个形式系统中，对“若 $p\to q$ 且 $q\to r$ ，那么 $p\to r$ ”的严格证明可能长下面这个样子（右侧是注释，我们省略规则的明确定义，但读者应该能看出这些规则是自然的）。倘若阅读有困难也没关系，读者不必完全读懂，只需感受一下：

$\begin{array}{rll} (0) & ((p \rightarrow q) \land (q \rightarrow r)) \to (p \rightarrow r) & \text{待证目标} \\[6pt] (1) & (p \rightarrow q) \land (q \rightarrow r) & \text{引入假设1} \\[6pt] (2) & p \rightarrow q & \text{由 (1)，根据合取消去规则取左边分量得到} \\[6pt] (3) & q \rightarrow r & \text{由 (1)，根据合取消去规则取右边分量得到} \\[6pt] (4) & p & \text{引入假设2} \\[6pt] (5) & q & \text{由 (2) 和 (4)，根据假言推理规则推出} \\[6pt] (6) & r & \text{由 (3) 和 (5)，根据假言推理规则推出} \\[6pt] (7) & p \rightarrow r & \text{消去假设2，引入蕴含式} \\[6pt] (8) & ((p \rightarrow q) \land (q \rightarrow r)) \rightarrow (p \rightarrow r) & \text{消去假设1，引入蕴含式，得到待证目标} \\[6pt] (9) & \Box & \text{证明结束} \end{array}$

由此，一个新的时代开启了。一些人以此为分界线，称这一时期 (1890-1930) 以后的数学为现代数学。

如今的数学工作强烈受到形式系统的影响。这种影响指的并不是所有人都要写完全形式化的证明，而是一种潜移默化的形式化信念。这种信念要求大部分概念的定义都需要具体到让人们相信这可以被形式化的程度，且原则上，证明也应该具体到让人们相信这可以被翻译成形式系统上的一步步推导的程度。否则，人们就可能怀疑或不接受这样的定义与证明。

为什么通常做到可以让人们相信的程度就够了，而不是要求完全的形式化？原因之一是，形式化的证明太过复杂繁琐，就像上面的例子那样，这个命题平时会不加证明地直接使用，在形式化证明中却要写 $9$ 行，可想而知其他证明的形式化版本有多复杂冗长。原因之二则更关键：纯形式化的方式并不符合人类的思维方式，也无法传达背后的数学直觉。即便想要写出完全形式化的证明，人们通常也要先写出或先想好一个朴素的半自然语言半形式化的证明，再逐步把它翻译成形式语言。而读懂一份完全形式化的证明到底在做什么更是非常困难，因此在数学教育或数学交流中难以直接使用完全形式化的证明。

但是，如果定义和证明还是混杂了自然语言，那不是和以前没有区别吗？并不是这样的。这里的关键在于，自然语言在现代数学中所处的位置已经悄然改变了。早期数学中的自然语言直接作为论证本身，因而更容易依赖图形直观、物理与几何意义、以及问题背景，也更容易产生未经说明的跳步；现代数学中的自然语言则像是对形式系统中推理的压缩，只有人们相信它可以被翻译成纯形式化的表述时，它才会被人们接受。

在这种环境下经受数学教育的人们也会自然而然地接受相应的训练，这也是形式化数学所产生影响的一部分。前述的极限和连续性的例子可能就是如今数学系学生最早接触到的足够形式化的例子之一，他们将在数学学习中大量、反复接触这样的东西，适应形式化的思想和观点，从而能够更好地判断“能否形式化”，使他们的相信更可靠。当然，一个自然的问题是：人都会犯错，仅仅靠相信难道不会导致错误吗？的确会，这件事我们稍后再谈。

数学与形式化数学：误区及其澄清

前述内容已经大致完整，关于形式化数学的普及往往就停留在这里。但是如果真的停在这里，就很容易导致读者产生误解。

看起来数学家们已经完美解决了问题：只要在形式系统里回答「是什么」的问题就足够了，且一劳永逸，是吗？很难说是或不是，这是个微妙的问题。

我们上面的论断往往都加了一个前提：“在形式系统中”。 在形式系统中 ，你给出的定义都是清楚的； 在形式系统中 ，你做出的证明永远不会含糊、出现歧义，总是可以机械地验证证明的正确性。形式系统内部的定义和推理规则都是一些符号，完全不需要自然语言，但形式系统本身的定义呢？

我们没有给出形式系统的正式定义，但可以料想的是，我们无法完全脱离自然语言来定义它。借用维特根斯坦所说的“语言的边界是世界的边界”的字面意思，我们总得用点什么来定义它吧？如果不使用自然语言，我们就没有“谈论”和“定义”的工具了。

当然，你可以用形式系统来定义形式系统，我们也的确会这么做。但这只是把问题往上推了一层，并不能解决问题：你用来定义形式系统的另一个形式系统又是怎么定义的呢？推到最后，我们还是不得不使用一些自然语言和朴素的数学来定义它。比如，当我们说“ $1$ 个符号”的时候，这本身就用到了自然语言，且同时用到了朴素的数学，自然数 $1$ 。

希尔伯特等人当然早就明确知道这一点。希尔伯特认为，可以用很简单的“有限算数推理”来讨论和刻画形式系统。于是大的图景是这样的：

我们只需要拿出一小撮数学内容就可以基于此搭建形式系统、发展形式化数学。比如，一个典型的例子是，原始递归算术(注 10)就可以充当这一小撮东西，它只包含最朴素的自然数运算和非常基本的归纳法。这一小撮是真的很小，但无论如何，我们确实需要那么一小撮东西才能把这一切搭建起来。于是我们可以澄清一些常见的误区：

[ 误区1]. 如今，数学已经完全被形式化了，形式化数学就是数学的全部。

这可能是刚刚接触数理逻辑与集合论的人常常会产生的误解。上述的分析已经表明了这是错误的，因为在迄今为止我们所见到的所有数学实践中，形式化数学本身总是仍然需要一些朴素的、超出形式化数学之外的一些数学。换句话说，迄今为止，形式化数学没有覆盖全部的数学实践，并且尚未表现出可以完全不依赖元数学层的迹象。只是，形式化数学用到的非形式化的元数学部分对于大部分人来说实在太小、太基本、太不起眼，而且它起到了良好的隔离作用：在你承认形式系统已经存在的前提下，你的确可以完全在形式系统内部工作而完全不碰形式系统外的东西，让人们产生形式化数学似乎就是全部数学的错觉。

[ 误区2]. 数学是不具备意义的机械的符号推导游戏。

这一误区和上一条往往是连着的，有些人认为数学=形式化数学，而形式化数学又是纯粹的、可以不带有语义的符号推导，从而得到了数学是无意义的符号推导的朴素哲学观点。既然已经说过上一条是错误的，这一条自然也被动摇了：即便你认为形式化数学是无意义的符号推导，但还有搭建形式化数学的非形式化数学存在。无论你认为那部分数学是什么，但它至少不是符号推导游戏。除非你找到一种真正的脱离非形式化数学的方法完成形式化的工作，否则这总是一个过于极端、难以捍卫的观点。

不过，如果我们从这个误区稍微往后退一步，就能看到形式系统的另一益处（也可能是害处？）：它将许多数学哲学问题与数学实践隔离开来。形式系统中的证明确实可以视为是在摆弄一些符号，我们可以机械地检验证明，证明的正确性和那些符号的意义无关；而那些符号究竟具有怎样的意义，是否对应于现实中或者我们心中的某些对象——比如我们写下的 $\mathbb{N}$ 是否真的对应于我们心中的自然数集，这些则是另外的数学哲学问题。数学工作者往往不需要关心这些数学哲学问题就可以在形式系统内工作，这的确是一层干净的隔离；但另一方面，这也让不少数学学习者和工作者越来越缺乏对数学哲学的了解。

话说回来，若数学不是符号推导游戏，那它究竟是什么？形式化数学又扮演什么样的角色？这当然是非常复杂的数学哲学问题，能力与篇幅所限，我们无法给出详尽的讨论。不过，我们可以给出一些简单的观察和论述。

[ 实践观察]. 在形式化数学诞生以前，数学活动、数学实践就已经存在，且形成了一套相对稳定的对象域，如自然数、实数轴、欧氏空间等。20世纪的许多形式化数学的尝试中，数学工作者试图用形式系统来刻画预先存在于数学实践中的某个结构。
现实中，绝大多数数学工作者并不是在某个形式系统里做完全机械的纯符号推导。相反，他们仍然在头脑里以一种非形式化的形式思考，借助他们在数学实践中养成的直觉、图像与图示、甚至于借助某些问题固有的物理意义与现实意义来思考问题，再用自然语言、图片、符号的混搭方式来组织自己的证明。
现代数学实践中，一个可信的证明通常需要在原则上可以被形式化，纵然数学工作者们往往不会给出真正形式化的证明，而是停留在能说服其他人“这可以被严格形式化”的程度。

我们不在这里讨论太多数学哲学。至少上述的实践观察表明，对于数学工作者而言，非形式化的数学实践往往是先行的，而具体的形式系统则像是后来加上去的一层刻画、验证的工具。但由于形式化证明已经成为了证明应有的标杆，所以许多数学家其实秉持相对混杂的数学哲学立场，自己也不甚明了。我们截取 Peter Smith 的一段话(注 11)：

Imre 很快地勾勒了几种关于数学的哲学立场，他称之为柏拉图主义（platonism）和形式主义（formalism）。他的说法是：数学家在对“自己究竟在做什么”的预设上，往往倾向于采取柏拉图主义的立场（也就是说，他们预设自己是在探索某个确定的抽象数学宇宙，那里有客观存在的真理等待被发现）；但当他们写公开的证明时，又会转变成形式主义者。
……
……Imre 把形式主义刻画成一种关于数学本质的观点，大致是：“数学完全就是在摆弄无意义的符号，是一场游戏：按照给定的规则，看你能从某些符号串‘推导’出哪些别的符号串。”首先值得强调的是，至少就数学哲学史上那些真正严肃的参与者而言，这多少像是个“稻草人”立场。比如，伟大的希尔伯特通常被视为典型的形式主义者，但他的立场要细腻复杂得多。只是，好吧，我也确实听过其他数学家用这种天真的“一切不过是摆弄符号”的说法来描述数学。而我想指出的是：把任何形式的形式主义（不论是像 Imre 这样朴素的版本还是更复杂的版本）与推进形式化这一计划混为一谈是一种错误。

Peter Smith 批评的稻草人立场正是我们之前谈到的一个误区，他说得更严厉一些。鉴于数学家们的数学哲学立场往往也不甚清楚，我们就不在这里碰这个难题了。但无论我们秉持什么样的哲学立场，是否深入思考数学哲学，非形式化数学与形式化数学在实践中的地位都是不可忽视的，数学工作者以非形式化的方式思考，以形式化的方式和可形式化的信念作为一种可靠的校验。

人总会出错。2002年的菲尔兹奖得主弗沃特斯基 (Vladimir Voevodsky, 1966-2017) 工作的领域非常艰深复杂，他1989年发表的论文在1998年才被发现错误，而且直到2013年他才确定这的确是一个错误[8]。类似的事情在他的领域中不止一次出现，令他非常担忧，这导致他后来直接转换方向，去做用计算机辅助验证形式化证明的工作(注 12)。

是的，人们可以用计算机来帮助编写形式化证明和验证形式化证明。计算机的诞生和发展一定程度上缓解了“人工编写和验证形式化证明极度困难”的困境。在笔者写下这段文本时，Lean (一款开源交互式定理证明器) 社区维护的大型通用数学库 mathlib 已经完成了 125901 个定义和 262213 个定理的形式化工作，有七百余人直接做出贡献[9]。现有的许多大定理如四色定理[10]都已经转写成形式化证明、经计算机验证其正确性，不过这仍然是相当大的工程，往往要耗费数年。但随着各种库的完善以及近年来深度学习的发展，将人类证明翻译成机器可验证的形式化证明的难度正在降低。非形式化数学与形式化数学(当然)在同步向前发展，或许我们可以期待有朝一日证明助手 (proof assistant) 迭代到足够好用的程度，能够自动转写我们写下的大部分自然语言证明为形式化证明并加以验证。

这篇文章已经不短，但它仍然只是浅尝辄止。我们没有回答最初的伯特兰悖论具体要如何解决，没有给出更完善的微积分数学史，没有给出形式系统相关内容的基本定义和实例，也没有对数学哲学做出什么充分的讨论。这其中的每一点都值得单独拿出来讨论，会带出一门课，或本身就是一门课甚至更多。对于那些连基本的分析学都尚没有开始学习的读者，也不必着急，继续一点一点学习即可。本文若能让这样的读者望见远方有一座形式化的灯塔，让他们走到那里之前不至于太过迷茫；能在接触抽象语言定义的概念时不再烦躁，理解其形式化的必要；或者在追求极端的形式化数学时想起形式化并不是数学的全部——若能做到这一点的话，本文的作用就已经足够了。

Remarks

这一部分是出于严谨性打的补丁，或是相对于正文来说比较复杂、深入、困难的扩展内容，可以略过。

注 1. 莱布尼茨其实已经阐述过与现代 $\varepsilon-\delta$ 语言含义相接近的内容[11, p.291]，但只是在形式和性质上相似，并不意味着莱布尼茨认为这是连续性的定义或实质意涵。这更像是从他心中的连续性推出来的性质之一。

注 2. 历史是十分复杂的，不是线性向前推进的。限于篇幅，文中仅能线性地描述其中一支，事实上也有许多其他数学家做出努力。且即便只是这一支，笔者也仅是在每一代人中取出较有代表性的一人，再整体总结，远远不能尽述。另一方面，也并非所有数学家都着眼于这方面的工作。比如同一时代的大数学家欧拉 (Leonhard Euler, 1707-1783) ，虽然也表达了严格化的精神，但实践中仍然把无穷小量以等于零或不等于零的方式混合应用[12]，这并不妨碍欧拉极大发展了整个分析学与数学。

注 3. 柯西对无穷小量本体论问题的实际态度颇为模糊暧昧。20 世纪的史学工作者如 Grabiner 等认为柯西是 $\varepsilon-\delta$ 语言的先驱，给出了现代标准分析的定义雏形，也成为现今教科书提及历史时的主流叙述。21 世纪的史学工作者如 Katz 等人则对这种偏向辉格史观的解读方式提出质疑[13, pp. 15-17]。如今学界仍在争论，各执一词，不能确定。

注 4. 我们这里引用的连续性定义来自 Kronecker 的讲义（经Eugen Netto 编辑整理）[14, p. 12]，鉴于 Kronecker 和 Weierstrass 走得很近，而这一表述形式也的确来自于 Weierstrass，正文中就泛泛地将其称之为“魏尔斯特拉斯风格的表述”。为了使读者不必费心关注字母使用的差异，正文的表述稍微调整了字母的使用并做了简单的等价变形。这不改变原意。

另外，正文中连续性的定义悄悄省略了函数的定义域 $\mathbb{R}$ 。这是因为本文不打算碰“什么是实数”、“ $\mathbb{R}$ 究竟是如何定义的”这样的难题。

注 5. 这一论断实际上使用了“排中律” (law of excluded middle)，即命题与命题的否定一定有一个是真的，或者形式化地说， $P\lor \neg P$ 恒真。实际上，正文中的例子就是对排中律的一个简单诘难（由于现任法国国王不存在，那么“现任法国国王是秃头”与“不是秃头”可能会被解读为都是假的，从而违背了排中律）；但罗素作为排中律的支持者，他将这一命题换成更清晰的逻辑符号表达，从而恢复了排中律的有效性。

读者可能认为，排中律总是无条件成立的，时至今日主流数学也的确仍然这样默认。某种程度上这是因为它太好用，就像希尔伯特说过的[15]，“从数学家那里拿走排中律，就像禁止天文学家使用望远镜或禁止拳击手使用拳头”。但的确有一些人（通常秉持数学哲学中的直觉主义）认为排中律并不应该无条件成立，如直觉主义的奠基者布劳威尔 (L. E. J. Brouwer, 1881-1966)，由此发展出直觉主义数学。这一话题的深入讨论已经远超出本文的范围。

注 6. 为了方便，我们这里使用的符号是现代的，而不是罗素使用的符号。事实上，罗素当时也没有完全使用逻辑符号来表达，但是他的表达是逻辑化的。

注 7. 有些读者可能对正文中的命题有另外的翻译方式：若 $x$ 是唯一的现任法国国王，则 $x$ 不是秃头，即

$\forall x\bigl( (K(x)\land \forall y(K(y)\to y=x))\rightarrow \neg B(x)\bigr)$

这样根据“前件为假，命题为真”的“空真”原则 (vacuously true)，由于现任法国国王不存在， $K(x)$ 始终为假，这是一个真命题。这的确也是一种翻译方式，且实质上和正文中的第一种是等价的。只需简单地把第一种中 $\neg \exists$ 的否定放到里面去，再根据 $P\land \neg Q$ 与 $P\to Q$ 互为否定进行变形即可验证。

注 8. 若只能选一个人作为形式系统诞生和发展的代表，当然是正文中的希尔伯特。然而，数学发展也是基于时代的，现代意义的形式系统概念并非由某个人一次性提出，而是从早期的弗雷格、皮亚诺，到希尔伯特与希尔伯特学派（一个模糊的概念，此处指1910-1930在哥廷根与希尔伯特做相关工作的数学家们），再到后来的哥德尔 (Kurt Gödel, 1906-1978)、图灵 (Alan Turing, 1912-1954)，逐渐形成越来越明确的定义。哥德尔于1963年回顾时说[16, p.7]，“由于图灵1937年的工作，现在可以给出形式系统的精确、无可置疑的一般定义”。

注 9. 非常遗憾，经过考量，我决定不给出形式系统的正式定义，也不举任何具体的例子，否则它会变得过于难。对于尚没有进行经典微积分这一层次的数学学习的读者，笔者也不认为过早地扎进形式系统中是一件有益的事情，他们可以在 $\varepsilon-\delta$ 的磨炼中逐渐认识到形式化是怎样一件事。

另外值得注意的是，形式系统如今其实是一个很宽泛的、甚至常常被滥用的术语。严格的讲解需要把形式语言、语法与语义、结构与模型、理论、证明系统等概念拆开来一一说明，还要阐述「真」与「可证」之间的区别。这些远超本文的范围，所以正文中忽略了这一部分，也没有提到模型和真值这一层面，只是留在语法与证明这一层，刻意用笼统的“形式系统”一词把它们都装进去，仅以传达直觉与大致方向为目的。

顺便一提，许多读者可能听说过哥德尔的一些结果，比如他的完备性定理和不完备性定理。按理来说，讲形式化数学却完全不触及哥德尔的结果，这是一种遗憾，或许也是不完善之处。但是在「真」与「可证」的区别都尚未澄清的情况下，想要真正理解哥德尔的结果几乎是不可能的。我们仅在这里浅尝辄止地提一下：哥德尔的结果表明，希尔伯特的设想不能以最乐观的版本完成。但是这一“挫败”并不影响我们正文中阐述的内容，甚至可以说，哥德尔的结果本身就是形式化数学带来的巨大成就的一部分。

注 10. 技术上，原始递归算术 (PRA) 可以编码、研究其他的形式系统，也就是正文中所说的“用形式系统定义形式系统”的实际含义，因此可以在其中形式化地编码和讨论我们更熟悉的、实际常用的 ZFC 等较强的系统。Tait 等人将这一路线视为是对希尔伯特的有限主义 (finitism) 的一种精确重述[17, p.5]；但是 Zach 等人认为希尔伯特学派的一些证明中实际使用了超出 PRA 的内容，故不能与 PRA 简单等同[18]。这部分是历史问题，并不影响 PRA 的数学地位。

值得注意的是，我们在这里总是使用“希尔伯特的有限主义”一词，因为有各种不同的主张（甚至是不同层面的主张）都可以冠名为有限主义，需要加上额外限定才能不致混淆。

注 11. 相关内容可参考[19]，推荐对数学哲学感兴趣的读者进一步阅读，不仅扩展了我们这里的粗浅讨论，也包含了许多其他内容。

其中译推荐参考https://zhuanlan.zhihu.com/p/683120242

注 12. 若读者想要简单了解什么是计算机辅助形式化证明，可以参考 Lean 社区发布的小游戏，边玩边学：

https://adam.math.hhu.de/#/g/leanprover-community/nng4

参考文献

[1] File:Bertrand1‑figure.Svg ‑ Wikipedia. URL: https://commons.wikimedia.org/wiki/File:Bertrand1-figure.svg (visited on 02/03/2026).
[2] File:Bertrand2‑figure.Svg ‑ Wikipedia. URL: https://commons.wikimedia.org/wiki/File:Bertrand2-figure.svg (visited on 02/03/2026).
[3] File:Bertrand3‑figure.Svg ‑ Wikipedia. URL: https://commons.wikimedia.org/wiki/File:Bertrand3-figure.svg (visited on 02/03/2026).
[4] J. Bair et al. “Leibniz’s Well‑Founded Fictions and Their Interpetations”. In:Matematychni Studii 49.2 (June 30, 2018), pp. 186–224. ISSN: 1027‑4634. DOI:10.15330/ms.49.2.186-224. URL: http://matstud.org.ua/texts/2018/49_2/186-224.pdf (visited on 02/03/2026).
[5] H. J. M. Bos. “Differentials, Higher‑Order Differentials and the Derivative inthe Leibnizian Calculus”. In: Archive for History of Exact Sciences 14.1 (1974),pp. 1–90. ISSN: 0003‑9519, 1432‑0657. DOI: 10.1007/BF00327456. URL: http://link.springer.com/10.1007/BF00327456 (visited on 02/03/2026).
[6] Earliest Uses of Symbols of Set Theory and Logic. Maths History. URL: https://mathshistory.st- andrews.ac.uk/Miller/mathsym/set/ (visited on 02/04/2026).
[7] Bertrand Russell. “On Denoting”. In: Mind 14.56 (1905), pp. 479–493. JSTOR: 2248381. URL: https://www.jstor.org/stable/2248381 (visited on 02/04/2026).
[8] Vladimir Voevodsky. “The Origins and Motivations of Univalent Founda‑tions”. In: The Institute Letter (2014), pp. 8–9.
[9] Mathlib Statistics. URL: https://leanprover-community.github.io/mathlib_stats.html (visited on 03/06/2026).
[10] Georges Gonthier. “Formal Proof–the Four‑Color Theorem”. In: Notices of the AMS 55.11 (2008), pp. 1382–1393. URL: https://www.ams.org/notices/200811/tx081101382p.pdf?referer=www.clickfind.com.au (visited on 02/05/2026).
[11] Hardy Grant. “Leibniz and the Spell of the Continuous”. In: The College Mathematics Journal 25.4 (Sept. 1994), pp. 291–294. ISSN: 0746‑8342, 1931‑1346. DOI: 10.1080/07468342.1994.11973624. URL: https://www.tandfonline.com/doi/full/10.1080/07468342.1994.11973624 (visited on 02/03/2026).
[12] Giovanni Ferraro. “Euler, Infinitesimals and Limits”. In: (Jan. 3, 2012).
[13] Piotr Blaszczyk, Mikhail G. Katz, and David Sherry. “Ten Misconceptions from the History of Analysis and Their Debunking”. In: Foundations of Science 18.1 (Mar. 2013), pp. 43–74. ISSN: 1233‑1821, 1572‑8471. DOI: 10.1007/s10699-012-9285-8. arXiv: 1202.4153 [math]. URL: http://arxiv.org/abs/1202.4153 (visited on 02/04/2026).
[14] Eugen Netto. Vorlesungen über die Theorie der Einfachen und der Vielfachen Integrale. B. G. Teubner, 1894. URL: http://archive.org/details/rcin.org.pl.WA35_13014_4769__Vorlesungen_78413 (visited on 03/05/2026).
[15] Foundations of Mathematics By David Hilbert (1927). URL: https://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm?utm_source=chatgpt.com (visited on 02/05/2026).
[16] Jean‑Yves Beziau. “What Is‘Formal Logic’”. In: Proceedings of the XXII World Congress of Philosophy. Vol. 13. Korean Philosophical Association Seoul, 2008, pp. 9–22. URL: https : / / www . academia . edu / download / 52271386 / form -bonn.pdf (visited on 02/05/2026).
[17] Stephen G. Simpson. “Partial Realizations of Hilbert’s Program”. In: The Journal of Symbolic Logic 53.2 (1988), pp. 349–363. URL: https://www.cambridge.org / core / journals / journal - of - symbolic - logic / article / partial realizations-of-hilberts-program/66FDE948158C90D3818B011A45D466E5 (visited on 02/05/2026).
[18] Richard Zach. “The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert’s Program”. In: Synthese 137.1 (Nov. 1, 2003), pp. 211–259. ISSN: 1573‑0964. DOI: 10.1023/A:1026247421383. URL: https://doi.org/10.1023/A:1026247421383 (visited on 03/06/2026).
[19] Peter Smith. Does Mathematics Need a Philosophy? Logic Matters. Feb. 15, 2023. URL: https://www.logicmatters.net/2023/02/15/does- mathematicsneed-a-philosophy/ (visited on 02/05/2026).