易字变形

易字变形
术语名称	易字变形
英语名称

易字变形指对一个谓词公式，其中的部分作为子公式的量化公式被替换成其易字式。 两个公式互为易字变形意味着两公式间可通过多次易字互相转换，过程中保持语义性质不变。这是一种等价关系。

定义

简单易字变形

对谓词公式 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \phi' }[/math] ，若存在公式 [math]\displaystyle{ \psi }[/math] 、原子公式 [math]\displaystyle{ p }[/math] 、互为易字式的两个量化公式 [math]\displaystyle{ \psi,\psi' }[/math] ，使得 [math]\displaystyle{ \phi=\chi[\psi/p],\phi'=\chi'[\psi'/p] }[/math] ，则称 [math]\displaystyle{ \phi,\phi' }[/math] 互为简单易字变形。

易字变形

定义两谓词公式间的易字变形关系为简单易字变形关系的等价闭包：

1. [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \phi }[/math] 本身的易字变形。
2. [math]\displaystyle{ \phi' }[/math] 是 [math]\displaystyle{ \phi }[/math] 的易字变形， [math]\displaystyle{ \phi'' }[/math] 是 [math]\displaystyle{ \phi' }[/math] 的简单易字变形，则 [math]\displaystyle{ \phi'' }[/math] 是 [math]\displaystyle{ \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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理