演绎定理
| 演绎定理 | |
|---|---|
| 术语名称 | 演绎定理 |
| 英语名称 | deduction theorem |
| 别名 | 条件证明规则, DT |
演绎定理(deduction theorem，DT)是重要的元定理。这一定理表明条件命题的证明和命题间的演绎可以互相转化，表现了元语言中中的可演绎性和对象语言中蕴含词之间有对应关系，可以向系统中引入条件证明规则作为一个推理步骤。也就是说在讨论元定理时，可演绎性可以与可证明性一同处理。
演绎定理是大部分推理系统的基础。
定理
对公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi,\psi }[/math] ，有： [math]\displaystyle{ \Gamma, \phi \vdash \psi }[/math] 则 [math]\displaystyle{ \Gamma \vdash \phi\rightarrow\psi }[/math] 。
注：
- 可推广到多个前提。 [math]\displaystyle{ \Gamma,\phi_1,\cdots,\phi_k \vdash \psi }[/math] 则有 [math]\displaystyle{ \Gamma\vdash \phi_1\rightarrow\cdots\rightarrow\phi_k\rightarrow\psi }[/math] 。
- 在谓词逻辑中需要公式是闭式，对自由变元使用概括规则加入全称量词。
意义
- 逆命题 [math]\displaystyle{ \Gamma\vdash\phi\rightarrow\psi }[/math] 则 [math]\displaystyle{ \Gamma,\phi\vdash\psi }[/math] ，可由切消定理和分离规则推出。
- 实现了假言推理和条件命题之间的转换，解释了元语言层次的可演绎性和对象层次的蕴含词的关系。
- 统一了演绎和证明，使得相关讨论中可以只讨论其中的一种情况。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |