自然演绎

自然演绎把数学证明中两种动作分开：怎样构造一种证据，以及拿到这种证据后可以做什么。要证明合取，就分别提供两部分；要使用合取，就选出所需部分。要证明蕴涵，就暂时把前件当作可用资源，在其作用域内推出后件，然后关闭这项假设。要使用蕴涵，则把它应用到前件。这种局部的“构造—使用”配对，使联结词的意义体现在推理规则里，而不只是体现在真值表中。

开放假设是证明的一部分，不是写在旁边的注释。一个推导节点除了公式，还隐含它依赖哪些假设出现；引入蕴涵、消去析取或消去存在量词时，只能解除规则明确标记的那些出现。Fitch 盒、带标号的推导树和序列式记法只是三种作用域可视化方式，核心都是防止已经关闭的前提重新泄漏进结论。

引入后立刻消去通常形成一段没有实质信息的绕路。例如先由 $A,B$ 构造 $A\wedge B$，马上又投影回 $A$。规范化会把这段推导直接缩成原来的 $A$ 推导；对应到带类型的程序，它类似构造一对值后立即取第一分量。不断消去这类最大公式，可得到更直接的正常证明，并解释自然演绎为何适合 Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。。

证明 $P\to (Q\to P)$ 可以清楚展示嵌套作用域。先临时假设 $P$；在这个盒子里再假设 $Q$，原先的 $P$ 仍可使用，因此由 $\to I$ 关闭 $Q$ 得到 $Q\to P$；最后关闭 $P$，得到目标。若关闭外层 $P$ 后又在别处直接引用它，错误在于依赖管理，而不是公式的真值。

量词的新鲜性可以用反例看得更清楚。由开放假设 $P(a)$ 不能用 $\mathrm{\forall }I$ 推出 $\mathrm{\forall }x,P(x)$，因为已知信息只关乎那个特定的 $a$。同样，从 $\mathrm{\exists }x,P(x)$ 消去存在量词时，可以令新名字 $a$ 暂代表某个见证，并在假设 $P(a)$ 下推出与 $a$ 无关的 $C$；若最终结论仍是 $Q(a)$，就把一个未知见证错误地当成了可公开命名的对象。

最小的直觉主义自然演绎不接受排中律 $A\vee \mathrm{\neg }A$、双重否定消去 $\mathrm{\neg }\mathrm{\neg }A\to A$ 或经典反证法作为无条件规则。经典自然演绎可以额外加入其中一种足够强的经典原则，并推出其余常见形式。两种系统共享大量规则，但可证明公式不同；不能在声称“直觉主义证明”时悄悄使用经典步骤。

规则局部并不意味着自动证明搜索简单。向后使用 $\vee E$ 需要选择中间析取式，量词规则需要选择项或新变量，经典原则还会扩大搜索空间。规范化保证可删去某类绕路，却不等于为任意公式提供高效的证明发现算法。

演绎定理公理库演绎定理Deduction theorem在适当证明系统中，把一个临时前提移入蕴含式前件。在 Hilbert 风格系统中是一条关于可推导性的元定理；自然演绎把同一模式直接做成 $\to I$，因此假设解除成为对象系统中的一步。相继式演算公理库相继式演算Sequent calculus以左右公式序列构成相继式并用结构规则和逻辑规则推导的证明演算。则把左右上下文与结构规则显式化，更适合研究 cut 消去和证明搜索。二者能表达相近逻辑，却以不同方式组织局部推理，不能把记法差别误当成完全相同的证明对象。

规范化带来正常形和子公式性质等元理论结果，并通过 Curry–Howard 把假设对应为变量、蕴涵引入对应为函数抽象、蕴涵消去对应为函数应用。证明助理中的 tactic 或 term mode、函数式语言的类型检查，以及结构化数学证明中的临时假设盒，都在不同层面复用了这种作用域纪律。