# Prove formula using skolemization and resolution

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.