公理的祖先是逻辑或形式二者之一

$$$$

写在前面

子曰：“朝闻道，夕死可矣。”

——《论语·里仁第四》

Bourbaki 学派认为数学没有先验的公理，我并不完全认同这一观点（其实我甚至不完全理解这一观点）。本文尝试以公理化集合论和 Church Numerals 两个系统为例，直观展示公理的祖先不是上帝，而是逻辑或形式二者之一。

我的导师曾经在软件学院教授《离散数学》，这是我本科阶段最喜欢的课程之一，也是我了解他的研究方向的入口。目前我的研究课题是数据库程序鲁棒性，该问题涉及到形式语言、形式化方法和数理逻辑，该领域的论文往往通篇都是希腊字母、形式逻辑符号和命题充要条件的证明。我在《数理逻辑》开课之前自学了一些集合论与形式化相关的内容，很幸运能够在研究生阶段开始之前管窥整个数学大厦的基石。笔者既不是数学专业的研究人员，也谈不上数学爱好者，仅在此与同好分享一些浅陋观点。挂一漏万，还请读者批评指正。

本文参考了：

• 皮卡第儒勒-凡尔纳大学柳渝老师博客：科学网—数学中的三个危机 ：逻辑主义、直觉主义和形式主义 - 译文 - 柳渝的博文；
• 清华大学数学系的课程：集合论：从高中到大学；
• 南京大学计算机写冯新宇、李樾老师的课程：SICP 2023 Fall @ NJU；
• 邱奇数 - 维基百科，自由的百科全书。

数学史上的集合论

历史和哲学负有多种永恒的责任，同时也是简单的责任。

——雨果

在人类应用数学史的过程中，我们可以将其分为三个关键时期，每个时期以数学危机的产生和解决作为里程碑。

古代数学，特别是埃及和希腊时期，是数学发展的奠基阶段。这个时期，最重要的贡献莫过于 Euclid 的《几何原本》。这部著作系统化了几何学，奠定了我们今天所称的欧几里得几何，这也是大多数中学生第一次接触到的近似形式化的、逻辑严密的定理和证明。除了几何学，Ptolemaeus 在天文学和三角学上的研究也具有重要意义。然而，这个时期也面临着第一次数学危机，即希腊数学家发现了无理数。毕达哥拉斯学派认为一切数都应该是有理的，但正方形对角线与边长之比 $\sqrt{2}$ 的存在打破了这一信念，引发了数与几何之间的矛盾。这也使得希腊的悖论成为该时期的重要思想遗产，尤其是芝诺悖论，它对后来的数学和哲学思维产生了深远影响。

到了近代数学，17 世纪下半叶的数学面临了第二次数学危机。微积分的发明极大地推动了数学，特别是在物理和几何中的应用。牛顿和莱布尼茨几乎同时提出了微积分的理论，这为理解变化和运动提供了新的工具。然而，微积分的基础当时还不够严谨，尤其是无穷小量的概念不明确，这成为数学的第二次危机。这一危机直到 19 世纪由柯西和魏尔斯特拉斯通过极限理论才得以缓解。这个时期，Lagrange 和 Gauss 的贡献尤其突出。拉格朗日在变分法方面的工作，使得物理学和几何学紧密结合；高斯则在数论、代数等多个领域取得了革命性的成果。

现代数学，特别是 20 世纪下半叶，随着集合论的发展，经历了第三次数学危机。康托尔的集合论为无穷集的研究提供了基础，但也引发了新的悖论，如 Russell 悖论。这次危机不仅是集合论的问题，还牵涉到数学的基础。在这一背景下，Bourbaki 学派通过形式化的方式试图解决这些问题，主张将数学各分支统一公理化。现代数学的研究方式更加抽象，范畴论的引入成为研究的核心之一。Grothendieck 的工作使得代数几何学得到了极大推进，他的范畴论思想使得数学的很多分支走向统一。而 Chern（陈省身）在微分几何方面的突破也将数学应用于更多物理问题中，尤其是在现代物理学中扮演了重要角色。

通过这三个阶段，我们可以看到数学从早期几何的初步探索，经过微积分的严谨化，再到集合论的形式主义发展，逐步演变为一个更加抽象和结构化的学科。每个阶段的危机虽然带来了挑战，但也促使了数学的革新与进步。在这个过程中，从朴素集合论到公理化集合论的进步，为数学大厦提供的坚实的地基，使得可以用形式逻辑的方法在这个地基之上构筑整个数学大厦，尽管大厦本身还存在一些不尽如人意之处（哥德尔不完备定理）。

高中阶段的数学在有意识地引导学生使用集合的逻辑来处理问题。例如：

1. 不等式的解集应当写作 $x\in [-5,0)\cup (0,3)$，而不是 $-5\le x<3\mathrm{且}x\ne 0$；
2. 点在线上、点在面上、线在面上分别表示为 $A\in l,A\in \alpha ,l\subset \alpha$。

遗憾的是，许多高中数学老师并未详细解释这种数学语言的本质，以至于包括笔者在内的大多数中学生把元素和集合的关系当成了“小球和盒子”的关系：点 $A$ 是不可再分的小球，直线 $l$ 和平面 $\alpha$ 是装球的盒子，盒子（集合）之间的关系只能是 $\subset$ 而不能是 $\in$。

当我在《离散数学》课程中接受了“所有的东西都是集合”这一观念后，连自然数这种幼儿园级别的数学模型都可以转化成集合问题，而集合问题只有简单的 $\in$ 和 $\notin$ 两种（辅之以逻辑关系），这简直太美妙了。但老师马上用 Russell 悖论打得我们措手不及：

$$A=\{x|x\notin x\}$$

在课堂上，老师并没有告诉我 ZFC 公理是如何解决这一问题的。这是我自学公理化集合论的开始。似乎一切都意味着，既然公理化集合论是整个数学大厦的基石，那么在既定逻辑上进行形式推演似乎是数学研究的终南捷径——只要这条路不会通向矛盾，这条路就是好的。

但是，我在自学计算机理论的过程中接触到了 Alonzo Church 发明的 lambda 演算和 Church Numerals。这种独立于逻辑而存在的形式运算是震撼人心的，我意识到不仅可以“逻辑生形式”，还可以“形式生逻辑”。这也是我第一次接触到“形式主义”流派的数学。

尽管如此，需要强调，笔者作为软件工程专业的研究生，并不是逻辑主义、形式主义和直觉主义任何一个学派的信徒，只能基于自己理解的相当有限的数学来讨论。

本文以公理化集合论为切入点，论证逻辑往往是形式的前提，也就是大多数学生所认为的“公理、定理和引理是对的，所以我可以直接搬来用”。本文其次以 Church Numerals 为例，论证形式不仅可以独立于逻辑，还可以成为逻辑之母。最后，本文尝试总结观点：形式和逻辑可以分别产生对方，进而产生公理；因此，没有先验的公理。

公理化集合论：因为对，所以有用

我们设置栅栏，把羊群围住，免受狼的侵袭，但是很可能在围栅栏时就已经有一只狼被围在其中了。

——庞加莱

庞加莱的栅栏论是对 Russell 悖论的一个形象比喻。本章将详细讨论 ZFC 公理被巧妙地“发明”（而不是“发现”）这一过程，并辅之以朴素集合论的结论来直观展示。

集合的定义

首先我们要定义什么是集合。

概括公理

若 $P(x)$ 是一个命题，则 $\{x|P(x)\}$ 是一个集合。

概括公理是朴素集合论当中最符合直觉的定义，它直观描述了“符合某一条件的元素构成一个集合”这件事情。但是这也直接导致了一个悖论：

Russell 悖论

由概括公理，$\{x|x\notin x\}$ 是一个集合，设其为 $S$。那么一方面 $S\in S$ 成立；另一方面 $S\notin S$ 成立。

本章将多次回到 Russell 悖论，探讨公理集合论的“栅栏”是如何被设计出来以绕过可能存在的“狼”。

接下来，我们要讨论两个集合什么时候会“相等”。这里的“相等”是一个逻辑概念。

外延公理

$$X=Y⟺\mathrm{\forall }x(x\in X⟺x\in Y)$$

只管来说，外延公理意味着“两个集合相等，当且仅当他们当中的元素相同”。这是判断两个集合相等的唯一判据。在《数理逻辑》这门课的习题当中，我们多次使用了这一判据。

朴素集合论中集合有确定性、无序性和不重复性。这些性质都由以上公理蕴含。

不重复性定理

$$\{a\}=\{a,a\}$$

证明使用了外延公理：

$$x\in \{a\}⟺x=a⟺x\in \{a,a\}$$

确定性和无序性更为简单，本文不再赘述。

概括公理给出了集合的定义，其优点在于具有相当大的任意性，因此它能够统摄从代数到几何的各种数学理论。但 Russell 悖论的存在意味着概括公理具有太大的任意性。我们需要对增加一些限制。

分离公理

$X$ 是一个集合，$P(x)$ 是一个命题，则 $X$ 中满足 $P(x)$ 的集合构成一个集合，即 $\{x\in X|P(x)\}$ 是一个集合。

分离公理要求构造集合时，新集合的元素必须来自某个已知的集合，然后使用命题 $P(x)$ 从原集合中分离出一部分元素组成新的集合。分离公理主要用于构造子集。

空集

设 $X$ 是一个集合，则根据分离公理 $\{x\in X|x\ne x\}$ 是一个集合，记为 ${\mathrm{\varnothing }}_X$，称为依赖 $X$ 的空集。

对于任意两个集合 $X$ 和 $Y$，由外延公理可知 ${\mathrm{\varnothing }}_X={\mathrm{\varnothing }}_Y$，所以根据任意一个集合构造出的空集都是相等的，将其记为 $\mathrm{\varnothing }$，称为空集。至此，我们得到了一个不依赖于其他集合的空集。

集合的运算

我们已经完成了对集合、子集和空集的公理化定义，这些内容与朴素集合论的直观表述并无冲突。接下来我们将展示如何对集合间的运算进行公理化定义。

交集、差集和子集

对于两个集合 $X,Y$，根据分离公理，定义 $\{x\in X|x\in Y\}$ 是一个集合，将其记为 $X\cap Y$，称为 $X$ 和 $Y$ 的交集。利用外延公理容易验证，$X\cap Y=Y\cap X$。

同理，定义 $X\setminus Y=\{x\in X|x\notin Y\}$，称为 $X$ 和 $Y$ 的差集（或 $X$ 除去 $Y$）。

对于两个集合 $X$ 和 $Y$，如果 $x\in X⟹x\in Y$，那么称 $X$ 是 $Y$ 的一个子集，记为 $X\subset Y$。分离公理中构造的每一个集合 $\{x\in X|P(x)\}$ 都是集合 $x$ 的子集；另一方面，每一个子集 $Y$ 都可以表示为分离公理 $$\set{x \in X | x \in Y}$$ 的形式。如果 $X$ 是 $Y$ 的子集且两者并不相等，则称 $X$ 是 $Y$ 的真子集。

除了并集之外，朴素集合论中的运算都已经构造出来。下面来构造并集。

并集公理

$$\mathrm{\forall }X\mathrm{\exists }Y\mathrm{\forall }x((\mathrm{\exists }Z\in X)(x\in Z)⟺x\in Y)$$

上述公理描述了这样一件事情：对于每个集合 $X$，存在一个集合 $Y$，使得对于 $X$ 当中的每个 $x$，$Y$ 都包含 $x$ 当中的元素，且 $Y$ 不包含其他元素，即 $Y=\bigcup _{Z\in X}Z$。

幂集是集合论中的重要概念。事实上，我们目前只知道空集是存在的，如果没有幂集公理，集合论中可能只有空集这一个集合。幂集公理可以帮助我们构造有任意多个元素的集合。

幂集公理

$$\mathrm{\forall }X\mathrm{\exists }Y(x\subset X⟺x\in Y)$$

$Y$ 是 $X$ 的幂集，记为 $Y=P(X)$ 或 $Y=2^X$。

根据外延公理，集合的幂集是唯一的。显然，如果 $X$ 当中有 $|X|$ 个元素，则 $Y$ 中有 $2^{|X|}$ 个元素。我们容易根据空集的存在性、幂集公理和分离公理构造有任意有限多个元素的集合。例如，构造有 3 个元素的集合：

$$\begin{gathered} A=\mathrm{\varnothing }\text{ \\ B=2A={∅} \\ C=2B={∅,{∅}} \\ D=2C∖C={∅,{∅},{{∅}}}} \end{gathered}$$

上述构造方式只是众多构造方式中的一种。

从有穷到无穷

当数学的方向转向无穷这一课题的时候，魔鬼就必然会出现。

——Gauss

既然连 Gauss 这样的数学天才都对无穷问题望而却步，那么数学界到目前为止还对“无穷”是否存在莫衷一是也就不足为奇。幸而，Cantor 早已替我们向无穷发起了挑战，并且取得了一些胜利，尽管这些胜利并不被广为承认。

我们已经能够构造任意多个有限元素的集合，我们希望更进一步构造有无穷多元素的集合。容易发现，这一点并不能够从已知的公理推出，因此我们需要无穷公理。

无穷公理

$$\mathrm{\exists }X(\mathrm{\varnothing }\in X)\wedge (x\in X⟹P(x)\in X)$$

无穷公理有很多种等价的写法，我们这里使用了幂集。事实上无穷公理构造的集合就是自然数集，无穷公理内嵌了 Peano 公理。

朴素集合论的集合运算中还有 Cartesian 积。Cartesian 积 本质上是根据两个集合构造有序数对。我们首先给出构造无序数对的配对公理：

配对公理

$$\mathrm{\forall }X\mathrm{\forall }Y\mathrm{\exists }Z((x=X\vee x=Y)⟺x\in Z)$$

至此，朴素集合论中的常见集合和运算都已经被形式化地构造完毕。

在我们完成了朴素集合论的构造之后，我们希望关注如何避免 Russell 悖论。我们已经用任意性弱的分离公理取代了概括公理，我们要做的是防止分离公理“进化”为概括公理。不难发现，如果我们承认“所有集合构成一个集合”，那么分离公理就会“进化”为概括公理，我们希望避免这种情况。

我们希望表述一个公理，即所有集合放在一起不构成一个集合，但是这种表述显然非常不“形式化”。对于这个以所有集合为元素的“集合”，它的哪一个元素是最诡异的呢？那便是它自己。事实上 Russell 悖论也正是取出了这一个集合所导致的。于是我们必须把这一个元素否定掉。同样，在否定掉这一点后，我们也要否定掉所有“套娃”式的定义。

正则公理

$$\mathrm{\forall }X((X=\mathrm{\varnothing })\vee \mathrm{\exists }Y((Y\in X)\wedge (X\cap Y=\mathrm{\varnothing })))$$

我们不容易看出正则公理是如何避免了“一个集合包括它自身”。因此我们需要一些正则公理的推论来辅助理解：

定理 1：不存在集合 $X=\{X\}$。

证明：由正则公理，对于非空集合 $X$ 存在元素 $Y\in X$（由于 $X$ 只有一个元素，因此 $Y=X$），但 $X\cap Y=X\ne \mathrm{\varnothing }$，矛盾。

定理 2：不存在集合 $X$，使得 $X\in X$（即防止分离公理“进化”为概括公理，从而避免 Russell 悖论）。

证明：由分离公理，$Y=\{y\in X|y=X\}$ 是一个集合，显然 $Y=\{X\}$。由正则公理，存在 $Y$ 的元素 $Z\in Y$（由于 $Y$ 只有一个元素，因此 $Z=X$），$Z\cap Y=X\cap \{X\}=X\ne \mathrm{\varnothing }$。

至此，我们已经看到了正则公理是如何防止分离公理“进化”为概括公理，从而避免了 Russel 悖论。除了以上定理之外，正则公理还有几个有趣的推论，读者自证不难。

定理 3：不存在集合 $X_n$ 使得 $X_{n+1}\in X_n$，其中 $n$ 是自然数；

定理 4：不存在集合 $X$ 使得 $X=\{\{X\}\}$。

杨振宁老师认为，人类可以在已知的数学之外“发明”数学，但这种“发明”的结果其实是早已存在的。在这个意义上，这种“发明”本质上并没有不同于化学家“发现”水由氢和氧组成。在“发明”正则公理以避免 Russell 悖论的过程中，数学家们只是破解了 Russell 悖论成立的前提条件：分离公理、排中律（反证法）和“所有集合构成一个集合”。分离公理这样符合直觉的规则显然不应该被舍弃，排中律作为形式逻辑的基石也绝不应被否定（尽管有些秉持直觉主义数学哲学观的数学家们会通过否定排中律来避免 Russell 悖论）。因此，只能牺牲“所有集合构成一个集合”这条既不符合直觉又不被公认的前提条件。正如本文在一开始提到的“数学没有先验的公理”，我们围绕目标构造条件的“发明”公理的方式也从侧面验证了这一观点。

除了以上这些公理之外，还有替代公理和选择公理。受限于篇幅，笔者在这里简要列出这两条公理。

替代公理

$X$ 是一个集合，$x\in X$，$P(x,y)$ 是一个命题，若 $(P(x,y_1)\wedge P(x,y_2))⟹y_1=y_2$，则 $\{y|\mathrm{\exists }xP(x,y)\}$ 是一个集合。

选择公理

给定若干个相互不交的非空集合，存在着至少一个集合，它与每个非空集合的交恰好有一个公共元素。

至此，我们完成了 ZFC 公理集合论当中的所有公理。我们依靠巧妙设计的公理，解决了在本章开头庞加莱提出的问题，为数理逻辑乃至整个数学的大厦奠定了一个看起来十分坚固的基石。虽然它暂时还被哥德尔不完备定理所动摇，但我们这些应用数学的工作者大可以捂住眼睛装作看不见，集合论的稳定性使我们暂时担心被恶魔所迷惑。

Church Numerals：独立于逻辑的形式系统

逻辑学家 Alonzo Church 发明了一种完全使用函数来表示非负整数的系统，称为 Church numerals（丘奇数）。其目的是表明函数足以描述所有数论：如果我们有函数，我们就不需要假设数字存在，而是可以发明它们。

Church numerals 是数理逻辑和程序设计语言（Programming Language，PL）领域结合的伟大产物，是我大一学年接触到的第一优美简洁的数学结构；与之相比，von Neumann 把 Peano 公理嵌入集合论这一成就只能排在第二。事实上，Church numerals 的定义思想与自然数几乎相同，都是基于 Peano 公理。不同的是，公理化集合论的定义过程需要大量使用 $\mathrm{\forall },\mathrm{\exists },⟺,=$ 这些逻辑运算作为应用 Peano 公理的前提，而 Church numerals 的定义过程完全不需要以上任何一种逻辑运算。

有必要说明，以下出现的代码均为笔者大一上学期《计算机程序的构造和解释》的课程作业。但幸好 Church numerals 足够简洁，这些代码在今天看来仍然不需要修改。

限于篇幅，我们不得不跳过二元关系和函数、Peano 公理的各种表述、两种等价的数学归纳法以及抽象程序设计语言当中的 lambda 演算，来直接介绍令人心动的 Church numerals。因此在继续阅读本文之前，请确保自己能够熟知并应用以上知识。

像 Peano 公理那样定义自然数

与集合论下 Peano 公理对自然数的定义一样，首先我们要定义数字 0 存在。鉴于我们的整个体系并不应该引入任何“数”，也即 PL 中的变量，我们应该用函数来定义数字 0。

def zero(f): # iterate for 0 times, zero(f)(x) = x
	return lambda x: x

把函数作为研究对象，我们能想到的运算似乎很少，只有组合（compose）和迭代（iterate）两种。显然，我们把 0 定义为函数迭代 0 次最符合直觉。此时，无论函数 $f$ 为何，在 $x$ 上迭代零次的结果必然是 $x$ 本身。因此，这个自然数 0 是可以独立于参数函数而存在的。

有了 0 之后，我们再定义 1、2 也并不困难。

def one(f): # one(f)(x) = successor(zero)(f)(x) = f(x)
	return lambda x: f(x)

def two(f): # two(f)(x) = successor(one)(f)(x) = f(f(x))
	return lambda x: f(f(x))

这里的定义讨了个巧，就是我们已经知道函数 $f(x)$ 迭代一次之后就是 $f(x)$ 本身，所以 1 自然是就是 $f$ 本身了，2 自然也就是 $f^2$（这里的上角标 2 表示迭代 2 次，而不是平方）。

但是按照这样定义下去，我们还要定义 3、4 以至于无穷。既然在 Peano 公理中可以直接定义 $1=0^{+}$，那我们也借鉴这种思想，只要定义了后继运算，那么连 1 的定义都可以省略。

这里使用 $f$ 来描述函数的迭代过程，但其实 1、2 和 0 一样，都是不依赖参数函数本身而存在的。在 python 或者抽象语言中，函数本身就是一个数据类型，可以被赋值。我们修改对几个自然数的定义。接下来的定义设计有些困难，我们不妨先来看看 Wikipedia 上的前人是怎么描述的：

有了上面的表格，我们根据答案构造过程就容易多了。既然在我们的 Church Numerals 体系当中，自然数也是函数，那么自然数 n 的后继 successor(n) 其数据类型应该与 n 一致。自然数 n 的数据类型为函数，并且是“以一个函数为参数的函数”，其签名为 n(f)，其中 f 也是函数（甚至可以和其他的形参 f 不是同一个函数）。那我们观察可得 successor(n)(f)(x) = f(n(f)(x))。显然这里后继运算是与作为参数的函数 f 无关的，那么我们容易得到下面的定义：

def successor(n):
    return lambda f: lambda x: f(n(f)(x))

one = successor(zero)
two = successor(one)
three = successor(two)

至此，我们的 Church Numerals 体系已经包含了整个 Peano 公理，我们也有了自己的自然数体系！

对于非数学专业的学生来说（例如笔者本人），Peano 公理与公理化集合论是孪生兄弟，似乎二者生来就是为了对整个数学体系进行公理化，因为集合论作为数学“大一统”理论本身的理论价值要超过其应用价值（似乎只有笔者这样的计算机理论/关系数据库工作者才会觉得集合论有用）。但我们的 Church Numerals 向程序员们展示，即使没有集合论，Peano 公理仍然可以定义自然数。

超越 Peano 公理：加法、乘法和幂

Talk is cheap, show me your codeoutput!

——Programmers

虽然我们已经自称定义了自然数，但我们需要向不那么懂数学的程序员们展示这件事。上面定义的 zero, one, two 等都是藏在内存里的、看不见的数学结构。我们最好能够把他们输出到屏幕上。这就需要用到 python 本身的 int 变量类型。注意，这一数据类型只用于将 Church Numeral 转化成 CPU 可以识别的控制信号，把自然数输出到屏幕，我们的整个 Church Numerals 体系与数据类型无关，与和任何变量、函数都无关。

increment = lambda x: x + 1

def church_to_int(Church_n):
	return Church_n(increment)(0)

运行 python 程序，在键盘上输入 church_to_int(three)，我们满意地看到了 3。现在，我们终于可以向其他程序员展示，我们不依赖任何变量和函数就能够定义出自然数。接下来，我们要充分利用 Church Numerals 的优点，简洁地定义自然数运算。这将超越 Peano 公理和公理化集合论这对孪生兄弟！

加法 直观来说，$n+1$ 就是在 $n$ 外面套一个 successor 函数，即 successor(n)，我们在前面已经反复使用了这种思想。那么我们要表达 $n+m$，只需要在 $n$ 外面套 $m$ 层 successor 函数即可。巧合的是，我们对自然数的定义正是通过迭代函数实现的，而并不关心这个函数是什么。既然如此，我们只要使用 n(successor) 表示“迭代 $n$ 次 successor”这个函数即可。

def add_church(Church_m, Church_n):
	return Church_n(successor)(Church_m)

乘法 与加法的定义思路类似，我们只需要把 $m\times n$ 视作 $0+(m\times n)$ 即可。具体定义证明留给读者自己思考。

def mul_church(Church_m, Church_n):
	return Church_m(Church_n(successor))(zero)

幂 从加法到乘法的过渡与从乘法到幂的过渡类似，证明留给读者自己思考。

def pow_church(Church_m, Church_n):
	return Church_n(Church_m)

以上只提供了 python 版本的 Church Numerals 定义，即是为了方便读者在计算机上运行测试，也能够避免读者盯着文章太久而不认识 $\lambda$ 这个字母（当然，主要还是为了体现对我本专业的尊重）。与之等价的纯形式化 lambda 定义在附录中给出，以供读者对照参考。

参照以上的思路，我们还可以定义后继的逆运算前驱。进而定义减法甚至除法。附录给出了 lambda 演算的定义，欢迎读者参考给出 python 版本的定义。

到目前为止，我们只提供了自然数的算数运算，并没有逻辑运算。因此，我们暂时无法定义自然数上的 $=$ 和 $<$。我们将在下一节解决这个问题。

逻辑是形式之母，但也可以反过来

而世之奇伟、瑰怪，非常之观，常在于险远，而人之所罕至焉，故非有志者不能至也。

——王安石《游褒禅山记》

我们已经展示了，脱离逻辑而存在的形式演算同样有魅力。遗憾的是，逻辑是现代公民的通用素质但形式演算不是。正如王安石所说，大多数不仔细钻研形式演算的人无法领略这种魅力的。接下来我们将进一步证明，形式也可以导出逻辑。

逻辑中的 $\mathrm{true}$ 和 $\mathrm{false}$ 是不需要定义的。但奇妙的是，lambda 演算甚至可以在逻辑诞生之前形式地定义逻辑：

$$\begin{gathered} \mathrm{true}\equiv \lambda a.\lambda b.a\text{ \\ false≡λa.λb.b} \end{gathered}$$

容易看出，这两个 lambda 表达式定义对两个参数是对称的。事实上，如果我们交换这两个定义，同样可以得到完整的逻辑定义。

基于以上定义，我们给出部分逻辑运算的定义：

$$\begin{gathered} \mathrm{and}\equiv \lambda p.\lambda q.pqp\text{ \\ if≡λp.λa.λb.pab} \end{gathered}$$

更多逻辑运算（$\mathrm{or},\mathrm{not},\mathrm{xor},=$）的定义留待读者思考。当然，笔者也在附录中提供了定义。

虽然笔者一直使用“定义逻辑”来表达 lambda 表达式的强大逻辑，但这种表述未必很合适。因为在整个数学史上，甚至整个人类思维发展史上，都是先有了 $\mathrm{true},\mathrm{false}$ 和各种逻辑连接词，然后再有了 lambda 演算。一些数学家认为，不能因为张三生的孩子像李四，就说“张三定义了李四”。但笔者认为，既然数学史上后出生的集合论可以定义先出生的自然数，那么说“形式产生了逻辑”也未尝不可。

公理：祖先为逻辑或形式二者之一

古希腊几何学家阿波洛尼乌斯总结了圆锥曲线理论，一千八百年后由德国天文学家开普勒将其应用于行星轨道理论。 数学家伽罗华公元 1831 年创立群论，一百余年后获得物理应用。 公元 1860 年创立的矩阵理论在六十年后应用量子力学。 数学家 J.H 莱姆伯脱，高斯，黎曼，罗马切夫斯基等人提出并发展了非欧几何。高斯一生 都在探索非欧几何的实际应用，但他抱憾而终。非欧几何诞生一百七十年后，这种在当时毫无用处的理论以及由之发展而来的张量分析理论成为爱因斯坦广义相对论的核心基础。 何夕提出并于公元 1999 年完成的微连续理论，一百五十年后这一成果最终导致了大统一场理论方程式的诞生。

本文分别以公理化集合论和 Church Numerals 为例，论证了如下结论：

1. 逻辑可以产生形式；
2. 形式也可以产生逻辑；
3. 没有先验的公理，公理往往是被“发明”而不是被“发现”；
4. 形式和逻辑二者之一可独立产生公理。

后记

西江月·证明

即得易见平凡，仿照上例显然。留作习题答案略，读者自证不难。

反之亦然同理，推论自然成立，略去过程 $Q.E.D.$，由上可知证毕。

笔者每每被数理逻辑的作业困扰时，脑内就会开始自动吟唱这首《西江月》。好在撰写这篇文章并不需要费尽心思去证明太显然的事情。本文是笔者首次在数学领域讨论自己的观点。粗陋浅薄，贻笑大方，还请读者不吝赐教。

笔者在学习集合论的过程中参考了教材、讲义和多个不同来源的文献，不得不频繁陷入逻辑主义、形式主义和直觉主义的争论当中。为了厘清这几个学派的观点，笔者查阅了一部分通俗的网络材料，认为以自己浅薄的哲学基础还无法理解集合论作为数理逻辑的基石面临着怎样的压力。南京大学数学系李春老师曾在微积分课上告诉我们“数学的尽头是哲学”，当时的我并不能理解这一观点。在仔细分析了集合论这个小专题和哥德尔不完备定理后，我认识到数学和其他学科一样，有着自己的学科边界，在边界之上的问题只能留待更进一步的哲学体系来讨论。

笔者目前的研究方向是数据库程序鲁棒性充要条件。我在推导充要条件时必须要依赖数据库理论领域内的学者提出的各式各样的隔离级别公理，有些公理甚至没有形式化的表达。感谢《数理逻辑》指导我梳理形式与逻辑的关系，在专业领域之外给了我一些灵感的火星。希望自己能够在科研的漫漫前路上时长会想起来，在某个数学的故纸堆里，还有如 Church Numerals 这样未灭的星星之火。

古往今来的数学家，其成就有如银河般浩瀚璀璨，比如 Euclid、Euler 和 Gauss 的理论就是我中学竞赛时期的一点课余爱好。笔者学习《数理逻辑》这门课，当然不是奢望成为和他们一样的一颗星星，只是想要学会使用望远镜，以期比其他看星星的孩子看得更清楚、更明白一些。

哀吾生之须臾，羡长江之无穷；知不可乎骤得，托遗响于悲风。

附录：与 Church Numerals 的 python 定义等价的 lambda 表达式定义