一致性
| 一致性 | |
|---|---|
| 术语名称 | 一致性 |
| 英语名称 | consistency |
| 一致的 | |
|---|---|
| 术语名称 | 一致的 |
| 英语名称 | consistent |
一致性(consistency)在证明论中有两种含义。 其一可指一个形式化公理系统中，不会同时证明出一对互为否定的定理。 其二可指形式化公理系统中给定多个前提不会同时演绎出一对互为否定的结论。
通常的可演绎关系都会满足爆炸原理成立，如果一个推理系统不一致，可以推导出一对矛盾，则可以证明出任何公式，失去使用这一系统推理的意义。因此也可以表述为：公理系统是一致的，当且仅当其所有定理的集合不是所有公式的集合。
定义
对给定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] ，若不存在公式 [math]\displaystyle{ \phi }[/math] 使得 [math]\displaystyle{ \vdash \phi }[/math] 且 [math]\displaystyle{ \vdash \lnot \phi }[/math] ，称公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 是一致的(consistent)。否则称公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 是不一致的(inconsistent)。
对给定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 及公式集 [math]\displaystyle{ \Gamma }[/math] ，若不存在公式 [math]\displaystyle{ \phi }[/math] 使得 [math]\displaystyle{ \Gamma \vdash \phi }[/math] 且 [math]\displaystyle{ \Gamma \vdash \lnot \phi }[/math] ，称公式集 [math]\displaystyle{ \Gamma }[/math] 在公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中是一致的(consistent)。否则称公式集 [math]\displaystyle{ \Gamma }[/math] 在公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中是不一致的(inconsistent)。
性质
对形式化公理系统中的一个公式集：
- 若公式集是一致的，则其演绎结论的集合也是一致的。
- 若公式集是可满足的，则公式集一定是一致的。
- 公式集 [math]\displaystyle{ \Gamma }[/math] 是不一致的，当且仅当，对所有公式 [math]\displaystyle{ \phi }[/math] 有 [math]\displaystyle{ \Gamma\vdash\phi }[/math] 。
- 对公式集 [math]\displaystyle{ \Gamma }[/math] 和 公式 [math]\displaystyle{ \phi }[/math] ， [math]\displaystyle{ \Gamma\vdash\phi }[/math] 当且仅当 [math]\displaystyle{ \Gamma\cup\{\lnot\phi\} }[/math] 不一致。
- 对非空公式集 [math]\displaystyle{ \Gamma }[/math] ， [math]\displaystyle{ \Gamma }[/math] 是不一致的，当且仅当，对任意公式 [math]\displaystyle{ \phi }[/math] 有 [math]\displaystyle{ \Gamma\setminus\{\phi\}\vdash \lnot\phi }[/math] 。
- 对公式集 [math]\displaystyle{ \Gamma }[/math] 和 公式 [math]\displaystyle{ \phi }[/math] ，若 [math]\displaystyle{ \Gamma }[/math] 是一致的，则 [math]\displaystyle{ \Gamma\cup\{\phi\} }[/math] 和 [math]\displaystyle{ \Gamma\cup\{\lnot\phi\} }[/math] 中有一个是一致的，一个是不一致的。
对形式化公理系统的一致性也有类似以上的性质。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |