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

[[分类:谓词逻辑]]{{DEFAULTSORT:yi4zi4}}
{{#seo:
|keywords=析取范式, 合取范式, 范式, DNF, CNF
|description=本文介绍析取范式（DNF）和合取范式（CNF）的定义、性质与转换方法，包括这两种范式作为命题公式标准形式的概念，其结构特点及其在逻辑化简和计算机科学中的重要性。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-09
}}
{{InfoBox
|name=易字
|eng_name=variable renaming
|aliases=易名,更名
}}
[[量化公式]]中，将被量词约束的作用变项及辖域中的所有出现，更换为同一个新的个体变项名称的操作称为'''易字变形'''，简称'''易字'''('''variable renaming''')。易字是一个语法上的等价变换，不影响公式的逻辑性质。经过易字的公式称为原公式的'''易字式'''。

易字通常不作为单独操作提出，其主要目的是在描述如何对[[谓词公式]]进行语法上的变形时，特别是涉及改变量词辖域时，需要保证个体词之间互不相同，避免名称冲突改变个体词出现时受到约束，导致实际结构发生改变的情况。

如公式 <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> 。

== 定义 ==

对公式 <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>\phi(y/x)</math> 或 <math>\phi\{x\mapsto y\}</math> 等记号。从一个公式得到其易字式的操作称为'''易字变形'''，简称'''易字'''('''variable renaming''')。易字式可以按照如下规则递归定义在谓词公式上：

* 对项 <math>t</math> 如下定义 <math>t[y/x]</math> （严格地说，因为不是公式，项的易字操作结果不能叫做“易字式”，但是一般也没有“易字项”之类的名称）：
** 个体变项 <math>x</math> 进行易字操作的结果定义为 <math>x[y/x]=y</math> ；
** 对任意不是 <math>x</math> 的个体常项或个体变项 <math>z</math> 进行易字操作的结果定义为 <math>z[y/x]=z</math> ；
** 对 <math>f(t_1,\cdots,t_n)</math> 进行易字操作的结果定义为 <math>(f(t_1,\cdots,t_n))[y/x]=f(t_1[y/x],\cdots,t_n[y/x])</math> 。
* 对公式 <math>\phi</math> 定义 <math>\phi[y/x]</math> ：
** 原子公式 <math>p(t_1, \cdots t_n)</math> 的易字式定义为 <math>p(t_1[y/x], \cdots, t_n[y/x])</math> ；
** <math>(\lnot \phi)[y/x] = \lnot \phi[y/x]</math> ；
** <math>(\phi \cdot \psi)[y/x] = \phi[y/x] \cdot \psi[y/x]</math> ；
** <math>(\mathsf{Q} x \phi)[y/x]</math> 定义为 <math>\mathsf{Q} y (\phi[y/x])</math> 。


{{谓词逻辑}}