Skolemization problem:∀x∃y∀z∃u (A(x,y,z,u) v B(y,u))

Question

Everything in the title but an explanation would be nice beside an answer! I don't really know if I should use constants or functions.

Answer 1

Skolemization is performed by replacing every existentially quantified variable $y$ with a term $f(x_i)$ whose function symbol $f$ is new.

If the formula is in prenex normal form, the variables $x_i$ of this term are the variable universally quantified whose quantifiers precede that of $y$.

The function $f$ introduced in this process is called a Skolem function (or Skolem constant if it is of zero arity, i.e. if the existential quantifier to be removed is not preceded by any universal quantifier).

Thus, in order to "skolemize" :

$∀x∃y∀z∃u \ldots$

we need a 1st skolem function $f(x)$ for the $∃y$ existential quantifier (1-arity, because $∃y$ is preceded by $∀x$) and a 2nd one $g(x,z)$ for the $∃u$ existential quantifier (2-arity, because $∃u$ is preceded by $∀x$ and $∀z$).