(4)、消去存在量词。若存在量词不在全称量 词的辖域内,则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量;若该存在量词在一个或多个全称 量词的辖域内,则用这些全称量词指导变元的 个函数替换该存在量词约束的变元。这样的 函数称为 Skolem函数。 例如∨x1Vx2xn3yP(x1x2,xny)中y可用 Skolem函数f ,xn)替换为x1Vx2 VX,P(XI xn, f(x1,x,,.,n)（4）、消去存在量词。若存在量词不在全称量 词的辖域内，则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量；若该存在量词在一个或多个全称 量词的辖域内，则用这些全称量词指导变元的 一个函数替换该存在量词约束的变元。这样的 函数称为Skolem函数。 例如x1 x2 • • •xnyP(x1 ,x2 ,…, xn ,y)中y可用 Skolem函数f(x1 ,x2 ,…, xn )替换为x1 x2 • • • xnP(x1 ,x2 ,…, xn ,f(x1 ,x2 ,…, xn ))