查看“︁埃尔布朗定理”︁的源代码

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

==前束范式==

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

可以用公式在如下[[重写]]规则下的逻辑等价来证实：
:<math>\forall x ( P(x) \rightarrow Q ) \equiv \exists x P(x) \rightarrow Q</math>
:<math>\forall x ( P \rightarrow Q(x) ) \equiv P \rightarrow \forall x Q(x)</math>
它们的[[德·摩根定律|存在对偶]]：
:<math>\exists x ( P(x) \rightarrow Q ) \equiv \forall x P(x) \rightarrow Q</math>
:<math>\exists x ( P \rightarrow Q(x) ) \equiv P \rightarrow \exists x Q(x)</math>
这里的 <math>x</math> 在 <math>Q</math> 中是自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。

==定义==

==证明==

[[Category:数学定理|A]]