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?