前束范式

在谓词演算中，一个公式是前束范式的，如果它可以被写为量词在前，随后是被称为母体的无量词部分的字符串。所有经典逻辑公式都逻辑等价于某个前束范式公式。

可以用公式在如下重写规则下的逻辑等价来证实：

$\forall x ( P(x) ) \land Q \equiv \forall x ( P(x) \land Q )$

$\forall x ( P(x) ) \lor Q \equiv \forall x ( P(x) \lor Q )$

$\exists x ( P(x) ) \land Q \equiv \exists x ( P(x) \land Q )$

$\exists x ( P(x) ) \lor Q \equiv \exists x ( P(x) \lor Q )$

进一步推论可得：(可透过改写 $P \rightarrow Q$ 为 $\lnot P \lor Q$ 推论得出)

$\forall x ( P(x) \rightarrow Q ) \equiv \exists x P(x) \rightarrow Q$

$\forall x ( P \rightarrow Q(x) ) \equiv P \rightarrow \forall x Q(x)$

它们的存在对偶：

$\exists x ( P(x) \rightarrow Q ) \equiv \forall x P(x) \rightarrow Q$

$\exists x ( P \rightarrow Q(x) ) \equiv P \rightarrow \exists x Q(x)$

这里的 $x$ 在 $Q$ 中是非自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。

某些证明演算只处理公式写为前束范式的理论。对于开发算术层次和分析层次这个观念是基本的。

前束范式是哥德尔证明他的哥德尔完备定理的主要工具。