前束范式

每一谓词表达式，通过等值变换，可以将式中的量词逐步前移，最后将表达式中的一切量词都未被否定地置于公式的最前方，并且它们的辖域都延伸至公式的末端，则成为该表达式的前束范式。 例如，∨λF(_x∨乛G(_x)),∨_x∃y (R(_xy)→R(_y,x))。 一公式的前束范式不是唯一的。这种范式的优点在于：当对谓词演算作一般性的研究时，在量词以后的整个表这式可以当作命题演算中的复合命题处理。还可以对前束范式作进一步变换，使其中没有自由变项，又至少有一存在量词，并且所有存在量词都位于全称量词之前，则称此范式为∃-前束范式，又称斯科伦范式。例如，∃_x∨_y(G(x,y)→H(x,y)),∃_x∃_y∨λ(H(x,_y)→F(_x,y)每一谓词表达式都有—∃前束范式，两者可以互推，即一个表达式是普遍有效的，当且仪当它的∃-前束范式是普遍有效的。