Axiom of well-ordering

Well-ordering theorem

For any set X, there is a binary relation R which well-orders X. This means R is a linear order on X such that every nonempty subset of X has a member which is minimal under R.

\forall X\exists R(R\;{\mbox{well-orders))\;X).

Given axioms 1–8, there are many statements provably equivalent to axiom 9, the best known of which is the axiom of choice.

Axiom of Choice (AC)

Let X be a set whose members are all non-empty. Then there exists a function f from X to the union of the members of X, called a "choice function", such that for all Y ∈ X one has f(Y) ∈ Y.

Since the existence of a choice function when X is a finite set is easily proved from axioms 1–8, AC only matters for certain infinite sets. AC is characterized as nonconstructive because it asserts the existence of a choice set but says nothing about how the choice set is to be "constructed". Much research has sought to characterize the definability (or lack thereof) of certain sets whose existence AC asserts.