Getting the Heavy Maths out the Way: Definitions

Intuitively, the [-axiom_mathematics axiom] of choice states that, given a collection of non-empty sets, there is a function which selects a single element from each of the sets.

More formally, given a set $~$X$~$ whose elements are only non-empty sets, there is a function $$~$ f: X \rightarrow \bigcup_{Y \in X} Y $~$$ from $~$X$~$ to the union of all the elements of $~$X$~$ such that, for each $~$Y \in X$~$, the image of $~$Y$~$ under $~$f$~$ is an element of $~$Y$~$, i.e., $~$f(Y) \in Y$~$.

In [-logical_notation logical notation], $$~$ \forall_X \left( \left[\forall_{Y \in X} Y \not= \emptyset \right] \Rightarrow \left[\exists \left( f: X \rightarrow \bigcup_{Y \in X} Y \right) \left(\forall_{Y \in X} \exists_{y \in Y} f(Y) = y \right) \right] \right) $~$$

Axiom Unnecessary for Finite Collections of Sets

For a finite set $~$X$~$ containing only finite non-empty sets, the axiom is actually provable (from the [-zermelo_fraenkel_axioms Zermelo-Fraenkel axioms] of set theory ZF), and hence does not need to be given as an [-axiom_mathematics axiom]. In fact, even for a finite collection of possibly infinite non-empty sets, the axiom of choice is provable (from ZF), using the [-axiom_of_induction axiom of induction]. In this case, the function can be explicitly described. For example, if the set $~$X$~$ contains only three, potentially infinite, non-empty sets $~$Y_1, Y_2, Y_3$~$, then the fact that they are non-empty means they each contain at least one element, say $~$y_1 \in Y_1, y_2 \in Y_2, y_3 \in Y_3$~$. Then define $~$f$~$ by $~$f(Y_1) = y_1$~$, $~$f(Y_2) = y_2$~$ and $~$f(Y_3) = y_3$~$. This construction is permitted by the axioms ZF.

The problem comes in if $~$X$~$ contains an infinite number of non-empty sets. Let's assume $~$X$~$ contains a countable number of sets $~$Y_1, Y_2, Y_3, \ldots$~$. Then, again intuitively speaking, we can explicitly describe how $~$f$~$ might act on finitely many of the $~$Y$~$s (say the first $~$n$~$ for any natural number $~$n$~$), but we cannot describe it on all of them at once.

To understand this properly, one must understand what it means to be able to 'describe' or 'construct' a function $~$f$~$. This is described in more detail in the sections which follow. But first, a bit of background on why the axiom of choice is interesting to mathematicians.