在命题逻辑里,每一公式都有与之等值的范式,范式是一种统一的表达形式。当研究一个公式的特点(如永真、永假)时,范式起着重要的作用。对谓词逻辑的公式来说也有范式,其中前束范式与原公式是等值的,而其他范式与原公式只有较弱的关系。

一、前束范式

  定义 说公式A是一个前束范式, 如果A中的一切量词都位于该公式的最左边(不含否定词)且这些量词的辖域都延伸到公式的末端。
  前束范式A的一般形式为
  (Q1x1)…(Qnxn) M (x1, …, xn)
  其中Qi为量词(i = 1, …, n), M称作公式A的母式(基式), M中不再有量词。
  定理 谓词逻辑的任一公式都可化为与之等值的前束范式, 但其前束范式并不唯一。
  我们并不一般性地证明这个定理(只是为了避免叙述上的不便),而是通过例子给出化前束范式的过程。

  前束范式要求公式中所有的量词都非否定的出现在公式的最前面,且它们的辖域都延伸至公式的最后,即前束范式从形式上可以分成首标和母式两部分(注意并不是分成了两个子公式,因为首标不能单独作为公式)。因为母式中不含量词,它实际上可以看成是一个命题逻辑的公式。同时,命题公式都可看成是前束范式的特殊情况。
  但是,前束范式还有不足之处,那就是它的首标比较杂乱,对全称量词和存在量词的排列未作规定。如果规定前束范式的首标中所有存在量词都在全称量词前面,则成为所谓的Skolem标准型。