Resolution in first order logic

Question

I have been reading an AI textbook and first order logic and here is a statement I encountered: Everyone who loves all animals is loved by someone. While the book writes this in FOL as:

$\forall x [\forall y Animal(y) \implies Loves(x,y)] \implies \exists x(Loves(y,x))$

my version is:

$\forall x[\forall y Loves(x,Animal(y))] \implies \exists x(Loves(y,x))$

Questions: are the two statements same? If yes, when i convert this to CNF, i get a statement like not(A) OR B. I am not sure how this can be converted to CNF.

Answer 1

The formula is wrongly "formalized".

"Everyone who loves all animals is loved by someone"

must be "unwind" as follows :

(i) "$x$ Loves all Animals", i.e. "all Animals are Loved by $x$" :

$\forall y[Animal(y) \rightarrow Loves(x,y)]$;

(ii) "this $x$ is Loved by someone" :

$\exists yLoves(y,x)$.

Putting the two together :

$\forall y[Animal(y) \rightarrow Loves(x,y)] \rightarrow \exists yLoves(y,x)$.

This $x$ is "generic"; i.e. we want to assert the formula for "every $x$"; thus we have to put an universal quantifier $\forall x$ in front of the entire formula :

$\forall x(\forall y[Animal(y) \rightarrow Loves(x,y)] \rightarrow \exists yLoves(y,x))$ --- (*).

---

This is not the same as :

$\forall x[\forall y Loves(x,Animal(y))] \rightarrow \exists x(Loves(y,x))$.

First of all, the formula is not well-formed : $Animal(y)$ is a predicate and not a term (i.e. a name"); thus, you cannot put it in an argument-place of another predicate like $Loves(x,y)$.

In any cases, some quantifiers have the wrong "scope". The first $\forall x$ does not bind the $x$ in $\exists x(Loves(y,x))$ and thus we are "losing" the link between "the everyone who loves all animals" and "the one which is loved by someone".

If we restore the correct scope of the initial $\forall x$ in $\exists x(Loves(y,x))$ we have to change the bound variable for the $\exists$ quantifier.

---

For Conjunctive Normal Form, we have to avoid using the same (bound) variable twice; thus, we rewrite (*) as :

$\forall x(\forall y[Animal(y) \rightarrow Loves(x,y)] \rightarrow \exists zLoves(z,x))$

then replace $P \rightarrow Q$ with $\lnot P \lor Q$ :

$\forall x(\lnot \forall y[\lnot Animal(y) \lor Loves(x,y)] \lor \exists zLoves(z,x))$

and then use the equivalence betwee $\lnot \forall$ and $\exists \lnot$ and De Morgan, to get :

$\forall x(\exists y[Animal(y) \land \lnot Loves(x,y)] \lor \exists zLoves(z,x))$

Finally we have to move $\exists$ quantifiers outwards :

$\forall x \exists y \exists z ([Animal(y) \land \lnot Loves(x,y)] \lor Loves(z,x))$.

Answer 2

I would suggest that, not the animal, but someone loves x, so:

$\forall x[\forall y Loves(x,Animal(y))] \implies \exists z(Loves(z,x))$

I'll let someone else wade in on conjunctive normal form.

Answer 3

Your formalization is not correct. (it is still good that you asked the question!)

$Animal$ is a (unary) predicate, so $Animal(y)$ represents a truthvalue. So the formula $Loves(x,Animal(y))$ is saying that a thing, namely $x$, loves a truthvalue, namely $Animal(y)$. This is a very odd thing to claim. Indeed, the formula $Loves(x,Animal(y))$ is not even well-formed according to the usual formation rules of first-order logic.