# Conversion from FOL to CNF

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!

• To get proper spacing around $\land$ in the last equation where the first operand is missing in the second line, you can add a dummy first operand {}. Apr 3, 2023 at 8:20

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