等项替换
| 等项替换 | |
|---|---|
| 术语名称 | 等项替换 |
| 英语名称 | |
等项替换指在任何谓词公式中，如果两个项相等，就能互相替换。 这里项的相等指两个项在给定条件下的任意赋值下都相等，而且替换要求它们之间可自由代入。
定义
对公式 [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] 的满足也成立。