完备性(逻辑)
外观
| 完备性 | |
|---|---|
| 术语名称 | 完备性 |
| 英语名称 | completeness |
| 别名 | 完全性 |
完备性(completeness)指一个公理系统中,一个前提所逻辑蕴含(若为命题逻辑,则为重言蕴含)的结论都是能从前提演绎出的。 也就是说,这个推理系统在推理上是充分的、强大的,凡是成立的,都是能推导出的。其中任意在语义上有后承关系东西在语义上都一定也可以从语法上推演,不会有任何语义上正确的公式无法通过这个推理系统推理出。
定义
对公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中,给定其中任意前提 [math]\displaystyle{ \Gamma }[/math] 和结论 [math]\displaystyle{ \phi }[/math] ,若 [math]\displaystyle{ \Gamma \vDash \phi }[/math] ,则 [math]\displaystyle{ \Gamma \vdash \phi }[/math] 。特别地,对 [math]\displaystyle{ \vDash\phi }[/math] 的情况有 [math]\displaystyle{ \vdash\phi }[/math] ,即普遍有效公式一定是可证明的。
| 证明论 | |
|---|---|
| 形式化公理系统(形式化、公理化) | |
| 推理系统 | Hilbert 风格/公理系统:Hilbert 表示 |
| Gentzen 风格-自然演绎系统: Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | |
| Gentzen 风格-相继式演算: Gentzen 式相继式演算 | |
| 证明、演绎 | 演绎、可演绎、证明、可证明 |
| 命题、定理 | 公理/公理模式、定理、元定理、变形规则 |
| 推理规则性质 | 保存真实性、保存重言性 |
| 公理系统性质 | 可靠性、完备性/完全性、一致性、独立性 |