可自由代入（个体变项）
| 可自由代入 | |
|---|---|
| 术语名称 | 可自由代入 |
| 英语名称 | |
一个个体变项的可自由代入指，对一个谓词公式，将其中某个个体变项的全部出现替换为另一个项时，不会影响其语义的代入。 实际上，影响语义的情况主要是指，新的项或其中某个个体变项，在代入后会落在某个作用在这一变项的量词的辖域内，导致这个个体变项的量化情况改变。
定义
对公式 [math]\displaystyle{ \phi }[/math] ，个体变项 [math]\displaystyle{ x }[/math] 和项 [math]\displaystyle{ t }[/math] ，若对 [math]\displaystyle{ t }[/math] 中的每一个个体变项 [math]\displaystyle{ y }[/math] ， 个体变项 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的每一个自由出现都不在 [math]\displaystyle{ \forall y }[/math] 或 [math]\displaystyle{ \exists y }[/math] 的辖域内，则称项 [math]\displaystyle{ t }[/math] 对个体变项 [math]\displaystyle{ x }[/math] 在公式 [math]\displaystyle{ \phi }[/math] 中可自由代入( [math]\displaystyle{ t }[/math] is free for [math]\displaystyle{ x }[/math] in [math]\displaystyle{ \varphi }[/math] <ref>https://math.stackexchange.com/q/2938727</math> )。
注：显然，以下几种情况一定都可自由代入。
- [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有自由出现。甚至，[math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有出现。
- [math]\displaystyle{ t }[/math] 中没有个体变项。
- [math]\displaystyle{ t }[/math] 中个体变项在 [math]\displaystyle{ \phi }[/math] 中没有对应的量化表达式。
- [math]\displaystyle{ t }[/math] 中的个体变项只有 [math]\displaystyle{ x }[/math] 。