前束范式

维基百科,自由的百科全书
跳到导航 跳到搜索

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

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

進一步推論可得:(可透過改寫 推論得出)

它们的存在对偶

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

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

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