# 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