Axiome d'extensionnalité
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<ref>Plus prétentieuse et moins claire selon Modèle:Halmos65, chap. I, Modèle:P..</ref>, 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’axiome
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.
Énoncé en calcul des prédicats égalitaire
Dans ce cas, l'axiome d'extensionnalité s'énonce ainsi :
Ce qui revient à dire que : si tout élément de l'ensemble Modèle:Math est aussi un élément de Modèle:Math, et si tout élément de l'ensemble Modèle:Math appartient à l'ensemble Modèle:Math, alors les deux ensembles Modèle:Math et Modèle:Math sont égaux.
On sait que l'inclusion entre deux ensembles, notée Modèle:Math<ref>Notation pour l'inclusion utilisée par exemple par Modèle:Krivine98 I.3, Modèle:P. et Modèle:Harvsp, chap. I, Modèle:P..</ref> ou Modèle:Math se définit par :
- Modèle:Math signifie Modèle:Math
On en déduit donc une autre formulation de l'axiome d'extensionnalité, qui est d'ailleurs celle originale de Ernst Zermelo :
Cette dernière formulation justifie l'utilisation courante de la double inclusion pour montrer une égalité entre deux ensembles : pour montrer que deux ensembles Modèle:Math et Modèle:Math sont égaux, il suffit de montrer que Modèle:Math est inclus dans Modèle:Math et que Modèle:Math est inclus dans Modèle:Math.
La réciproque est une propriété ordinaire de l'égalité, vraie pour n'importe quelle relation binaire.
Extensionnalité et axiomes de l'égalité
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 Modèle:Math. Plus formellement le schéma d'axiomes de substitution pour l'égalité est :
- Modèle:Math pour toute formule Modèle:Math ne contenant pas d'autre variable libre que Modèle:Math.
(ce schéma d'axiomes, auquel il faut ajouter la réflexivité, Modèle:Math, 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 :
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.
Égalité et extensionnalité en calcul des prédicats pur
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<ref>C'est le choix fait par exemple dans Modèle:Ouvrage.</ref> :
- Modèle:Math (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é<ref>Modèle:Harvsp.</ref> :
- Modèle:Math (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é :
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 :
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<ref>De façon plus intrinsèque, il s'agit d'une induction sur la structure de la formule. Modèle:Harvsp, utilisent de façon analogue une récurrence sur le nombre de sous-formules.</ref>.
Conséquences de cet axiome
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 Modèle:Math, un de ses arguments que l'on notera Modèle:Math étant distingué, les autres, s'il en existe, sont notés Modèle:Math et servent de paramètres, il n'existe pas toujours un ensemble Modèle:Math défini comme l'ensemble des objets Modèle:Math qui vérifient Modèle:Math<ref>Un exemple d'un tel prédicat est Modèle:Math, voir « Paradoxe de Russell » et « Schéma d'axiomes de compréhension ».</ref>, c'est-à-dire tel que pour tous Modèle:Math et pour tout Modèle:Math,
Supposons que l'on ait démontré l'existence d'un tel ensemble Modèle:Math<ref>En dehors de l'extensionnalité, de l'axiome du choix et de l'axiome de fondation, les axiomes de la théorie des ensembles ZFC énoncent justement l'existence d'un ensemble ayant pour éléments ceux qui satisfont une certaine propriété et appartiennent à un ensemble prédéfini.</ref>. Dans ce cas, cet ensemble Modèle:Math est l'unique ensemble des Modèle:Math vérifiant Modèle:Math : 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 Modèle:Math pour l'ensemble vide, Modèle:Math pour le singleton construit à partir de Modèle:Math, Modèle:Math pour la paire formée par Modèle:Math et Modèle:Math…
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.
Théories des ensembles non extensionnelles
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<ref>Voir Modèle:Article ou Modèle:Article.</ref>.
Variantes de l'axiome d'extensionnalité
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.
