## 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 *∀_{Set}*X*,
AC_{X}*, where *AC_{X}*
names the following equivalent statements *

(1) ∀_{Set}*E*,∀*R*⊂*X*×*E*,
(∀*x*∈*X*, ∃*y*∈*E*, *xRy*) ⇒ (∃*f*∈
*E*^{X}, ∀*x*∈*X*, *xRf*(*x*))*.
*

Or in short : for any graph R, *X* = Dom *R*
⇒ ∃*f* ∈ (Im *R*)^{X}, Gr *f*
⊂ *R*.

(2) *Any product over X of nonempty sets is
nonempty : *(∀*x*∈*X*, *A*_{x}
≠ ∅) ⇒ ∏_{x∈X }*A*_{x} ≠
∅.

(3) ∀_{Fnc} *g*, Im *g* = *X* ⇒ ∃*f* ∈
(Dom *g*)^{X}, *g*০*f*=Id_{X}.

Proof of equivalence :

(1)⇒(2) by *R* = ∐_{x∈X}*
A*_{x} ;

(2)⇒(3) by *A*_{x}=*g*^{•}(*x*)
;

(3)⇒(1) Im π_{0|R} = Dom*R* = *X*
⇒ ∃(*h*×*f*) ∈ *R*^{X},
*h*=Id_{X} ∧Gr *f* ⊂ *R*. ∎

(We also have (2)⇒(1) by *A*_{x} = ⃗*R*(*x*),
and (1)⇒(3) by *R *= ^{t}Gr *g*)
**Finite choice theorem.** If *X* is finite then AC_{X}.

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*≠∅) ⇒ (∃*x*∈*A*, ∃*y*∈*B*,
∃*z*∈*C*, (*x*,*y*,*z*)∈*A*×*B*×*C*)
⇒ *A*×*B*×*C* ≠ ∅.∎
The different statements AC_{X} are related by the following implications:

- If there is an injection from
*Y* to *X* then AC_{X}
implies AC_{Y};
- If both AC
_{X} and AC_{Y} hold then
AC_{X∪Y} and AC_{X×Y} also hold;
- For any family of sets (
*A*_{n}) indexed by *I*, if AC_{I}
and all AC_{An} hold then
AC_{∐i∈I Ai} holds. -
If moreover
*U*=⋃_{i∈I} *A*_{i} satisfies ∃*f* ∈ *I*^{U}, ^{t}Gr *f*
⊂ ∐_{i∈I} *A*_{i} then AC_{U} 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*
⇒ ∏_{A∈E}* A* ≠ ∅*. *

(5) *For any partition **P** of a set **E*,
∃*K*⊂*E*, ∀*A*∈*P*, ∃! : *K*∩*A*

(6) *For any sets **E*,*F*,*G and any
g*: *F* ↠ *G*, {*g*০*f* | *f*
∈ *F*^{E}}=*G*^{E}.

Proofs:

(2)⇒(4) is obvious ;

(4)⇒(5) (*x*∈∏_{A∈P}* A* ∧ *K*
= Im *x*) ⇒ (*K*⊂*E* ∧∀*A*∈*P*,
*x*_{A}∈*A* ∧ ∀*B*∈*P*,
*x*_{B} ∈ *A*∩*B* ⇒ *A*=*B*)

(5)⇒(3) Let *P* = Im *g*^{•}. Then *f* =
(*X*∋*x* ↦ ϵ(*K*∩*g*^{•}(*x*)))
= *g*_{|K}^{−1} ⇒ *g*০*f* =
Id_{X}.

(AC_{E} 1)⇒(6) ∀*h*∈*G*^{E},
(∀*x*∈*E*, ∃*y*∈*F*,
*g*(*y*)=*h*(*x*)) ⇒ (∃*f*∈*F*^{E},
∀*x*∈*E*, *g*(*f*(*x*))=*h*(*x*))

(AC_{G} 3)⇒(6) : ∃*i*∈*F*^{G},
*g*০*i*=Id_{G} ∧ ∀*h*∈*G*^{E},
*i*০*h* ∈ *F*^{E}∧ *g*০*i*০*h*=*h*.

(6)⇒(3) : *E*=*G* ⇒ Id_{E}
∈ {*g*০*f* | *f* ∈ *F*^{E}}. ∎
Remarks:

- (4) ⇒(2) is also easy : ∅ ∉ {
*A*_{x}|
*x*∈*X*} = *E*, then *f* ∈ ∏_{A∈E} *A*
⇒ (*f*(*A*_{x}))_{x∈X}
∈ ∏_{x∈X} *A*_{x}.
- (6) has a converse : (Dom
*g* =*F* ∧ *E*≠∅ ∧
{*g*০*f* | *f*∈*F*^{E}} =
*G*^{E}) ⇒ Im *g* = *G*.