Théorie des ensembles de von Neumann-Bernays-Gödel

La théorie des ensembles de von Neumann–Bernays–Gödel, abrégée en NBG ou théorie des classes, est une théorie axiomatique essentiellement équivalente à la théorie ZFC de Zermelo-Fraenkel avec axiome du choix (et avec les mêmes variantes possibles), mais dont le pouvoir expressif est plus riche. Elle peut s’énoncer en un nombre fini d’axiomes, et donc sans schéma, au contraire de ZFC (voir schéma d'axiomes de compréhension et schéma d'axiomes de remplacement). Ceci n’est possible que grâce à une modification du langage de la théorie, qui permet de parler directement de classe, une notion par ailleurs utile en théorie des ensembles et qui apparaissait déjà, de façon assez informelle, dans les écrits de Georg Cantor dès avant 1900.

La théorie des classes a été introduite en 1925 par John von Neumann, mais celui-ci avait pris des fonctions pour objets primitifs. Elle est reformulée en termes de théorie des ensembles et simplifiée par Paul Bernays vers 1929. Kurt Gödel en donne une version inspirée de celle de Bernays, pour sa preuve de cohérence relative de l'axiome du choix et de l'hypothèse du continu par les constructibles, lors de conférences à Princeton en 1937-1938 (publiées en 1940).

Une théorie des classes plus forte, la théorie de Morse-Kelley, a été proposée plus tard par plusieurs mathématiciens, et apparaît pour la première fois en 1955 dans le livre de topologie générale de John L. Kelley.

Les classes

Les classes en théorie des ensembles

Les théories des ensembles comme la théorie de Zermelo (dans sa ré-énonciation moderne) et ses extensions (Zermelo–Fraenkel, ZFC, etc.) s’énoncent dans le langage du calcul des prédicats du premier ordre égalitaire construit sur le seul symbole de l’appartenance. Autrement dit, les énoncés n’utilisent que des variables, qui désignent des ensembles, l’égalité et l’appartenance, qui sont des relations entre ces ensembles ; ils combinent des relations avec les symboles logiques, connecteurs et quantificateurs. En particulier, les seuls objets de base de la théorie sont les ensembles.

Ces théories des ensembles ne disposent pas de variables pour les classes, qui sont des collections d’ensembles bien définies, dont certaines sont « trop grosses » pour être des ensembles sans conduire à des paradoxes. Ainsi, la collection des ensembles qui n’appartiennent pas à eux-mêmes ne peut être un ensemble, selon le paradoxe de Russell. Elle est pourtant bien définie : c’est une classe. On ne peut donc parler de classe dans ces théories qu’au travers des prédicats du langage qui les définissent (comme cela est exposé dans l’article sur les classes).

Les classes comme objets primitifs

Une autre solution est d'ajouter des variables pour les classes, on a maintenant deux types d'objets de base, les ensembles et les classes, et il est tout à fait possible d'axiomatiser une telle théorie de façon à ne pas modifier les énoncés démontrables de la théorie des ensembles d'origine, ceux qui ne font donc pas appel à ces nouvelles variables de classe. La théorie NBG est une telle théorie. Il en existe en fait autant de variantes que pour la théorie des ensembles dans le langage d'origine, suivant les axiomes que l'on choisira ou non d'ajouter.

Les classes et les prédicats

Une fois ajoutées au langage des variables de classes, il est très simple d'axiomatiser NBG à partir de ZFC : il suffit d'ajouter un schéma d'axiomes, le schéma de compréhension pour les classes, qui associe une classe à tout prédicat (à une variable) de la théorie des ensembles. Les prédicats à plusieurs variables peuvent être représentés grâce aux couples de Wiener-Kuratowski. Il n'y a plus qu'à ré–énoncer tous les axiomes de la théorie ZFC en restreignant les variables aux ensembles. Les schémas d'axiomes, qui utilisent un axiome par prédicat de la théorie des ensembles, peuvent alors être représentés par un seul axiome, grâce à la notion de classe.

Il y a cependant une petite difficulté : comme on a étendu le langage de la théorie, celui-ci permet de définir de nouveaux prédicats. Il faut donc contraindre les classes à être définies par les anciens prédicats, ceux qui n'utilisent pas de variable de classe. En fait il suffit qu'ils n'utilisent pas de quantificateur sur les classes, les variables non quantifiées sont de simples paramètres, auxquels ultimement ne pourront être substitués que des prédicats purement ensemblistes.

Ainsi on obtient une théorie des classes très similaire à ZFC mais qui n'est toujours pas finiment axiomatisée : le schéma de remplacement de ZFC peut être remplacé par un seul axiome, mais on a introduit un nouveau schéma. Cependant, il est maintenant possible de réduire ce schéma à un nombre fini de cas, en mimant dans les classes la construction inductive des formules de ZFC : les règles de construction sont en nombre fini, et à chacune correspond un axiome d'existence. Comme les formules à plusieurs variables libres sont représentées à l'aide de listes finies de variables construites par les couples de Wiener-Kuratowski, il faut ajouter quelques axiomes pour gérer celles-ci. Outre que cela conduirait à une théorie plus forte, il est indispensable que les prédicats ne soient pas tous les prédicats du nouveau langage pour que cette construction soit possible.

Ce procédé n'est pas particulier à la théorie des ensembles, et a été adapté à d'autres théories avec schémas d'axiomes, par exemple dans le cadre de l'arithmétique.

Axiomatisation de NBG

Classes et ensembles

La théorie NBG a deux types d'objets, les ensembles et les classes. Intuitivement tous les ensembles sont des classes mais certaines classes, appelées classes propres, ne sont pas des ensembles. On a deux possibilités pour représenter cette situation. Bernays utilise un calcul du prédicat du premier ordre, mais avec deux sortes d'objets de base, les ensembles et les classes. Gödel utilise le calcul des prédicats du premier ordre, avec une seule sorte d'objet, ici les classes, en définissant la notion d'ensemble par un prédicat sur les classes. Ce prédicat peut se définir à partir de l'appartenance : les ensembles sont les classes qui appartiennent à au moins une classe, il n'est donc pas besoin d'introduire un nouveau symbole de prédicat. La différence entre les deux approches n'est pas très essentielle. Dans le premier cas on ne peut écrire qu'une classe appartient à une classe, un tel énoncé n'a pas de sens, mais, quand le membre gauche est une classe qui définit un ensemble, on peut lui faire correspondre un énoncé correct. Dans le second cas on peut écrire un tel énoncé, mais il est toujours faux par définition si le membre gauche n'est pas un ensemble. L'approche suivie par Bernays est peut-être plus immédiate mais introduit une certaine redondance puisqu'un ensemble a deux représentations, l'une en tant qu'ensemble, l'autre en tant que classe.

Le langage de la théorie

Le point de vue adopté est le second, les seuls objets primitifs sont les classes, les seules variables du langage sont des variables de classe. Une autre notion primitive de la théorie est la notion d’appartenance, notée « ∈ ». Comme la théorie des ensembles ZFC, la théorie NBG est une théorie logique égalitaire du premier ordre, avec l'appartenance comme symbole non logique primitif. La théorie NBG est donc, comme ZFC, exprimée en calcul des prédicats du premier ordre égalitaire.

Est un ensemble toute classe qui appartient à au moins une classe :

« x est un ensemble » signifie : ∃C x ∈ C.

Les classes qui ne sont pas des ensembles sont appelées classes propres :

« X est une classe propre » si et seulement si : ∀C X ∉ C.

Toute classe est donc soit un ensemble, soit une classe propre, et aucune classe n’est les deux à la fois (du moins si la théorie est cohérente).

L'existence d'au moins une classe propre sera une conséquence des axiomes de compréhension pour les classes : on montre que la classe des x qui n'appartiennent pas à eux-mêmes ne peut être un ensemble, c'est l'argument du paradoxe de Russell. Dès qu'il existe une classe propre, par définition de celles-ci, il ne peut pas exister de classe des classes propres tout comme de classe de toutes les classes.

L'existence d'au moins un ensemble sera également une conséquence des axiomes (axiome de l'ensemble vide par exemple). On verra que l'on peut déduire des axiomes de cette théorie l'existence d'une classe de tous les ensembles, que l'on notera « V », c'est-à-dire que l'on aura pour tout x :

x ∈ V ssi ∃C x ∈ C.

On sait définir le prédicat « être un ensemble », on peut donc définir des quantifications relativisées aux ensembles de la façon usuelle, pour une formule Φ :

∀ x^V Φ est une abréviation de ∀ x[( ∃C x ∈ C) → Φ] et signifie « pour tout ensemble x, Φ »,

∃ x^V Φ est une abréviation de ∃ x[( ∃C x ∈ C) ∧ Φ] et signifie « il existe un ensemble x tel que Φ ».

On va ainsi traduire les axiomes de ZFC en les relativisant aux ensembles (l'usage de ces notations ne présuppose pas l'existence de la classe V).

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é

• axiome d'extensionnalité

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 :

∀C₁, … , C_n ∀A, B[A=B → (Φ A C₁ … C_n → Φ B C₁ … C_n)]

qui a pour cas particulier la réciproque de l'axiome d'extensionnalité.

Axiomes ensemblistes

La formulation des axiomes ensembliste est reprise de celle de 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^V ∀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.

Axiome de la paire

Si x et y sont des ensembles, alors il existe un ensemble dont ils sont les uniques éléments.

C'est-à-dire : ∀x^V ∀y^V ∃p^V ∀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 }.

Axiomes de la réunion et de l'ensemble des parties

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.

• Axiome de la réunionSi 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 partiesSi 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^V ∃a^V∀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.

Axiome de l'infini

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^V[∅ ∈ 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 » et les première et seconde projections d'un couple. On peut donc dire qu'une classe C est fonctionnelle si elle respecte la propriété suivante :∀z[z ∈ C → ∃x^V∃y^V 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^V ∃a^V ∀z^V[z ∈ a ↔ ∃t(t ∈ x ∧ (t,z) ∈ C)]).

Axiome de fondation dit aussi axiome de régularité

Tout ensemble non vide possède au moins un élément avec lequel il n’a pas d’élément commun.

Ou :

∀x^V[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 x₀ ∋ x₁ ∋ x₂ … ∋ x_i ∋ x_i+1 … , par exemple un ensemble ne peut appartenir à lui-même).

Axiome du choix

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^V( { ∀z[ z ∈ u → z ≠ ∅ ∧ ∀z’([z’ ∈ u ∧ z’ ≠ z] → z ∩ z’ = ∅) ] } → ∃c^V ∀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, (x₀, … , x_n-1, x_n) = ((x₀, … , x_n-1), x_n).

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^V ∀y^V[(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^V(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^V[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 les lois 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^V[x ∈ E ↔ ∃y^V (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^V ∀y^V[(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 suffisants, 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^V ∀y^V ∀z^V [(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^V ∀y^V ∀z^V [(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 x₁, … , x_n, C₁, … , C_p, on a :

∀C₁ … ∀C_p ∃ D ∀x₁^V … ∀x_n^V [(x₁, … , x_n) ∈ 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 (x₁, … , x_n) 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 substituant une formule adéquate, éliminer les occurrences des paramètres C_i à 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 x_i ∈ x_j, où i ≠ j et celles de la forme x_i ∈ C, où C est l'un des paramètres C_k. Pour x_i ∈ x_j, le résultat se déduit directement de l'axiome pour l'appartenance si i = 1, j = n = 2. Pour x_i ∈ 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 :

1. ∀C ∃D ∀x^V ∀y^V [(y,x) ∈ D ↔ (x,y) ∈ C] ;
2. ∀C ∃D ∀x^V ∀y^V ∀z^V [(z, x,y) ∈ D ↔ (x,y) ∈ C] ;
3. ∀C ∃D ∀x^V ∀y^V ∀z^V [(x,z, y) ∈ D ↔ (x,y) ∈ C] ;
4. ∀C ∃D ∀x^V ∀y^V ∀z^V [(x,y, z) ∈ D ↔ (x,y) ∈ C].

Le résultat suit, pour une formule atomique du premier type envisagé, soit x_i ∈ x_j, 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 (x₁, …, x_i-1) en une application de l'énoncé 2 du lemme, puis les variables (x_i+1, …, x_j-1) une par une en itérant l'énoncé 3 du lemme, puis les variables (x_j+1, …, x_n) 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 x_i ∈ 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 x_i, 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 métathéorie.

Autres forme de l'axiome du choix

La théorie NBG permet d'exprimer une forme plus forte de l'axiome du choix, que l'on appelle axiome du choix global, ou principe du choix, et qui exprime l'existence d'une classe fonctionnelle définie sur tout l'univers, qui à chaque ensemble non vide associe un élément de cet ensemble. Cet axiome équivaut à ce que la classe V de tous les ensembles soit une classe bien ordonnée. Cet axiome a évidemment pour conséquence l'axiome du choix usuel, et Gödel a en fait démontré la cohérence, relativement à NBG sans axiome du choix, de NBG avec axiome du choix global.

La formulation originelle de von Neumann utilisait l'axiome de limitation de taille, qui a pour conséquence l'axiome du choix global, et équivaut à celui-ci et à l'axiome de remplacement relativement aux autres axiomes.

NBG et ZFC

La théorie NBG ne peut être logiquement équivalente à la théorie ZFC, puisque son langage est « plus riche », et contient donc des énoncés, qui parlent des classes en général, et qui ne peuvent être déterminés par ZFC. Cependant, NBG et ZFC démontrent exactement les mêmes énoncés restreints au langage de la théorie des ensembles. On dit alors que NBG est une extension conservative de ZFC : NBG peut montrer de nouvelles propriétés, mais celles-ci utiliseront nécessairement des quantifications sur les classes, NBG ne démontrera rien de nouveau pour des énoncés purement ensemblistes. Pour une formulation de NBG avec deux sortes d'objets, il s'agit vraiment des mêmes énoncés. Pour une présentation avec une seule sorte d'objet comme celle donnée ci-dessus, on fait correspondre à un énoncé de ZFC un énoncé obtenu en relativisant chaque quantificateur à la classe des ensembles.

Une conséquence est la propriété (plus faible) que ces théories sont équi-cohérentes : d'une contradiction démontrée dans ZFC, on déduirait évidemment une contradiction dans NBG puisque sa démonstration peut s'y reproduire telle quelle, en relativisant les énoncés aux ensembles, mais réciproquement d'une contradiction démontrée dans NBG, on déduirait aussi une démonstration de cette contradiction dans ZFC, puisqu'il n'y a aucun mal à exprimer celle-ci dans le langage de ZFC (quand une contradiction est démontrable, tout est démontrable). La théorie NBG, bien que plus expressive, n'est donc pas plus « risquée » que ZFC.

Cependant, bien que Gödel l'ait adoptée pour la première démonstration significative de cohérence relative, celle de l'axiome du choix et de l'hypothèse du continu, les théoriciens des ensembles préfèrent utiliser le langage de la théorie ZF : en permettant de parler d'une nouvelle notion, celle de classe, on ne peut que compliquer ce genre de preuves, où l'on raisonne sur la théorie. La théorie NBG est encore invoquée, en tant que théorie pour formaliser les mathématiques, quand on a besoin de classes propres par exemple en théorie des catégories.

Le changement de langage est bien une nécessité pour obtenir une axiomatisation finie de la théorie des ensembles. Richard Montague a montré en 1961 que l'on ne pouvait trouver un nombre fini d'axiomes équivalent à ZF : ZF n'est pas finiment axiomatisable (bien sûr sous l'hypothèse que ZF est cohérente).

Sources

• (en) John von Neumann, « An Axiomatization of Set Theory », dans Jean van Heijenoort, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Cambridge, Massachusetts, Harvard University Press, 1967 (texte de 1925 traduit en anglais et réimprimé).
• (en) Paul Bernays, « A System of Axiomatic Set Theory–Part I », J. Symb. Logic, vol. 2, n^o 1,‎ 1937, p. 65-77 (JSTOR 2268862).
• (en) Abraham Adolf Fraenkel et Paul Bernays, Axiomatic Set Theory, Amsterdam, North Holland, 1958 – réédité, sous le seul nom de Bernays en 1991, Dover (ISBN 0-48-666637-9). Reprise par Bernays de ses articles de 1937 à 1954, avec des modifications ; chapitre historique sur ZF en introduction par Fraenkel.
• (en) Kurt Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory, Princeton University Press, 1940 (ISBN 0691079277, lire en ligne), chap. I, p. 3-7.
• (en) Akihiro Kanamori, « Bernays and Set Theory », Bulletin of Symbolic Logic, vol. 15,‎ 2009, p. 43–69 (DOI 10.2178/bsl/1231081769, lire en ligne).
• (en) Richard Montague, « Semantic Closure and Non-Finite Axiomatizability I », dans Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics (Warsaw, 2-9 septembre 1959), Pergamon, 1961, p. 45-69.
• (en) Elliott Mendelson (en), An Introduction to Mathematical Logic, Chapman & Hall, 1997, 4^e éd. (1^re éd. 1964). Une introduction à la théorie des ensembles par la théorie NBG, axiomatisée à la façon de Gödel.

Voir aussi

Théorie des ensembles de Kripke-Platek