保存重言性：修订间差异

2026年1月23日 (五) 12:31的最新版本

保存重言性
术语名称	保存重言性
英语名称	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] ，保证在同一模型下语义上还是有效式。

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:bao3cun2chong2yan2xing4}}
+{{#seo:
+|keywords=推理规则, 保存重言性
+|description=证明论中，描述推理规则的性质时，如果一个公式在所有赋值下成立，进行相应规则的变形后仍然在所有赋值下成立，称其保存重言性或保存有效性。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-03
+}}
 {{InfoBox
 |name=保存重言性
 |eng_name=tautology-preserving
-|aliases=validity-preserving
+|aliases=保存有效性,validity-preserving
 }}
-'''保存重言性'''('''tautology-preserving''')指一个推理规则，应用于[[重言式]]时只能得到重言式。
+'''保存重言性'''('''tautology-preserving''')指一个推理规则，应用于[[重言式]]/[[有效式]]时只能得到重言式或有效式。表示一个推理规则中两个公式的[[可演绎]]关系保证每个模型上的满足关系。
+== 定义 ==
+对一个推理规则、[[谓词语言]]及该语言的一个[[结构（逻辑）|模型]] <math>\mathfrak{I}</math> ，对 <math>\mathfrak{I}\vDash\phi</math> 任意公式 <math>\phi</math> ，即对该模型上任意[[赋值（谓词逻辑）|赋值]] <math>\sigma = (\mathfrak{I}, A)</math> 均有 <math>\sigma\vDash\phi</math> ，将给定规则应用于这一公式得到公式 <math>\psi</math> 后，仍然有 <math>\mathfrak{I}\vDash\psi</math> ，则称这一推理规则为'''保存重言性'''('''tautology-preserving''')的/'''保存有效性'''('''validity-preserving''')的。
+注：一般来说，命题逻辑的重言式用保存重言性，谓词逻辑的有效式用保存有效性。进行同一研究时经常不区分。
+== 性质 ==
+* 只有模型上的重言或有效被保证，不保证局部赋值的满足。即对于不满足的模型下的部分赋值不做要求，若 <math>\mathfrac{I}\nvDash\phi</math> ，哪怕有某个其上的赋值满足 <math>\sigma\vDash\psi</math> ，也不要求其满足 <math>\sigma\nvDash\psi</math> 。
+== 意义 ==
-反过来说，如果应用于某一可假的公式，即使在某个[[真值表|赋值]]下是真命题，在这个赋值下对应的结果不一定是真命题；
+保存重言性描述语法上的变形规则，在语义上对应的性质。一个规则保存真实性说明了对这一规则形式下的可演绎关系 <math>\phi\vdash\psi</math> ，保证在同一模型下语义上还是有效式。
-只有原公式在任意赋值下都是真命题时，得到的结果才在任意赋值下都是真命题。
 {{证明论}}