What is the computational substance of the axiom of choice?

tailcalled

This post is also available on my Substack.

I feel like online discussions of the axiom of choice either get impenetrably technical, or uselessly vague. Through realizability semantics, I’ve gotten an intuition for the axiom of choice that I want to share in elementary terms (without getting all the way into the effective topos). I will take a somewhat eccentric approach to it, showing the everyday utility of the axiom of choice, as well as the implications from a constructive rather than a classical point of view.

What is it

The post would probably be incomplete without sharing the definition of the axiom of choice, even though its technical specifics will be unclear to readers for now:

Axiom of Choice: For every family A_i of inhabited^[1] sets, there is a function f : I → ⋃_iA_i mapping each index i to a member f(i) ∈ A_i.

I think the nuances of this are hard to understand without seeing how it is used in practice.

A proof using choice

Let’s start with a simple proof that uses the axiom of choice, admittedly in an “overkill” way (the theorem is easily proven without choice):

Theorem: There are functions numerator(x) and denominator(x) that map rational numbers x to integers such that x = numerator(x)/denominator(x).

Before we get into the proof, first recall the definition of the rational numbers ℚ: They can be represented by fractions a/b of integers a and b such that b ≠ 0, and two rational numbers a/b and c/d are considered equal if ad = cb. That rational numbers are represented as fractions should make the above theorem sound almost trivial.

Still, it’s not too easy. You might think you could just map numerator(a/b) = a, denominator(a/b) = b. However, these “functions” are not well-defined; 2/4 and 3/6 are equal as rational numbers, and so the functions ought to give equal results on them, yet e.g. the numerators of them are 2 and 3 respectively.

This is the gap between mere existence (for any rational x, there exists a and b such that x = a/b) and functional relationships that the axiom of choice serves to solve. First, the setup:

Lemma: For any rational number x, the set parts(x) = { (a, b) ∈ ℤ² | x = a/b } is inhabited.

Proof: For a/b, we have the member (a, b) ∈ parts(a/b). ∎

We now have the conditions necessary to apply the axiom of choice. The rest of the proof is fairly straightforward:

Proof of the main theorem: By the axiom of choice (set I = ℚ, A_i = parts(i)), there is a function mapping each rational number x to a pair of numbers (a(x), b(x)) such that x = a(x)/b(x). Set numerator(x) = a(x) and denominator(x) = b(x). ∎

This proof is nonconstructive. We know that e.g. numerator(2/4) = numerator(3/6), because otherwise numerator would not be a function. However, we don’t know whether the axiom of choice picked the numerator to be 1, 2, 3, a billion, Graham’s number, or some even more monstrous number.

Sidenote: Axiom of choice vs rules for choosing

The axiom of choice is overkill here. We could instead have used less-heavy machinery: Writing x in lowest terms, and setting the numerator and denominator to those. This would have the advantage of being constructive, with it being clear what the numerator and denominator of an arbitrary rational number is. However, it requires a bit of extra care to prove that the lowest terms are unique.

“Lowest terms” gives a specific rule for picking members from parts(x), making the axiom of choice unnecessary. In some cases in math (for instance when we are working with an essentially-arbitrary set which we know nothing about), there is no rule at all that we can use for choosing the elements we want, and thus the axiom of choice becomes necessary there.

Representations and Diaconescu’s theorem

Why might one not accept the axiom of choice? One (unconventional) answer is if one wants everything in math to be computable. This is achievable if one uses only constructive reasoning, but the axiom of choice is not constructive, and in fact Diaconescu’s theorem shows that the axiom of choice implies the existence of a function containing the solution to arbitrary mathematical problems.^[2]

Let’s pick a family of problems P_n. We could for instance let n range over all statements describable in the language of arithmetic, and let P_n denote “the nth statement is true”. This family would include many unsolvable problems, such as every instance of the halting problem, as well as many open problems including the Collatz conjecture.

Theorem: If the axiom of choice holds, there is a function dec : N → { false, true } such that dec(n) is true if and only if P_n holds.

Proof:

The trick is that the axiom of choice needs to hand us a function that respects equality of representations, so we will deliberately engineer representations L_n and R_n that are equal if and only if P_n is true.

More specifically, if P_n is true, we want L_n = R_n = { 0, 1 }, while if P_n is false, we want L_n = { 0 }, R_n = { 1 }. However, we cannot just declare this by fiat as that would require us to be able to inspect whether P_n is true. Instead, we will make use of the fact that we can always carve a subset out of a set using any property, even one we cannot decide:

L_n = { x ∈ { 0, 1 } | x = 0 or P_n }

R_n = { x ∈ { 0, 1 } | x = 1 or P_n }

Now, the fact that they are sets means that we don’t automatically have any way of checking whether they are equal. This is where we need the axiom of choice. Notice that L_n and R_n are always inhabited, no matter P_n, by 0 and 1 respectively. This sets them up nicely for the axiom of choice:

I = { L_n | n ∈ N } ∪ { R_n | n ∈ N }

A_i = i

If we apply the axiom of choice, we get a function f such that f(L_n) ∈ L_n and f(R_n) ∈ R_n. But notice that if f(L_n) = f(R_n), we must have that L_n and R_n overlap, and therefore they must be equal and P_n holds. Meanwhile if f(L_n) ≠ f(R_n), then L_n ≠ R_n and P_n fails. So we can define the function dec(n) by f(L_n) = f(R_n). ∎

Representations and countable choice

We have to be careful that we don’t throw out the baby with the bathwater. Consider for instance the following theorem:

Theorem: For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.

This can be proved using the axiom of choice on the fact that there exist rational numbers close to x. However, without the axiom of choice, there are universes in which this statement fails, which seems pretty pathological.

It turns out that for our computable universe, though, there is a restricted axiom of choice that allows the above theorem to go through. To understand this restricted choice, we should look closer at our proof for the numerator/denominator of the rationals.

For rational numbers x, we could show that there existed integers a and b such that x = a/b. Our proof was constructive in the sense that it contained an algorithm for exhibiting a and b (namely, pick them from the fraction representation). The algorithm was not a function because the rational numbers had multiple representations, but that doesn’t prevent it from being a perfectly valid algorithm.

However, some sets have a single canonical representation for their members; in particular, natural numbers can be represented with numerals 0, 1, 2, … . This forces algorithms that take natural numbers as input to give well-defined outputs, because there is no nondeterminism in the inputs that can risk causing nondeterminism in the outputs.

Thus, any algorithm that witnesses an ℕ-indexed existence statement also witnesses an ℕ-indexed function. Therefore we computationally have:

Axiom of countable choice: For every family A_n of inhabited sets, there exists a function f : ℕ → ⋃_nA_n mapping n to f(n) ∈ A_n.

Conclusion

So what’s so computationally difficult about the axiom of choice? All of the computational difficulty lies in the one fact: One mathematical object may have many representations, and the choice function is forced to be consistent over them. As we saw with numerator/denominator of the rationals, and Diaconescu’s theorem, in most cases where the axiom of choice is used, this representation-challenge isn’t incidental to its use, it’s the whole point of using it.

This is intentionally far from the standard introduction to choice, which would have talked about pairs of socks and involved duplicating balls. I feel like my introduction gives some information that is largely complementary to the standard introduction, though people who focus on classical mathematics may very well disagree.

Andrej Bauer, Five Stages of Accepting Constructive Mathematics (Bulletin of the AMS, 2017) — the best gentle on-ramp to constructive reasoning, including a discussion of what choice does and doesn’t mean constructively.
Per Martin-Löf, 100 Years of Zermelo’s Axiom of Choice: What Was the Problem With It? — explains why choice is a theorem in intensional type theory but becomes problematic exactly when quotients/extensionality enter, which is the representation issue in this post from another angle.
Fred Richman, Constructive Mathematics Without Choice — what analysis looks like when you drop even countable choice, and which theorems (like the rational-approximation one above) survive.
Andrej Bauer, Notes on Realizability (lecture notes) — the realizability semantics behind this post, developed carefully but from the ground up.
Andrej Bauer, Realizability as the Connection Between Computable and Constructive Mathematics — shorter survey version, good if the lecture notes are too much.
R. Diaconescu, Axiom of Choice and Complementation (Proc. AMS, 1975), and Goodman & Myhill, Choice Implies Excluded Middle (1978) — the original sources for the theorem above.
Errett Bishop & Douglas Bridges, Constructive Analysis — the classic text; note how sequences-with-moduli sidestep the need for choice in many places.
Troelstra & van Dalen, Constructivism in Mathematics (2 vols.) — the encyclopedic reference for constructive logic, choice principles (countable choice, dependent choice, AC-NN), and realizability.
The nLab articles on axiom of choice, countable choice, and the presentation axiom (CoSHEP) — the presentation axiom is precisely the statement that every set is covered by one with “canonical representations,” generalizing why countable choice held above.
Horst Herrlich, Axiom of Choice (Springer Lecture Notes) — the classical side: a tour of what breaks with and without choice.
Martin Hyland, The Effective Topos (1982) — for readers who want to go all the way into the semantics this post deliberately stopped short of.

^{^}
Inhabited means that it has a member, is “nonempty”. I avoid the term “nonempty” and prefer the term “inhabited” because the former introduces extra negations.
^{^}
I say this is an unconventional motivation because usually one accepts excluded middle, i.e. P or not P. Excluded middle rules out computability, and the usual statement of Diaconescu’s theorem would be phrased as proving excluded middle. However, even in computable semantics, individual instances of excluded middle are technically true; it is only once it becomes an infinite family of claims that it becomes irrecoverably problematic.

[-]Svyatoslav Usachev9d20

I am surprised that the following theorem requires axiom of choice:

It seems to me that it has a constructive proof with computable x̂, it goes like this:

To calculate x̂(n):

Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).

Here we have an algorithm that calculates x̂(n) in a finite number of steps for any particular x and n, so x̂ is computable.

[-]tailcalled8d*20

Do note the followup that axiom of countable choice is constructively computable and therefore the choice-using proof goes through computably. The universe that kills countable choice is not the computable universe RT(K₁), but rather the continuous universe Sh(ℝ), where everything is a continuous function out of the real numbers. The failure of "For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x." in that universe translates to the failure of "For any continuous function x : ℝ → ℝ, there exists a continuous family of sequences x̂ : ℝ×ℕ → ℚ converging to x.". The trouble with that statement is that ℚ is discrete, so x̂ is forced to be constant in its first parameter.

Your proof is perfectly valid in classical math with excluded middle. However, classical math lacks the computational substance that this post centers around.

Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.

"While |x| > a" requires excluded middle over |x| > a. Constructively, the inequality operator for real numbers only supports a weaker form of excluded middle called comparison: if x < y then x < z or z < y. Not a huge problem for this part of the proof as you could just case split by |x| > a or |x| < a+1.

Though if you do this, because these are overlapping conditions, its no longer deterministic, so a isn't a function of x.

You essentially just want a rational upper bound for x, though. This does exist (not as a function as that would be discontinuous) and you don't need to do an algorithm for figuring it out. (Under the hood in RT(K₁), this is essentially because representations of real numbers come packaged with an upper and lower rational bound.)

Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).

"Pick the half that contains x" requires excluded middle too, for comparing the midpoint with x. Again you could probably add an epsilon of leeway to let comparison go through, but then there's no functional relationship, and you need countable choice to pin down x̂.

26