证明
| 证明 | |
|---|---|
| 术语名称 | 证明 |
| 英语名称 | 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)。
| 证明论 | |
|---|---|
| 形式化公理系统（形式化、公理化） | |
| 举例 | 公理系统、自然演绎系统 |
| 证明、演绎 | 证明、可证明、演绎、可演绎 |
| 命题、定理 | 公理、定理、元定理、变形规则 |
| 推理规则性质 | 保存真实性、保存重言性 |
| 公理系统性质 | 可靠性、完全性、一致性、独立性 |