2.10. Axiome du choix

Propriétés de la composition curryfiée

Proposition. ∀Set E,F,G, ∀f ∈ FE,
  1. Im f = F ⇒ Inj(GF ∋ g ↦ g⚬f)
  2. (Inj(GF ∋ g ↦ g⚬f) ∧ ∃≥2:G) ⇒ Im f = F
  3. (Inj f ∧ G ≠ ∅) ⇒ {g⚬f | g∈GF} = GE
  4. ({g⚬f | g∈GF} = GE ∧ ∃≥2:G) ⇒ Inj f
  5. (E ⊂ F ∧ G ≠ ∅) ⇒ {g|E | g∈GF} = GE
  6. (Inj f ∧ E ≠ ∅) ⇒ ∃g∈EF, g⚬f = IdE
Preuves :
1. fait en 2.9 ; preuve plus simple: ∀g,h∈GF, (∀x∈E, g(f(x)) = h(f(x))) ⇔ (∀y∈F, g(y) = h(y)) ⇔ g=h
2. ( ) ⇒ ∃z≠z′∈G, (F∋y ↦ z)⚬f = (F∋y ↦ (y ∈ Im f ? z : z′))⚬f ∴ (∀y∈F, y ∈ Im f ∨ z = z′) ∴ Im f = F
3. Inj f ⇒ ∀z∈G, ∀h∈GE, h = (F ∋ y ↦ (y ∈ Im f ? h(f -1(y)) : z))⚬f
4. ∀z≠z′∈G, ∀x∈E, ∀g∈GF, g⚬f = (E∋y↦ (y = x ? z : z′)) ⇒ ∀y∈E, f(y) = f(x) ⇒ g(f(y)) = g(f(x)) = z ⇒ y = x.
5. et 6. sont des cas particuliers de 3.∎

Le cas G = V2 donne les propriétés suivantes de h = (℘(F)∋B↦ f⋆(B)) :

Im f = F ⇔ Inj h
Inj f ⇔ Im h = ℘(E)

De plus {f[A]|A ⊂ E} = ℘(Im f) car ∀B ⊂ Im f, f[f⋆(B)] = B.

Proposition. Pour tous ensembles E, F et toute fonction g de domaine F,

  1. Inj g ⇒ Inj(FE ∋ f ↦ g⚬f)
  2. (Inj(FE ∋ f ↦ g⚬f) ∧ E ≠ ∅) ⇒ Inj g
  3. ∀SetG, ({g⚬f | f∈FE} = GE ∧ E ≠ ∅) ⇒ Im g = G.
Preuves:
1. ∀f,f'∈FE, (Inj g ∧ ∀x∈E, g(f(x)) = g(f'(x))) ⇒ (∀x∈E, f(x) = f'(x)).
2. ∀y,z∈F, g(y) = g(z) ⇒ g⚬(E ∋ x ↦ y) = g⚬(E ∋ x ↦ z) ⇒ (∀x∈E, y = z) ⇒ (E ≠ ∅ ⇒ y = z).
3. (laissé en exercice au lecteur).∎

Axiome du choix sur un ensemble (ACX)

L'axiome du choix (AC) est un énoncé exprimable dans toute théorie des ensembles avec ensemble des parties, qui «sent vrai» et est commode à accepter comme axiome; mais nous n'en aurons en fait pas besoin dans le reste de ce travail.

Il a plusieurs formulations équivalentes (en clair, c'est le nom commun de ces énoncés équivalents). Les principales ont le même format (∀SetX, ACX) où ACX désignifie l'une des formules équivalentes suivantes, de variable libre X dans la classe des ensembles:

(AC3X) et (AC4X) sont plus souvent utilisés dans les cas d'égalité (respectivement X = Im g et X = Dom R) qui sont équivalents aux cas généraux, les preuves d'équivalence fonctionnant de la même manière: Autres déductions faciles

Dépendences entre divers ACX

Une grande réussite de la logique mathématique a été de prouver l'indépendance de AC par rapport au reste de la théorie des ensembles: même le très fort système ZF, s'il est cohérent, ne peut ni le prouver ni le réfuter, car chaque univers où AC est vrai en inclut un autre où il est faux, et vice versa. Cela sera commenté plus en détail en 5.5 (sans les détails des preuves qui sont beaucoup trop difficiles).
Les diverses manières dont AC peut être faux dans différents univers peuvent être en partie triées en spécifiant quels X satisfont ACX. Les différents ACX sont liés par les implications suivantes: Les preuves sont faciles et laissées en exercice au lecteur.

Théorème du choix fini. Si X est fini alors ACX.

Ce sera facilement déductible du cas des singletons AC{x} (qui est trivial) et de la préservation par union binaire (ACX ∧ ACY) ⇒ ACX∪Y lorsque la finitude sera formellement définie (4.6).
Donnons seulement déjà un schéma de démonstrations, une pour chaque nombre explicite d'éléments de X. Par exemple le cas de X avec 3 éléments se réduit à (AC2V3) dont la preuve peut s'écrire

∀SetX,Y,Z, (X ≠ ∅ ∧ Y ≠ ∅ ∧ Z ≠ ∅) ⇒ (∃x∈X, ∃y∈Y, ∃z∈Z, (x,y,z) ∈ X×Y×Z) ⇒ X×Y×Z ≠ ∅.∎

Autres énoncés simplement équivalents à AC

Théorème. Les énoncés suivants sont équivalents à l'axiome du choix:
(AC5) Tout ensemble E d'ensembles non-vides a une fonction de choix: ∅ ∉ E ⊂ Set ⇒ ∏ IdE ≠ ∅.
(AC6) Pour toute partition P d'un ensemble E, ∃K⊂E, ∀A∈P, ∃!: K∩A.
(AC7) Pour tous ensembles E,F,G et tout g: F ↠ G, {g⚬f | f ∈ FE} = GE.

Preuves:
(AC2)⇒(AC5) est évident;
(AC5)⇒(AC6) : (x∈ ∏ IdP ∧ K = Im x) ⇒ (K⊂E ∧ ∀A∈P, xA ∈ K∩A ∧ ∀B∈P, xB ∈ A ⇒ A∩B ≠ ∅ ⇒ A = B)
(AC6)⇒(AC3) : ∀Fnc g, X ⊂ Im g ⇒ ∃K⊂Dom g, (∀A∈ Im(g•), ∃! : K∩A) ∴ ∃f ∈ (Dom g)X, (∀x∈X, {f(x)} = K∩g•(x)) ∴ g⚬f = IdX.
(AC1E)⇒(AC7) : ∀h∈GE, (∀x∈E, ∃y∈F, g(y) = h(x)) ⇒ (∃f∈FE, ∀x∈E, g(f(x)) = h(x))
(AC3G)⇒(AC7) : ∃j∈FG, g⚬j = IdG ∴ ∀h∈GE, j⚬h ∈ FE ∧ g⚬j⚬h = h.
(AC7)⇒(AC3) : ∀SetX, ∀Fncg, X = Im g ⇒ IdX ∈ XX = {g⚬f | f ∈ (Dom g)X}. ∎

Note: (AC5)⇒(AC2) est aussi facile : ∅ ∉ Im A ⊂ Set ⇒ ∃f ∈ ∏ IdIm A, f⚬A ∈ ∏ A.

Il existe bien d'autres énoncés équivalents à AC, qui ne seront pas utilisés dans cet exposé, et pour lesquels les preuves d'équivalence sont beaucoup plus difficiles. Les lecteurs intéressés peuvent les trouver ailleurs.

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
2.1. Premiers axiomes de théorie des ensembles
2.2. Principe de génération des ensembles
2.3. Curryfication et uplets
2.4. Quantificateurs d'unicité
2.5. Familles, opérateurs booléens sur les ensembles
2.6. Graphes
2.7. Produits et ensembles des parties		 2.8. Injections, bijections
2.9. Propriétés des relations binaires ⇦
2.10. Axiome du choix
⇨ Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
⇨ 3. Algebra - 4. Arithmetic - 5. Second-order foundations

En anglais : Set theory and Foundations of Mathematics : Axiom of choice