查看“︁个体变项代入”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=代入
|eng_name=subtitution
}}
对[[个体词（谓词逻辑）|个体变项]]的'''代入'''('''subtitution''')指在一个[[项（谓词逻辑）|项]]或一个[[谓词公式]]中，将某个个体变项的全体出现，全部用另一个项来替换的操作。

== 定义 ==

=== 代入 ===

从全体个体项所构成的集合到全体项所构成的集合的映射，称为一个'''代入'''('''substitution''')。

对于把 <math>x_1, \dots, x_n</math> 分别替换为 <math>t_1, \dots, t_n</math> 的代入，也记作 <math>t_1/x_1, \dots, t_n/x_n</math> 。

注：特别地，映射可以将部分个体项投影到其自身，即映射 <math>u</math> 允许存在某个 <math>t_i=u(x_i)=x_i</math> 。

=== 项的代入 ===

对任意项 <math>s</math> 和代入 <math>u</math> ，递归地定义项 <math>s</math> 做代入 <math>u</math> 的结果 <math>s(u)</math> 为：
# 若 <math>s</math> 是个体常项 <math>c</math> ，则 <math>s(u)=c</math> 。
# 若 <math>s</math> 是个体变项 <math>x</math> ，则 <math>s(u)=u(x)</math> 。
# 若 <math>s</math> 是 <math>f(s_1, \dots, s_n)</math> ，则 <math>s(u)=f(s_1(u), \dots, s_n(u))</math> 。

<math>s(u)</math> 也记作 <math>s[t_1/x_1, \cdots, t_n/x_n]</math> 。

=== 公式的代入 ===

对任意公式 <math>\phi</math> 和代入 <math>u</math> ，递归地定义公式 <math>\phi</math> 做代入 <math>u</math> 的结果 <math>\phi(u)</math> 为：
# 若 <math>\phi</math> 是 <math>P(s_1, \dots, s_n)</math> ，则 <math>\phi(u)=P(s_1(u), \dots, s_n(u))</math> 。
# 若 <math>\phi</math> 是 <math>\lnot\psi</math> ，则 <math>\phi(u)=\lnot(\psi(u))</math> 。
# 若 <math>\phi</math> 是 <math>\phi\odot\chi, \odot\in C_2</math> ，则 <math>\phi(u)=\psi(u) \odot \chi(u)</math> 。
# 若 <math>\phi</math> 是 <math>\mathsf{Q}x \psi, \mathsf{Q} \in \{\forall, \exists\}</math> ，则 <math>\phi(u)=\mathsf{Q}x \psi(u^{-x})</math> 。
其中 <math>u^{-x}</math> 是 <math>u</math> 中将 <math>x</math> 改为映射到 <math>x</math> 的结果。

<math>\phi(u)</math> 也记作 <math>\phi[t_1/x_1, \cdots, t_n/x_n]</math> 。


{{谓词逻辑}}