∀x [∃y Animal (y) ∧ ¬Loves(x, y)] ∨ [∃z Loves(z, x)]
In the CNF conversion process, at the skolemize step, why the above statement use skolem function rather than a constant like 'A' or 'B' for ∃z Loves(z, x) part.
The book's answer is
∀x [Animal (F(x)) ∧ ¬Loves(x, F(x))] ∨ Loves(G(x), x)
Could someone elaborate the explanation given in there?
Should we always need to read the meaning before deciding what to use?
See Skolem normal form.
If the existential quantifier is inside the scope of one or more universal quantifiers, we need a function symbol.
If the existential quantifier is not inside the scope of an universal quantifiers, we need a constant symbol.
The "intuition" is: for $\exists x \ P(x)$ we can choose e new constant symbol $c$ and "name" with it the existsing object such that $P$ holds of it.
For the case $\forall x \ \exists y \ P(y)$ we have to write $\forall x \ P(f(x))$ because we know that "for every $x$ there is an $y$ such that" and this does not mean that we have a unique $y$ in the universe of discourse, but only an $y$ for every $x$, i.e. something like "$f: x \to y=f(x)$".