前束范式

维基百科,自由的百科全书
跳转至: 导航搜索

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

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

\forall x ( P(x) ) \and Q \equiv \forall x ( P(x) \and Q )
\forall x ( P(x) ) \or Q \equiv \forall x ( P(x) \or Q )
\exists x ( P(x) ) \and Q \equiv \exists x ( P(x) \and Q )
\exists x ( P(x) ) \or Q \equiv \exists x ( P(x) \or Q )

進一步推論可得:(可透過改寫 P \rightarrow Q\lnot P \or Q 推論得出)

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

它们的存在对偶

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

这里的 xQ 中是非自由的,并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。

某些证明演算只处理公式写为前束范式的理论。对于开发算术层次分析层次这个观念是基本的。

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