易字

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

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

意义及举例

如公式 [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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理