Namespaces
Variants
Actions

Difference between revisions of "Skolem function"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
(One intermediate revision by one other user not shown)
Line 1: Line 1:
A concept in predicate logic. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857401.png" /> is a predicate formula with individual variables (cf. [[Individual variable|Individual variable]]) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857402.png" />, whose domains are sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857403.png" />, respectively, then a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857404.png" /> is called a Skolem function or resolving function for the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857405.png" /> if for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857406.png" /> one has
+
<!--
 +
s0857401.png
 +
$#A+1 = 15 n = 0
 +
$#C+1 = 15 : ~/encyclopedia/old_files/data/S085/S.0805740 Skolem function
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857407.png" /></td> </tr></table>
+
{{TEX|auto}}
 +
{{TEX|done}}
  
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857408.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s0857409.png" />. For example, for every formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574010.png" /> of the language of the restricted predicate calculus it is possible to construct a formula of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574011.png" /> (called the Skolem normal form of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574012.png" />), where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574013.png" /> does not contain new quantifiers but does contain new function symbols, such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574014.png" /> is deducible in predicate calculus if and only if its Skolem normal form is.
+
A concept in predicate logic. If  $  A ( x _ {1} \dots x _ {n} , y) $
 +
is a predicate formula with individual variables (cf. [[Individual variable|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|Gödel completeness theorem]]) and elsewhere.
 
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|Gödel completeness theorem]]) and elsewhere.
Line 9: Line 37:
 
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|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.
 
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|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 [[#References|[6]]]) and the negation of the [[Suslin hypothesis|Suslin hypothesis]] (see [[#References|[5]]]) from Gödel's axiom of constructibility. The Novikov–Kondo theorem on the uniformization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s085/s085740/s08574015.png" />-relations from [[Descriptive set theory|descriptive set theory]] confirms the existence of a certain type of Skolem function (see [[#References|[2]]]).
+
By way of an example one can point to Jensen's result on the deducibility of Chang's two-cardinals conjecture (see [[#References|[6]]]) and the negation of the [[Suslin hypothesis|Suslin hypothesis]] (see [[#References|[5]]]) from Gödel's [[axiom of constructibility]]. The Novikov–Kondo theorem on the uniformization of $  \Pi _ {1}  ^ {1} $-
 +
relations from [[Descriptive set theory|descriptive set theory]] confirms the existence of a certain type of Skolem function (see [[#References|[2]]]).
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  J.R. Shoenfield,  "Mathematical logic" , Addison-Wesley  (1967)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  C.C. Chang,  H.J. Keisler,  "Model theory" , North-Holland  (1973)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  Yu.L. Ershov,  E.A. Palyutin,  "Mathematical logic" , Moscow  (1987)  (In Russian)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  K. Devlin,  "Constructibility"  J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland  (1977)  pp. 453–489</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  K.J. Devlin,  "Aspects of constructibility" , ''Lect. notes in math.'' , '''354''' , Springer  (1973)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  J.R. Shoenfield,  "Mathematical logic" , Addison-Wesley  (1967)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  C.C. Chang,  H.J. Keisler,  "Model theory" , North-Holland  (1973)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  Yu.L. Ershov,  E.A. Palyutin,  "Mathematical logic" , Moscow  (1987)  (In Russian)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  K. Devlin,  "Constructibility"  J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland  (1977)  pp. 453–489</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  K.J. Devlin,  "Aspects of constructibility" , ''Lect. notes in math.'' , '''354''' , Springer  (1973)</TD></TR></table>

Latest revision as of 08:14, 6 June 2020


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)
How to Cite This Entry:
Skolem function. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Skolem_function&oldid=12101
This article was adapted from an original article by V.N. Grishin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article