个体变项代入

代入
术语名称	代入
英语名称	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{ t_i=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] 为：

1. 若 [math]\displaystyle{ s }[/math] 是个体常项 [math]\displaystyle{ c }[/math] ，则 [math]\displaystyle{ s(u)=c }[/math] 。
2. 若 [math]\displaystyle{ s }[/math] 是个体变项 [math]\displaystyle{ x }[/math] ，则 [math]\displaystyle{ s(u)=u(x) }[/math] 。
3. 若 [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{ s(u) }[/math] 也记作 [math]\displaystyle{ s[t_1/x_1, \cdots, t_n/x_n] }[/math] 。

公式的代入

对任意公式 [math]\displaystyle{ \phi }[/math] 和代入 [math]\displaystyle{ u }[/math] ，递归地定义公式 [math]\displaystyle{ \phi }[/math] 做代入 [math]\displaystyle{ u }[/math] 的结果 [math]\displaystyle{ \phi(u) }[/math] 为：

1. 若 [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] 。
2. 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \lnot\psi }[/math] ，则 [math]\displaystyle{ \phi(u)=\lnot(\psi(u)) }[/math] 。
3. 若 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \phi\odot\chi, \odot\in C_2 }[/math] ，则 [math]\displaystyle{ \phi(u)=\psi(u) \odot \chi(u) }[/math] 。
4. 若 [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] 的结果。

[math]\displaystyle{ \phi(u) }[/math] 也记作 [math]\displaystyle{ \phi[t_1/x_1, \cdots, t_n/x_n] }[/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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理