Why is Skolem normal form equisatisfiable while the second order form equivalent? 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:
$\phi$(x,f(x))
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? 
 A: It's perhaps best to think about this first in the context of a particular structure and a particular formula, where you can easily see what's going on.  Consider the structure of the natural numbers with the usual ordering relation $<$.  The sentence $\forall x\exists y\,(x<y)$ is true in this structure, because for every natural number $x$ there is a larger one $y$, for example $x+1$ (or $x+17$ or $(2x)!$ or lots of other choices).  Equivalently, the second-order sentence $\exists F\forall x\,(x<F(x))$ is true in the same structure, witnessed by functions like $F(x)=x+1$ (or $F(x)=x+17$ or $F(x)=(2x)!$, or lots of other functions $F$).
On the other hand, we cannot say (as you did) that $\forall x\exists y\,(x<y)\models\forall x\,(x<F(x))$.  To see this, notice first that this "logical consequence" relationship concerns structures for a language that has not only the relation symbol $<$ but also the function symbol $F$. Consider the structure of natural numbers with $<$ as before and some interpretation of the function symbol $F$. Then $\forall x\exists y\,(x<y)$ is true (regardless of the interpretation of $F$ because it doesn't mention $F$), but whether $\forall x\,(x<F(x))$ is true depends on how we interpret $F$.  It's true if we take $F(x)=x+1$ (or $F(x)=x+17$ or $F(x)=(2x)!$, or lots of other functions $F$), but it's false if we take $F(x)=0$ (or $F(x)=17$ or $F(x)=\lfloor x/2\rfloor$, or lots of other functions).  But $\models$ means that every structure satisfying what's on the left of $\models$ also satisfies what's on the right. So in our case, it would require that $\forall x\,(x<F(x))$ is true regardless of how we interpret $F$ as long as $\forall x\exists y\,(x<y)$ is true.  Since that doesn't hold when $F$ is "badly" interpreted ($0$ or $17$ or $\lfloor x/2\rfloor$), we don't have $\forall x\exists y\,(x<y)\models\forall x\,(x<F(x))$.  The most we can say is that, having satisfied $\forall x\exists y\,(x<y)$, we can, by suitably interpreting $F$, also satisfy $\forall x\,(x<F(x))$ --- and vice versa. That's what "equisatisfiable" means.
