易字：修订间差异

2026年1月9日 (五) 12:07的最新版本

易字
术语名称	易字
英语名称	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] 。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第1行： / 第1行： @@
-[[分类:谓词逻辑]]
+[[分类:谓词逻辑]]{{DEFAULTSORT:yi4zi4}}
+{{#seo:
+|keywords=易字, 易字式, 易字变形
+|description=本文介绍量化公式的易字操作及其易字式的定义、性质与转换方法，包括这种操作的特点及意义。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-09
+}}
 {{InfoBox
 |name=易字
-|eng_name=
+|eng_name=variable renaming
+|aliases=约束变项易字,易名,更名
 }}
-[[量词|量化公式]]中，将被量化的个体变元及辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其'''易字式'''，操作称为'''易字变形'''。
+[[量化公式]]中，将被量词约束的作用变项及辖域[[个体变项代入|代入]]为同一个新的[[个体词（谓词逻辑）|个体变项]]名称的操作，称为'''易字'''('''variable renaming''')。易字是一个语法上的等价变换，不影响公式的逻辑性质。经过易字的公式称为原公式的'''易字式'''，两者[[逻辑等值]]。
+易字通常不作为单独操作提出，但为变形的严谨性，必须进行相关讨论。主要目的是描述对[[谓词公式]]进行语法上的变形，特别是涉及改变量词辖域的变形时，需要保证个体词之间互不相同，避免名称冲突导致个体词出现的约束情况改变、命题实际结构改变。
 == 定义 ==
-对公式 <math>\forall x\phi</math> 和 <math>\exists x\phi</math> ，个体变元 <math>y</math> 不在其中自由出现，且对 <math>x</math> 在 <math>\phi</math> 中可自由代入，则
+对公式 <math>\forall x\phi</math> 和 <math>\exists x\phi</math> ，个体变项 <math>y</math> 不在其中[[自由出现]]，且 <math>y</math> 对 <math>x</math> 在 <math>\phi</math> 中[[可自由代入（个体变项）|可自由代入]]，则记将 <math>\phi</math> 中的 <math>x</math> [[个体变项代入|代入]]为 <math>y</math> 的公式为 <math>\phi[y/x]</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> 的'''易字式'''。从一个公式得到其易字式的操作称为'''易字'''('''variable renaming''')。
-* 公式 <math>\forall y (\phi(y/x))</math> 称为公式 <math>\forall x \phi</math> 的易字式；
-* 公式 <math>\exists y (\phi(y/x))</math> 称为公式 <math>\exists x \phi</math> 的易字式。
+== 性质 ==
+* 易字不改变语义相关的性质，只是语法上改变谓词公式的形式。
+* 易字改变部分语法性质。
+** 特别是关于[[可自由代入（个体变项）|可自由代入]]相关的性质会受到易字的影响，为保证可自由代入，通常对不满足这一性质的公式进行适当的易字操作以将其转化为可自由代入的公式。
+== 意义及举例 ==
+如公式 <math>\forall x p(x) \land \exists x q(x)</math> 中，两个量词的辖域没有重叠，本身不会引起问题；但是如果将其转换为[[前束范式]]，则需要更改其辖域，此时分步转换为 <math>\forall x (p(x) \land \exists x q(x))</math> 之后是 <math>\forall x \exists x (p(x) \land q(x))</math> 。这里存在一个问题，子公式从 <math>p(x) \land \exists x q(x)</math> 到 <math>\exists x (p(x) \land q(x))</math> 的转换中更改了 <math>\exists x</math> 的辖域，导致其辖域中出现了本来是自由变量（子公式中）的 <math>x</math> ，改变了公式的结构。因此需要强制其名称不同，对其中某个子公式进行易字，得到如 <math>p(x) \land \exists y q(y)</math> ，并转换为 <math>\exists y (p(x)\land q(y))</math> ，然后得到完整公式 <math>\forall x \exists y (p(x)\land q(y))</math> 。
 {{谓词逻辑}}