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.
