A theory $ T $ is said to have **Skolem functions** if for every formula $ \phi(x;y) $ there is a term $ t(y) $ such that whenever $ M \models T $, $ b \in M $, and $ \phi(M;b) $ is non-empty, then $ t(b) \in \phi(M;b) $.

By the Tarski-Vaught criterion, having Skolem functions is enough to ensure that every substructure of a model is an elementary substructure.

Every structure can be expanded to have Skolem functions, by a process called **skolemization**. For each formula $ \phi(x;y) $, one adds a term $ t_\phi $ and chooses $ t_\phi(b) \in \phi(M;b) $ arbitrarily, for every $ b $ for which $ \phi(M;b) \ne \emptyset $. After doing this, new formulas may have appeared, so the process must be iterated $ \omega $ times. This process is highly non-canonical, and breaks most model-theoretic properties. It is useful as a tool in proving results like the Downwards Löwenheim-Skolem theorem, and the existence of Ehrenfeucht-Mostowski models.

A theory $ T $ is said to have **definable Skolem functions** if for every formula $ \phi(x;y) $ there is a definable function $ f(y) $ such that whenever $ M \models T $, $ b \in M $, and $ \phi(M;b) $ is non-empty, then $ f(b) \in \phi(M;b) $. This is a weaker condition than having Skolem functions.

An equivalent condition to having definable skolem functions is that every definably closed subset of a model is an elementary substructure.

The theory of algebraically closed fields does not have definable skolem functions, but the theories of real closed fields and $ p $-adically closed fields do. Any o-minimal expansion of $ RCF $ has definable skolem functions (in fact, has definable choice).

If $ T $ has definable Skolem functions, $ T^{eq} $ need not have definable Skolem functions. In fact, this happens if and only if $ T $ has definable choice, a condition stronger than elimination of imaginaries.