前束範式

在謂詞演算中，如果一個公式可以被寫為量詞在前，被稱為母體的無量詞部分在後的形式，則稱其為前束範式的，所有經典邏輯公式都邏輯等價於某個前束範式公式。

可以用公式在如下重寫規則下的邏輯等價來證實：

${\displaystyle \forall x(P(x))\land Q\equiv \forall x(P(x)\land Q)}$

${\displaystyle \forall x(P(x))\lor Q\equiv \forall x(P(x)\lor Q)}$

${\displaystyle \exists x(P(x))\land Q\equiv \exists x(P(x)\land Q)}$

${\displaystyle \exists x(P(x))\lor Q\equiv \exists x(P(x)\lor Q)}$

進一步推論可得：(可透過改寫 ${\displaystyle P\rightarrow Q}$ 為 ${\displaystyle \lnot P\lor Q}$ 推論得出)

${\displaystyle \forall x(P(x)\rightarrow Q)\equiv \exists xP(x)\rightarrow Q}$

${\displaystyle \forall x(P\rightarrow Q(x))\equiv P\rightarrow \forall xQ(x)}$

它們的存在對偶：

${\displaystyle \exists x(P(x)\rightarrow Q)\equiv \forall xP(x)\rightarrow Q}$

${\displaystyle \exists x(P\rightarrow Q(x))\equiv P\rightarrow \exists xQ(x)}$

這裡的 ${\displaystyle x}$ 在 ${\displaystyle Q}$ 中是非自由的，並注意通過這些規則的持續應用所有量詞都可以移動到公式的前面。

某些證明演算只處理公式寫為前束範式的理論。本概念為研究算數階層和分析階層（英語：Analytical hierarchy）所必需。

前束範式是哥德爾證明他的哥德爾完備性定理的主要工具。