Hello people I have a simple question. I have this formula from which I need to remove all the implications. Here it is.
$\forall x ( [ Roman(x) \wedge know ( x, Marcus )] \rightarrow [ hate (x, Caesar ) \vee ( \forall y \exists z hate(y,z) \rightarrow thinkcrazy(x,y)) ])$
And here is the answer.
$\forall x \neg [Roman(x) \wedge know (x, Marcus)] \vee [ hate(x,Caesar) \vee (\forall y \neg \exists z hate(y,z) \vee thinkcrazy(x,y))]$
Then thing I can't understand is, why isn't the second universal quantificator negated (the one for y)? When do you do a negation on the quantifier ?
You have to remove the implication connective from :
Starting from the rightmost one, you have correctly used the equivalence between $p \rightarrow q$ and $\lnot p \lor q$.
But we have a problem with some missing parentheses; if we assume that the subformula is :
$∀y(∃zhate(y,z) \rightarrow thinkcrazy(x,y))$
then we can rewrite it as :
But this is an assumption [please, note that the "standard" convention is that the quantifiers apply to as little as possible]; if instead we "read" the subformula with a "narrow" scope for the universal quantifier, we must have instead :
$\lnot ∀y∃zhate(y,z) \lor thinkcrazy(x,y))$.
Going on with the first interpretation, we proceed in the same way, for the leftmost $\rightarrow$, obtaining :
Conclusion
You have to check for the correct formula.