4
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ Second formula : the "central" $\land$ must be $\lor$. $\endgroup$ – Mauro ALLEGRANZA Nov 6 '18 at 15:55
  • 2
    $\begingroup$ It is better to start from the outer negation : $\lnot βˆ€π‘₯βˆƒπ‘¦ \lnot$ is $βˆƒπ‘₯βˆ€π‘¦$. $\endgroup$ – Mauro ALLEGRANZA Nov 6 '18 at 15:56
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ @xyz - Are you able to skolemize? Or would you prefer that I complete my answer adding the part about skolemization and distribution? $\endgroup$ – Taroccoesbrocco Nov 6 '18 at 16:44
  • $\begingroup$ Would this be the solution? (¬P(y,X)∨R(X,T(y))∨S(V(y)))∨(Q(y)∨R(X,T(y))∨S(V(y))) $\endgroup$ – xyz Nov 6 '18 at 17:03
  • $\begingroup$ @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)))$. $\endgroup$ – Taroccoesbrocco Nov 6 '18 at 17:14

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.