Skolem form transformation I have to submit an exercise and it must be correct in order to access the exam. If you can tell me if this is right It would be really helpful.
Statement:
Find a Skolem form of the following formula:
$F = \forall x \exists y \forall w \exists z \neg(Q(k(y),f(x)) \vee P(u(w), a, s(z))$
So following the algorithm I've done these transformations:
$F = \forall a \forall x \exists y \forall w \neg(Q(k(y),f(x)) \vee P(u(w), a, s(g(a,x,w)))$
$F = \forall a \forall x \forall w \neg(Q(k(h(a,x)),f(x)) \vee P(u(w), a, s(g(a,x,w)))$
Is this ok? Thanks in advance!
 A: Since Skolemization is defined only for closed formulas, I guess in the starting formula $F$ you forgot an external $\forall a$.
So, your starting formula should be
\begin{equation}
F = \forall a \forall x \exists y \forall w \exists z \,\neg\big(Q(k(y),f(x)) \vee P(u(w), a, s(z)) \big)
\end{equation}
What you do is almost correct. Your error is that you have to start Skolemization from the outermost existential quantifier, and not from the innermost. 
Indeed, if you start from the innermost ($\exists z$ in $F$) the Skolem function $g$ replacing $z$ should depend on $a,x,w$ AND $y$.
Starting Skolemization from the outermost existential quantifier $\exists y$, after a first step you have
$\forall a \forall x  \forall w \exists z\, \neg\big(Q(k(\mathbf{h}(a,x)),f(x)) \vee P(u(w), a, s(z))\big)$
for some Skolem function $\mathbf{h}(a,x)$. A second Skolemization step yields the Skolem normal form
$\forall a \forall x  \forall w \neg\big(Q(k(\mathbf{h}(a,x)),f(x)) \vee P(u(w), a, s(\mathbf{g}(a,x,w)))\big)$
for  some Skolem function $\mathbf{g}(a,x,w)$.
