The axiom of choice

The axiom of choice was something I found quite complicated as an undergraduate; it was summarised as “you can make infinitely many choices at the same time” but because I didn’t really know much about set theory it took me a while before this description made any sense.

In Lean’s type theory, the situation is much simpler (at least in my mind). There are two universes in Lean (at least for the purposes of this course) – Prop and Type. The Prop universe is for proofs, and the Type universe is for data. The axiom of choice is a route from the Prop universe to the Type universe. In other words, it is a way of getting data from a proof.

nonempty X

If X : Type then nonempty X : Prop is the true-false statement asserting that X is nonempty, or equivalently, that there’s a term of type X. For example here’s part of the API for nonempty:

import tactic

example (X : Type) : (∃ x : X, true) ↔ nonempty X :=
begin
  exact exists_true_iff_nonempty
end

This example shows that given a term of type nonempty X, you can get a term of type ∃ x : X, true (i.e., “there exists an element of X such that a true statement is true”). We would now like to go from this to actually get a term of type X! In constructive mathematics this is impossible: because h lives in the Prop universe, Lean forgot how it was proved. However in classical mathematics we can pass from the Prop universe to the Type universe with classical.choice h, a term of type X. This gives us a “noncomputable” term of type X, magically constructed only from the proof h that X was nonempty. Mathematically, “noncomputable” means “it exists, but we don’t actually have an algorithm or a formula for it”. This is a subtlety which is often not explicitly talked about in mathematics courses, probably because it is often not relevant in a mathematical argument.

You might wonder what the code for this classical.choice function looks like, but in fact there isn’t any code for it; Lean simply declares that classical.choice is an axiom, just like how in set theory the axiom of choice is declared to be an axiom.

When I first saw this axiom, it felt to me like it was way weaker than the set theory axiom of choice; in set theory you can make infinitely many choices of elements of nonempty sets all at once, whereas in Lean we’re just making one choice. But later on I realised that in fact you could think of it as much stronger than the set theory axiom of choice, because you can interpret classical.choice as a function which makes, once and for all, a choice of an element of every single nonempty type, so it easily implies the usual set-theoretic axiom of choice.

classical.some

In my experience, the way people want to use the axiom of choice when doing mathematics in Lean is to get an element of X not from a hypothesis ∃ x : X, true, but from a hypothesis like ∃ x : X, x^2 = 2 or more generally ∃ x : X, p x where p : X → Prop is a predicate on X. The way to do this is as follows: you run classical.some on h : ∃ x : X, p x to get the element of X, and the proof that this element satisfies p is classical.some_spec h. Here’s a worked example.

import analysis.complex.polynomial -- import proof of fundamental theorem of algebra

open_locale polynomial -- so I can use notation ℂ[X] for polynomial rings

open polynomial -- so I can write `X` and not `polynomial.X`

noncomputable theory -- we are not supplying algorithms for being able
-- to compute what is about to happen

def f : ℂ[X] := X^5 + X + 37 -- a random polynomial

theorem f_has_a_root : ∃ (z : ℂ), f.is_root z :=
begin
  apply complex.exists_root, -- the fundamental theorem of algebra
  -- it remains to show that f has degree > 0
  sorry -- proof omitted (more annoying than you would think!)
end

-- let z be a root of f
def z : ℂ := classical.some f_has_a_root

-- proof that z is a root of f
theorem z_is_a_root_of_f : f.is_root z :=
begin
  exact classical.some_spec f_has_a_root,
end