埃尔布朗定理

在逻辑学中，埃尔布朗定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系，因此埃尔布朗定理可能是一种已知的确定手段来判断一个命题的命题逻辑计算是否是有限的，对于一个含有复杂谓词的公式，它的谓词逻辑计算也起到同样的判断。通过对埃尔布朗定理的应用，部分解决回答了上述问题。但是虽然有Gödel(哥德尔)，Tarski(塔尔斯基)，Church(邱奇)，Turing(图灵)和其他科学家在逻辑学领域中卓越的研究成果，但是至今不存在一个算法，能够决定一个普遍公式的谓词逻辑计算是否是可计算的这样一个问题，我们不知道这个算法是否是可以被证明的。

在谓词演算中，一个公式是前束范式的，如果它可以被写为量词在前，随后是被称为矩阵的非量化部分的字符串。所有一阶公式都逻辑等价于某个前束范式公式。

可以用公式在如下重写规则下的逻辑等价来证实：

${\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}$ 中是自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。