Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

想象一下，你正试图建造一台终极的“证明助手”——一个超级聪明的机器人，它能帮助人类检查数学和逻辑作业，以确保其 100% 正确。几十年来，大多数这类机器人都是使用一种被称为依赖类型论 (Dependent Type Theory, DTT) 的特定蓝图构建的。这就像是用一套非常复杂、高科技的乐高积木来建造机器人，每一块积木都有特定的标签，机器人在允许你将它们拼在一起之前，会先检查这些标签是否完全匹配。

但在本文中，作者 Dale Miller 指出，还有另一种——或许是更好的——构建机器人的方式。他主张我们应该研究结构证明论 (Structural Proof Theory)，特别是名为相继式演算 (Sequent Calculus) 的框架。不要把这看作是一套僵化的乐高积木，而要把它看作一个动态的、移动的拼图，其中的碎片可以滑动和变形，只要逻辑成立即可。

以下是为什么 Miller 认为这种“拼图”方法可能优于“乐高”方法的理由，使用了六个核心观点：

1. 将“是什么”与“如何做”分离

在乐高世界（DTT）中，机器人同时决定两件事：你正在使用什么样的逻辑，以及如何构建证明。这就像是在说：“我们只能使用红色的积木来搭建塔楼，而且唯一的堆叠方式就是垂直向上。”
Miller 建议我们应该将这两者分离。我们可以决定逻辑（游戏的规则），然后选择任何我们想要的证明结构来解决它。这就像是你决定要踢足球，但随后意识到你可以通过踢球、头球，甚至如果规则允许的话，使用“弹射炮”来得分。相续式演算让你可以使用许多不同的“招式”（如自然演绎、真值表或归结原理），而不会被强迫进入单一、僵化的风格。

2. “证明即代码”的问题

乐高方法将证明视为一种计算机程序（一个 λ-term）。虽然计算机擅长运行程序，但它们有时很挑剔。有时，程序会走一条奇怪的路径来获取答案，或者因为在等待特定类型的输入而卡住。
Miller 指出，乐高方法必须处理一些混乱的问题，比如“层级 (universe levels)”（一种组织类型以防止它们相互冲突的复杂方式）和“证明无关性 (proof irrelevance)”（浪费时间去检查那些实际上并不重要的证明部分）。相继式演算则更为简单；它不需要担心这些沉重的类型规则，因为它更直接地处理证明结构，就像处理流程图而不是复杂的代码脚本一样。

3. 处理“经典”逻辑（“要么/要么”问题）

有些逻辑是“直觉主义”的（你必须通过构建某物来证明它的存在），而有些是“经典”的（你只需证明某物不可能不存在即可证明其存在）。
乐高方法在平滑处理“经典”风格方面表现挣扎。它通常需要添加额外的、笨拙的规则才能使其工作。Miller 认为，相继式演算从设计之初就是为了能够同样好地处理这两种风格，就像一个通用的适配器，无需臃né 转换器就能适配任何插头。

4. 拥抱“也许”（非确定性）

这是一个大点。乐高机器人被构建为“确定性”的，这意味着它们必须遵循单一、笔直的路径来检查证明。如果遇到死胡同，它们就会停止。
Miller 建议，允许一点点“非确定性”（猜测和回溯）实际上是一种超能力。想象一个迷宫。一个确定性的机器人走一条路，如果撞墙就停止。一个非确定性的机器人可以尝试一条路，撞墙后说“哎呀”，然后立即尝试另一条路。
Miller 认为，通过让证明检查器进行“猜测”和回溯，我们可以使“证明证书”（你交上去的作业）变得更小。机器人承担了繁重的搜索工作，因此你不需要写下每一个步骤。这是一种权衡：一份更小的作业单，换取一个需要思考得更多的机器人。

5. “移动绑定”的魔力

这是本文最令人兴奋的技巧。在逻辑中，我们经常处理被“绑定”的变量（例如“对于所有 x...”中的“x”）。在乐高世界中，这些变量通常是固定不动的，处理它们是一场技术噩梦（例如著名的 POPLMark 挑战）。
Miller 提出了一个视角，认为这些变量是可移动的。他称之为 λ-树语法 (λ-tree syntax)。
想象变量是一个名字标签。在乐高世界中，如果你移动那个人，名字标签可能会掉下来或产生混淆。在 Miller 的世界里，名字标签是粘在那个人身上的。无论你如何移动那个人（或证明），名字标签都会随之移动。
他引入了一个特殊的工具，称为 ∇-量词 (∇-quantifier)（读作 "nabla"）。你可以把它看作一个“局部作用域”按钮。当你按下它时，它表示：“这个变量仅属于这个特定的证明部分，它永远无法逃脱。”这使得处理具有复杂规则的语言（如编程语言或建模计算机通信方式的 π-演算）变得极其容易。

6. Abella 机器人

Miller 不仅仅是在空谈，他还建造了一个机器人来证明这是行得通的。它叫做 Abella。
Abella 是一个完全基于这些相继式演算原则构建的定理证明器。它利用“移动绑定”和 “∇-量词”来轻松处理关于变量命名和移动的复杂逻辑。虽然基于乐高的机器人（如 Coq 或 Lean）非常流行且拥有庞大的预构建证明库，但 Abella 表明，对于某些棘手的问题——特别是涉及变量如何命名和移动的问题——这种新方法更加自然且优雅。

核心结论

Miller 并不是在说乐高机器人（依赖类型论）不好，或者应该把它们丢弃。他承认它们已经成熟、应用广泛，并且在许多领域都表现出色。
然而，他建议，对于我们如何设计这些证明助手的基础，相继式演算提供了一个更灵活、更简单且更强大的工具包。它将逻辑与结构分离，拥抱智能猜测，并以一种目前的标准难以企及的优雅方式，处理“移动变量”这一棘手问题。这是一个邀请，邀请我们从不同的角度看待问题，使用一个在逻辑的其他领域已经取得成功的框架，但该框架尚未在交互式证明助手的世界中占据中心地位。