Axiome de la théorie des ensembles affirmant que pour toute famille d'ensembles non vides il existe une fonction de choix qui sélectionne un élément dans chaque ensemble ; souvent noté AC et indépendant des axiomes de Zermelo–Fraenkel (ZF), son acceptation entraîne des conséquences non constructives.

Principe

À partir d'une collection d'ensembles non vides, on peut choisir simultanément un représentant dans chaque ensemble ; cela permet des constructions qui ne peuvent pas toujours être réalisées par des règles explicites ou des algorithmes dans ZF seul.

Démonstration

En pratique, AC permet de former un ensemble de représentants pour une famille arbitraire (par exemple choisir une base pour chaque espace vectoriel), même lorsqu'aucune règle définissable ne choisit les représentants de manière uniforme.

Mauvaise application

Considérer AC comme une procédure constructive est erroné : il garantit l'existence de fonctions de choix mais ne fournit pas, en général, de sélections explicites ou d'algorithmes ; supposer des conséquences constructives (comme le choix définissable) sans hypothèses supplémentaires est incorrect.

Conséquence

Conduit à de nombreux résultats standards (théorème de Tychonoff pour produits arbitraires, existence de bases de tout espace vectoriel, équivalences avec le lemme de Zorn) mais aussi à des objets contre‑intuitifs (ensembles non mesurables, paradoxes de type Banach–Tarski) sous logique classique.

Inversion

Rejeter AC (travailler en ZF sans AC) empêche certaines preuves d'existence et peut restaurer la constructivité et la mesurabilité dans certains modèles ; de nombreux théorèmes équivalents à AC échouent ou doivent être reformulés, montrant le rôle central de l'axiome.

Limite

L'énoncé porte sur des familles arbitraires d'ensembles non vides ; il ne précise pas la définissabilité, l'efficacité ou les bornes de cardinalité des fonctions de choix. En contextes constructifs ou calculables, des principes de choix affaiblis ou des choix témoins sont préférables.

Tension sémantique

Conflit avec les philosophies constructives et calculables qui exigent des sélections explicites ; la tension entre accepter une existence non constructive puissante et préserver le contenu algorithmique ou définissable est centrale en fondements.

Synthèse

L'axiome du choix est un postulat d'existence permettant la sélection dans des familles arbitraires d'ensembles non vides ; il est puissant et non constructif, équivalent à de nombreux principes classiques, produisant à la fois théorèmes usuels et objets pathologiques si on le laisse sans restriction.