上一页

ⓘ 前束范式




                                     

ⓘ 前束范式

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

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

∀ x P x) ∧ Q ≡ ∀ x P x ∧ Q) {\displaystyle \forall xPx)\land Q\equiv \forall xPx\land Q)} ∀ x P x) ∨ Q ≡ ∀ x P x ∨ Q) {\displaystyle \forall xPx)\lor Q\equiv \forall xPx\lor Q)} ∃ x P x) ∧ Q ≡ ∃ x P x ∧ Q) {\displaystyle \exists xPx)\land Q\equiv \exists xPx\land Q)} ∃ x P x) ∨ Q ≡ ∃ x P x ∨ Q) {\displaystyle \exists xPx)\lor Q\equiv \exists xPx\lor Q)}

進一步推論可得:可透過改寫 P → Q {\displaystyle P\rightarrow Q} 為 ¬ P ∨ Q {\displaystyle \lnot P\lor Q} 推論得出

∀ x P x → Q) ≡ ∃ x P x → Q {\displaystyle \forall xPx\rightarrow Q)\equiv \exists xPx\rightarrow Q} ∀ x P → Q x) ≡ P → ∀ x Q x {\displaystyle \forall xP\rightarrow Qx)\equiv P\rightarrow \forall xQx}

它们的存在对偶:

∃ x P x → Q) ≡ ∀ x P x → Q {\displaystyle \exists xPx\rightarrow Q)\equiv \forall xPx\rightarrow Q} ∃ x P → Q x) ≡ P → ∃ x Q x {\displaystyle \exists xP\rightarrow Qx)\equiv P\rightarrow \exists xQx}

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

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

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