2 added "plugging into functions"

In classical logic, there is a natural symmetry (or duality) between the universal and the existential quantifier, and each one can be expressed in terms of the other. (Similar to the duality between $\vee$ and $\wedge$ in classical propositional logic.)

Classical logic and constructive mathematics interpret the universal quantifier in the same way, but they differ on what the existential quantifier means. An intuitionist or constructivist will only claim $A\vee B$ ($\exists x:A(x)$, respectively) if he knows that $A$ holds, or knows that $B$ holds (if he knows an $x$ for which $A(x)$ holds, respectively).

But this asymmetry between $\forall$ and $\exists$ also appears in textbooks based on classical logic. Assumptions such as "There exists $x$ with $\forall y( y+x=y)$" are almost always "skolemized"; this means that a new constant symbol $0$ and a new axiom $\forall y (y+0=y)$ is introduced. It is a basic fact of logic that skolemization is "allowed" (technical term: leads to a conservative extension).

Similarly, a sentence "forall $\varepsilon$ \delta$there is a an$\delta$\varepsilon$ such that $A(\delta, \varepsilon)$" is often reformulated in a skolemized for form as "[there is a function $\epsilon(\cdot)$ such that] for all $\delta$ we have $A(\delta, \epsilon(\delta))$".

I do not know any references, but in my opinion there are several reasons:

1. historically, the notion of a function $\epsilon(\cdot)$ (or a constant $0$) .has been around for much longer than the concept of an existential quantifier.

2. [EDIT] Related: you can plug constants and functions into functions; e.g., from $A(c)$ and $\forall x: B(x, f(x))$ most formal proof systems will trivially derive $A(c) \wedge B(c,f(c))$. Depending on your system, it may not be so trivial to get from $\exists x: A(x)$ and $\forall x\, \exists y: B(x,y)$ to $\exists x\, \exists y: A(x)\wedge B(x,y)$

3. (arguably,) from a didactical as well as the linguistic point of view it is easier to talk about $0$ and $\epsilon(\delta)$ rather than "the/some element satisfying $\cdots$" or "some $\varepsilon$ which by our assumption on continuity must exist". (This is in particular true if there is a unique or canonical object $0$ or $\epsilon(\delta)$.)

4. Skolemized sentences have fewer quantfiers, so they are easier to understand

5. Dependencies between variables become clearer. Also, skolemization is the most convenient form to express Henkin quantifiers ("for all $x,y$ there exists $p$, $q$ such that $\cdots$, but $p$ depends only on $x$, and $q$ only on $y$").

6. Even though most mathematicians base their arguments (often subconsciously) on classical logic, they still have a feeling for what a "constructive" proof is, and they will prefer a constructive proof over a nonconstructive one. Skolemization allows one to keep track of the non-computable or non-constructive steps in an argument. (E.g.: "For every $k$ there is an $N=N(k)$ such that for all $m>N(k)$ $foo(m,k)$ holds --- here, $N(k)$ can/cannot be directly computed from $k$.")

1

In classical logic, there is a natural symmetry (or duality) between the universal and the existential quantifier, and each one can be expressed in terms of the other. (Similar to the duality between $\vee$ and $\wedge$ in classical propositional logic.)

Classical logic and constructive mathematics interpret the universal quantifier in the same way, but they differ on what the existential quantifier means. An intuitionist or constructivist will only claim $A\vee B$ ($\exists x:A(x)$, respectively) if he knows that $A$ holds, or knows that $B$ holds (if he knows an $x$ for which $A(x)$ holds, respectively).

But this asymmetry between $\forall$ and $\exists$ also appears in textbooks based on classical logic. Assumptions such as "There exists $x$ with $\forall y( y+x=y)$" are almost always "skolemized"; this means that a new constant symbol $0$ and a new axiom $\forall y (y+0=y)$ is introduced. It is a basic fact of logic that skolemization is "allowed" (technical term: leads to a conservative extension).

Similarly, a sentence "forall $\varepsilon$ there is a $\delta$ such that $A(\delta, \varepsilon)$" is often reformulated in a skolemized for as "[there is a function $\epsilon(\cdot)$ such that] for all $\delta$ we have $A(\delta, \epsilon(\delta))$".

I do not know any references, but in my opinion there are several reasons:

1. historically, the notion of a function $\epsilon(\cdot)$ (or a constant $0$) has been around for much longer than the concept of an existential quantifier

2. (arguably,) from a didactical as well as the linguistic point of view it is easier to talk about $0$ and $\epsilon(\delta)$ rather than "the/some element satisfying $\cdots$" or "some $\varepsilon$ which by our assumption on continuity must exist". (This is in particular true if there is a unique or canonical object $0$ or $\epsilon(\delta)$.)

3. Skolemized sentences have fewer quantfiers, so they are easier to understand

4. Dependencies between variables become clearer. Also, skolemization is the most convenient form to express Henkin quantifiers ("for all $x,y$ there exists $p$, $q$ such that $\cdots$, but $p$ depends only on $x$, and $q$ only on $y$").

5. Even though most mathematicians base their arguments (often subconsciously) on classical logic, they still have a feeling for what a "constructive" proof is, and they will prefer a constructive proof over a nonconstructive one. Skolemization allows one to keep track of the non-computable or non-constructive steps in an argument. (E.g.: "For every $k$ there is an $N=N(k)$ such that for all $m>N(k)$ $foo(m,k)$ holds --- here, $N(k)$ can/cannot be directly computed from $k$.")