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.