命题即类型

证明即程序

下面是命题“$A$ 蕴含 $B$”的一个证明，用普通的数学文字写成：

假设 $A$。那么……（某些论证）……所以 $B$ 成立。

这个证明的形状是一个函数：它接收某样东西，即相信 $A$ 的理由，产出另一样东西，即相信 $B$ 的理由。如果把这句话当真，把“相信 $A$ 的理由”视为类型 $A$ 的一个值，那么 $A \to B$ 的证明就是从 $A$ 到 $B$ 的函数，而命题 $A \to B$ 就是这个函数的类型。

这一观察就是 Curry-Howard 对应。它说：

• 命题是类型，
• 命题的证明是该类型的项，
• 命题 $A$ 为真，当且仅当存在某个类型为 $A$ 的项 $t$，记作 $t : A$。

三个例子就能看出这个想法已经走了多远。左栏是命题，中栏是写成函数的证明，右栏是证明思路的文字说明。这里 $\lambda x.\,e$ 表示接收 $x$ 并返回 $e$ 的函数。

再看第三行。要证明蕴含有传递性，先假设 $A \to B$ 和 $B \to C$，然后在给定 $A$ 时，用第一个假设得到 $B$，再用第二个得到 $C$。证明项说的正是这件事：$f$ 和 $g$ 是假设，$a$ 是 $A$ 的证明，$g\,(f\,a)$ 依次应用它们。使用一个假设就是应用一个函数；正是这一步把真正的推理和单纯复述假设区分开来，第 3 章会再回到这一点。

量词变成依赖函数

同样的想法可以推广到“对所有”。要证明 $B(x)$ 对每个 $x : A$ 成立，我们给出一个方法：拿到任意具体的 $x$，就产出 $B(x)$ 的一个证明。这又是一个函数，只是多了一个变化：返回类型依赖于参数。对 $x = 3$ 它返回 $B(3)$ 的证明，对 $x = 7$ 则返回 $B(7)$ 的证明。结果类型可以提到参数的函数类型称为依赖函数类型（dependent function type），或 $\Pi$ 类型，写作

普通函数类型 $A \to B$ 是 $B$ 不提到 $x$ 的特例。

例如，“每个命题都蕴含自身”是对命题的量化。若 $\Sort{0}$ 是命题的类型，这句话就是

它的证明是这样一个函数：接收命题 $P$，再接收 $P$ 的证明 $p$，然后返回 $p$：

注意绑定子现在带有类型：$\lambda(P : \Sort{0})$ 表示 $P$ 取遍命题，$\lambda(p : P)$ 表示 $p$ 是传入的那个具体 $P$ 的证明，而类型检查器需要这些标注。

内核做什么

由此得到定理证明器背后的核心思想。

内核不对真假做推理，而是实现规定项何时具有某个类型的类型规则，并机械地检查给定的项在这些规则下是否具有给定的类型。这算不算证明检查，取决于类型规则是否忠实地实现了某种逻辑，这是第 4 章的主题。规则是否可靠，即是否任何项都不可能具有假命题的类型，是第 13 章和第 14 章的主题。

这种分工决定了证明器的设计：策略、自动化、判定过程，甚至大语言模型，都可以负责寻找证明，即使它们有错误，生成的项仍须由内核检查。只有内核必须正确，因此设计目标是让它尽量小巧；本书的内核连注释在内也不到一千五百行 Rust。

路线图

第一部分各章为一个类型论构建内核，这个类型论刚好大到足以充当一种逻辑。

1. 第 2 章确定语言：宇宙、变量、$\Pi$ 类型、$\lambda$ 抽象和应用。
2. 第 3 章给出类型规则，每种项一条，外加一条允许在类型内部进行计算的规则。
3. 第 4 章说明这些规则就是一种逻辑的规则，并定义一致性。
4. 第 5 章把规则变成算法，并与 Rust 实现逐一对照。
5. 第 6 章在正确的证明、错误的证明和需要计算的证明上手工运行该算法。

有两个操作在第三部分之前被有意当作黑箱：替换和定义相等。两者都容易陈述，也都容易出错，而内核的正确性依赖于它们。