My question stems from the comments following Asaf Karagila's answer here : Why can't you pick socks using coin flips?
At some point there was a discussion about whether or not a countable union of countable sets is countable if one does not assume AC.
I upvoted this comment for I thought it quite right :
@phs: Maybe your confusion comes from the meaning of the term "countable". It gives you the existence of a bijection with the natural numbers (an enumeration of the set), but it does not give you (choose for you) such a bijection. For one set (or finitely many) existential elimination will hand you a concrete enumeration, but not so for infinitely many sets at a times. – Marc van Leeuwen Mar 19 '14 at 13:11
Then I got to this one :
@Marc: That's not fully correct. You sort of slide the case where the model and the meta-theory disagree on the integers (i.e. non-standard integers), in which case this only holds for the meta-theory integers; but it's true internally for everything the model think is finite. It's an even finer point than the place where choice is used in the above proof. I do agree it's a good intuition, but it's not really the reason why this fails. In fact, it's not the reason at all. (This is quite delicate, and I only understood that about a year ago, and I even made that mistake before.) – Asaf Karagila Mar 19 '14 at 18:57
This comment appears quite rich and deeply interesting. I must confess however that I don't fully understand it. I was wondering if anyone could provide me with a more detailed explanation of what is said in this comment.
If you have two sets $A$ and $B$ which are non-empty, then it means that the statement $\exists x\exists y(x\in A\land y\in B)$ is true. Now by existential instantiation we get $a,b$ such that $a\in A\land b\in B$. So the function defined as $\{\langle A,a\rangle,\langle B,b\rangle\}$ is a choice function as wanted.
One could argue, if so, that finite choice follows from the fact that if you have a finite set of non-empty sets, then you can write that statement as $\exists x_1\ldots\exists x_n(\ldots)$, and then using existential instantiation get the choice function as before.
But this is not accurate. If $M$ is a model of $\sf ZF$ which has non-standard integers, then there is some $N\in M$ such that $M\models N\text{ is an integer}$, but $x$ does not correspond to any actual integer from our meta-theory. So we cannot write any statement with $N$ quantifiers, because $N$ is not really a finite integer. Therefore applying existential instantiation fails here, and you have an existential crisis:
If you can't do that, then we cannot say that $\sf ZF$ proves that "For every finite set of non-empty sets there is a choice function". Because in that statement finite means "internally finite", and not "finite in the meta-theory".
This is solved by the fact that $\sf ZF$ proves induction. So we can do induction internally to $M$, and there you only have to deal with two existential quantifiers. One for the choice function of a set of smaller size (the induction hypothesis) and one for the choice of element from the additional set (the inductive step).
So it's true that existential instantiation is how we solve this crisis of choice. But one has to be vigilant and understand that this is not an application from the meta-theory by recursion. It is an internal recursion that just... works!