I have the following formula that I am trying to prove is valid:

$$\exists x \forall y q(x,y) \rightarrow \forall y \exists x q(x,y)$$

By following the Skolemization algorithm in the book "Mathematical Logic for Computer Science" by Mordechai Ben-Ari, I get the following:

$$\neg (\exists x \forall y q(x,y) \rightarrow \forall y \exists x q(x,y)) \qquad \qquad \text{Negated formula}$$ $$\neg (\exists x \forall y q(x,y) \rightarrow \forall w \exists z q(z,w)) \qquad \qquad \text{Rename bound variables}$$ $$\neg (\neg \exists x \forall y q(x,y) \lor \forall w \exists z q(z,w)) \qquad \qquad \text{Eliminate boolean operators}$$ $$\exists x \forall y q(x,y) \land \exists w \forall z \neg q(z,w) \qquad \qquad \text{Push negation inwards}$$ $$\exists x \forall y \exists w \forall z (q(x,y) \land \neg q(z,w)) \qquad \qquad \text{Extract quantifiers}$$ $$\text{(no change)} \qquad \qquad \text{Distribute matrix}$$ $$\forall y \forall z (q(a,y) \land \neg q(z,f(y))) \qquad \qquad \text{Replace existential quantifiers}$$

I'm not sure how to reach the empty clause from here. I'd appreciate a hint.


When you extract the quantifiers, pull out the $\exists w$ before you pull out the $\forall y$... that'll eliminate the dependency of $w$ on $y$

That is, you get:

$\exists x \forall y \ q(x,y) \land \exists w \forall z \ \neg q(z,w) \Leftrightarrow$

$\exists x (\forall y \ q(x,y) \land \exists w \forall z \ \neg q(z,w)) \Leftrightarrow$

$\exists x \exists w (\forall y \ q(x,y) \land \forall z \ \neg \ q(z,w)) \Leftrightarrow$

$\exists x \exists w \forall y (q(x,y) \land \forall z \ \neg q(z,w) \Leftrightarrow$

$\exists x \exists w \forall y \forall z (q(x,y) \land \neg q(z,w))$

Skolemizing now gets you:

$\forall y \forall z (q(a,y) \land \neg q(z,b))$

Thus clauses $\{q(a,y)\}$ and $\{\neg q(z,b)\}$

And by substituting $a$ for $z$ and $b$ for $y$ these can be resolved to the empty clause.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.