构造逻辑

在逻辑学和数学的世界里，我们常常理所当然地认为每个陈述要么为真，要么为假——这是一个由经典逻辑支配的黑白分明的现实。但是，如果真理不是等待被发现，而是需要被构建的东西呢？这便是构造逻辑的核心前提。它要求为每一个真理主张提供切实的证据——一个“构造”，从而挑战了我们最基本的假设。本文旨在弥合经典逻辑的抽象确定性与计算和证明的逐步、可验证过程之间的鸿沟。它将带领读者进入这个迷人的世界，从其核心原则和机制出发，我们将通过重新定义真理本身来从头重建逻辑。随后，我们将探索其强大的应用和跨学科联系，揭示支撑现代软件验证乃至整个计算机科学基础的逻辑证明与计算机程序之间惊人的对应关系。

想象你是一位建筑师。在古典建筑学中，你可能会基于某些材料具有绝对、不变属性的假设来设计一座宏伟的大教堂。你假设一块花岗岩是绝对坚固的，一根横梁是绝对刚性的。这就是经典逻辑的世界——一个充满绝对真理的世界，其中每个陈述要么是明确的真，要么是明确的假，就像一个开关只有开和关两种状态。

构造逻辑则邀请我们成为另一种建筑师——一位务实的工程师。它告诉我们，我们不能简单地假设一根横梁是坚固的；我们必须证明它的强度。我们必须提供计算过程、压力测试和蓝图。一个陈述是“真的”，只有当我们为其构造了一个证明。这不仅仅是一种哲学偏好；这是一种深刻的转变，它改变了我们用以构建数学和计算世界的逻辑工具的根本意义。让我们打开工具箱，在新的光芒下审视这些工具。

在经典逻辑中，我们认为陈述的真值（真或假）是独立于我们的知识而存在的。“存在无限多对孪生素数”这个陈述要么为真，要么为假，即使我们不知道是哪一种。构造逻辑，特别是被称为​​布劳威尔-海廷-柯尔莫哥洛夫（Brouwer-Heyting-Kolmogorov, BHK）解释​​的框架，提出了一个激进的替代方案：一个逻辑陈述的意义就是它的证明。证明不仅仅是一种验证；它本身就是证据。一个陈述为真，当且仅当我们拥有一个作为其证明的​​构造​​。

什么是构造？可以把它看作一段数据或一个算法。这个简单的想法对我们曾经熟悉的每一个逻辑联结词都产生了戏剧性的影响。

让我们看看，当我们要求为一切事物提供构造时，我们熟悉的与、或、蕴含和非会发生什么变化。

• ​​合取 ($A \land B$)​​：要证明“$A$ 与 $B$”，你必须提供一个 $A$ 的证明和一个 $B$ 的证明。这很直观。$A \land B$ 的一个证明就是一个序对 $\langle p, q \rangle$，其中 $p$ 是 $A$ 的证明，$q$ 是 $B$ 的证明。这里没有什么意外。

• ​​析取 ($A \lor B$)​​：这里我们遇到了第一个冲击。在经典逻辑中，你可以在不知道哪一个为真的情况下证明“$A$ 或 $B$”。例如，一个经典证明可能会表明，如果 $A$ 为假，那么 $B$ 必定为真，这便足够了。而构造主义者认为这种做法非常不令人满意。要构造性地证明“$A$ 或 $B$”，你必须提供一个 $A$ 的证明或一个 $B$ 的证明，并且你必须明确说明你证明的是哪一个。

  $A \lor B$ 的证明是一个“带标签”的对象。它是一个序对，例如 $\langle 0, p \rangle$（其中 $p$ 是 $A$ 的证明），或 $\langle 1, q \rangle$（其中 $q$ 是 $B$ 的证明）。要证明“117 是偶数或 117 是奇数”，你不能只是挥挥手；你必须提供一个包含标签 '1'（表示右侧选项）以及证明 $117 = 2 \times 58 + 1$ 的计算过程的包裹。这一严格要求带来了一个显著的特性，称为​​析取性质​​：如果在构造逻辑中一个定理的形式为 $A \lor B$，那么要么 $A$ 本身是一个定理，要么 $B$ 是一个定理。这里没有模棱两可的余地。

最深刻的变化发生在蕴含和否定上。它们不再是静态的关系，而变成了动态的过程。

• ​​蕴含 ($A \to B$)​​：“如果 $A$，则 $B$”的证明是什么？它不是对真值表的核对。$A \to B$ 的一个构造性证明是一种​​方法​​、一个​​算法​​、一个“证明转换器”。它是一个构造，承诺能将你可能找到的任何 $A$ 的证明，机械地转换为一个 $B$ 的证明。

  这是逻辑与计算之间联系的跳动的心脏。在优美的 ​​Curry-Howard 同构​​中，命题被看作数据类型，证明被看作程序。$A \to B$ 的证明实际上就是一个程序，它接受一个类型为 $A$ 的对象作为输入，并返回一个类型为 $B$ 的对象。例如，在一种编程语言中，我们可能将其写成一个函数：lambda x: A. M，其中 M 是执行转换工作的函数体。证明就是函数本身。

• ​​否定 ($\neg A$)​​：某事“不为真”是什么意思？在经典逻辑中，这仅仅意味着它是假的。在构造主义中，否定是一种反驳形式。我们将 $\neg A$ 定义为 $A \to \bot$ 的缩写，其中 $\bot$（“底”或“谬”）代表一种荒谬，一种永远不可能存在证明的矛盾。

  因此，$\neg A$ 的一个证明是一种方法，它能将任何假设的 $A$ 的证明转换为一个矛盾。要证明“$\sqrt{2}$ 不是有理数”，你不能仅仅断言它的无理性。你必须提供一个方法，说：“给我任何声称 $\sqrt{2}$ 是分数 $p/q$ 的证明，我将遵循这些步骤推导出一个矛盾（例如，一个偶数等于一个奇数）。” 证明一个否定命题是展示其荒谬性的一个主动过程。

有了我们新的构造主义工具箱，我们回到经典逻辑的古老殿堂，发现它的一些核心支柱已不再稳固。

其中最著名的是​​排中律（Law of the Excluded Middle, LEM）​​，即对于任何命题 $P$，“$P$ 或非 $P$”（$P \lor \neg P$）这个陈述总是为真。对经典主义者来说，这是不言自明的。对构造主义者来说，这是一个异乎寻常的主张。要证明 $P \lor \neg P$，就需要一个通用算法，对于任何命题 $P$，该算法都能要么生成一个 $P$ 的证明，要么生成一个 $\neg P$ 的证明。这样的算法意味着每个数学问题都是可判定的！我们知道情况并非如此——停机问题就是一个著名的反例。因此，构造逻辑勇敢地拒绝将排中律作为一条通用公理。

这种拒绝给数学界最珍视的技术之一——​​反证法​​——带来了直接而惊人的后果。

想象两位逻辑学家，经典主义者 Clara 和直觉主义者 Iris，正在审查一个证明。该证明试图为一个软件建立一个安全属性 $S$。它首先假设该属性为假（$\neg S$），经过一系列有效步骤后，推导出一个逻辑矛盾（$\bot$）。

Clara 胜利地宣布：“啊哈！这个假设导出了荒谬，所以它必定是假的。因此，$S$ 是真的！”

Iris 摇了摇头。“没那么快，”她说。“你只是成功地证明了假设 $\neg S$ 会导致矛盾。这为我们提供了一个 $\neg S \to \bot$ 的有效证明。根据我们对否定的定义，这是一个 $\neg(\neg S)$ 的证明。”

对于 Iris 以及任何构造主义者来说，这个证明仅仅表明了性质 $S$ 是不可反驳的。它并没有提供 $S$ 本身的直接、构造性证明。从 $\neg\neg S$ 到 $S$ 的经典跳跃是​​双重否定消除​​的一个实例，这一原则等价于排中律。对于构造主义者来说，这种跳跃是一种毫无根据的信念飞跃。有趣的是，反向的蕴含关系 $P \to \neg\neg P$ 在构造逻辑中是完全有效的。给定一个 $P$ 的证明，你当然可以证明它不可能被反驳！。

我们如何才能想象一个 $P \lor \neg P$ 可能不为真的逻辑？我们能画出一幅图景吗？逻辑学家 Saul Kripke 用他优雅的 ​​Kripke 语义学​​为我们提供了这样一幅图景。

想象一下，我们的知识不是静态的，而是随着时间的推移而增长。我们可以将其建模为穿越“可能世界”景观的旅程，每个世界代表一个知识状态。我们可以从一个世界移动到另一个世界，但只能以增加我们知识的方式移动；我们永远不会忘记已经确立的东西。这被建模为一个世界集合 $W$ 和一个可达关系 $\le$。如果 $w \le v$，意味着 $v$ 是一个可以从 $w$ 到达的“未来”知识状态。基本规则是​​单调性​​：如果你在世界 $w$ 中知道一个事实 $A$，那么在任何未来的世界 $v$ 中你仍然知道它。

强制关系 $w \Vdash A$ 意味着“在知识状态 $w$ 中，我们有 $A$ 的一个证明”。下面是它如何作用于我们的联结词：

• $w \Vdash A \land B$ 如果我们当前在世界 $w$ 中既有 $A$ 的证明，也有 $B$ 的证明。
• $w \Vdash A \lor B$ 如果我们当前在世界 $w$ 中有 $A$ 的证明或 $B$ 的证明。
• $w \Vdash A \to B$ 如果对于从 $w$ 可达的所有未来世界 $v$（即 $v \ge w$），若我们在世界 $v$ 中得到了 $A$ 的证明，那么我们在世界 $v$ 中也必须有 $B$ 的证明。蕴含的承诺必须对所有可能的未来都成立！
• $w \Vdash \neg A$ 如果在从 $w$ 可达的任何未来世界 $v$ 中，我们都永远找不到 $A$ 的证明。

让我们用一个玩具宇宙来看看一条旧定律是如何失效的。考虑一个只有两个世界的宇宙：我们当前的状态 $w_0$ 和一个可能的未来状态 $w_1$，其中 $w_0 \le w_1$。假设我们在 $w_0$ 不知道 $P$ 是否为真，但我们发现在 $w_1$ 它变为真。再假设 $Q$ 永远不为真。用形式化术语来说：$V(P) = \{w_1\}$ 且 $V(Q) = \emptyset$。

现在，让我们测试一个经典的重言式，称为​​皮尔斯定律（Peirce's Law）​​：$((P \to Q) \to P) \to P$。它在我们的起点 $w_0$ 处为真吗？

1. 首先，考虑 $w_0$ 处的 $P \to Q$。它为真吗？规则说，如果对于所有未来世界，$P$ 都蕴含 $Q$，那么它就成立。但在未来世界 $w_1$ 中，我们有 $P$ 为真（$w_1 \Vdash P$），而 $Q$ 为假（$w_1 \nVdash Q$）。所以这个承诺被打破了。因此，$w_0 \nVdash P \to Q$。
2. 接下来，考虑 $w_0$ 处的更大部分 $(P \to Q) \to P$。它成立吗？规则问：在所有未来世界中，$(P \to Q)$ 是否蕴含 $P$？我们来检查一下。
   • 在 $w_0$，我们刚看到 $w_0 \nVdash P \to Q$。所以前提为假，蕴含关系空洞地成立。
   • 在 $w_1$，我们也需要检查。结果是 $w_1 \nVdash P \to Q$。所以前提再次为假，蕴含关系成立。 由于这个承诺在所有未来世界都成立，我们得出结论 $w_0 \Vdash (P \to Q) \to P$。
3. 最后，我们检查完整的公式：$((P \to Q) \to P) \to P$ 在 $w_0$ 处。我们刚刚发现左边部分 $(P \to Q) \to P$ 在 $w_0$ 处为真。但右边部分 $P$ 在 $w_0$ 处不为真（$w_0 \nVdash P$）。一个前提为真、结论为假的蕴含是假的。

因此，我们找到了一个世界 $w_0$，在其中皮尔斯定律失效了。它不是构造逻辑的一条普适定律。同样简单的模型也显示了排中律的失效。在 $w_0$，我们没有 $P$ 的证明。我们也没有 $\neg P$ 的证明，因为在未来的 $w_1$，$P$ 变为真，所以我们无法保证它总是可被反驳的。由于在 $w_0$ 处 $P$ 和 $\neg P$ 都不被强制为真，它们的析取 $P \lor \neg P$ 也不能被强制为真。

通过要求真理是我们能够构建并握在手中的东西，我们并没有摧毁逻辑。我们发现了一种新的逻辑，它更精妙，并且在许多方面，更符合发现和计算的过程。我们用一幅动态的、不断演进的知识地图，换下了一张静态的、黑白分明的世界照片。

我们已经看到，构造逻辑是一种关于真理的不同思考方式，它建立在证据和构造的理念之上。但这仅仅是哲学家的游戏，一种与“现实”世界无关的奇特数学方言吗？远非如此。事实证明，构造逻辑的原则不仅是经典推理的替代方案；它们正是现代计算的蓝图。这两个世界之间深刻的联系，即​​Curry-Howard 同构​​，如同一块罗塞塔石碑，让我们能够在逻辑证明的语言和计算机程序的语言之间进行翻译。本章将带领我们穿越这片令人惊奇而美丽的景象，探索逻辑与计算合二为一的领域。

乍一看，程序员编写的代码和逻辑学家涂写的证明似乎是完全不同的两种活动。然而，通过构造逻辑的视角，我们发现它们是同一枚硬币的两面。函数式编程语言的每一个基本构件，在逻辑中都有一个直接而精确的对应物。

蕴含，$A \to B$，即逻辑学家的“如果 $A$，则 $B$”，恰好是程序中的函数类型——一个给定类型为 $A$ 的输入，便能产生类型为 $B$ 的输出的过程。合取，$A \land B$（“$A$ 与 $B$”），是乘积类型或序对——一个同时包含类型 $A$ 的值和类型 $B$ 的值的数据结构。逻辑常数“真”（$\top$）和“假”（$\bot$），则分别对应于只有一个平凡值的“单元类型”（$1$）和没有任何值的“空类型”（$0$）。

但最美的对应关系，或许在于析取，$A \lor B$（“$A$ 或 $B$”）。它在计算中的孪生兄弟是和类型，$A + B$，其值要么是类型 $A$ 的值，要么是类型 $B$ 的值，并带有一个标签以告知我们是哪一种。现在，思考一下程序员必须如何使用这样的值。如果你有一个类型为 $A+B$ 的变量，你不能直接使用它；你必须写一个 case 语句，明确处理两种可能性：如果得到的是一个类型为 $A$ 的值该怎么办，如果得到的是一个类型为 $B$ 的值又该怎么办。编译器会强制执行这一点；忘记处理任何一种情况都是一个错误。这种“情况完备性”确保你的程序不会因为不知道如何继续而卡住。

这完全就是构造逻辑中析取消除的规则。要使用一个 $A \lor B$ 的证明，逻辑学家必须提供两个独立的子证明：一个证明从假设 $A$ 可以得出期望的结论 $C$，另一个证明从假设 $B$ 也可以得出 $C$。由于 $A \lor B$ 的证明只保证两者之一成立而未指明是哪一个，一个严谨的论证必须为两种情况都做好准备。程序员对健壮代码的需求和逻辑学家对严谨推理的需求是完全相同的。从非常真实的意义上说，编译器就是一位逻辑学家。

这种对应关系甚至更深。运行一个程序意味着什么？在这个世界里，它意味着简化一个证明。想象一个证明包含了一个逻辑上的弯路——例如，你费尽周折证明了 $A \to B$，然后在下一步就用一个已知的 $A$ 的证明来推断 $B$。这是一个“切除”(cut)。你本可以直接将 $A$ 的证明代入从一开始就推导 $B$ 的过程中。这个简化过程称为​​切消​​（cut-elimination）。它在计算中的等价物是什么？函数调用。$A \to B$ 的证明是一个 lambda 函数, $\lambda x. M$。$A$ 的证明是一个参数, $N$。带有“切除”的组合证明就是函数应用 $(\lambda x. M) N$。简化证明——即消除切除——的行为，恰好就是 $\beta$-归约的行为：将 $N$ 替换 $M$ 中的 $x$。运行一个程序，实际上就是让一个证明变得更直接、更优雅的过程。

这种转换是双向的。如果程序就是证明，我们就可以利用程序的性质来发现关于逻辑的真理。这一对应关系最惊人的成就之一，是逻辑本身一致性的证明——一个保证你永远无法证明矛盾的担保。

其论证过程既优美又深刻。在我们的系统中，矛盾 $\bot$ 对应于空类型 $0$。要证明逻辑是一致的，我们必须表明不可能证明 $\bot$。用计算术语来说，这意味着不可能构造一个类型为 $0$ 的程序。

现在，我们转向计算机科学的一个基本定理：简单类型 lambda 演算的​​强规范化定理​​。它指出，这个演算中每一个类型正确的程序都必须终止。不存在无限循环。每一个归约序列（证明简化序列）都必须最终结束于一个“范式”——一个无法再被归约的程序。

让我们暂时假设逻辑是不一致的。这意味着我们可以写出一个类型为 $0$ 的封闭程序 $M$。根据强规范化定理，这个程序 $M$ 必须在某个范式 $V$ 中终止。因为归约保持类型，所以 $V$ 的类型也必须是 $0$。但是一个类型为 $0$ 的范式会是什么样子？要回答这个问题，我们来看引入规则。一个范式的值必须是由一个构造器创建的。但是空类型 $0$ 没有任何构造器！没有办法从零开始创建一个类型为 $0$ 的值。因此，不存在类型为 $0$ 的范式。

我们得到了一个矛盾。我们的假设——即我们可以写出一个类型为 $0$ 的程序——必定是错误的。因此，$\bot$ 的证明不可能存在。逻辑是一致的。这是一个惊人的结果：计算的一个性质（停机性）证明了逻辑最深刻的性质之一（一致性）。

正是这个原理驱动着现代​​证明助手​​，如 Coq、Agda 和 Lean。在这些系统中，你通过编写一个程序来证明一个数学定理。系统的类型检查器随后会验证你的程序是否具有与你想证明的定理相对应的类型。停机性（或在更复杂系统中类似的其他性质）的保证确保了你所写的是一个有效的、构造性的证明。通过扩展到​​依赖类型​​，这种对应关系可以扩展到完整的谓词逻辑，其中类型可以依赖于值。这使得表达极其丰富的规范成为可能，例如，证明一个排序函数不仅返回一个列表，而且该列表是排好序的，并且是原始列表的一个排列。这是形式化验证编程的核心，其中软件不仅被测试，而且被形式化地证明是正确的。

细心的读者会注意到，我们的对应关系是与直觉主义逻辑建立的。那么经典逻辑呢？它拥有像排中律（$P \lor \neg P$）这样强大的非构造性原则。不存在一个简单的程序，对于任意类型 $P$，能够神奇地产生一个类型为 $P$ 的值或一个从 $P$ 到空类型的函数。

然而，故事并未就此结束。这种联系比初看起来要深刻得多。经典逻辑同样具有计算意义，但它对应于更奇特的编程特性：​​控制算子​​。著名的是，Timothy Griffin 发现像 call/cc (call-with-current-continuation) 这样的算子——它允许程序将“计算的剩余部分”捕获为一个函数并稍后跳回——恰好对应于皮尔斯定律，一个与双重否定消除和排中律等价的原则。这揭示了经典推理中看似“神奇”的方面，在高级控制流中看似“怪异”的方面得到了镜像。[@problem-id:2985613]

我们还可以使用所谓的​​否定翻译​​将经典逻辑系统地嵌入到直觉主义逻辑中。这些翻译以一种使其在构造上可证的方式重新解释经典陈述，通常是通过将它们包裹在双重否定中。例如，虽然选择公理——以及经典逻辑中相关的 Skolem 化技术——在构造上是无效的，但它的双重否定版本可以在构造框架内被恢复和理解。这使我们能够发现隐藏在经典证明中的构造性内容，并精确地理解采取了哪些非构造性步骤。

构造逻辑由于对证据更为明确，提供了对证明更丰富、更精细的视角。但这种丰富性是否伴随着代价？令人惊讶的是，答案来自计算复杂性理论。判断一个给定的命题公式是否为重言式（普遍为真）的问题，对于经典逻辑来说是著名的 ​​coNP-完全​​ 问题。然而，对于直觉主义逻辑，同样的问题是 ​​PSPACE-完全​​ 的——这是一个难度大得多的问题类别。

其直觉在于，一个经典赋值存在于一个单一、静态的世界中。要检查一个公式，你只需检查所有可能的真值指派。然而，一个直觉主义证明必须在所有可能的“知识状态”构成的整个宇宙中都有效，这个宇宙可以被建模为一个世界之树（一个 Kripke 模型）。一个直觉主义证明必须提供一个在我们穿越这棵树时都有效的一致方法。验证这一点涉及一种在证明者和反驳者之间穿越可能性之树的游戏，这种结构与量化布尔公式（TQBF）——典型的 PSPACE-完全问题——的求值过程密切相关。构造性证明是一个更强大的对象，验证它的存在是一项更艰巨的任务。

同样地，这个分析视角也可以转向数学本身。利用构造性和可计算性的工具，​​逆向数学​​领域分析经典定理，以探究证明它们真正需要哪些公理。考虑命题逻辑的紧致性定理。一个经典证明使用了超滤子引理，一个与选择公理相关的非构造性原则。另一个证明则构造了一棵搜索树。逆向数学表明，在一个弱基础理论之上，紧致性定理是不可证的，事实上，它等价于一个称为弱哥尼希引理（Weak Kőnig's Lemma）的原则——一种弱形式的选择公理。这种分析揭示了一个定理精确的非构造性“成本”，使我们能够根据其基础强度对数学的支柱进行分类。

这场始于将证明与程序简单等同的旅程，已将我们引向编程语言设计、软件验证、计算复杂性以及数学基础本身的前沿。Curry-Howard 同构远不止是一个技术上的奇闻轶事；它是我们关于真理的概念与我们关于构造的方法之间一场深刻而无尽的对话，揭示了形式科学核心处一种优美而深刻的统一。