[!info] related notes

• 所属 MOC: logic-moc
• 前置概念:
• 并列概念:
• 易混淆概念:
• 关系笔记:

自然演绎

一句话定义

自然演绎（Natural Deduction）是一种形式证明系统：从给定前提出发，每一步只使用明确允许的推理规则，最终得到目标结论。

它把“我觉得这个结论能推出”改造成：

第 1 行来自哪个前提？
第 2 行用了哪条规则？
第 3 行依赖哪些行？
结论到底怎样一步步得到？

为什么叫“自然”演绎

它试图把日常中自然使用的推理动作形式化，例如：

• 已知 P ∧ Q，可以取出 P；
• 已知 P 和 Q，可以合成 P ∧ Q；
• 已知 P → Q 和 P，可以得到 Q；
• 为了证明 P → Q，可以暂时假设 P，再在子证明中推出 Q。

相比只靠真值表枚举全部赋值，自然演绎更像真正的“推导过程”。

最小例子

前提：

1. P → Q
2. P

目标：Q。

证明：

1. P → Q    Premise
2. P        Premise
3. Q        → Elimination, 1,2

第 3 行就是 Modus Ponens，也称条件消去。

引入规则与消去规则

自然演绎常围绕一个统一思想组织：

Introduction：怎样证明一个联结词构成的命题？
Elimination：已经有这种命题后，可以从中取出什么？

合取 ∧

∧ Introduction

P
Q
────
P ∧ Q

∧ Elimination

P ∧ Q
─────
P

或得到 Q。

条件 →

→ Elimination

P → Q
P
─────
Q

就是肯定前件。

→ Introduction：条件证明

为了证明：

P → Q

可以暂时假设 P，然后在这个假设下推出 Q：

1. [P]      Assumption
2. ...
3. Q
4. P → Q    → Introduction, 1–3

关键是：P 只是局部假设。证明完成后，它被 discharge（解除），最终不再作为无条件前提存在。

一个条件证明例子

前提：

P → Q
Q → R

证明：

P → R

过程：

1. P → Q       Premise
2. Q → R       Premise
3. [P]         Assumption
4. Q           →E 1,3
5. R           →E 2,4
6. P → R       →I 3–5

这就是把“如果 P 导致 Q、Q 又导致 R，那么 P 导致 R”正式写成证明。

否定与矛盾

很多自然演绎系统把：

¬P

理解为：

P → ⊥

其中 ⊥ 表示矛盾 / absurdity。

因此要证明 ¬P，可以：

1. 暂时假设 P；
2. 推出矛盾；
3. 解除 P，得到 ¬P。

反证法 Reductio ad Absurdum

要证明 P，可以暂时假设 ¬P，如果该假设最终导致矛盾，就得到 P。

经典逻辑中常写：

[¬P]
  ...
  ⊥
─────
P

但需要注意：不同逻辑系统对反证、双重否定消去等规则的允许程度不完全相同。直觉主义逻辑就比经典逻辑更谨慎。

析取 ∨

∨ Introduction

从 P 可以推出：

P ∨ Q

因为只要一边为真，析取就为真。

∨ Elimination：分类讨论

如果你知道：

P ∨ Q

并且：

从 P 能推出 R
从 Q 也能推出 R

那么可以推出 R。

结构：

P ∨ Q
[P] → ... → R
[Q] → ... → R
────────────
R

这就是形式化的“无论是哪种情况，都会得到 R”。

双条件 ↔

证明 P ↔ Q，通常要分别证明：

P → Q
Q → P

也就是两个方向都成立。

因此“充要条件”的证明天然是双向的。

证明与真值表的区别

真值表

回答：

有没有某个赋值让所有前提为真而结论为假？

优点：机械、直观、适合少量原子命题。

缺点：n 个原子命题需要 2^n 行，规模快速增长。

自然演绎

回答：

我能否通过合法局部规则，从前提构造出结论？

优点：展示为什么能推出，并可扩展到谓词逻辑。

二者都可以用于证明有效性，只是视角不同：

真值表 = 语义视角
自然演绎 = 证明 / 句法视角

证明中最容易犯的错误

1. 偷偷使用未给出的命题

证明不能因为某句话“现实中大概是真的”就直接加进去。

2. 子证明中的假设泄漏

局部假设只能在其作用域内使用。

这和编程中的 block scope 很像：

外层不能随便使用已经退出作用域的局部假设。

3. 把目标当成前提

如果为了证明 Q，直接把 Q 当作无条件前提使用，就变成循环。

4. 规则方向用反

从 P → Q 和 Q 不能用 →E 得到 P；那是肯定后件。

与编程 / 类型系统的类比

自然演绎与类型系统之间存在著名的 Curry–Howard 对应：粗略地说，命题可以看作类型，证明可以看作构造该类型的程序。

例如：

P → Q

可以类比成一个函数类型：

(p: P) => Q

如果你手上有：

f : P → Q
p : P

应用函数得到：

f(p) : Q

这和 Modus Ponens 结构完全对应。

这个类比很有启发性，但入门阶段不用把逻辑和类型论完全混在一起。

学习自然演绎的正确顺序

建议先掌握：

1. ∧I / ∧E
2. →E / →I
3. ∨I / ∨E
4. 否定与 ⊥
5. 反证法
6. 再进入 ∀ / ∃ 的量词规则

不要一开始背几十条规则。重点是理解：每种联结词如何被构造、如何被拆开。

快速自测

前提：

P ∧ Q
Q → R

目标：R。

最短证明：

1. P ∧ Q     Premise
2. Q → R     Premise
3. Q         ∧E 1
4. R         →E 2,3

一句记忆

自然演绎不是告诉你“结论看起来合理”，而是要求每一步都出示通行证。