I asked in another question when is it appropriate to de-Skolemize a statement. The answer, I'm not sure I'm satisfied with yet, relies on a second order logical equivelance, but Skolem normal form isn't logically equivalent. I've read first order Skolemization can be defined through a second order logic equivelance:
$\forall$x$\exists$y $\phi$(x,y) $\iff$ $\exists$F$\forall$x $\phi$(x,F(x))
From this we can omit the quantifiers, and treat all variables as implicitly universally quantified:
I also understand that Skolem normal form is equisatisfiable:
$\forall$x$\exists$y $\phi$(x,y) $\vDash$ $\phi$(x,f(x))
[I apparently incorrectly understood it, see accepted answer]
But apparently this is not equivalent.
What does this mean? Can we freely move between Skolem normal form and the second order sentence even though they aren't equivalent? I only see equisatisfiability with Skolemization used to prove satisfiability or unsatisfiability, and I haven't seen it used to prove logical consequence from first order formulas except through unsatisfiability with searching for a contradiction.
Why is the second order form of a first order sentence that moves existential quantifiers out of scope of universal quantifiers logically equivalent, while Skolem normal form only equisatisfiable?