Are $\forall x \in A, \exists y \in B, p(x,y)$ and $\exists f \in B^{A}, \forall x \in A, p(x,f(x))$ equivalent?

Question

Let $P := \forall x \in A, \exists y \in B, p(x,y)$ and $Q := \exists f \in B^{A}, \forall x \in A, p(x,f(x))$

It seems like the Q is stronger than P. I can prove P from Q, but not the other way around. I'm not sure how to construct the function because classical existence confuses me.

However, the implication from the second to the first seems possible when I think about it intuitionistically and use a realizability interpretation.

A proof of $P$ is a function $g$ from $A$ to proofs of $\exists y \in B, p(x,y)$. A proof of $\exists y \in B, p(x,y)$ is a pair $(y,q)$ where $y \in B$ and $q$ is a proof of $p(x,y)$. So in the proof of $Q$, we can just take $f$ to be the projection of $g$ onto the first factor.

So there should be a classical proof, right? What does a formal proof (I guess in classical second-order logic) look like?

My original motivation is that the definition of continuity is in the first form, where I like to think of it more in the second form. Like this explanation: "If you give me any epsilon, then I can find a delta such that... But actually, I can automate my job. I can give you a function where if you give me an epsilon, I can feed it to my function to give you that delta." You can then think of the function in the proof as a sort of error controlling function, and that would probably lead to some interesting or more intuitive definitions and proofs in real analysis.

Answer 1

Classically the implication (1)$\rightarrow$(2) is equivalent to the axiom of choce.

From choice to $(1)\rightarrow(2)$: For $x\in A$ let $S_x=\{y\in B: p(x, y)\}$. By $(1)$ each $S_x$ is nonempty, so by Choice we get a choice function; but this is exactly the $f$ demanded by $(2)$.

From $(1)\rightarrow (2)$ to choice: Suppose I have a family $\mathcal{F}$ of nonempty sets. Let $A=\mathcal{F}$, $B=\bigcup\mathcal{F}$, and let $$p(x, y)\equiv y\in x.$$ Since the elements of $\mathcal{F}$ are nonempty, (1) holds; but any $f$ satisfying $(2)$ will be a choice function for $\mathcal{F}$.

---

EDIT: Building off of your specific motivation: for most reasonable cases we don't need the axiom of choice. For instance, for continuity, you can pick the supremum of all the $\delta$s which work, divided by two. What's driving this approach is that the reals satisfy certain closure properties (suprema and infima of appropriate sets exist), and the sets involved in the definition of continuity are reasonable (e.g. the set of $\delta$s which work for given $\epsilon$ is a downwards-closed set of positive reals).

Another approach would be to pick the least rational $\delta$ which works, according to some fixed well-ordering of the rationals. What's driving this method is that the reals, while not well-orderable, have a dense subset which is well-orderable, and again the sets involved in the definition of continuity aren't too complicated (if there is any $\delta$ which works, there is a rational $\delta$ which works).

Answer 2

You have re-discovered an interesting fact: the axiom of choice, while being "strong" in classical mathematics, is not very strong in constructive mathematics. Errett Bishop, in his text on constructive analysis, went so far as to say that the axiom of choice is a consequence of "the very meaning of existence". What he meant, as you see, is that it is hard to see how you could prove $(\forall x)(\exists y) \phi(x,y)$ constructively without also proving $(\exists f)(\forall x)\phi(x, f(x))$. In particular, as you noted, the axiom of choice does have a realizer, in the sense that if the hypothesis is realizable then so is the conclusion.

As for a proof in classical second-order logic, there are two options. Some authors include the choice scheme $$ (\forall x)(\exists y) \phi(x,y) \to (\exists f)(\forall x)\phi(x, f(x))$$ as an axiom, for each $\phi$. In that case, the proof is trivial. Otherwise, that scheme is not provable from the remaining axioms of second-order logic (even with the full set existence axiom scheme).