Axiomes de la théorie NBG
La théorie NBG reprend les axiomes de ZFC, modifiés pour tenir compte des classes, auxquels elle ajoute des axiomes reliant classe et prédicat.
Extensionalité
Si deux classes ont les mêmes éléments, alors elles sont identiques.
c'est-à-dire que :
∀A, B [∀ x(x ∈ A ↔ x ∈ B) → A = B]
L'axiome a pour cas particulier l'axiome d'extensionnalité pour les ensembles (on peut bien sûr supposer que A et B sont des ensembles, dans toute utilisation de cet énoncé, x ne peut que désigner un ensemble, il est inutile de le préciser). La généralisation aux classes va de soi. On rappelle que, comme dans toute théorie égalitaire, l'égalité satisfait, en plus de la réflexivité, le schéma d'axiomes suivant, qui énonce que si A = B, toute propriété de A est une propriété de B :
∀C1, … , Cn ∀A, B[A=B → (Φ A C1 … Cn → Φ B C1 … Cn)]
qui a pour cas particulier la réciproque de l'axiome d'extensionnalité.
Axiomes ensemblistes
Pour ces axiomes, on reprend leur formulation dans ZFC, en relativisant les quantifications aux ensembles (il n'est pas forcément nécessaire de relativiser toutes les quantifications aux ensembles, certaines le sont déjà implicitement, mais ceci n'a pas grande importance). Grâce aux classes les schémas d'axiomes deviennent des axiomes.
- Axiome de l'ensemble vide
L'axiome de l'ensemble vide ne se déduit plus directement de la compréhension, comme dans ZFC, puisque si l'on suppose en logique du premier ordre que le modèle d'interprétation est toujours non vide, il peut très bien ici ne contenir qu'une classe (la classe vide). On a donc besoin de l'axiome :
Il existe un ensemble qui n'a pas d'éléments.
C'est-à-dire :
∃a ∀x x ∉ a.
Tout comme dans ZFC, l'unicité de cet ensemble découle de l'axiome d'extensionnalité ; on peut parler de l'ensemble vide, et utiliser la notation usuelle ∅.
L'ensemble vide est aussi la classe vide, mais l'existence de la classe vide aurait pu se démontrer par compréhension sur les classes (voir la suite) sans axiome spécifique. On verra que, par un axiome de passage au complémentaire, l'existence de la classe de tous les ensembles se déduira de l'existence de la classe vide.
Si x et y sont des ensembles, alors il existe un ensemble dont ils sont les uniques éléments.
C'est-à-dire :
∀x ∀y ∃p ∀z[z ∈ p ↔ (z=x ∨ z = y)].
Tout comme dans ZFC, l'unicité de cet ensemble pour x et y donnés découle de l'axiome d'extensionnalité ; on peut donc bien parler de la paire x, y et on peut introduire la notation { x , y }.
On se contente de rappeler les deux axiomes suivants, dont les énoncés se formalisent dans le langage de la théorie des classes exactement de la même façon.
Si x est un ensemble, alors il existe au moins un ensemble qui soit la réunion des éléments de x, c’est-à-dire auquel appartiennent tous les éléments des éléments de x et eux seuls.
- Axiome de l'ensemble des parties
Si x est un ensemble, alors il existe un ensemble contenant les sous-ensembles de x et eux seuls.
- Axiome de compréhension pour les ensembles ou axiome de séparation
Dans ZFC, il s'agit d'un schéma d'axiomes ; dans NBG, il se ramène au seul axiome suivant :
L'intersection d'une classe et d'un ensemble est encore un ensemble : pour toute classe C et tout ensemble x, il existe un ensemble a qui regroupe les éléments de x qui appartiennent aussi à C.
C'est-à-dire :
∀C∀x ∃a∀z[z ∈ a ↔ (z ∈ x ∧ z ∈ C)].
Dans ce contexte, où la compréhension est en fait gérée au niveau des classes (section suivante), on parlera plutôt d'axiome de séparation.
Il existe un ensemble auquel appartient l’ensemble vide et qui est clos par l'opération qui à l'ensemble x associe l'ensemble x ∪ {x}.
∃a[∅ ∈ a ∧ ∀x(x ∈ a → x ∪ {x} ∈ a)].
On peut bien parler de singleton et de réunion binaire ensembliste en présence de l'axiome de la paire, de l'axiome de la réunion, et de l'axiome d'extensionnalité (pour l'unicité).
- Axiome de remplacement dit aussi axiome de substitution
Là encore, ce qui est un schéma d'axiomes dans ZFC, se ramène à un seul axiome dans NBG. Mais il faut pour cela avoir défini les couples. On prend la définition usuelle de Wiener-Kuratowski, pour deux ensembles x et y on a par définition :
(x,y)={{x},{x,y}}.
L'usage de cette notation requiert l'axiome de la paire et l'axiome d'extensionnalité. On définit facilement le prédicat « être un couple », les premières et secondes projections d'un couple. On peut donc dire qu'une classe est fonctionnelle :
C fonctionnelle signifie ∀z[z ∈ C → ∃x∃y z=(x,y)] ∧ ∀x∀y∀y’[(x,y) ∈ C ∧ (x,y’) ∈ C → y = y’].
On peut maintenant énoncer l'axiome :
Soit une classe C fonctionnelle, alors pour tout ensemble x, il existe un ensemble a regroupant les secondes composantes des couples de C dont la première composante appartient à x.
C'est-à-dire :
∀C(C fonctionnelle → ∀x ∃a ∀z[z ∈ a ↔ ∃t(t ∈ x ∧ (t,z) ∈ C)]).
Tout ensemble non-vide possède au moins un élément avec qui il n’a pas d’élément commun.
Ou :
∀x[x ≠ ∅ → ∃a(a ∈ x ∧ a ∩ x = ∅)].
Les énoncés utilisent des notations introduites pour la clarté ( ∅, ∩) mais se traduisent sans mal en énoncés de la théorie des classes (cet axiome interdit les chaînes infinies décroissantes d'appartenance x0 ∋ x1 ∋ x2 … ∋ xi ∋ xi+1 … , par exemple un ensemble ne peut appartenir à lui-même).
La version de Zermelo est la plus simple à formaliser :
Pour toute famille d’ensembles non-vides disjoints deux à deux, il existe un ensemble contenant un élément et un seul de chaque ensemble de la famille.
C'est-à-dire :
∀u{ ∀z[ z ∈ u → z ≠ ∅ ∧ ∀z’([z’ ∈ u ∧ z’ ≠ z] → z ∩ z’ = ∅) ] → ∃c ∀z[ z ∈ u → ∃! x (x ∈ z ∩ c)] },
où ∃!x Φx signifie ∃x [Φx ∧ ∀y (Φy → y = x)] (il existe un unique x tel que Φx).
Là encore, les symboles « ∅ » et « ∩ » s'éliminent facilement.
Compréhension pour les classes
On pourrait énoncer un schéma d'axiomes de compréhension pour les classes, à savoir que, tout prédicat du langage de la théorie dont les quantificateurs sont restreints aux ensembles détermine une classe (le schéma est énoncé, comme théorème, en fin de section).
Le prédicat peut contenir des paramètres, qui ne désignent pas nécessairement des ensembles. Il s'agirait d'un schéma d'axiomes, un axiome pour chaque formule. Cependant ce schéma peut s'axiomatiser finiment. Essentiellement, grâce aux classes, il est possible de reconstruire toutes les formules (dont les quantificateurs sont restreints aux ensembles !) en les ramenant, essentiellement, à un nombre fini de cas particuliers. On a un axiome pour la relation d'appartenance (formules atomiques), des axiomes pour chaque opérateur logique (négation, conjonction, quantification existentielle), et des axiomes qui permettent de permuter de façon homogène les éléments d'une classe de n-uplets, de façon à pouvoir faire passer n'importe quelle composante en queue, et donc de se restreindre à ce cas pour la quantification existentielle. Les précédents axiomes permettent bien de définir, comme usuellement en théorie des ensembles, les couples (et donc les n-uplets) de Wiener-Kuratowski :
(x,y)={{x},{x,y}}
Il faut faire un choix pour la définition des n-uplets. On convient dans la suite que par définition :
(x) = x ;
pour n > 1, (x0, … , xn-1, xn) = ((x0, … , xn-1), xn).
Les quatre premiers axiomes correspondent aux constructions des formules de la théorie des ensembles : formules atomiques (appartenance, l'égalité s'en déduit), négation, conjonction et quantification existentielle. Le choix des axiomes, en particulier des trois derniers, tout comme le nombre de ceux-ci n'ont rien d'intrinsèque, et on peut trouver des variantes suivant les ouvrages.
- Relation d'appartenance - Il existe une classe contenant exactement tous les couples d'ensembles tels que le premier appartienne au second.
∃A ∀x ∀y[(x,y) ∈ A ↔ x ∈ y]
On peut se passer, par extensionnalité, d'un axiome spécifique pour les formules atomiques égalitaires.
- Complémentaire - Pour toute classe, il existe une classe complémentaire regroupant les ensembles n'appartenant pas à cette classe.
∀C ∃D ∀x(x ∈ D ↔ x ∉ C)
Remarque : On montre ainsi l'existence de la classe de tous les ensembles, notée V, qui est la classe complémentaire de la classe vide.
- Intersection - Quelles que soient deux classes, il existe une classe des éléments qui leur sont communs.
∀C ∀D ∃N ∀x[x ∈ N ↔ (x ∈ C ∧ x ∈ D)]
On peut utiliser le signe d'intersection usuel pour les classes. Par exemple l'axiome de séparation peut se réexprimer en disant que pour toute classe C, et pour tout ensemble x, x ∩ C est un ensemble. On déduit de cet axiome et de l'axiome précédent, par loi de de Morgan, l'existence de la classe-réunion de deux classes.
- Domaine - Il existe une classe regroupant les premières composantes d'une classe de couples.
∀C ∃E ∀x[x ∈ E ↔ ∃y (x,y) ∈ C]
Par passages au complémentaire, on en déduit un résultat analogue pour le quantificateur universel.
On a maintenant des axiomes pour gérer au niveau des classes les variables des prédicats. On a besoin, pour construire des prédicats à plusieurs variables, d'ajouter des variables « inutiles ». Par exemple (Φx ∧ Ψxy), formule à deux variables libres, est obtenue par conjonction d'une formule à une variable libre et d'une formule à deux variables libres. Si la classe C représente Φ, et si E est une classe de couples représentant Ψ, on peut utiliser le produit cartésien par la classe V de tous les ensembles, et remarquer que (C × V) ∩ E représente (Φx ∧ Ψxy). Mais pour cela il faut l'axiome suivant, qui montre l'existence de la classe C × V (produit cartésien de C par la classe V).
- Produit par V - Pour toute classe, les couples dont la première composante est élément de cette classe forment eux-mêmes une classe.
∀C ∃D ∀x ∀y[(x,y) ∈ D ↔ x ∈ C]
L'axiome du domaine permet de représenter la quantification existentielle seulement sur la dernière composante des n-uplets de la classe correspondante, de même que l'axiome du produit par V ne permet que d'ajouter une composante en fin de n-uplet. Des permutations sont donc utiles pour gérer l'ordre de ces composantes. Les permutations sont l'objet des deux derniers axiomes, qui seront suffisant, vu les résultats connus sur les permutations, et la représentation des n-uplets par itération des couples.
- Permutation circulaire - Pour toute classe de triplets, les triplets obtenus par permutation circulaire de ceux-ci forment une classe.
∀C ∃D ∀x ∀y ∀z [(x,y,z) ∈ D ↔ (z,x,y) ∈ C]
- Transposition - Pour toute classe de triplets, les triplets obtenus par transposition des deux premières composantes forment une classe.
∀C ∃D ∀x ∀y ∀z [(x,y,z) ∈ D ↔ (y,x,z) ∈ C]
Remarque : on en déduit l'équivalent de l'axiome de transposition pour les couples (énoncé 1 du lemme ci-dessous).
On déduit de ces sept axiomes le schéma de compréhension pour les classes, ou, comme le nomme Gödel, le théorème général d'existence des classes, qui est donc un schéma de théorèmes.
Proposition (schéma de compréhension pour les classes). Pour toute formule Φ dont toutes les quantifications sont relativisées aux ensembles, et dont les variables libres sont parmi x1, … , xn, C1, … , Cp, on a :
∀C1 … ∀Cp ∃ D ∀x1 … ∀xn [(x1, … , xn) ∈ D ↔ Φ].
Preuve. On montre ce résultat, pour toute formule Φ dont toutes les quantifications sont relativisées aux ensembles, et pour toute suite finie de variables (x1, … , xn) contenant (au sens ensembliste) les variables libres de Φ, par induction sur la construction de Φ. En calcul des prédicats du premier ordre, toute formule peut s'écrire avec ¬, ∧, ∃, et donc, une fois le résultat démontré pour les formules atomiques, il suit directement par les axiomes du complémentaire, de l'intersection, et du domaine. Dans ce dernier cas on utilise la définition des n-uplets choisie ; bien-sûr il est indispensable que la quantification soit relativisée aux ensembles pour pouvoir utiliser l'axiome. Il reste donc à montrer le résultat pour les formules atomiques. Plutôt que de traiter toutes les formes de celles-ci, on va, préalablement à l'induction, éliminer certaines formes d'entre elles.
Tout d'abord on peut, en utilisant l'extensionnalité éliminer les égalités. On peut également, en susbstituant une formule adéquate, éliminer les occurrences des paramètres Ci à gauche de l'appartenance (C ∈ D équivaut à ∃ E (E ∈ D ∧ E = C) et l'égalité s'élimine par extensionnalité, ce qui ne réintroduit pas C à gauche d'une appartenance). On peut également éliminer les formules de la forme X ∈ X par une méthode analogue à la précédente.
Il reste deux types de formules atomiques à traiter, celles de la forme xi ∈ xj, où i ≠ j et celles de la forme xi ∈ C, où C est l'un des paramètres Ck. Pour xi ∈ xj, le résultat se déduit directement de l'axiome pour l'appartenance si i = 1, j = n = 2. Pour xi ∈ C, il est évident si i = n = 1. Dans les autres cas il faut donc pouvoir éventuellement renverser l'ordre des variables (premier type de formules), et ajouter des variables « inutiles » en tête, en queue, et, pour le premier type de formules, entre les deux variables. C'est l'objet du lemme suivant.
Lemme. On démontre dans NBG, à l'aide des 4 axiomes du produit par V, de permutation circulaire, de transposition, et d'existence du domaine, que :
- ∀C ∃D ∀x ∀y [(y,x) ∈ D ↔ (x,y) ∈ C] ;
- ∀C ∃D ∀x ∀y ∀z [(z, x,y) ∈ D ↔ (x,y) ∈ C] ;
- ∀C ∃D ∀x ∀y ∀z [(x,z, y) ∈ D ↔ (x,y) ∈ C] ;
- ∀C ∃D ∀x ∀y ∀z [(x,y, z) ∈ D ↔ (x,y) ∈ C].
Le résultat suit, pour une formule atomique du premier type envisagé, soit xi ∈ xj, par récurrence sur le nombre de variables, en itérant des applications des énoncés du lemme, dans l'ordre d'énonciation (l'ordre n'est pas indifférent, on utilise la définition des n-uplets à partir des couples). Si l'on suppose que i < j, on ajoute toutes les variables (x1, …, xi-1) en une application de l'énoncé 2 du lemme, puis les variables (xi+1, …, xj-1) une par une en itérant l'énoncé 3 du lemme, puis les variables (xj+1, …, xn) une par une par l'énoncé 4 (en fait l'axiome du produit par V). Le cas j < i se ramène au cas précédent par l'énoncé 1 du lemme.
Pour une formule atomique du second type envisagé, soit xi ∈ C, on utilise l'axiome du produit par V, la variable ajoutée est mise en tête par le premier énoncé du lemme, pour ajouter en une fois toutes les variables qui précèdent xi, puis on complète de façon itérée, par l'axiome du produit par V.
Le lemme se démontre, pour le 4 par l'axiome du produit par V. Pour le 1 on utilise le 4, l'axiome de transposition, et l'axiome du domaine. Pour le 3 on utilise le 4 puis les deux axiomes de permutations pour obtenir la bonne transposition. Pour le 2 c'est le 4 puis l'axiome de permutation circulaire.
Remarque : la démonstration établit comment démontrer une infinité de théorèmes de NBG, elle utilise un raisonnement par récurrence dans la meta-théorie.