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)$.