What is the image of skolemization? For simplicity, consider first order logic with one binary relation in the signature.
Any $\forall x \exists y. \phi(x,y)$ gives rise to skolemization, converting the formula into $\forall x. \phi(x,f(x))$, and by that adding a function symbol to the signature.
My question is, what precisely are the cases in which we can go the other way around. So we're given a formula in first order logic with one binary relation and several function symbols. In which cases can we write a logically-equivalent formula with no function symbols and one binary relation symbol? Maybe it's impossible to capture all such cases, but I feel that the inverse of skolemization is easier to get hold on.
For more [probably unnecessary] rigor, one might say that two formulas over different signatures are never logically equivalent. So clearly I mean to have same set of models after ignoring the interpretation of the function symbols in the functional signature.

One thing to think about is that a function $f$ is a binary relation that is right-unique (functional).
So, if you are given $\forall x. \phi(x,f(x))$, and you want to translate that back to some 2-place predicate $\phi(x,y)$, then you'll have to do something like: $$\forall x \exists y (\phi(x,y) \land \forall z (\phi(x,z) \to z = y))$$
