易字
| 易字 | |
|---|---|
| 术语名称 | 易字 |
| 英语名称 | |
量化公式中，将被量化的个体变元及辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其易字式，操作称为易字变形。
定义
对公式 [math]\displaystyle{ \forall x\phi }[/math] 和 [math]\displaystyle{ \exists x\phi }[/math] ，个体变元 [math]\displaystyle{ y }[/math] 不在其中自由出现，且对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/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] 的易字式。