# 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))$$
• @TroyMcClure I am little confused then. OK, so I assumed that $\phi$ would be a 2-place predicate/relation symbol (... or is it a general formula?) And we use that predicate in $\phi(x,f(x))$ ... so how is using that very same predicate in $$\forall x \exists y (\phi(x,y) \land \forall z (\phi(x,z) \to z = y))$$ adding another symbol that you are not already using? Jun 27 at 15:36
• the question is about moving from a formula $\phi$ over a signature that has one relation symbol and one function symbol (none of which is $\phi$), to a formula with only one relation symbol Jun 27 at 15:42
• @TroyMcClure OK, I think I get it: so you have some formula $\phi$ that contains a single 1-place function symbol (though possible multiple instances of it), and one 2-place relation symbol (though again with possible multiple instances of it) and want to find a formula $\phi'$ that is equivalent o $\phi$ that just contains that same 2-place relation symbol (though again with possible multiple instances of it) but no further relation of function symbols. Can you add identity statements though? Those are typically not seen as part of the signature. Jun 27 at 15:52
• @TroyMcClure Hmm, right, yeah, I see the difficulty: why would the relation you already be able to take on the role of the function? For example, using a function means that you need to have a function-value ... so if you want to use $R(x,y)$ where $y$ is going to play the role of $f(x)$ you are in immediate trouble if $x$ doesn't stand in a relation to any $y$. So, what would you do with a formula like $\exists x (\forall y \neg R(x,y) \land f(x) = x)$? Jun 27 at 16:34