查看“︁易字”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=易字
|eng_name=
}}
[[量词|量化公式]]中，将被量化的个体变元及辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其'''易字式'''，操作称为'''易字变形'''。

== 定义 ==

对公式 <math>\forall x\phi</math> 和 <math>\exists x\phi</math> ，个体变元 <math>y</math> 不在其中自由出现，且对 <math>x</math> 在 <math>\phi</math> 中可自由代入，则
* 公式 <math>\forall y (\phi(y/x))</math> 称为公式 <math>\forall x \phi</math> 的易字式；
* 公式 <math>\exists y (\phi(y/x))</math> 称为公式 <math>\exists x \phi</math> 的易字式。


{{谓词逻辑}}