查看“︁可自由代入（个体变项）”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=可自由代入
|eng_name=
}}
在一个[[谓词公式]]中，一个[[项（谓词逻辑）|项]]对一个[[个体词（谓词逻辑）|个体变项]]'''可自由代入'''，指将公式中这个个体变项全部出现替换为这个项时，不会影响其语义。
可能影响语义的情况包括，这个项中某个个体变项在代入后，会落在某个作用在这一变项的量词辖域内，导致这个个体变项的量化情况改变。

== 定义 ==

对公式 <math>\phi</math> ，个体变项 <math>x</math> 和项 <math>t</math> ，若对 <math>t</math> 中的每一个个体变项 <math>y</math> ， 个体变项 <math>x</math> 在 <math>\phi</math> 中的每一个自由出现都不在 <math>\forall y</math> 或 <math>\exists y</math> 的辖域内，则称项 <math>t</math> 对个体变项 <math>x</math> 在公式 <math>\phi</math> 中可自由代入( <math>t</math> is free for <math>x</math> in <math>\varphi</math> <ref>https://math.stackexchange.com/q/2938727</ref> )。

注：显然，以下几种情况一定都可自由代入。
# <math>x</math> 在 <math>\phi</math> 中没有自由出现。甚至，<math>x</math> 在 <math>\phi</math> 中没有出现。
# <math>t</math> 中没有个体变项。
# <math>t</math> 中个体变项在 <math>\phi</math> 中没有对应的量化表达式。
# <math>t</math> 中的个体变项只有 <math>x</math> 。


{{谓词逻辑}}