L'axiome du choix global affirme qu'il existe une fonction de choix global τ, c'est-à-dire une fonction telle que, pour tout ensemble non-vide z, τ(z) est un élément de z.
L'axiome du choix global ne peut pas être exprimé directement dans le langage de ZFC (théorie des ensembles de Zermelo–Fraenkel avec l'axiome du choix), car la fonction de choix τ est une classe propre et il n'est pas possible de quantifier sur les classes dans ZFC. Il peut être exprimé en ajoutant une nouvelle fonction τ dans le langage de ZFC, avec la propriété que τ est une fonction de choix globale. C'est une extension conservatrice de ZFC : tout énoncé ne faisant pas intervenir le symbole τ et qui est démontrable dans cette extension est démontrable dans ZFC (Fraenkel, Bar-Hillel & Levy 1973, p.72). D'autre part, Gödel a montré que, en supposant l'axiome de constructibilité, on peut définir une fonction de choix explicite (bien qu'un peu compliquée) τ dans le langage ZFC, donc dans un certain sens, l'axiome de constructibilité implique celui de choix global.
Dans le langage de la théorie des ensembles de von Neumann–Bernays–Gödel (NBG) et de la théorie des ensembles de Morse-Kelley, l'axiome du choix global peut être exprimé directement (Fraenkel, Bar-Hillel & Levy 1973, p.133), et est équivalent à diverses autres formulations :
- Chaque classe d'ensembles non-vides a une fonction de choix.
- V \ {∅} a une fonction de choix (où V est la classe de tous les ensembles).
- Il y a un bon ordre de V.
- Il y a une bijection entre V et la classe de tous les nombres ordinaux.
Dans la théorie des ensembles de von Neumann–Bernays–Gödel, l'axiome du choix global n'ajoute pas de conséquence sur les ensembles (qui ne sont pas des classes propres) au-delà de ce qui peut être déduit à partir de l'axiome du choix ordinaire.
L'axiome du choix global est une conséquence de l'axiome de limitation de taille.
