自然演绎 · aiwiki.page

自然演绎是逻辑学中的一类证明系统，通过应用推理规则将演绎推理形式化。其显著特征是在临时假设下进行推理：证明中可以包含一个子论证，而该子论证的假设随后会被撤销。这种结构体现了数学证明中常见的推理模式，例如先假设前件，再推导出后件，从而证明一个条件命题。“自然”指的是这种系统旨在贴近日常论证方式，而不是说它不受形式约束。(plato.stanford.edu)

历史发展与表示方式

格哈德·根岑和斯坦尼斯瓦夫·雅希科夫斯基分别在1934年发表的研究中独立提出了自然演绎系统。根岑用树形结构表示推导，以推理步骤连接各个公式；雅希科夫斯基则发展了组织子证明的方法。他们的方法将假设性推理纳入形式系统，使其成为明确的组成部分。此后，自然演绎在20世纪50至60年代的逻辑学入门教材中得到广泛采用。(plato.stanford.edu)

不同的表示方式都保留了这一基本结构。在证明树中，假设位于由其推导出的结论上方，撤销标记则指出结论在何处不再依赖这些假设。在菲奇记法中，带编号的行以及缩进或方框围起的子证明用于显示假设的作用范围。各类表示方式的约定有所不同，因此，同一个论证可以具有不同的外观，而其逻辑内容并无差别。(plato.stanford.edu)

引入规则与消去规则

在命题逻辑中，规则通常按引入与消去配对组织。引入规则说明如何确立一个复合公式；消去规则说明如何使用一个已经确立的复合公式。这些规则用于构造形式证明，而不是计算真值表。(leanprover.github.io)

典型规则包括：

**合取：**由 $A$ 和 $B$ 推出 $A\land B$ ；由 $A\land B$ 推出任一合取支。
**蕴涵：**如果一个子证明在假设 $A$ 下推导出 $B$ ，则撤销该假设，并推出 $A\to B$ 。由 $A\to B$ 和 $A$ 推出 $B$ ；这一消去规则就是肯定前件式。
**析取：**由 $A$ 推出 $A\lor B$ ，由 $B$ 也可同样推出。要使用 $A\lor B$ ，需分别在假设 $A$ 和假设 $B$ 下推导出同一个结论 $C$ ，然后撤销这两个分情况讨论的假设。
**否定：**在假设 $A$ 下得出矛盾（记作 $\bot$ ），即可推导出 $\neg A$ 。由 $A$ 和 $\neg A$ 推出 $\bot$ 。
**假：**在标准的直觉主义系统和经典系统中，可以由 $\bot$ 推出任意公式。(leanprover.github.io)

消去规则不一定会得出更短的公式：例如，析取消去可以确立两个分支都支持的任意结论。(leanprover.github.io)

假设、假设撤销与示例

撤销假设会改变结论所依赖的前提。它既不意味着临时假设为真，也不会撤销其他仍然有效的假设。在子证明内部推导出的公式，不能在忽略其对该子证明假设的依赖的情况下，直接拿到子证明外使用。(plato.stanford.edu)

例如，合取交换律可通过如下推导得到：

1. | A ∧ B                 假设
2. | A                     ∧ 消去，1
3. | B                     ∧ 消去，1
4. | B ∧ A                 ∧ 引入，3，2
5. (A ∧ B) → (B ∧ A)       → 引入，1–4

第2至4行依赖第1行。第5行撤销该假设，确立了一个不再依赖任何前提的条件命题。这个例子说明，从某个假设证明一个结论，与证明该假设蕴涵该结论，是两件不同的事。(leanprover.github.io)

量词与一阶逻辑

一阶逻辑的自然演绎增加了量词规则。全称消去允许由 $\forall x\,P(x)$ 得到 $P(t)$ ，前提是代入不会造成变量捕获。存在引入允许由 $P(t)$ 得到 $\exists x\,P(x)$ 。(leanprover.github.io)

与之配对的规则则对任意参数施加限制。全称引入只有在 $a$ 不自由出现于该推导所依赖的任何未撤销假设中时，才允许由 $P(a)$ 推导出 $\forall x\,P(x)$ 。否则，针对某个受到特殊约束的对象得到的结果，就可能被误当作适用于所有对象的结果。(leanprover.github.io)

存在消去使用一个新的参数 $a$ 和假设 $P(a)$ 开启子证明。如果结论 $C$ 不依赖于这个见证对象的具体身份，就可以由 $\exists x\,P(x)$ 推出 $C$ ： $a$ 不得自由出现于 $C$ 或其他相关的未撤销假设中。等号规则通常包括自反性和等项替换。(leanprover.github.io)

经典系统与直觉主义系统

自然演绎是一种证明系统的形式，并不限定采用哪一种逻辑。标准的直觉主义逻辑使用上述构造性的引入规则和消去规则。加入双重否定消去、排中律或适当的经典反证法规则，即可得到经典逻辑。在通常的直觉主义基础系统上，这些原则彼此等价。(leanprover.github.io)

两者的区别在于，从矛盾中能够确立什么。在直觉主义逻辑中，假设 $A$ 并推导出 $\bot$ ，足以确立 $\neg A$ 。假设 $\neg A$ 并推导出 $\bot$ ，则直接确立的是 $\neg\neg A$ ；要进一步推出 $A$ ，还需要一条经典原则。(leanprover.github.io)

元理论与计算解释

证明论研究这些推导的性质。可靠性将可推导性与逻辑有效性联系起来：若 $\Gamma\vdash A$ ，则 $\Gamma\models A$ 。完备性则相对于所选的语义学确立反向关系。这些性质关乎证明与语义后承之间的对应，而不是寻找证明的难易程度。(leanprover.github.io)

规范化消除某些推理中的绕行，例如先引入一个合取式，随即又取出其中一个合取支。规范化结果取决于具体的演算；处理经典规则时尤其需要谨慎。自然演绎与相继式演算密切相关，后者的切消定理为分析证明结构提供了另一种途径。(plato.stanford.edu)

在柯里—霍华德对应下，适当的自然演绎系统与带类型的计算演算相对应。命题对应类型，证明对应项，蕴涵引入对应函数抽象，蕴涵消去对应函数应用。这将自然演绎与类型论及编程语言联系起来。Lean证明助手等证明助手通过可由机器检查的证明表达式来表示相关推理，不过，它们的底层基础比初等自然演绎更为丰富。(cs.cmu.edu)