2.12. Axiom of choice

The axiom of choice is a statement with several equivalent formulations, named as an «axiom» because it cannot be deduced from other axioms of set theory but it «feels true» and, when taken as an axiom, it does not increase the risk of contradictions but has convenient consequences. But we will actually not need it in the rest of this work.

Axiom of choice (AC). It says SetX, ACX, where ACX names the following equivalent statements
(1) ∀SetE,∀RX×E, (∀xX, ∃yE, xRy) ⇒ (∃fEX, ∀xX, xRf(x)).
Or in short : for any graph R
, X = Dom R ⇒ ∃f ∈ (Im R)X, Gr fR.
(2) Any product over X of nonempty sets is nonempty : (∀xX, Ax ≠ ∅) ⇒ ∏xX Ax ≠ ∅.
(3) ∀Fnc g, Im g = X ⇒ ∃f ∈ (Dom g)X, gf=IdX.

Proof of equivalence :
(1)⇒(2) by R = ∐xX Ax ;
(2)⇒(3) by Ax=g(x) ;
(3)⇒(1) Im π0|R = DomR = X ⇒ ∃(h×f) ∈ RX, h=IdX ∧Gr fR. ∎
(We also have (2)⇒(1) by Ax = R(x), and (1)⇒(3) by R = tGr g)

Finite choice theorem. If X is finite then ACX.

A rigorous proof for the general case will need a formal definition of finiteness. Now let us only give a schema of proofs, one for each explicit number of elements of X, using expression (2): for example with 3 elements, for each triple of sets (A,B,C),
(A≠∅∧B≠∅∧C≠∅) ⇒ (∃xA, ∃yB, ∃zC, (x,y,z)∈A×B×C) ⇒ A×B×C ≠ ∅.∎

The different statements ACX are related by the following implications:

The proofs are easy and left as an exercise to the reader.

Theorem. The following statements are equivalent to the axiom of choice:
(4) Any set E of nonempty sets has a choice function: ∅ ∉ E ⇒ ∏AE A ≠ ∅.
(5) For any partition P of a set E, ∃KE, ∀AP, ∃! : KA
(6) For any sets E,F,G and any g: FG, {gf | fFE}=GE.

(2)⇒(4) is obvious ;
(4)⇒(5) (x∈∏AP AK = Im x) ⇒ (KE ∧∀AP, xAA ∧ ∀BP, xBABA=B)
(5)⇒(3) Let P = Im g. Then f = (Xx ↦ ϵ(Kg(x))) = g|K−1gf = IdX.
(ACE 1)⇒(6) ∀hGE, (∀xE, ∃yF, g(y)=h(x)) ⇒ (∃fFE, ∀xE, g(f(x))=h(x))
(ACG 3)⇒(6) : ∃iFG, gi=IdG ∧ ∀hGE, ihFEgih=h.
(6)⇒(3) : E=GIdE ∈ {gf | fFE}. ∎


Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
2.3. Tuples, families
2.4. Boolean operators on families of sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
2.7. The powerset
2.8. Injectivity and inversion
2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations and partitions
2.12. Axiom of choice
2.13. Notion of Galois connection
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations