Skolemization algorithm for a formula I'd like to know if I my Skolemization is right:
$$(\exists x(P(x)\lor R(x)))\to((\exists xP(x))\lor(\exists xR(x)))\\(\exists x(P(x)\lor R(x)))\to((\exists yP(y))\lor(\exists zR(z)))\\(\exists x(P(x)\lor R(x)))\to\exists y\exists z.(P(y)\lor R(z))\\\forall x\exists y\exists z.((P(x)\lor R(x)))\to(P(y)\lor R(z))\\\forall x.(P(x)\lor R(x))\to(P(f(x))\lor R(g(x)))$$
Thanks.
 A: Almost!
Two issues


*

*no elimination of $\to$ (the algorithm is easily modified to accomodate this, but the step should be done at least according to Ben-Ari's book)

*choice of order of quantifiers. This is not strictly speaking wrong, but could be done more strategically. See below.
$$(\exists x\left(P(x) \lor R(x)\right)) \to  ((\exists x P(x)) \lor (\exists x R(x)))$$
Rename
$$(\exists x\left(P(x) \lor R(x)\right)) \to  ((\exists y P(y)) \lor (\exists z R(z)))$$
Eliminate all but $\lor, \neg, \land$:
$$\neg (\exists x\left(P(x) \lor R(x)\right)) \lor  ((\exists y P(y)) \lor (\exists z R(z)))$$
Push in (to move to NNF)
$$(\forall x \neg\left(P(x) \lor R(x)\right)) \lor  ((\exists y P(y)) \lor (\exists z R(z)))$$
$$(\forall x \left(\neg P(x) \land \neg R(x)\right)) \lor  ((\exists y P(y)) \lor (\exists z R(z)))$$
Extract (this can be done in several orders)
$$(\forall x \left(\neg P(x) \land \neg R(x)\right)) \lor  \exists y \exists z  (P(y) \lor R(z)))$$
$$\exists y \exists z \forall x \left(\neg P(x) \land \neg R(x)) \lor  (P(y) \lor R(z)))\right)$$
As there are no universal quantifiers preceding $\exists y, \exists z$ we get constants, as opposed to Skolem functions. Selecting fresh constant for $y$, then one for $z$. 
$$\forall x \left[ (\neg P(x) \land \neg R(x)) \lor  (P(a) \lor R(b))\right]$$
You could (in an equally valid fashion) extract $\forall x$ first (so the prefix looks like $\forall x\exists y \exists z$), turning this into
$$\forall x \left[ (\neg P(x) \land \neg R(x)) \lor  (P(f(x)) \lor R(f(x)))\right]$$
But if you can avoid it (if you're doing unification later on), you likely want to.
