保存重言性
| 保存重言性 | |
|---|---|
| 术语名称 | 保存重言性 |
| 英语名称 | tautology-preserving |
| 别名 | 保存有效性, validity-preserving |
保存重言性(tautology-preserving)指一个推理规则，应用于重言式/有效式时只能得到重言式或有效式。表示一个推理规则中两个公式的可演绎关系保证每个模型上的满足关系。
定义
对一个推理规则、谓词语言及该语言的一个模型 [math]\displaystyle{ \mathfrak{I} }[/math] ，对 [math]\displaystyle{ \mathfrak{I}\vDash\phi }[/math] 任意公式 [math]\displaystyle{ \phi }[/math] ，即对该模型上任意赋值 [math]\displaystyle{ \sigma = (\mathfrak{I}, A) }[/math] 均有 [math]\displaystyle{ \sigma\vDash\phi }[/math] ，将给定规则应用于这一公式得到公式 [math]\displaystyle{ \psi }[/math] 后，仍然有 [math]\displaystyle{ \mathfrak{I}\vDash\psi }[/math] ，则称这一推理规则为保存重言性(tautology-preserving)的/保存有效性(validity-preserving)的。
注：一般来说，命题逻辑的重言式用保存重言性，谓词逻辑的有效式用保存有效性。进行同一研究时经常不区分。
性质
- 只有模型上的重言或有效被保证，不保证局部赋值的满足。即对于不满足的模型下的部分赋值不做要求，若 [math]\displaystyle{ \mathfrac{I}\nvDash\phi }[/math] ，哪怕有某个其上的赋值满足 [math]\displaystyle{ \sigma\vDash\psi }[/math] ，也不要求其满足 [math]\displaystyle{ \sigma\nvDash\psi }[/math] 。
意义
保存重言性描述语法上的变形规则，在语义上对应的性质。一个规则保存真实性说明了对这一规则形式下的可演绎关系 [math]\displaystyle{ \phi\vdash\psi }[/math] ，保证在同一模型下语义上还是有效式。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |