I've never had a problem with the axiom of choice, but it has often confused me how many authors find full choice so much different from finite choice. In my head they seem quite similar. We are picking elements in either case–why treat the infinite case as fundamentally different from the finite one? [Note: This is a rhetorical question, which I answer later, to motivate the remainder of the post.]
Their answer was to emphasize that finite choice was provable in ZF, but the full axiom of choice is independent. Okay, so then I'd delve into the proofs of finite choice, and get even more confused. They'd start with the trivial claim that an empty set has a choice function, the empty function. So far so good. Then they'd work by induction, sometimes skipping all the details. My problem was that this was exactly the point where I (and apparently others, see this previous question) got confused. What axiom of set theory allows someone to pick a single element from a single non-empty set?
The answer to this question is probably obvious to most logicians, but it took me a lot of delving to find it. The answer is: It isn't an axiom of set theory that allows this choice. It is the principle of "existential elimination" from first order logic. In other words, singleton choice is a meta-logical assumption. It says that we interpret the sentence
$$
\exists x(x\in y)
$$
as asserting the ability to pick (non-constructively) an element $x$ inside $y$. [I'm being a bit informal here, but hopefully you get the idea.]
So in my mind that begs the question of why our semantics does not treat the sentence
$$
\forall y \exists x (x\in y)
$$
as asserting the ability to pick (non-constructively) for each $y$ an element $x_y\in y$. [The subscript here is merely to emphasize that the choice of $x$ depends on $y$.]
Thus my question:
Is there a natural semantics/language where the sentence $\forall y \exists x\ P(x,y)$ is interpreted as the ability to pick for each $y$ some $x_y$ such that $P(x_y,y)$ holds?
It seems like this is somewhat strengthening the usual interpretation of $\forall$, by allowing infinitely many operations (one for each $y$) simultaneously.
Edited to add: Motivated by Goldstern's comment below, an alternate way to frame my question might be: Is ZF+GC (Zermelo-Fraenkel set theory with global choice) a sufficiently strong theory in which the semantics I proposed above is sound?
Best Answer
I like this question very much.
I find the difference between the two readings of $\forall x\exists y\ P(x,y)$ to be similar to the issues often brought up by questions of uniformity in mathematical existence assertions. So this may be a good keyword leading to further discussion. For example, the discussion of uniformity in my answer to the question Can a problem be simultaneously NP and undecidable?.
To explain a little, in the context of computability theory, say, in the ordinary mathematical reading of $\forall x\exists y\ P(x,y)$, there is no reason to think that there should be a computable function mapping each $x$ to such a $y$. But if we assert that the existence claim is uniform, then this means something much closer to the semantics about which you inquire, namely, that there should be a computable function allowing us to pass from $x$ to a witness $y$.
In ZFC set theory, the axiom of choice can be interpreted as the assertion that all existence claims of the form $\forall x\in u\exists y\ P(x,y)$ are uniform, so that there is a function $f$ with domain $u$ so that $P(x,f(x))$ for each $y\in u$. In class theories such as KM, the global axiom of choice is the assertion that all assertions of the form $\forall x\exists y\ P(x,y)$ are uniform, so that there is a class function $F$ with $P(x,F(x))$ for all $x$.
Since the issue of the uniformity of existence assertions is often central in many mathematical domains, I propose that this is the answer to your question.