AxiomeAxiomes de ZF

Axiome du choix (ZFC) ⋆

⋆ Axiome du choix

Cet axiome ne fait pas partie de $\mathsf{ZF}$ . Il est indépendant des autres : ni lui ni sa négation ne se démontrent dans $\mathsf{ZF}$ , si celle-ci est cohérente (Gödel, 1938 ; Cohen, 1963).

C'est la forme donnée par Zermelo en 1908 à l'axiome du choix : elle ne parle que d'appartenance, et peut donc être énoncée avant que les applications soient définies.

Énoncé

Pour tout ensemble $\mathcal F$ d'ensembles non vides et deux à deux disjoints, il existe un ensemble $C$ qui rencontre chaque élément de $\mathcal F$ en exactement un point : $\forall A \in \mathcal F\ \ \exists!\, c\ \ (c \in A \wedge c \in C).$

Remarque

Une fois les applications définies, il équivaut à la forme usuelle, comme le montre le nœud Formes de l'axiome du choix : pour toute famille $(A_i)_{i \in I}$ d'ensembles non vides, il existe une application $f$ de domaine $I$ telle que $f(i) \in A_i$ pour tout $i$ . Ses formes affaiblies, comme le choix dénombrable, apparaissent au nœud ℕ.

Remarque

La formule $\exists!\, c\ \varphi$ , « il existe un unique $c$ tel que $\varphi$ », abrège $\exists c\, \big(\varphi \wedge \forall d\, (\varphi[d/c] \to d = c)\big)$ .

Repose sur

Langage de ZF

Sert à

Aucune fiche de ce graphe ne l'utilise encore.