查看“︁等项替换”︁的源代码

[[分类:谓词逻辑]][[分类:推理理论]]{{DEFAULTSORT:deng3xiang4ti4huan4}}
{{#seo:
|keywords=等项替换
|description=本文介绍等项替换的定义、性质与转换方法，包括这种操作的特点及意义。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-15
}}
{{InfoBox
|name=等项替换
|eng_name=
}}
'''等项替换'''指在任何[[谓词公式]]中，如果两个项相等，就能互相替换。
这里项的相等指两个项在给定条件下的任意[[赋值（谓词逻辑）|赋值]]下都相等，或者说通过[[等词]]连接得到的是有效式；替换要求它们之间[[可自由代入（个体变项）|可自由代入]]。

== 定义 ==

对公式 <math>\phi</math> 若 <math>s_1 \dots s_n</math> 和 <math>t_1 \dots t_n</math> 两组，分别对 <math>x_1 \dots x_n</math> 在 <math>\psi</math> 中可自由代入，且对任意模型上的任意赋值，满足对每对 <math>s_i,t_i</math> 都有 <math>s_i^\sigma = t_i^\sigma</math> （即 <math>\sigma\vDash s_i=t_i</math>），此时有 <math>\phi[s_1/x_1, \dots, s_n/x_n] = \phi[t_1/x_1, \dots, t_n/x_n]</math> （即对任意 <math>\sigma</math> 有 <math>\sigma\vDash\phi[s_1/x_1, \dots, s_n/x_n]</math> 当且仅当 <math>\sigma\vDash\phi[t_1/x_1, \dots, t_n/x_n]</math> ，也即 <math>\vDash \phi[s_1/x_1, \dots, s_n/x_n] \leftrightarrow \phi[t_1/x_1, \dots, t_n/x_n]</math>），称为'''等项替换'''。

将赋值 <math>\sigma</math> 的满足对应到一组前提 <math>\Gamma</math> 的满足也成立。


{{谓词逻辑}}