The axiom of choice is the most esoteric math concept you are likely to encounter. You might think it has no relevance to computing, but you would be wrong.

A Programmers Guide To Theory
First Draft

There is a more recent version of this:

Now available as a paperback and ebook from Amazon.

A Programmers Guide To Theory - NP & Co-NP

Contents

1. What Is Computable?
2. Finite State Machines
3. What is a Turing Machine? 
4. Computational Complexity
5. Non-computable numbers
6. The Transfinite
7. Axiom Of Choice
8. Lambda Calculus
9. Grammar and Torture
10. Reverse Polish Notation - RPN
11. Introduction to Boolean Logic
12. Confronting The Unprovable - Gödel And All That
13. The Programmer's Guide to Fractals
14. The Programmer's Guide to Chaos*
15. Prime Numbers And Primality Testing
16. Cellular Automata - The How and Why
17. Information Theory
18. Coding Theory
19. Kolmogorov Complexity

*To be revised

Before we get started, I need to say that this isn't a rigorous mathematical exposition of the axiom of choice. What it is attempting to do is to give the idea of the "problem" to a non-mathematician, i.e. an average programmer. I also need to add that while there is nothing much about the axiom of choice that a practical programmer needs to know to actually get on with programming it, it does have connections with computer science and computability. The axiom of choice may not be a particularly practical sort of mathematical concern, but it is fascinating and it is controversial. 

Ernst Zermelo

The axiom of choice was introduced by Ernst Zermelo in 1904 to prove what seems a very reasonable theorem. In set theory you often find that theorems that seem to state the obvious actually turn out to be very difficult to prove. In this case the idea that needed a proof was the "obvious" fact that every set can be well ordered. That is, there is an order relation that can be applied to the elements so that every subset has a least element under the order. This is Zermelo's well-ordering theorem. To prove that this is the case Zermelo had to invent the axiom of choice. 

It now forms one of the axioms of Zermelo-Fraenkel set theory which is, roughly speaking, the theory that most would recognize as standard set theory. There are a lot of mathematical results that depend on the axiom of choice, but notice it is an axiom and not a deduction. That is, despite attempts to prove it from simpler axioms, no proof has ever been produced. 

Mathematicians generally distinguish between Zermelo-Fraenkel set theory without the axiom of choice and a bigger theory where more things can be proved with the axiom of choice. 

More cartoon fun at xkcd a webcomic of romance,sarcasm, math, and language

So exactly what is the axiom of choice - it turns out to be surprisingly simple and if you read the cartoon caption you will find that it tells you nearly everything you need to know:

"The axiom of choice allow you to select one element from each set in a collection"

- yes, it really is that simple.

A countable collection of sets is just an enumeration of sets S_i for a range of values of i. The axiom of choice says that for each and every i you can pick an element from the set S_i. It is so obvious that it hardly seems worth stating as an axiom - but it has a hidden depth. 

Another way of formulating the axiom of choice is to say that for any collection of sets there exists a choice function f which selects one element from each set, i.e. f(S_i) is an element of S_i.

Notice that if you have a collection of sets that comes with a natural choice function then you don't need the axiom of choice. The fact you have an explicit choice function means that you have a mechanism for picking one element for each set. The axiom of choice is a sort of reassurance that even if you don't have an explicit choice function one exists - you just don't know what it is. 

Another way to look at this is that the axiom of choice says that a collection of sets for which there is no choice function doesn't exist. 

To Infinity And...

So where is this hidden depth that makes this obvious axiom so controversial?

The answer is, and nearly always is in these cases, infinity.

If you have a finite collection of sets then you can prove that there is a choice function by induction - and you don't need the axiom of choice as it is a theorem of standard set theory. 

Things start to get a little strange when we work with infinite collections of sets. In this case, even if the collection is a countable infinity of sets, you cannot prove that there is a choice function for any arbitrary collection and hence you do need the axiom of choice. That is, to make set theory carry on working you have to assume that there is a choice function in all cases. 

In the case where you have a non-countable infinity of sets then things are more obviously difficult. Some non-countable collections do have obvious choice functions and others don't.

This only way to see what the difficulties are is to look at some simple examples.

First consider the collection of all closed finite intervals of the reals i.e. intervals like the set of points x satisfying a ≤ x ≤ b or [a,b] in the usual notation. This is an infinite and uncountable collection of sets but there is an obvious choice function. All you have to is define F([a,b]) as the mid point of the interval. Given you have found a choice function there is no need to invoke the axiom of choice.

Now consider a collection of sets that sounds innocent enough - the collection of all subsets of the reals. It is clear that you can't use the mid-point of each subset as a choice function because not every subset would have a mid-point. You need  to think of this collection of subsets as including sets that are arbitrary collections of points. Any rule that you invent for picking a point is bound to encounter sets that don't have a point with that property (note; this isn't a rigorous argument). 

Now you can start to see the difficulty in supplying a choice function. No matter what algorithmic formulation you invent some sub-sets just wont have a point that satisfies the specification. You cannot for example use the smallest value in the sub-set to pick a point because open sets don't necessarily have a smallest value using the usual < relationship.  

So now the real problem is made clear - this is a problem to do with computability and this is why it is relevant to computer science. If there is no choice function for the collection of all subsets of the reals then the axiom of choice fails and so do all of the theorems that are proven using it. 

The axiom of choice simply asserts that there is such a function - it doesn't tell you how to find it. 

At the moment it looks as if the weight of mathematical opinion is that we can't find a choice function for the totality of sub-sets of the reals even though the axiom of choice insists that one exists. 

So this is a collection of sets where proof by intimidation (see the cartoon)  simply wouldn't be practical. 

Choice And Computability

If this sounds familiar from what you know of computer science then it should.

The axiom of choice is roughly speaking asserting that the choice function is computable or realizable or whatever you want to call it even if we don't know what it is.

In many cases where something is non-computable we can blame it on the fact that there aren't enough programs to go around. For example, there are only a countable number of programs but there are an uncountable number of real numbers - hence the majority of real numbers aren't computable.

In this case though the problem seems to be that the variability of the sub-sets is such that there isn't sufficient regularity for a program to specify one point in each subset. You might think that the solution is to allow computable functions that return an arbitrary point in the set but it could be that there are sets so complex that there is no formal rule that can pick such a point out. For example consider a set that is composed of just non-computable numbers - how can the choice function return one of them? 

When you realize the connection between the axiom of choice and computability it seems less obvious that you can always exercise an arbitrary choice.