Skolem function

A concept in predicate logic. If $ A ( x _ {1} \dots x _ {n} , y) $ is a predicate formula with individual variables (cf. Individual variable) $ x _ {1} \dots x _ {n} , y $, whose domains are sets $ X _ {1} \dots X _ {n} , Y $, respectively, then a function $ f: X _ {1} \times \dots \times X _ {n} \rightarrow Y $ is called a Skolem function or resolving function for the formula $ \exists y A ( x _ {1} \dots x _ {n} , y) $ if for all $ x _ {1} \in X _ {1} \dots x _ {n} \in X _ {n} $ one has

$$ \exists y A ( x _ {1} \dots x _ {n} , y) \Rightarrow A ( x _ {1} \dots x _ {n} , f ( x _ {1} \dots x _ {n} )). $$

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 $ \forall $ and $ \exists $. For example, for every formula $ A $ of the language of the restricted predicate calculus it is possible to construct a formula of the form $ \exists x _ {1} \dots x _ {n} \forall y _ {1} \dots y _ {m} C $( called the Skolem normal form of $ A $), where $ C $ does not contain new quantifiers but does contain new function symbols, such that $ A $ is deducible in predicate calculus if and only if its Skolem normal form is.

Skolem functions are used in such fundamental theorems of mathematical logic as Herbrand's theorem, which reduces the question of deducibility of a predicate formula in predicate calculus to that of deducing an infinite sequence of propositional formulas in propositional calculus. They also figure in the Löwenheim–Skolem theorem (cf. Gödel completeness theorem) and elsewhere.

When one deals with formulas on an object domain with an additional structure, one may require a Skolem function to have a definite connection with this structure. For example, if the object domain belongs to the hierarchy of Gödel constructible sets (cf. Gödel constructive set), then one may require that the Skolem functions also belong to a definite level in this hierarchy. It is not always guaranteed that Skolem functions satisfying additional properties exist, but when they do, the effect of using them turns out to be very significant.

By way of an example one can point to Jensen's result on the deducibility of Chang's two-cardinals conjecture (see [6]) and the negation of the Suslin hypothesis (see [5]) from Gödel's axiom of constructibility. The Novikov–Kondo theorem on the uniformization of $ \Pi _ {1} ^ {1} $- relations from descriptive set theory confirms the existence of a certain type of Skolem function (see [2]).

References

[1]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[2]	J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)
[3]	C.C. Chang, H.J. Keisler, "Model theory" , North-Holland (1973)
[4]	Yu.L. Ershov, E.A. Palyutin, "Mathematical logic" , Moscow (1987) (In Russian)
[5]	K. Devlin, "Constructibility" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 453–489
[6]	K.J. Devlin, "Aspects of constructibility" , Lect. notes in math. , 354 , Springer (1973)