查看“︁前束范式”︁的源代码

在[[谓词演算]]中，如果一个公式可以被写为[[量词]]在前，被称为母体的无量词部分在后的形式，则称其为'''前束[[范式]]'''的，所有[[经典逻辑]]公式都[[逻辑等价]]于某个前束范式公式。

可以用公式在如下重写规则下的逻辑等价来证实：
:<math>\forall x ( P(x) ) \land Q \equiv \forall x ( P(x) \land Q )</math>
:<math>\forall x ( P(x) ) \lor Q \equiv \forall x ( P(x) \lor Q )</math>
:<math>\exists x ( P(x) ) \land Q \equiv \exists x ( P(x) \land Q )</math>
:<math>\exists x ( P(x) ) \lor Q \equiv \exists x ( P(x) \lor Q )</math>

進一步推論可得：(可透過改寫 <math>P \rightarrow Q</math> 為 <math>\lnot P \lor Q</math> 推論得出)
:<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> 中是非自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。

某些证明演算只处理公式写为前束范式的理论。本概念為研究[[算数阶层]]和{{le|分析階層|Analytical hierarchy}}所必需。

前束范式是[[哥德尔]]证明他的[[哥德尔完备性定理]]的主要工具。

[[Category:數理邏輯|Q]]
[[Category:模型论]]