证明
| 证明 | |
|---|---|
| 术语名称 | 证明 |
| 英语名称 | proof |
| 可证明的 | |
|---|---|
| 术语名称 | 可证明的 |
| 英语名称 | provable |
| 定理 | |
|---|---|
| 术语名称 | 定理 |
| 英语名称 | theorem |
| 别名 | thesis |
证明(proof)指某个推理系统的变形规则下，从空前提到某一结论的步骤。 对应地，这个步骤的存在性被称为可证明(provable)。 定理(theorem)即该系统中任一可证明的公式。
在证明论以外的语境下，无论有无前提均称为证明。但是在证明论中，与其范围一致的概念是演绎，只有其中无前提的部分才叫做证明。
定义
在指定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中，从空集 [math]\displaystyle{ \varnothing }[/math] 到公式 [math]\displaystyle{ \phi }[/math] 的一个演绎，即对公式 [math]\displaystyle{ \phi }[/math] ，满足下列条件的公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] ：
- [math]\displaystyle{ \phi_n = \phi }[/math]；
- 对任意 [math]\displaystyle{ k \lt n }[/math]， [math]\displaystyle{ \phi_k }[/math] 符合以下任一条件：
- 是 [math]\displaystyle{ \mathbf{H} }[/math] 中的公理；
- 能运用 [math]\displaystyle{ \mathbf{H} }[/math] 中的推理规则从 [math]\displaystyle{ \phi_0, \dots, \phi_{k-1} }[/math] 得到。
这样的公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中公式 [math]\displaystyle{ \phi }[/math] 的一个证明(proof)。
对任意公式 [math]\displaystyle{ \phi }[/math] ，以下条件等价：
- 公式 [math]\displaystyle{ \phi }[/math] 可从空集演绎（[math]\displaystyle{ \varnothing \vdash \phi }[/math]）；
- 存在从空集到 [math]\displaystyle{ \phi }[/math]的演绎；
- 存在 [math]\displaystyle{ \mathbf{H} }[/math] 中 [math]\displaystyle{ \phi }[/math] 的证明。
此时称 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中 可证明的(provable)，记作 [math]\displaystyle{ \vdash \phi }[/math] ，并称 [math]\displaystyle{ \phi }[/math] 为 [math]\displaystyle{ \mathbf{H} }[/math] 中的定理(theorem, thesis)。
性质
- 演绎定理的特例： [math]\displaystyle{ A\vdash B }[/math] 当且仅当 [math]\displaystyle{ \vdash A\rightarrow B }[/math] 。
- 作为特殊的演绎，在各推理系统中公式序列的表现：
- Hilbert 表示：在演绎过程中仅会出现公理及其直接变形，不存在提及假设的步骤。
- Gentzen 式自然演绎：证明树中所有叶结点都是公理或被解除的假设。
- Fitch 式自然演绎：根证明中不存在前提，子证明中的假设都随着子证明结束而解除。
- Suppes–Lemmon 式自然演绎：结论依赖的行都是公理。
- Gentzen 式相继式演算：证明数中所有叶结点都是公理，通常是 [math]\displaystyle{ A\vdash A }[/math] 的形式。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |