前束范式在谓词演算中,如果一个公示可以被写为量词在前,随后是被称为母体的无量词部分,则称其为前束范式的,所有经典逻辑公式都逻辑等价于某个前束范式公式。 可以用公式在如下重写规则下的逻辑等价来证实: ∀ 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)所必需。 前束范式是哥德尔证明他的哥德尔完备性定理的主要工具。