前束范式
在谓词演算中，如果一个公式可以被写为量词在前，被称为母体的无量词部分在后的形式，则称其为前束范式的，所有经典逻辑公式都逻辑等价于某个前束范式公式。
可以用公式在如下重写规则下的逻辑等价来证实：
∀
x
(
P
(
x
)
)
∧
Q
≡
∀
x
(
P
(
x
)
∧
Q
)
{\displaystyle \forall x(P(x))\land Q\equiv \forall x(P(x)\land Q)}
∀
x
(
P
(
x
)
)
∨
Q
≡
∀
x
(
P
(
x
)
∨
Q
)
{\displaystyle \forall x(P(x))\lor Q\equiv \forall x(P(x)\lor Q)}
∃
x
(
P
(
x
)
)
∧
Q
≡
∃
x
(
P
(
x
)
∧
Q
)
{\displaystyle \exists x(P(x))\land Q\equiv \exists x(P(x)\land Q)}
∃
x
(
P
(
x
)
)
∨
Q
≡
∃
x
(
P
(
x
)
∨
Q
)
{\displaystyle \exists x(P(x))\lor Q\equiv \exists x(P(x)\lor Q)}
进一步推论可得：(可透过改写
P
→
Q
{\displaystyle P\rightarrow Q}
为
¬
P
∨
Q
{\displaystyle \lnot P\lor Q}
推论得出)
∀
x
(
P
(
x
)
→
Q
)
≡
∃
x
P
(
x
)
→
Q
{\displaystyle \forall x(P(x)\rightarrow Q)\equiv \exists xP(x)\rightarrow Q}
∀
x
(
P
→
Q
(
x
)
)
≡
P
→
∀
x
Q
(
x
)
{\displaystyle \forall x(P\rightarrow Q(x))\equiv P\rightarrow \forall xQ(x)}
它们的存在对偶：
∃
x
(
P
(
x
)
→
Q
)
≡
∀
x
P
(
x
)
→
Q
{\displaystyle \exists x(P(x)\rightarrow Q)\equiv \forall xP(x)\rightarrow Q}
∃
x
(
P
→
Q
(
x
)
)
≡
P
→
∃
x
Q
(
x
)
{\displaystyle \exists x(P\rightarrow Q(x))\equiv P\rightarrow \exists xQ(x)}
这里的
x
{\displaystyle x}
在
Q
{\displaystyle Q}
中是非自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。
某些证明演算只处理公式写为前束范式的理论。本概念为研究算数阶层和分析阶层（英语：Analytical hierarchy）所必需。
前束范式是哥德尔证明他的哥德尔完备性定理的主要工具。