To clarify, I am a newbie to this and am just doing some practice problems out of a text. Just looking for some clarification.
The question is to convert $$\forall x \ \text{person}(x) \land [\exists z \ \text{petOf}(x,z) \land \forall y \ \text{petOf}(x,y) \implies \text{dog}(y)] \implies \text{doglover}(x)$$ from FOL to CNF. So far, I have this:
First, eliminate the outermost implication:
$$\forall x \ \neg [\text{person}(x) \land [\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y) \implies \text{dog}(y)]] \lor \text{doglover}(x)$$
Then, eliminate the innermost implication:
$$\forall x \ \neg [\text{person}(x) \land [\neg[\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y)] \lor \text{dog}(y)]] \lor \text{doglover}(x)$$
Now, we can move the negations inwards starting with the innermost terms:
$$\forall x \ \neg [\text{person}(x) \land [\forall z \ \neg \text{petOf}(x, z) \lor \exists y \ \neg \text{petOf}(x, y) \lor \text{dog}(y)]] \lor \text{doglover}(x)$$
Now for the outermost terms:
$$\forall x \ [\neg \text{person}(x) \lor [\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y) \land \neg \text{dog}(y)]] \lor \text{doglover}(x)$$
Now, we don't have to standardize variables since there are no repeats. Next, we can Skolemize existential variables as follows:
$$\forall x \ [\neg \text{person}(x) \lor [\text{petOf}(x, F(x)) \land \forall y \ \text{petOf}(x, y) \land \neg \text{dog}(y)]] \lor \text{doglover}(x)$$
Now, we can drop universal quantifiers:
$$[\neg \text{person}(x) \lor [\text{petOf}(x, F(x)) \land \text{petOf}(x, y) \land \neg \text{dog}(y)]] \lor \text{doglover}(x)$$
Finally, we can distribute $\land$ over $\lor$:
\begin{align*}
(\neg \text{person(x)} \lor \text{petOf}(x, F(x)) \lor \text{doglover}(x))
\land (\neg \text{person(x)} \lor \text{petOf}(x, y) \lor \text{doglover}(x)) \\ \land (\neg \text{person(x)} \lor \neg \text{dog}(y) \lor \text{doglover}(x))
\end{align*}
Some questions I have: when I eliminate the innermost implications, does the implication elimination apply to the whole clause $[\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y) \implies \text{dog}(y)]$ or just the $\forall y \ \text{petOf}(x, y) \implies \text{dog}(y)$? Second, did I correctly distribute? Is there a better process for doing this sort of problem, this got sort of messy and complicated.
Thanks for any help!
Best Answer
It’s not so much a question of what the implication elimination applies to, but what the operands of the implication actually are. If, like me, you’re not sure about the precedence conventions for logical operators, it might be worthwhile to use parentheses to disambiguate.
But in the case of $\exists z \ \text{petOf}(x,z) \land \forall y \ \text{petOf}(x,y) \implies \text{dog}(y)$ you don’t need parentheses or precedence conventions to conclude that you didn’t parse it correctly. You converted it to $\neg[\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y)] \lor \text{dog}(y)$, implying that you parsed it as $[\exists z \ \text{petOf}(x, z) \land \forall y \ \text{petOf}(x, y)] \implies \text{dog}(y)$. But that doesn’t make sense, because now the $y$ in $\text{dog}(y)$ is outside the scope of the universal quantifier for $y$. So the intended meaning must be $\exists z \ \text{petOf}(x, z) \land [\forall y \ \text{petOf}(x, y) \implies \text{dog}(y)]$ (which also makes sense contentwise – a person is a dog lover if they have at least one pet and all their pets are dogs).
You did apply the distribute law correctly.