Getting the Heavy Maths out the Way: Definitions

Intuitively, the of choice states that, given a collection of , there is a which selects a single element from each of the sets.

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

In , $${\forall }_X([{\forall }_{Y\in X}Y\ne \varnothing ]\Rightarrow \left[\exists (f:X\to \bigcup _{Y\in X}Y)\left({\forall }_{Y\in X}{\exists }_{y\in Y}f\right(Y)=y)\right])$$

Axiom Unnecessary for Finite Collections of Sets

For a $X$ containing only non-empty sets, the axiom is actually provable (from the of set theory ZF), and hence does not need to be given as an . In fact, even for a finite collection of possibly infinite non-empty sets, the axiom of choice is provable (from ZF), using the . 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\left(Y_1\right)=y_1$, $f\left(Y_2\right)=y_2$ and $f\left(Y_3\right)=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 number of sets $Y_1,Y_2,Y_3,\dots$. 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.