The (philosophical) intuition beyond this question is that as much as the Skolemization of a $\exists \forall$ first-order formula allows to introduce a Skolem constant which refers to an arbitrary individual (namely, an individual arbitrarily picked out), so the Skolemization of a $\forall \exists $ first-order formula allows to introduce a Skolem function which (should) refers to an arbitrary function.
Nevertheless, it is well known that, while the equisatisfiability of a $\forall \exists $ first-order formula and it's Skolem Normal Form (SNF) can be proved in FOL as (where $|\phi |$ means the satisfiability of $\phi $): $$|\forall x\exists y\varphi(x,y)| \iff |\forall x\varphi(x,f(x))|$$
The logical equivalence of a first-order formula and it's SNF can be proved only in SOL (I will refer to this as Skolem Theorem), on the assumption of the Axiom of Choice (AC), as: $$\forall x\exists y\varphi(x,y) \models \exists f\forall x\varphi(x,f(x))$$ My question is: what is the ZFC 'assumption' (or feature) that makes Skolem theorem essentially second-order? It seems to me that the metalanguage of FOL - namely ZFC - does not allow to prove the logical equivalence between a first-order formula and it's SNF within FOL.
I will now propose a solution - but any other suggestion is welcomed. I think that this problem is closely tied up with the fact that in ZFC, while every definable set can be proved to exist (see my question Why in ZFC any expressible set also exists?), not every set that exists can be defined. Let me explain: the Skolem functions in an expanded model are by no means unique. However, if the first-order formula is like:
$$\forall x\exists !y\varphi(x,y)$$
Then the logical equivalence with it's SNF can be proved in FOL without AC as: $$\forall x\exists !y\varphi(x,y) \models \forall x\varphi(x,f(x))$$ Moreover, this last equivalence defines the Skolem function for the antecedent formula. This is due to the fact that in ZFC one can define a selection set t (namely, a Skolem function) for another set s iff s contains some definable element [Fraenkel 1973, Foundations of Set Theory]. In the example above, s contains some definable element because $\exists !y$ is a singleton. Yet, the ZFC proof of the Skolem theorem requires to consider also model with no definable elements - such as the set of all well-ordering of the set of the real numbers. At this point, AC is required to guarantee the existence of a (Skolem) function which cannot be defined. Is this correct?
If this argument is sound, then there is a tension with the initial (philosophical) intuition. Let me explain: to prove the logical equivalence of $\forall \exists $ first-order formulas and their SNF we need AC - and so also SOL - cause there are models with no definable elements where the values of Skolem functions cannot be defined. Yet, to prove the logical equivalence of $\exists \forall$ first-order formulas and their SNF neither AC nor SOL are required. But how is it possible that the added Skolem constant denotes a non definable element? Going back to the initial (philosophical) intuition, it seems that in the metalanguage of FOL - namely ZFC - we can refer to arbitrary objects but not to arbitrary functions. Why so? This last question is tricky: while the former proof requires AC - and so it's carried out in ZFC - the latter proof can be given in a (pure) model-theoretic settings (such as for Henkin theory).
P.S. I have been thinking about this question for a while. Please, feel free to ask me any clarificatory questions.