:\neg \exists xP\Leftrightarrow \forall x\neg P,\neg \forall xP\Leftrightarrow \exists x \neg P
\color...{red}{\Longleftrightarrow} \forall x(\exists y\neg P(x,y)\vee \exists y(Q(x,y)\wedge \neg R(x,y))) C....消去存在量词(两种情况)
a. 存在量词不出现在全称量词的辖域内 b....存在量词出现在一个或者多个全称量词的辖域内 对于一般情况: \forall x_1(\forall x_2(\cdots \forall x_n(\exists yP(x_1,x_2,\cdots ,x_n...,y)))\cdots) 存在量词 y 的 Skolem 函数为 y=f(x_1,x_2,\cdots ,x_n) Skolem 化:用 Slolem 函数代替每个存在量词化的变量的过程
如本例中两个存在量词