查看“︁保存重言性”︁的源代码

[[分类:证明论]]{{DEFAULTSORT:bao3cun2chong2yan2xing4}}
{{#seo:
|keywords=推理规则, 保存重言性
|description=证明论中，描述推理规则的性质时，如果一个公式在所有赋值下成立，进行相应规则的变形后仍然在所有赋值下成立，称其保存重言性或保存有效性。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-03
}}
{{InfoBox
|name=保存重言性
|eng_name=tautology-preserving
|aliases=保存有效性,validity-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> ，保证在同一模型下语义上还是有效式。


{{证明论}}