个体变项代入
| 代入 | |
|---|---|
| 术语名称 | 代入 |
| 英语名称 | subtitution |
对个体变项的代入(subtitution)指在一个项或一个谓词公式中，将某个个体变项的全体出现，全部用另一个项来替换的操作。
定义
代入
从全体个体项所构成的集合到全体项所构成的集合的映射，称为一个代入(substitution)。
对于把 [math]\displaystyle{ x_1, \dots, x_n }[/math] 分别替换为 [math]\displaystyle{ t_1, \dots, t_n }[/math] 的代入，也记作 [math]\displaystyle{ t_1/x_1, \dots, t_n/x_n }[/math] 。
注：特别地，映射可以将部分个体项投影到其自身，即映射 [math]\displaystyle{ u }[/math] 允许存在某个 [math]\displaystyle{ u(x_i)=x_i }[/math] 。
项的代入
对任意项 [math]\displaystyle{ s }[/math] 和代入 [math]\displaystyle{ u }[/math] ，递归地定义项 [math]\displaystyle{ s }[/math] 做代入 [math]\displaystyle{ u }[/math] 的结果 [math]\displaystyle{ s(u) }[/math] 为：
- 若 [math]\displaystyle{ s }[/math] 是个体常项 [math]\displaystyle{ c }[/math] ，则 [math]\displaystyle{ s(u)=c }[/math] 。
- 若 [math]\displaystyle{ s }[/math] 是个体变项 [math]\displaystyle{ x }[/math] ，则 [math]\displaystyle{ s(u)=u(x) }[/math] 。
- 若 [math]\displaystyle{ s }[/math] 是 [math]\displaystyle{ f(s_1, \dots, s_n) }[/math] ，则 [math]\displaystyle{ s(u)=f(s_1(u), \dots, s_n(u)) }[/math] 。
公式的代入
对任意公式 [math]\displaystyle{ \phi }[/math] 和代入 [math]\displaystyle{ u }[/math] ，递归地定义公式 [math]\displaystyle{ \phi }[/math] 做代入 [math]\displaystyle{ u }[/math] 的结果 [math]\displaystyle{ \phi(u) }[/math] 为：
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ P(s_1, \dots, s_n) }[/math] ，则 [math]\displaystyle{ \phi(u)=P(s_1(u), \dots, s_n(u)) }[/math] 。
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \lnot\psi }[/math] ，则 [math]\displaystyle{ \phi(u)=\lnot(\psi(u)) }[/math] 。
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \phi\odot\chi, \odot\in C_2 }[/math] ，则 [math]\displaystyle{ \phi(u)=\psi(u) \odot \chi(u) }[/math] 。
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \mathsf{Q}x \psi, \mathsf{Q} \in \{\forall, \exists\} }[/math] ，则 [math]\displaystyle{ \phi(u)=\mathsf{Q}x \psi(u^{-x}) }[/math] 。
其中 [math]\displaystyle{ u^{-x} }[/math] 是 [math]\displaystyle{ u }[/math] 中将 [math]\displaystyle{ x }[/math] 改为映射到 [math]\displaystyle{ x }[/math] 的结果。