可自由代入（个体变项）

可自由代入
术语名称	可自由代入
英语名称

在一个谓词公式中，一个项对一个个体变项可自由代入，指将公式中这个个体变项全部出现替换为这个项时，不会影响其语义。

不可自由代入的情况包括：这个项代入后，其中至少一个个体变项会落在作用在同名个体变项的量词辖域内，导致这个个体变项的量化情况改变。

定义

对公式 [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{ \phi }[/math] )。

含义

可自由代入意味着将这个公式中，这一个体变项的全部出现都代换成这个项，不会出现由于命名冲突导致语义改变的情况。 若不满足可自由代入的条件，意味着存在名称冲突，此时总是可以通过易字解决对应冲突。

因此，在其他涉及代入的讨论中，可以限制给定个体变项和给定项之间满足可自由代入关系，若出现不可自由代入的先进行易字以转化为这种情况，以简化讨论中对符号重复情况的限制。

例子

显然，以下几种情况一定都可自由代入。

1. [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有自由出现。甚至，[math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有出现。
2. [math]\displaystyle{ t }[/math] 中没有个体变项。
3. [math]\displaystyle{ t }[/math] 中个体变项在 [math]\displaystyle{ \phi }[/math] 中没有对应的量化表达式。
4. [math]\displaystyle{ t }[/math] 中的个体变项只有 [math]\displaystyle{ x }[/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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理