二、Skolem标准形 　　前束范式对前束量词没有次序要求，也没有其他要求。如果对前束范式进而要求所有存在量词都在全称量词之左，或是只保留全称量词而消去存在量词，便得Skolem标准形。不难想象，仍保持与原公式的等值性就不可能了，只能保持在某种意义下的等值关系。 　　1.前束范式 　　一个公式的前束范式或说Skolem标准形为 　　(x1)…(xi)(xi+1)…(xn) M (x1, …, xn) 　　即存在量词都在全称量词的左边, 且可保证至少有一个存在量词(i≥1), 其中M(x1, …, xn)中不再含有量词也无自由个体变项。 　　定理　谓词逻辑的任一公式A, 都可化成相应的前束范式, 并且A是普遍有效的当且仅当其前束范式是普遍有效的。 　　这定理是说对普遍有效的公式，它与其前束范式是等值的。而一般的公式与其$前束范式并不是等值的。自然仅当A是普遍有效的, 方使用前束范式。 　　2.Skolem标准形 　　另一种Skolem标准形是仅保留全称量词的前束形。 　　定理 谓词逻辑的任一公式A, 都可化成相应的Skolem标准形(只保留全称量词的前束形), 并且A是不可满足的当且仅当其Skolem标准形是不可满足的。 　　这定理是说对不可满足的公式，它与其Skolem标准形是等值的，而一般的公式与其Skolem标准形并不是等值的。自然仅当A是不可满足的方使用Skolem标准形。 　　消存在量词是将相应变元以函数代入，可这样来理解，如(x)(y)P(x, y)的Skolem标准形是(x)P(x, f(x))。因为(x)(y)P(x, y)的意思是对任一x，都有一个y使P(x, y)成立，那么这个y通常是依赖于x，可视作x的某个函数f(x)。从而有Skolem标准形(x)P(x, f(x)), 然而所能找到的y不必然是x的函数f, 于是(x)(y)P(x, y)与(x)P(x,f(x))不等值。 在{1, 2}域上 　　　(x)(y)P(x, y) 　　= P(1, 1)∨P(1, 2))∧(P(2, 1)∨P(2, 2)) 　　　(x)P(x, f (x)) 　　= P(1, f (1))∧P(2, f (2)) 　　两者明显的不等值，但在不可满足的意义下两者是一致的。 　　这种标准形，对使用归结法的定理证明来说是重要的。 　　这可讨论前束形(在所有的$的左边), 而且一个公式与它的前束形在可满足意义下是一致的。