First let me say that I have read tons of questions and answers on AC but none helps me get past this issue, so I am posting my own question.
Let's say we have an infinite family of disjoint non-empty sets $\{ X_{\lambda} \}_{\lambda \in I}$.
What's wrong with the following reasoning:
- $\forall \lambda \in I \; \exists x_{\lambda} \in X_{\lambda}$
- Then, there exists a choice function, which maps $\lambda \to x_{\lambda}$
Everything I read says that you can do it for one set only (and then by induction for finitely many sets), but I see absolutely no reason why this argument that I wrote doesn't work (without AC) for any collection of sets.
Best Answer
There are a lot of subtleties here. For one, existence in itself is a semantic property of objects, whereas proofs are syntactic objects. So, in some sense, things can easily exist in a universe of mathematics, even if we cannot prove or disprove their existence. Especially when we cannot do those things. This is the essence of independence.
This is why examples related to the failure of choice are always so wishy-washy and rely on bad analogies or handwaving. It is simply the case that the axiom of choice is consistent with $\sf ZF$, and so no such failures might exist; or it might be that the axiom of choice fails, but in a manner so remote from "everyday sets", that it is hard to give satisfying examples.
But suppose that we wanted to only assume $\sf ZF$, how can we still determine whether a family admits a choice function or not? Well. If we can prove that a family satisfying some condition admits a choice function, then this must be true in every universe of $\sf ZF$, independent of whether or not the axiom of choice holds there.
Sometimes we can do this by utilising facts and giving explicit definitions. For example, say that we are given a family of compact subsets of real numbers, then we know that each such set is both closed and bounded from below, and therefore it has a minimum. So we can define a function explicitly mapping each compact set to its minimum.
But what is "define a function" anyway? Well, we utilise the axioms of $\sf ZF$ to prove that there is a choice function, or a transversal set (which is easier to state in the pure language of set theory), or whatever object is of interest here.
The other way is to simply prove there is a function, even if we can't give it an explicit definition. So, in our example, if we simply wish to prove that a finite family admits a choice function, since we have no properties to rely on for that "explicit definition", we need to have something more general.
The naive idea would be to utilise the logic, apply Existential Instantiation repeatedly, so if we have $\{A_0,\dots,A_n\}$, we can use EI to obtain $a_0\in A_0,\dots,a_n\in A_n$, and then consider the formula which defines the function $f(A_n)=a_n$.
This is a good intuition, but it fails once you realise that we also have to take into consideration models where there are non-standard integers. The problem here is that there will now be sets that are considered to be "finite" from the universe's point of view, but they are too big for the naive iteration of EI to work. Luckily, $\sf ZF$ proves its own internal induction, and we internalise the EI thing, so we can simply make the claim that if $\cal A$ admits a choice function and $A$ is non-empty, then $\mathcal A\cup\{A\}$ admits a choice function: use EI to get a choice function for $\cal A$, then again to get an element from $A$, and then put them together. Easy peasy, with only two applications of EI.
So, why doesn't that work for any good ol' family of sets? Well, the proof simply fails. You need to know that by removing a single set from the family, you will obtain a choice function. If the family is finite, this is internally a terminating process (within finitely many steps), and the whole thing works; but if the family is infinite, then removing elements one after the other has no means to guarantee that the process terminates.
And indeed, we know that if $\sf ZF$ is at all consistent, then it is also consistent that for any infinite set $X$, there is a family of finite sets indexed by $X$ which will not admit a choice function. So, it's not just that the above proof doesn't work, no proof works.
So, if you want to prove that a choice function exists, you need an axiom that guarantees that a choice function exists. This is exactly what the axiom of choice does.
But, let me be clear, your confusion is quite natural. I sat through a talk about proof mining and natural-language proof assistants. The speaker pointed out that due to its second-order nature, the proof assistant proves the axiom of choice, exactly by switching quantifiers. In fact, in some constructive foundations of mathematics, the statement "$\cal A$ is a family of non-empty sets" requires you to have a uniform witness that each set is non-empty, which means that the axiom of choice is but a mere theorem.
Here we see the difference between shoes and socks very clearly. For pairs of shoes, there is a uniform way to show that a pair of shoes is "not empty", whereas for socks there is no uniform discerning property that will work for all pairs. So the fact we can pick one pair, choose one sock, and then pick a second pair, and so on, has no bearing on the fact that there is no uniform way to describe a property that only works for a single sock in all the pairs simultaneously.
The only way to go through this confusion, I'm afraid, is to work out some of these things, study a few choiceless models, and trying to develop a better intuition. To quote von Neumann, "Young man, in mathematics you don't understand things. You just get used to them."