Definition of choice in Lean

Question

In Lean, the axiom choice is implemented as follows:

axiom choice {α : Sort u} : nonempty α → α

Given only the assertion h that α is nonempty, choice h magically produces an element of α.

Now if I read literature (Jech) on set theory and the axiom of choice:

Axiom of Choice (AC). Every family of nonempty sets has a choice function.

If S is a family of sets and ∅ not in S, then a choice function for S is a function f on S such that f(X) ∈ X for every X ∈ S.

To me, these things don't seem to be equivalent. Can someone elaborate on this?

Answer 1

The axiom choice in Lean is indeed not the same as the axiom of choice in set theory. The axiom choice in Lean doesn't really have a corresponding statement in set theory. It says that there is a function that takes a proof that some type α is nonempty, and produces an inhabitant of α. In set theory, we cannot define functions that take proofs as arguments since proofs are not objects in set theory; they are in the layer of logic on top of that.

That said, the two choice axioms are not completely unrelated. From Lean's axiom choice, you can prove the more familiar axiom of choice from set theory, which you can find here:

theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop}
        (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x) :=
  ⟨_, fun x => choose_spec (h x)⟩

In other parts of the library, other equivalent statements to the axiom of choice are proven, like the one stating that every surjective function has a right inverse.

Maybe the statement closest to the version of the axiom of choice you quoted is the following:

theorem axiomOfChoice' {α : Sort u} {β : α → Sort v} (h : ∀ x, Nonempty (β x)) :
        Nonempty (∀ x, β x) :=
  ⟨fun x => Classical.choice (h x)⟩

In words, this says that given a family of nonempty types (sets), the type of choice functions is nonempty. As you can see the proof is immediate from Lean's choice.