A theory is said to have Skolem functions if for every formula there is a term such that whenever , , and is non-empty, then .
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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \phi(x;y)} , one adds a term and chooses arbitrarily, for every for which Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \phi(M;b) \ne \emptyset} . After doing this, new formulas may have appeared, so the process must be iterated 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} is said to have definable Skolem functions if for every formula Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \phi(x;y)} there is a definable function such that whenever Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle M \models T} , Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle b \in M} , and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \phi(M;b)} is non-empty, then Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle p} -adically closed fields do. Any o-minimal expansion of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle RCF} has definable skolem functions (in fact, has definable choice).
If Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} has definable Skolem functions, Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T^{eq}} need not have definable Skolem functions. In fact, this happens if and only if has definable choice, a condition stronger than elimination of imaginaries. ::: ::: :::