Why isn't Axiom of Choice a trivial result? Is it needed to prove existence of this recursive function?

Solution 1:

The key issue is that you're saying we "choose" the set $B$ to contain one element from each member of $\mathcal{A}$, but you're not specifying which elements these are. For a finite collection $\mathcal{A}$, this is no problem - there's always a finite list of instructions that could be specified, if one cared to take the time.

But for an infinite collection $\mathcal{A}$, it's not a consequence of ZF that you can make these choices - the way I think of it is that there's no way to finitely describe a process that selects one element from each set. Since ZF is in a language that can only finitely define things, ZF can't be sure that the sequence of choices can happen.

Now, many people would say that despite this the Axiom of Choice is still obviously true, which is why ZFC includes it as an axiom - Pairing is similarly trivial, for example. The weird thing is that the Axiom of Choice has weird consequences, like the Banach-Tarski Paradox, which made people suspect it might be false.

Solution 2:

The axiom of choice makes sense in the context of an axiomatic system describing a form of the notion of sets. You say

if we have the collection of sets A and we choose the set B to contain only one element from each set in A ...

but in the context of a fixed axiomatic system, like ZF, you can only do what the axioms let you do. The problem is, the axioms of ZF do not, directly or indiectly, let you do this choosing that you are planning to do. Zermelo and friends suspected this, so that is why they added AC to the list of axioms, but later it was actually proved that AC does not follow from ZF.

Solution 3:

Yes, this is an error in reasoning. And also lack of rigor.

First of all, if $B\subseteq A$ for some $A\in\cal A$, then $B\subseteq\bigcup\cal A$, rather than $B\in\bigcup\cal A$. Secondly, unless each $A$ was already a singleton, you don't have an obvious choice for $B$. Moreover, even if for each $A$ there is an obvious choice, it does not mean that there is a uniform way for defining this obvious choice.

So when you say for each $A$ let $B$ be some singleton such that $B\subseteq A$, you already appealed to the axiom of choice in its full power.