易字
| 易字 | |
|---|---|
| 术语名称 | 易字 |
| 英语名称 | variable renaming |
| 别名 | 约束变项易字, 易名, 更名 |
量化公式中，将被量词约束的作用变项及辖域代入为同一个新的个体变项名称的操作，称为易字(variable renaming)。易字是一个语法上的等价变换，不影响公式的逻辑性质。经过易字的公式称为原公式的易字式，两者逻辑等值。
易字通常不作为单独操作提出，但为变形的严谨性，必须进行相关讨论。主要目的是描述对谓词公式进行语法上的变形，特别是涉及改变量词辖域的变形时，需要保证个体词之间互不相同，避免名称冲突导致个体词出现的约束情况改变、命题实际结构改变。
定义
对公式 [math]\displaystyle{ \forall x\phi }[/math] 和 [math]\displaystyle{ \exists x\phi }[/math] ，个体变项 [math]\displaystyle{ y }[/math] 不在其中自由出现，且 [math]\displaystyle{ y }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入，则记将 [math]\displaystyle{ \phi }[/math] 中的 [math]\displaystyle{ x }[/math] 代入为 [math]\displaystyle{ y }[/math] 的公式为 [math]\displaystyle{ \phi[y/x] }[/math] ，称 [math]\displaystyle{ \forall y (\phi[y/x]) }[/math] 为 [math]\displaystyle{ \forall x \phi }[/math] 的易字式、 [math]\displaystyle{ \exists y(\phi[y/x]) }[/math] 为 [math]\displaystyle{ \exists x \phi }[/math] 的易字式。从一个公式得到其易字式的操作称为易字(variable renaming)。
性质
- 易字不改变语义相关的性质，只是语法上改变谓词公式的形式。
- 易字改变部分语法性质。
- 特别是关于可自由代入相关的性质会受到易字的影响，为保证可自由代入，通常对不满足这一性质的公式进行适当的易字操作以将其转化为可自由代入的公式。
意义及举例
如公式 [math]\displaystyle{ \forall x p(x) \land \exists x q(x) }[/math] 中，两个量词的辖域没有重叠，本身不会引起问题；但是如果将其转换为前束范式，则需要更改其辖域，此时分步转换为 [math]\displaystyle{ \forall x (p(x) \land \exists x q(x)) }[/math] 之后是 [math]\displaystyle{ \forall x \exists x (p(x) \land q(x)) }[/math] 。这里存在一个问题，子公式从 [math]\displaystyle{ p(x) \land \exists x q(x) }[/math] 到 [math]\displaystyle{ \exists x (p(x) \land q(x)) }[/math] 的转换中更改了 [math]\displaystyle{ \exists x }[/math] 的辖域，导致其辖域中出现了本来是自由变量（子公式中）的 [math]\displaystyle{ x }[/math] ，改变了公式的结构。因此需要强制其名称不同，对其中某个子公式进行易字，得到如 [math]\displaystyle{ p(x) \land \exists y q(y) }[/math] ，并转换为 [math]\displaystyle{ \exists y (p(x)\land q(y)) }[/math] ，然后得到完整公式 [math]\displaystyle{ \forall x \exists y (p(x)\land q(y)) }[/math] 。