易字式：修订间差异

2026年1月6日 (二) 15:59的最新版本

重定向到：

@@ 第1行： / 第1行： @@
-[[分类:谓词逻辑]]
+#重定向 [[易字]]
-{{InfoBox
+[[分类:谓词逻辑]]{{DEFAULTSORT:yi4zi4shi4}}
-|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> 的易字式。
-== 性质 ==
-谓词公式的易字式和原公式[[逻辑等值]]。
-{{谓词逻辑}}