# Conversion to Clausal Form

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?

• Second formula : the "central" $\land$ must be $\lor$. Nov 6 '18 at 15:55
• It is better to start from the outer negation : $\lnot ∀𝑥∃𝑦 \lnot$ is $∃𝑥∀𝑦$. Nov 6 '18 at 15:56

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)$$.
• @xyz - Almost. You skolemized correctly but you distributed in a wrong way. Your final formula should be (I prefer to use lower letters for constants and function symbols) $(\lnot P(y,c) \lor \lnot Q(y) \lor R(c,t(y)) \land (\lnot P(y,c) \lor \lnot Q(y) \lor S(v(y)))$. Nov 6 '18 at 17:14