L’axiome d’extensionnalité est l’un des axiomes-clés de la plupart des théories des ensembles, en particulier, des théories des ensembles de Zermelo, et de Zermelo-Fraenkel (ZF). Il énonce essentiellement qu'il est suffisant de vérifier que deux ensembles ont les mêmes éléments pour montrer que ces deux ensembles sont égaux, au sens où ils ont les mêmes propriétés, aucune propriété ne permettra de distinguer un ensemble de l'autre. Dit d'une façon plus approximative^[1], il affirme que quelle que soit la façon dont on définit un ensemble, celui-ci ne dépend que de son extension, les éléments qui lui appartiennent, et pas de la façon dont il a été défini.

Cet axiome peut paraître évident pour la notion intuitive d'ensemble, mais a des conséquences importantes sur la complexité de l'égalité dans la théorie. Pour vérifier l'égalité de deux ensembles, on est amené, à cause par exemple du schéma d'axiomes de compréhension, à vérifier des équivalences entre énoncés de complexité arbitraire, ces énoncés eux-mêmes pouvant utiliser l'égalité entre ensembles (rappelons qu'il n'y a que des ensembles dans les théories des ensembles usuelles).

L’axiome est donc intimement lié à la notion d’égalité de deux ensembles. Il permet de montrer l’unicité d’ensembles caractérisés par la donnée de leurs éléments, tels l’ensemble vide, les singletons, les paires, l'ensemble des parties d'un ensemble…

L’égalité peut être introduite en théorie des ensembles, de diverses façons. Actuellement, elle est le plus souvent considérée comme une relation primitive, axiomatisée au niveau logique. La théorie des ensembles est alors une théorie énoncée dans le langage du calcul des prédicats égalitaire du premier ordre, construit sur la seule relation d'appartenance.

Dans ce cas, l'axiome d'extensionnalité s'énonce ainsi :

∀A ∀B [ ∀x (x ∈ A ⇔ x ∈ B) ⇒ A = B ].

Ce qui revient à dire que : si tout élément de l'ensemble A est aussi un élément de B, et si tout élément de l'ensemble B appartient à l'ensemble A, alors les deux ensembles A et B sont égaux.

On sait que l'inclusion entre deux ensembles, notée A ⊂ B^[2] ou A⊆ B se définit par :

A ⊂ B    signifie    ∀ x (x ∈ A ⇒ x ∈ B)

On en déduit donc une autre formulation de l'axiome d'extensionnalité, qui est d'ailleurs celle originale de Ernst Zermelo :

(A ⊂ B et B ⊂ A) ⇒ A = B.

Cette dernière formulation justifie l'utilisation courante de la double inclusion pour montrer une égalité entre deux ensembles : pour montrer que deux ensembles A et B sont égaux, il suffit de montrer que A est inclus dans B et que B est inclus dans A.

La réciproque est une propriété ordinaire de l'égalité, vraie pour n'importe quelle relation binaire.

En calcul des prédicats (égalitaire), la propriété essentielle de l'égalité est la propriété de substitution, que l'on exprime sous la forme d'un schéma d'axiomes (une infinité d'axiomes, un par formule du calcul des prédicats ensembliste). La propriété de substitution énonce que si deux objets sont égaux, toute propriété vérifiée par l'un est vérifiée par l'autre. Il s'agit des propriétés exprimées dans le langage de la théorie, et elles peuvent dépendre d'éventuels paramètres a₁ … a_p. Plus formellement le schéma d'axiomes de substitution pour l'égalité est :

∀a₁ … ∀a_p ∀x ∀y [x = y ⇒ (P x a₁ … a_p ⇒ P y a₁ … a_p)]      pour toute formule P ne contenant pas d'autre variable libre que x a₁ … a_p.

(ce schéma d'axiomes, auquel il faut ajouter la réflexivité, ∀x   x = x, axiomatise alors l'égalité, on en déduit en particulier la symétrie et la transitivité).

On voit ainsi que la réciproque de l'axiome d'extensionnalité – si deux ensembles sont égaux, alors ils ont les mêmes éléments – est une propriété usuelle de l'égalité, un cas particulier du schéma que l'on vient d'énoncer :

∀A ∀B [ A = B ⇒ ∀x (x ∈ A ⇔ x ∈ B)].

L'axiomatisation de l'égalité est une formalisation en logique du premier ordre de la définition de l'égalité de Leibniz : deux objets sont égaux quand ils ont les mêmes propriétés, dit par contraposée, deux objets sont différents si une propriété permet de les distinguer.

Une alternative est de considérer la théorie des ensembles en calcul des prédicats du premier ordre sans égalité, et de définir cette dernière à partir de l'appartenance, par l'égalité extensionnelle^[3] :

x = y signifie ∀z (z ∈ x ⇔ z ∈ y)   (deux ensembles sont égaux quand ils ont les mêmes éléments).

On doit alors donner un axiome qui permet de retrouver les propriétés usuelles de l'égalité, et qui dans ce contexte, est parfois aussi appelé axiome d'extensionnalité^[4] :

∀x ∀y [∀z (z ∈ x ⇔ z ∈ y) ⇒ ∀u(x ∈ u ⇔ y ∈ u)]   (si deux ensembles ont les mêmes éléments, alors ils appartiennent aux mêmes ensembles)

soit avec la définition extensionnelle de l'égalité :

∀x ∀y [x = y ⇒ ∀u(x ∈ u ⇔ y ∈ u)].

Cet axiome apparaît alors comme un cas particulier de la propriété de substitution pour l'égalité du paragraphe précédent, celui où le prédicat en jeu est l'appartenance à un ensemble donné. La définition extensionnelle fournit un autre cas particulier :

∀x ∀y [x = y ⇒ ∀z(z ∈ x ⇔ z ∈ y)].

La propriété de substitution pour l'égalité se démontre alors pour tout prédicat par récurrence sur la longueur de la formule qui définit ce prédicat, les deux cas particuliers précédent constituant le cas de base^[5].

L'axiome d'extensionnalité permet d'assurer l'unicité d'ensembles définis par un prédicat, tels l'ensemble vide, la paire de deux ensembles donnés, dont l'existence est directement affirmée par certains autres axiomes ou se démontre à partir de ceux-ci.

Étant donné un prédicat quelconque P, un de ses arguments que l'on notera x étant distingué, les autres, s'il en existe, sont notés a₁ … a_p et servent de paramètres, il n'existe pas toujours un ensemble A défini comme l'ensemble des objets x qui vérifient P^[6], c'est-à-dire tel que pour tous a₁ … a_p et pour tout x,

x ∈ A ⇔ P x a₁ … a_p.

Supposons que l'on ait démontré l'existence d'un tel ensemble A^[7]. Dans ce cas, cet ensemble A est l'unique ensemble des x vérifiant P : l'unicité est une conséquence immédiate de l'axiome d'extensionnalité.

On introduit alors pour de tels ensembles, ou constructions ensemblistes, un symbole particulier pour le désigner, par exemple ∅ pour l'ensemble vide, { a } pour le singleton construit à partir de a, {a, b} pour la paire formée par a et b…

L'introduction de ces nouveaux symboles ne modifie pas réellement la théorie au sens suivant : les théorèmes (exprimés sans ces symboles) restent les mêmes, tout énoncé contenant ces nouveaux symboles peut être remplacé par un énoncé équivalent ne les contenant pas. Ceci se montre en utilisant les propriétés d'existence et d'unicité qui ont permis de les introduire.

L’axiome d’extensionnalité apparaît, sous une forme ou sous une autre, dans les axiomatiques de la théorie des ensembles, qui est le plus souvent une théorie des « ensembles extensionnels ». Il est cependant possible de s'intéresser, au moins en préalable, aux théories non extensionnelles, qui ont de meilleures propriétés en théorie de la démonstration, à cause du « quotient » complexe qu'induit l'égalité extensionnelle^[8].

L'axiome doit être adapté, pour des théories des ensembles avec ur-elements, qui n'ont aucun élément mais sont distincts de l'ensemble vide.

Classe

• Portail des mathématiques