等项替换：修订间差异

2026年1月8日 (四) 03:24的版本

等项替换
术语名称	等项替换
英语名称

等项替换指在任何谓词公式中，用两相等项进行替换的操作，以及这个操作保证逻辑等值的定理。

这里项的相等指两个项在给定条件下的任意赋值下都相等，或者说通过等词连接得到的是有效式；替换要求它们之间可自由代入。

定义

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

将赋值 [math]\displaystyle{ \sigma }[/math] 的满足改为一组前提 [math]\displaystyle{ \Gamma }[/math] 的满足也成立。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第10行： / 第10行： @@
 |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>\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> 的满足也成立。
+将赋值 <math>\sigma</math> 的满足改为一组前提 <math>\Gamma</math> 的满足也成立。
 {{谓词逻辑}}