When to use Skolem constant and a skolem function?
Andrew Henderson 
∀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?
$\endgroup$1 Answer
$\begingroup$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)$".
$\endgroup$ 4
