赫爾不蘭特定理

在謂詞演算中，一個公式是前束範式的，如果它可以被寫為量詞在前，隨後是被稱為矩陣的非量化部分的字元串。所有一階公式都邏輯等價於某個前束範式公式。

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

它們的存在對偶：

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