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