埃爾布朗定理

在邏輯學中，埃爾布朗定理(Herbrand's theorem)建立了命題邏輯計算和謂詞邏輯計算之間的關係，因此埃爾布朗定理可能是一種已知的確定手段來判斷一個命題的命題邏輯計算是否是有限的，對於一個含有複雜謂詞的公式，它的謂詞邏輯計算也起到同樣的判斷。通過對埃爾布朗定理的應用，部分解決回答了上述問題。但是雖然有Gödel(哥德爾)，Tarski(塔爾斯基)，Church(邱奇)，Turing(圖靈)和其他科學家在邏輯學領域中卓越的研究成果，但是至今不存在一個算法，能夠決定一個普遍公式的謂詞邏輯計算是否是可計算的這樣一個問題，我們不知道這個算法是否是可以被證明的。

前束範式

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

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

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

$\forall x(P\rightarrow Q(x))\equiv P\rightarrow \forall xQ(x)$

它們的存在對偶：

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

$\exists x(P\rightarrow Q(x))\equiv P\rightarrow \exists xQ(x)$

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