## 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:

• If there is an injection from Y to X then ACX implies ACY;
• If both ACX and ACY hold then ACXY and ACX×Y also hold;
• For any family of sets (An) indexed by I, if ACI and all ACAn hold then ACi∈I Ai holds.
• If moreover U=⋃i∈I Ai satisfies ∃fIU, tGr f ⊂ ∐i∈I Ai then ACU holds.
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.

Proofs:
(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}. ∎

Remarks:

• (4) ⇒(2) is also easy : ∅ ∉ {Ax| xX} = E, then f ∈ ∏AE A ⇒ (f(Ax))xX ∈ ∏xX Ax.
• (6) has a converse : (Dom g =FE≠∅ ∧ {gf | fFE} = GE) ⇒ Im g = G.
 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