前束范式

前束范式
术语名称	前束范式
英语名称	prenex normal form
别名	PNF

谓词公式可以表示为逻辑等值的标准形式。 全部量词都是常见量词，全部量化表达式都在最前，且量词均非否定、无取值范围、辖域覆盖到公式尾部，称为前束范式(prenex normal form, PNF)。 前束范式是谓词公式的重要的标准形式。

定义

首标
术语名称	首标
英语名称	prefix

基式
术语名称	基式
英语名称	matrix
别名	母式

对谓词公式，若其具有形式 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi }[/math] ，其中 [math]\displaystyle{ \phi }[/math] 不含量词，量词 [math]\displaystyle{ \mathsf{Q}_i \in \{\forall, \exists \} }[/math] 且每个约束变项 [math]\displaystyle{ x_i }[/math] 均有在 [math]\displaystyle{ \phi }[/math] 中的出现，则称其为一个前束范式(prenex normal form, PNF)。其中 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n }[/math] 称为首标(prefix)， [math]\displaystyle{ \phi }[/math] 称为母式/基式(matrix)。

对谓词公式 [math]\displaystyle{ \psi }[/math] ，若有一前束范式与其逻辑等值，则称其为公式 [math]\displaystyle{ \psi }[/math] 的一个前束范式。

注：有的定义不要求约束变项均有在基式中出现。

形式语言定义

前束范式构成的集合是谓词语言的子集，但合法前束范式要求约束变项与基式间的关系，是上下文有关文法。

性质

• 前束范式存在定理(prenex normal form theorem)：对每个公式 [math]\displaystyle{ \psi }[/math] ，都存在一个前束范式 [math]\displaystyle{ \phi }[/math] 与其逻辑等值。

转换算法

任意谓词公式都能通过以下步骤转换为前束范式。

1. 将非常用量词通过常用量词表达：仅通过 [math]\displaystyle{ \exists,\forall }[/math] 表达。
2. 消去非基本逻辑联结词（主要指蕴涵 [math]\displaystyle{ \rightarrow }[/math] 和等价 [math]\displaystyle{ \leftrightarrow }[/math] ）：将其他逻辑联结词替换为仅含 [math]\displaystyle{ \lnot,\land,\lor }[/math] 的表达方式。
3. 深化否定词到否定表达式：使用德·摩根律将限定对象不是原子公式的否定符号移到原子公式前。包括析取、合取、存在量词、全称量词外的否定符号均被移到内部，经此步骤后，否定词仅能作用于原子公式。
4. 检查各量词所作用的变项是否有重复，若存在，需要进行易字避免冲突。
5. 量词前移，使每个量词的辖域均覆盖全公式。

例子

• [math]\displaystyle{ \forall x \exists y \forall z (p(x, y) \land \lnot r(z)) }[/math]
• [math]\displaystyle{ \forall x \exists y \forall z p(x, y, z) }[/math] （基式是一个原子，不需要逻辑联结词）
• 若允许零元谓词， [math]\displaystyle{ p \land q }[/math] （基式中全部谓词都是零元谓词，没出现个体变项，就不需要量化表达式）

反例：

• [math]\displaystyle{ \lnot \forall x \exists y \forall z (p(x, y) \land \lnot r(z)) }[/math] ：其中第一个否定词作用的不是原子公式，应当放到原子公式前，即 [math]\displaystyle{ \exists x \forall y \exists z (\lnot p(x,y) \lor r(z)) }[/math] 。
• [math]\displaystyle{ \forall x \exists y (p(x, y) \land \forall z r(z)) }[/math] ：量化表达式 [math]\displaystyle{ \forall z }[/math] 未提前，需要将其和 [math]\displaystyle{ \forall x \exists y }[/math] 放在一起。另外，由于 [math]\displaystyle{ x,y }[/math] 出现在同一个原子公式中，而 [math]\displaystyle{ z }[/math] 出现在另一个里，此处 [math]\displaystyle{ \forall x \exists y }[/math] 之间存在固定顺序，而 [math]\displaystyle{ \forall z }[/math] 和这两个表达式的顺序不影响，可以放在这两个表达式的前面、中间或后面。
• [math]\displaystyle{ \exists x p(x) \land \forall x q(x) }[/math] ：也是未提前，但是由于同时出现了 [math]\displaystyle{ x }[/math] ，需要将一个进行易字处理，如 [math]\displaystyle{ \exists x \forall 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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理