易字变形

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

易字变形指一个谓词公式，其中的部分量化公式被替换成其易字式。

定义

简单易字变形

对谓词公式 [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\lt math\gt 本身的易字变形。 # \lt math\gt \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]）
谓词公式	解释/模型、赋值
	分类	普遍有效公式、可满足式、不可满足式
	范式	前束范式、Skolem 范式