切消定理
| 切消定理 | |
|---|---|
| 术语名称 | 切消定理 |
| 英语名称 | cut theorem |
| 别名 | 切割消去定理, cut-elimination theorem, Cut |
| 引理 | |
|---|---|
| 术语名称 | 引理 |
| 英语名称 | lemma |
切消定理(cut theory)是重要的元定理。这一定理表明演绎过程中可以将通过已经证明的命题（称为引理(lemma)）作为一个推理步骤，如果存在使用引理的推理过程，也一定存在不使用任何引理、只从公理和推理规则的推理过程。也就是说，引理的使用本身不会影响命题在推理系统中的可证明性、可演绎性。
切消定理基于演绎的定义，因此可适用于绝大多数推理系统。
定理
对任意公式集 [math]\displaystyle{ \Gamma }[/math] 、 [math]\displaystyle{ \Delta }[/math] 和公式 [math]\displaystyle{ \phi_1,\dots,\phi_k, \psi }[/math] ，若有 [math]\displaystyle{ \Gamma, \phi_1, \dots, \phi_k \vdash \psi }[/math] ，且对每个 [math]\displaystyle{ i = 1, \dots, k }[/math] 都有 [math]\displaystyle{ \Delta \vdash \phi_i }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \psi }[/math] 。
注：
- 部分材料中只使用只有一个 [math]\displaystyle{ \phi }[/math] 的版本。
- 一般记号上，相继式的右侧是析取关系，不能直接写成可演绎一个集合。
证明及构造
设 [math]\displaystyle{ \Gamma, \phi_1, \dots, \phi_k \vdash \psi }[/math] 的一个演绎为 [math]\displaystyle{ \psi_0 \dots \psi_l }[/math] ， 对 [math]\displaystyle{ i = 1, \dots, k }[/math] ， [math]\displaystyle{ \Delta \vdash \phi_i }[/math] 的一个演绎为 [math]\displaystyle{ \chi_1^i \dots \chi_{m_i}^i }[/math] 。
用序列 [math]\displaystyle{ \chi_1^i \dots \chi_{m_i}^i }[/math] 替换 [math]\displaystyle{ \psi_0 \dots \psi_l }[/math] 中 [math]\displaystyle{ \phi_1 \dots \phi_k }[/math] 的出现，得到新的序列。这个序列中重复的前提都是来自 [math]\displaystyle{ \Gamma\cup\Delta }[/math] 中的元素，最后一个是 [math]\displaystyle{ \psi }[/math] ，因此是从 [math]\displaystyle{ \Gamma\cup\Delta }[/math] 到 [math]\displaystyle{ \psi }[/math] 的一个演绎。
因此， [math]\displaystyle{ \Gamma,\Delta \vdash \psi }[/math] 。
意义
- 定理本身是为了 Gentzen 式相继式演算提出的，也称为“ Gentzen's Hauptsatz ”。但其也可用于其他系统。这一定理证明了形式化公理系统中都可以引入 cut 规则(cut rule)，也就是可以利用已经存在的证明作为一个步骤构造新的证明，这样“使用 cut 规则的证明”存在则一个“未使用 cut 规则的证明”(cut-free proof)也一定存在，总是能通过这个定理消除这些 cut 。
- 从 [math]\displaystyle{ \Delta }[/math] 可以演绎出 [math]\displaystyle{ \psi_i }[/math] ，这些 [math]\displaystyle{ \psi_i }[/math] 作为部分条件可以演绎出 [math]\displaystyle{ \psi }[/math] ，则可以以 [math]\displaystyle{ \Delta }[/math] 作为代替，“切去”中间 [math]\displaystyle{ \psi_i }[/math] 部分的出现。在通常的证明中很常出现这种证明方式，其中 [math]\displaystyle{ \Delta \vdash \phi_i }[/math] 称为引理(lemma)。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |