(logic) The conversion of a formula of first-order logic which involves the following steps: (1) replace free variables with constants, (2) replace any variable bound by an existential quantifier which lies in the scope of an even number of logical negations with a Skolem function, and (3) replace any variable bound by a universal quantifier which lies in the scope of an odd number of negations with a Skolem function.

(logic) A function which replaces a variable bound by an existential quantifier which lies in the scope of an even number of logical negations; such function is a function of the remaining bound variables whose scope contain the given variable (being replaced).

plural of Skolem function

(mathematical logic) A theorem stating that, if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ. The result implies that first-order theories are unable to control the cardinality of their infinite models, and that no first-order theory with an infinite model can have a unique model up to isomorphism.