Convert formula to skolem variant

Question

Example: Convert this formula to Skolem normal form

$(\exists x )(\forall y)(\exists u)(\exists v)(\forall w)(P(x,y,z)\lor R(x,u)\lor Q(u,v,w))$

Solution:

1. $(\forall y )(\forall z)(\exists u)(\exists v)(\forall w)(P(c,y,z)\lor R(c,u)\lor Q(u,v,w))$

2. $(\forall y )(\forall z)(\forall w)(P(c,y,z)\lor R(c,f(y,z))\lor Q(f(y,z),g(y,z),w))$

This is one of the examples, which we had in the lecture with solution, which is not really clear to me. I understand the algorithm and the definition of SNF, but I do not understand the operation in the first step.

Why there is substitution of variable 'x' for 'c'?

Why we cannot do the same with $(\exists x)$ as with the other "exists" quantifiers as we do in the second step?

Answer 1

See skolemization; the rule is :

replace each existentially quantified variable $x$ with a function $f$ having $n$ arguments, where $n$ is the number of universal quantifiers preceding the existential one.

If, as in your case, $n=0$ then the function $f$ has $0$ arguments, i.e. it is an individual constant.

The quantifiers $\exists u$ and $\exists v$ are preceded by $\forall y \forall z$ and thus they are replaced by two different $2$-arguments functions $f(y,z)$ and $g(y,z)$.