一阶逻辑前束范式

定义 设 $A$ 为一个一阶逻辑公式, 若 $A$ 为 $Q_1{x}_1...Q_k{x}_{k}B$ 的形式, 其中 $Q_i$ 为 $\forall$ 或 $\exists$, $B$ 为不含两次的公式, 则称 $A$ 为前束范式.

定理 一阶逻辑中的任何公式都存在与之等值的前束范式.