In first order logic we can eliminate existential quantifiers using a second order equivalence relation:
$\forall$x$\exists$y P(x, y) $\iff$ $\exists$f$\forall$x P(x, f(x))
Dropping the existential quantifier on the function gives skolemization. Now we can peform inferences and substitutions more freely.
Is there a skolemization procedure for higher order logic?
$\forall$x$\exists$y$\exists$R$\exists$f (P(x, y) $\land$ Q(f(x)) $\land$ R(y, f(x))) $\iff$ ?
and if there is one does it assume the axiom of choice or some other strong set theoretical assumption? How can we remove alternating quantifiers in second and higher order logic?
You just replace $\forall x \exists y.\phi$ by $\exists f \forall x.\phi[f(x)/y]$ for higher-order formulas $\phi$ in the same way that you did for a first-order formula. The Skolem functions will acquire more and more arguments as you go. The axiom of choice is needed to show that the skolemised formula is equivalent to the original.
Your example would skolemise like this:
$$ \forall x \exists y \exists R \exists f. P(x, y) \land Q(f(x)) \land R(y, f(x)) \Leftrightarrow \exists y' \exists R' \exists f \forall x. P(x, y'(x)) \land Q(f(x)) \land R'(x, y'(x), f(x)) $$
where I have made the slight optimisation of leaving $f$ as it is because it is already paramatrized by $x$.