# If $\forall x \exists y : R(x, y)$, then is it true that $y = y(x)$?

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.

1. 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.

2. 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.

-
$y = y(x)$ is meaningless. – anon Oct 28 '10 at 19:32
It's called a skolem function by the way. – anon Oct 28 '10 at 19:33
$y = y(x)$ is meaningless? Even if I agree, which I do, I had to force into my brain that it has the semantics "let y be a function of x" when reading Stewart's calculus, so blame his publisher, not me. – Robin Hoode Oct 28 '10 at 19:41
I know what you're trying to say but y is not a function of x. The skolem function, which by abuse of notation and the fact that it provides a useful mnemonic we sometimes call y. To be formal about it you have some context $\Gamma$ containing x - in which y is well formed - this is the sense in which y depends on x. – anon Oct 28 '10 at 19:47
@muad: $y=y(x)$ is not meaningless: it is the standard notation! – Mariano Suárez-Alvarez Oct 28 '10 at 20:08

You seem to be asking: if for every $x$ there is a $y$ for which $R(x,y)$ holds, can we then define a function $f$ (in the usual sense) such that for every $x$, $R(x,f(x))$ holds?

From a set-theoretic point of view, that statement is in fact none other than the Axiom of Choice.

The Axiom of Choice has many forms, but one form is the following: given a nonempty family of nonempty sets, $S_i$ with $i\in I$ ("nonempty family" means that $I$ is not empty, so we have some sets; "nonempty sets" means that each $S_i$ is not empty), there exists a "choice function": a way to select for each $i\in I$ an element of the corresponding $S_i$. Formally, there exists a function $f\colon I\to \cup S_i$ from the index set to the union of the sets, with the property that $f(i)\in S_i$ for each $i$.

Suppose that by assumption, for every $x$ in our universe $X$, the set $S_x = \{y\mid R(x,y)\}$ is nonempty, and you have a function $f$ with the desried property. The function $f$ will be a "choice function": a function $f:X \to \cup_{x\in U}S_x$ such that for each $x\in X$, $f(x)\in S_x$. Conversely, a choice function for the family $\{S_x\}_{x\in X}$ will yield and $f$ with the desired property. The existence of such functions for every nonempty family of nonempty sets is precisely the Axiom of Choice. Conversely, suppose that the Axiom of Choice fails, and let $\{S_x\}_{x\in X}$ be a nonempty family of nonempty sets for which no choice function exists. Then let $R(x,y)$ be "$y$ is in $S_x$". For every $x$ there exists a $y$ such that $R(x,y)$, since $S_x\neq\emptyset$. But since we are assuming that the family has no choice function, there does not exist any function $f$ such that for every $x$, $f(x)$ is in $S_x$. Thus, the question not only depends on the Axiom of Choice, but is equivalent to the Axiom of Choice.

In some circumstances, the exact nature of the sets $S_x$ mean that you do not need to invoke the Axiom of Choice, because we have some "natural way" of defining the choice. For instance, if every set $S_x$ is a subset of the natural numbers, then you can define $f(x)$ to be "the least element of $S_x$". Another standard example is when $S_x$ is a singleton for every $x$; that is, for each $x$ there exists one and only one $y$ for which $R(x,y)$ holds. In that case, you can define your function $f$ to be "$f(x)$ is the unique $y$ for which $R(x,y)$ holds".

But in general, the Axiom of Choice is, in some sense, "inherently non-constructive". And the thing is, the Axiom of Choice is independent of the usual axioms of set theory. Like the parallel postulate in geometry, you can accept it or not at your taste (the consequences of accepting and of not accepting it are different; for example, if you accept the Axiom of Choice, then that means that there is a way to slice a ball of radius 1 into a finite number of parts, and then rearrange the parts without changing their shape or size, into two balls of radius of 1; this is called the Banach-Tarski paradox; on the other hand, if you want all your vector spaces to have bases, then you must accept the Axiom of Choice. In short, it has good consequences and weird/bad consequences).

Edit: In the situation you have, it is possible to describe a function that will work; however, the "description" is a bit like cheating, in the sense that you can give an explicit rule for what the value of the function will be, but in practice it would be difficult to actually find the value. Namely, for every $\epsilon\gt 0$ you know that the set of $\delta\gt 0$ for which the implication $||v-v_0||\lt\delta\Rightarrow ||f(v)-f(v_0)||\lt\epsilon$ holds is nonempty. In particular, by the Archimedean property, the set $A_{\epsilon}=\{n\in\mathbb{N}| ||v-v_0||\lt\frac{1}{n} \Rightarrow ||f(v)-f(v_0)||\lt\epsilon\}$ is nonempty. This is a nonempty set of positive integers, so it has a least element. You can then define your function $\mathbf{f}\colon (0,\infty)\to(0,\infty)$ by the "formula" $\mathbf{f}(\epsilon)=1/\min(A_{\epsilon})$, the reciprocal of the smallest $n$ in the set. This definition would not require you to invoke the Axiom of Choice.

As to your question 2: you almost had it, I think, but you should not invoke (implicitly) the Axiom of Choice: pick a specific $\epsilon$ (for example, $|A|/2$). You know that there exists a $\delta\gt 0$ that works for that epsilon, so you pick any $\delta_0$ that works and use that. That would be the standard way of proving the proposition at hand. If you assume you have some kind of "black-box function" that will hand you a $\delta$ whenever you hand it an $\epsilon$, you are invoking the Axiom of Choice and you are making your proof somewhat non-constructive.

-
(Note also that this 'inherently non-constructive' axiom of choice is a theorem in the kinds of constructive logic that the original question contained a link to. See Martin Lof for a proof) – anon Oct 28 '10 at 20:01
@muad: I'm not sure I understand your comment; as I read the statement in that source, if you accept the axiom of choice, then the Axiom of Choice provides you with that "function" you need to prove the universal statement. Of course, if you are working in the constructible universe, then AC holds (is a theorem?) and everything is done in terms of "constructions". – Arturo Magidin Oct 28 '10 at 20:05
@Arturo Magidin, I don't mean the constructible universe stuff, but the Brouwer–Heyting–Kolmogorov one. – anon Oct 28 '10 at 20:09
@Arturo Magidin Thank you for quickly settling that question. I wish I knew more about the foundational aspects of logic and set theory, but unfortunately no such course exists at my school. – Robin Hoode Oct 28 '10 at 20:39
@robinhoode, yes you wont learn this at school. Especially because this sort of logic you were investigating is not the 'standard' ZFC/FOL that mathematicians use as the default assumption. But see the above link regarding axiom of choice if you are interested. I don't agree that the question is settling btw... – anon Oct 28 '10 at 20:42

Some texts define a relation as simply a set of ordered pairs and a function as a set of ordered pairs in which every first element is unique. So if for all $x$ there is a unique $y$ such that $R(x,y)$, then you can say you have a function $y(x)$. You have not specified that y has to be unique.

I'm not sure what you mean by "prove a relation" under question 1. Your proof seems fine to me.

-
Since I had bumped this post up already, I took the opportunity to fix the TeX in your answer; hope it's ok. – Srivatsan Nov 4 '11 at 14:00
@Srivatsan: Thanks – Ross Millikan Nov 4 '11 at 14:16