命题变元代入
| 代入 | |
|---|---|
| 术语名称 | 代入 |
| 英语名称 | subtitution |
对命题变元的代入(subtitution)指在一个命题公式（或谓词公式）中，将某个命题变元的全体出现，全部用另一个公式来替换的操作。
定义
代入
从全体命题变元所构成的集合到全体公式所构成的集合的映射，称为一个代入(substitution)。
对于把 [math]\displaystyle{ p_1, \dots, p_n }[/math] 分别替换为 [math]\displaystyle{ \phi_1, \dots, \phi_n }[/math] 的代入，也记作 [math]\displaystyle{ \phi_1/p_1, \dots, \phi_n/p_n }[/math] 。这一能用 [math]\displaystyle{ n }[/math] 个列出的情况称为有穷代入。
注：特别地，映射可以将部分个体变量投影到其自身，即映射 [math]\displaystyle{ s }[/math] 允许存在某个 [math]\displaystyle{ s(p_i)=p_i }[/math] 。
公式的代入
对任意公式 [math]\displaystyle{ \phi }[/math] 和代入 [math]\displaystyle{ s }[/math] ，递归地定义公式 [math]\displaystyle{ \phi }[/math] 做代入 [math]\displaystyle{ s }[/math] 的结果 [math]\displaystyle{ \phi(s) }[/math] 为：
- 若 [math]\displaystyle{ \phi }[/math] 是命题变元 [math]\displaystyle{ p }[/math] ，则 [math]\displaystyle{ \phi(s)=s(p) }[/math] 。
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \lnot\psi }[/math] ，则 [math]\displaystyle{ \phi(s)=\lnot(\psi(s)) }[/math] 。
- 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \psi\odot\chi, \circ\in C_2 }[/math] ，则 [math]\displaystyle{ \phi(s)=\psi(s) \odot \chi(s) }[/math] 。
[math]\displaystyle{ \psi(s) }[/math] 也记作 [math]\displaystyle{ \psi[\phi_1/p_1, \cdots, \phi_n/p_n] }[/math] 。