前束范式

前束范式（prenex normal form）是数理逻辑中使用谓词逻辑所描述的形式语言的一种格式。

前束范式定义

前束范式亦称前束式，一种谓词演算公式。指其一切量词都未被否定地处于公式的最前端且其辖域都延伸至公式的末端的谓词演算公式。设Q∈{∃，ᗄ}，一个公式α是前束范式，当且仅当存在一个不含量词的公式β，使得

α=(Q₁x₁)(Q₂x₂)…(Qₑxₑ)β.

例如，公式(ᗄx)为一个前束范式，而(ᗄx)→(∃y)R(y)不是前束范式，与一个谓词演算公式等价的前束范式公式称为谓词演算公式的前束范式，例如，公式p→(ᗄx)α(x)的前束范式为(ᗄx)，此处p为一个命题变元，其所有存在量词都在全称量词的前面出现的前束范式称为斯科朗范式，又称∃前束范式，一个公式α是斯科朗范式，当且仅当存在一个不含量词的公式β，使得

α=(∃x₁)(∃x₃)…(∃xₐ)(ᗄx₁) ·(ᗄx₂)…(ᗄxₑ)β(a≥0,e≥0).

一个公式，如果量词均在全式的开头，它们的作用域延伸到整个公式的末端，则该公式叫做前束范式(Prenex Normal Form)。

前束范式可记为下述形式

例如，

定义 设P是具有形式

利用换名规则、代替规则、量词的否定公式及量词辖域的扩张与收缩公式等，可以将任一谓词公式化成前束范式。

前束范式定理

任何一个谓词公式，均和一个前束范式等价。

证明 首先利用量词转化公式，把否定深入到命题变元和谓词填式的前面，其次，利用

前束范式求前束范式的过程

求一个谓词公式的前束范式的过程为：

(1)通过利用公式

(2)消去

(3)否定深入，即利用量词转化公式把否定联结词深入到命题变元和谓词填式的前面；

(4)运用换名规则和代替规则，将公式中所有变元均用不同的符号；

(5)量词前移，即利用量词辖域的扩张把量词移到前面。

前束范式例题解析

求下列公式的前束范式：

（1）

或者

（1）中可以看出一个公式的前束范式不是唯一的。

（2）