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

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).

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.

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[4].

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[5].

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[6].

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

« 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).

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.

• 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é[8].

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.

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[9] :

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.

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 }.

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.

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.

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é).

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)]).

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).

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.

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[10].

• 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[11], 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.