Is it true that for all proofs $\forall x \exists y : R(x, y)$, then $y = y(x)$?
A while back I remember reading a book on functional programming that was leading into some questions about what exactly mathematical proofs were and how they were related to functions. In fact, I just found the book: link to PDF, page 16 (marked page 3).
The author mentions that if we have a proof that $\forall x \exists y : R(x, y)$, then, in a sense, because $x$ is bound before $y$, then $y$ is dependent on $x$, and therefore $y = y(x)$. There may be counterexamples. Perhaps $y$ is a constant itself, but then $y(x)$ can also just be a constant function. I'm trying to understand under what circumstances this is not true.
Example:
Let $f : \mathbb {R}^n \to \mathbb R$ be continuous at a point $\vec{v_0}$ and $f(\vec{v_0}) = A < 0$. Prove that there exists a number $\delta > 0$ such that if $\| \vec{v} - \vec{v_0} \| < \delta $ then $f(\vec{v}) < 0$.
My argument was simply to use the statement of continuity at $\vec{v_0}$ to prove this. That is, since $f$ is continuous, the following holds:
$$ \forall \epsilon > 0 \quad \exists \delta > 0 : \quad \| \vec{v} - \vec{v_0} \| < \delta \Rightarrow \| f(\vec{v}) - f(\vec{v_0}) \| < \epsilon .$$
So, as referred to above, we must have $\delta = \delta(\epsilon)$. Then we can make the replacement $\delta = \delta(|A|)$, and we have the necessary $\delta$ to prove that $f(\vec{v}) < 0$.
I have one main question (the one that closes this), and one side question.
Under what conditions can we assume that $\forall x \exists y : R(x, y)$, then $y = y(x)$?
Are there indirect ways to prove a proposition of the form $\forall x \exists y : R(x, y)$ where $y$ is somehow not dependent on $x$ and also not a constant? Perhaps it varies on $R$, but that is given, I suppose. Certainly all $\epsilon$-$\delta$ proofs that I've come across have been constructive in this way.Is there a canonical way to prove the proposition above?
I actually struggled with a possible proof for a while before I came up with the technique above. I used this technique in a HW assignment and on my latest Advanced Calculus test. The HW was marked as correct although with the note that it was "indirect", while the test was marked as wrong. Granted, the HW was done by the TA, the test by my prof. I personally don't see a more "direct" way to prove this result.