 In the introductory examples in the present and the following section, let us confine attention to formulas in prenex form: a string of quantifiers followed by a quantifier-free first-order formula. If in a first-order sentence of such a form an existential quantifier \(\exists y\) lies in the syntactic scope of a universal quantifier \(\forall x\), then by the semantics \(\exists y\) automatically depends on \(\forall x\). This is so e.g. with the sentence \((\forall x)(\exists y) R(x, y)\). The dependence of \(\exists y\) on \(\forall x\) means that the witness of \(\exists y\) may vary with the value interpreting \(\forall x\). In order for the sentence to be true in a model \(M\), it suffices that there be a function \(f\) such that \(R(a, f(a))\) holds in \(M\), for any \(a\) interpreting \(\forall x\). Such functions, spelling out the dependencies of witnesses for existential quantifiers on interpretations of universal quantifiers, are known in logical literature as Skolem  functions.[4]  For comparison, in the sentence \((\exists y)(\forall x) R(x, y)\) the quantifier \(\exists y\) does not depend on the quantifier \(\forall x.\) For this sentence to be true in \(M\), one and the same witness \(c\) for \(\exists y\) must be good against any interpretation \(a\) of \(\forall x\), so that \(R(a, c)\) holds in \(M\). The corresponding Skolem function is a  constant.[5]