易字式

易字式
术语名称	易字式
英语名称

量化公式中，将被量化的个体变元及其辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其易字式，操作称为易字变形。

定义

对量化公式 [math]\displaystyle{ \forall x\phi }[/math] 和 [math]\displaystyle{ \exists x\phi }[/math] ，个体变元 [math]\displaystyle{ y }[/math] 不在其中自由出现，且对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/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] 的易字式。

性质

谓词公式的易字式和原公式逻辑等值。

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