前束范式

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

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

$\mathrm{\forall }x(P(x))\wedge Q\equiv \mathrm{\forall }x(P(x)\wedge Q)$

$\mathrm{\forall }x(P(x))\vee Q\equiv \mathrm{\forall }x(P(x)\vee Q)$

$\mathrm{\exists }x(P(x))\wedge Q\equiv \mathrm{\exists }x(P(x)\wedge Q)$

$\mathrm{\exists }x(P(x))\vee Q\equiv \mathrm{\exists }x(P(x)\vee Q)$

進一步推論可得：(可透過改寫 $P\to Q$ 為 $\mathrm{\neg }P\vee Q$ 推論得出)

$\mathrm{\forall }x(P(x)\to Q)\equiv \mathrm{\exists }xP(x)\to Q$

$\mathrm{\forall }x(P\to Q(x))\equiv P\to \mathrm{\forall }xQ(x)$

它们的存在对偶：

$\mathrm{\exists }x(P(x)\to Q)\equiv \mathrm{\forall }xP(x)\to Q$

$\mathrm{\exists }x(P\to Q(x))\equiv P\to \mathrm{\exists }xQ(x)$

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

某些证明演算只处理公式写为前束范式的理论。本概念為研究算数阶层和Template:Le所必需。

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