Conversion to Clausal Form

Question

I want to convert this formula to clausal form:
$\lnot \forall 𝑥 \exists 𝑦 \lnot((𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \to (\exists 𝑧 𝑅(𝑥,𝑧) \land ∃𝑧 𝑆(𝑧)))$

First I removed $\to$:

$\lnot \forall 𝑥 \exists 𝑦 \lnot(\lnot (𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \land (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧)))$

Then I wanted to reduce the scope of the negations:

$\lnot\forall 𝑥 \exists 𝑦 ((𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \land (∀𝑧\lnot 𝑅(𝑥,𝑧) \lor \forall 𝑧 \lnot 𝑆(𝑧)))$

Now my problem is, how can I eliminate the negation of the Quantifier $\lnot \forall 𝑥$?

Would $\exists 𝑥 \exists 𝑦 ((\lnot 𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \land (\forall 𝑧𝑅(𝑥,𝑧) \lor \forall 𝑧\lnot 𝑆(𝑧)))$ be the right solution?

Answer 1

As Mauro Allegranza said in his first comment, a first error is in your second formula: since $(A \to B) \equiv (\lnot A \lor B)$, your second formula should be \begin{align} \lnot \forall 𝑥 \exists 𝑦 \lnot(\lnot (𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \lor (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \end{align}

Concerning your question about $\lnot \forall x$, you have to consider that $\lnot \forall x A \equiv \exists x \lnot A$. Therefore, a correct conversion of your starting formula is the following: \begin{align} & \lnot \forall 𝑥 \exists 𝑦 \lnot((𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \to (\exists 𝑧 𝑅(𝑥,𝑧) \land ∃𝑧 𝑆(𝑧))) \\ \equiv \ &\lnot \forall 𝑥 \exists 𝑦 \lnot(\lnot (𝑃(𝑦, 𝑥) \land 𝑄(𝑦)) \lor (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \\ \equiv \ & \lnot \forall 𝑥 \exists 𝑦 \lnot(\lnot 𝑃(𝑦, 𝑥) \lor \lnot 𝑄(𝑦) \lor (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \\ \equiv \ & \exists 𝑥 \lnot \exists 𝑦 \lnot(\lnot 𝑃(𝑦, 𝑥) \lor \lnot 𝑄(𝑦) \lor (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \\ \equiv \ & \exists 𝑥 \forall 𝑦 \, \lnot \lnot(\lnot 𝑃(𝑦, 𝑥) \lor \lnot 𝑄(𝑦) \lor (∃𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \\ \equiv \ & \exists 𝑥 \forall 𝑦 \,(\lnot 𝑃(𝑦, 𝑥) \lor \lnot 𝑄(𝑦) \lor (\exists 𝑧 𝑅(𝑥,𝑧) \land \exists 𝑧 𝑆(𝑧))) \\ \equiv \ & \exists 𝑥 \forall 𝑦 \,(\lnot 𝑃(𝑦, 𝑥) \lor \lnot 𝑄(𝑦) \lor (\exists 𝑧 𝑅(𝑥,𝑧) \land \exists w 𝑆(w))) \\ \end{align}

Pay attention: according to Wikipedia's definition, the last formula is not a clausal form yet because of the existential quantifier in $\exists 𝑧 𝑅(𝑥,𝑧) \land \exists w 𝑆(w)$. To eliminate them (and the initial $\exists x$), you have to skolemize them. After skolemization, you have to (drop all universal quantifiers and) distribute $\lor$'s inwards over $\land$'s, i.e. repeatedly replace $A \lor ( B \land C )$ with $(A \lor B) \land (A \lor C)$.