# Skolem function

A concept in predicate logic. If is a predicate formula with individual variables (cf. Individual variable) , whose domains are sets , respectively, then a function is called a Skolem function or resolving function for the formula if for all one has Skolem functions were introduced by T. Skolem in the 1920s and have since been widely used in papers on mathematical logic. This is due to the fact that Skolem functions can be used to eliminate alternation of the quantifiers and . For example, for every formula of the language of the restricted predicate calculus it is possible to construct a formula of the form (called the Skolem normal form of ), where does not contain new quantifiers but does contain new function symbols, such that is deducible in predicate calculus if and only if its Skolem normal form is.
By way of an example one can point to Jensen's result on the deducibility of Chang's two-cardinals conjecture (see ) and the negation of the Suslin hypothesis (see ) from Gödel's axiom of constructibility. The Novikov–Kondo theorem on the uniformization of -relations from descriptive set theory confirms the existence of a certain type of Skolem function (see ).