查看“︁命题变元代入”︁的源代码

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

== 定义 ==

=== 代入 ===

从全体命题变元所构成的集合到全体公式所构成的集合的映射，称为一个'''代入'''('''substitution''')。

对于把 <math>p_1, \dots, p_n</math> 分别替换为 <math>\phi_1, \dots, \phi_n</math> 的代入，也记作 <math>\phi_1/p_1, \dots, \phi_n/p_n</math> 。这一能用 <math>n</math> 个列出的情况称为'''有穷代入'''。

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

=== 公式的代入 ===

对任意公式 <math>\phi</math> 和代入 <math>s</math> ，递归地定义公式 <math>\phi</math> 做代入 <math>s</math> 的结果 <math>\phi(s)</math> 为：
# 若 <math>\phi</math> 是命题变元 <math>p</math> ，则 <math>\phi(s)=s(p)</math> 。
# 若 <math>\phi</math> 是 <math>\lnot\psi</math> ，则 <math>\phi(s)=\lnot(\psi(s))</math> 。
# 若 <math>\phi</math> 是 <math>\psi\odot\chi, \circ\in C_2</math> ，则 <math>\phi(s)=\psi(s) \odot \chi(s)</math> 。


{{谓词逻辑}}