Théorie des ensembles de Von Neumann-Bernays-Gödel - Von Neumann–Bernays–Gödel set theory

Dans les fondements des mathématiques , la théorie des ensembles de von Neumann-Bernays-Gödel ( NBG ) est une théorie des ensembles axiomatique qui est une extension conservatrice de la théorie des ensembles de Zermelo-Fraenkel-Choice (ZFC). NBG introduit la notion de classe , qui est une collection d' ensembles définis par une formule dont les quantificateurs ne s'étendent que sur des ensembles. NBG peut définir des classes plus grandes que des ensembles, telles que la classe de tous les ensembles et la classe de tous les ordinaux . La théorie des ensembles de Morse-Kelley (MK) permet de définir des classes par des formules dont les quantificateurs s'étendent sur des classes. NBG est axiomatisable de manière finie, alors que ZFC et MK ne le sont pas.

Un théorème clé de NBG est le théorème d'existence de classe, qui stipule que pour chaque formule dont les quantificateurs ne s'étendent que sur des ensembles, il existe une classe constituée des ensembles satisfaisant la formule. Cette classe est construite en reflétant la construction étape par étape de la formule avec des classes. Puisque toutes les formules de la théorie des ensembles sont construites à partir de deux types de formules atomiques ( appartenance et égalité ) et d'un nombre fini de symboles logiques , seuls un nombre fini d' axiomes sont nécessaires pour construire les classes qui les satisfont. C'est pourquoi NBG est finiment axiomatisable. Les classes sont également utilisées pour d'autres constructions, pour gérer les paradoxes de la théorie des ensembles et pour énoncer l' axiome du choix global , qui est plus fort que l' axiome du choix de ZFC .

John von Neumann a introduit les classes dans la théorie des ensembles en 1925. Les notions primitives de sa théorie étaient fonction et argument . En utilisant ces notions, il a défini la classe et l'ensemble. Paul Bernays a reformulé la théorie de von Neumann en prenant classe et ensemble comme notions primitives. Kurt Gödel a simplifié la théorie de Bernays pour sa preuve de cohérence relative de l' axiome du choix et de l' hypothèse du continuum généralisé .

Cours de théorie des ensembles

Les usages des cours

Les classes ont plusieurs utilisations dans NBG :

• Ils produisent une axiomatisation finie de la théorie des ensembles.
• Ils sont utilisés pour énoncer une « forme très forte de l' axiome du choix », à savoir l' axiome du choix global : Il existe une fonction de choix global définie sur la classe de tous les ensembles non vides telle que pour chaque ensemble non vide C'est plus fort que les ZFC axiome de choix : Pour tout ensemble d' ensembles non vides, il existe une fonction de choix définie sur telle que pour tout${\style d'affichage G}$${\style d'affichage G(x)\dans x}$${\style d'affichage x.}$${\style d'affichage s}$ ${\style d'affichage f}$${\style d'affichage s}$${\style d'affichage f(x)\dans x}$${\displaystyle x\in s.}$
• Les paradoxes de la théorie des ensembles sont traités en reconnaissant que certaines classes ne peuvent pas être des ensembles. Par exemple, supposons que la classe de tous les ordinaux est un ensemble. Alors est un ensemble transitif bien ordonné par . Donc, par définition, est un ordinal. Par conséquent, , qui contredit être un bon ordre de Par conséquent, n'est pas un ensemble. Parce qu'une classe qui n'est pas un ensemble est appelée une classe propre , est une classe propre.${\displaystyle Ordre}$${\displaystyle Ordre}$${\style d'affichage \in }$${\displaystyle Ordre}$${\displaystyle Ord\in Ord}$${\style d'affichage \in }$${\displaystyle Ord.}$${\displaystyle Ordre}$${\displaystyle Ordre}$
• Les classes appropriées sont utiles dans les constructions. Dans sa preuve de la cohérence relative de l'axiome du choix global et de l' hypothèse du continuum généralisé , Gödel a utilisé des classes appropriées pour construire l' univers constructible . Il a construit une fonction sur la classe de tous les ordinaux qui, pour chaque ordinal, construit un ensemble constructible en appliquant une opération de construction d'ensembles aux ensembles précédemment construits. L'univers constructible est à l' image de cette fonction.

Schéma d'axiome contre théorème d'existence de classe

Une fois les classes ajoutées au langage de ZFC, il est facile de transformer ZFC en une théorie des ensembles avec des classes. Tout d'abord, le schéma axiome de la compréhension de classe est ajouté. Ce schéma d'axiome déclare : Pour chaque formule qui ne quantifie que sur des ensembles, il existe une classe constituée des - tuples satisfaisant la formule - c'est-à-dire, alors le schéma d'axiome de remplacement est remplacé par un seul axiome qui utilise une classe. Enfin, l' axiome d'extensionnalité de ZFC est modifié pour gérer les classes : si deux classes ont les mêmes éléments, alors elles sont identiques. Les autres axiomes de ZFC ne sont pas modifiés. ${\displaystyle \phi (x_{1},\ldots ,x_{n})}$${\style d'affichage A}$${\style d'affichage n}$${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots , x_{n})].}$

Cette théorie n'est pas finiment axiomatisée. Le schéma de remplacement de ZFC a été remplacé par un seul axiome, mais le schéma d'axiome de la compréhension de classe a été introduit.

Pour produire une théorie avec un nombre fini d'axiomes, le schéma d'axiome de la compréhension de classe est d'abord remplacé par un nombre fini d' axiomes d'existence de classe . Ensuite, ces axiomes sont utilisés pour prouver le théorème d'existence de classe, qui implique chaque instance du schéma d'axiome. La preuve de ce théorème ne nécessite que sept axiomes d'existence de classe, qui sont utilisés pour convertir la construction d'une formule en la construction d'une classe satisfaisant la formule.

Axiomatisation du NBG

Cours et ensembles

NBG a deux types d'objets : les classes et les ensembles. Intuitivement, chaque ensemble est aussi une classe. Il y a deux façons d'axiomatiser cela. Bernays a utilisé la logique multitriée avec deux sortes : les classes et les ensembles. Gödel a évité les tris en introduisant des prédicats primitifs : pour " est une classe" et pour " est un ensemble " (en allemand, " ensemble " est Menge ). Il a également introduit des axiomes indiquant que chaque ensemble est une classe et que si la classe est membre d'une classe, alors est un ensemble. L'utilisation de prédicats est le moyen standard d'éliminer les tris. Elliott Mendelson a modifié l'approche de Gödel en faisant en sorte que tout soit une classe et en définissant le prédicat d'ensemble comme Cette modification élimine le prédicat de classe de Gödel et ses deux axiomes. ${\displaystyle {\mathfrak {Cls}}(A)}$${\style d'affichage A}$${\style d'affichage {\mathfrak {M}}(A)}$${\style d'affichage A}$${\style d'affichage A}$${\style d'affichage A}$${\style d'affichage M(A)}$${\displaystyle \existe C(A\in C).}$

L'approche en deux parties de Bernays peut sembler plus naturelle au premier abord, mais elle crée une théorie plus complexe. Dans la théorie de Bernays, chaque ensemble a deux représentations : l'une en tant qu'ensemble et l'autre en tant que classe. De plus, il existe deux relations d'appartenance : la première, notée "∈", est entre deux ensembles ; la seconde, notée "η", se situe entre un ensemble et une classe. Cette redondance est requise par la logique multitriée car les variables de différentes sortes s'étendent sur des sous-domaines disjoints du domaine du discours .

Les différences entre ces deux approches n'affectent pas ce qui peut être prouvé, mais elles affectent la façon dont les déclarations sont écrites. Dans l'approche de Gödel, où et sont des classes est une déclaration valide. Dans l'approche de Bernays, cette affirmation n'a aucun sens. Cependant, si est un ensemble, il existe une instruction équivalente : définissez « l'ensemble représente la classe » s'ils ont les mêmes ensembles que les membres, c'est-à-dire que l' instruction où l'ensemble représente la classe est équivalente à celle de Gödel.${\style d'affichage A\dans C}$${\style d'affichage A}$${\style d'affichage C}$${\style d'affichage A}$${\style d'affichage a}$${\style d'affichage A}$${\displaystyle \forall x(x\in a\iff x\;\eta \;A).}$${\displaystyle a\;\eta \;C}$${\style d'affichage a}$${\style d'affichage A}$${\style d'affichage A\dans C.}$

L'approche adoptée dans cet article est celle de Gödel avec la modification de Mendelson. Cela signifie que NBG est un système axiomatique en logique des prédicats du premier ordre avec égalité , et ses seules notions primitives sont la classe et la relation d'appartenance.

Définitions et axiomes de l'extensionnalité et de l'appariement

Un ensemble est une classe qui appartient à au moins une classe : est un ensemble si et seulement si . Une classe qui n'est pas un ensemble est appelée une classe propre : est une classe propre si et seulement si . Par conséquent, chaque classe est soit un ensemble, soit une classe propre, et aucune classe n'est les deux (si la théorie est cohérente ). ${\style d'affichage A}$${\displaystyle \existe C(A\in C)}$${\style d'affichage A}$${\displaystyle \forall C(A\notin C)}$

Gödel a introduit la convention selon laquelle les variables majuscules s'étendent sur les classes, tandis que les variables minuscules s'étendent sur les ensembles. Gödel a également utilisé des noms qui commencent par une lettre majuscule pour désigner des classes particulières, y compris des fonctions et des relations définies sur la classe de tous les ensembles. La convention de Gödel est utilisée dans cet article. Il nous permet d'écrire :

Les axiomes et définitions suivants sont nécessaires pour la preuve du théorème d'existence de classe.

Axiome d'extensionnalité.  Si deux classes ont les mêmes éléments, alors elles sont identiques.

${\displaystyle \forall A\,\forall B\,[\forall x(x\in A\iff x\in B)\implies A=B]}$ 

Cet axiome généralise l' axiome d'extensionnalité de ZFC aux classes.

Axiome d'appariement .  Sietsont des ensembles, alors il existe un ensembledont les seuls membres sontet. ${\style d'affichage x}$${\style d'affichage y}$${\style d'affichage p}$${\style d'affichage x}$${\style d'affichage y}$

${\displaystyle \forall x\,\forall y\,\exists p\,\forall z\,[z\in p\iff (z=x\,\lor \,z=y)]}$ 

Comme en ZFC, l'axiome d'extensionnalité implique l'unicité de l'ensemble , ce qui permet d'introduire la notation${\style d'affichage p}$${\style d'affichage \{x,y\}.}$

Les paires ordonnées sont définies par :

${\style d'affichage (x,y)=\{\{x\},\{x,y\}\}}$

Les tuples sont définis de manière inductive à l' aide de paires ordonnées :

${\style d'affichage (x_{1})=x_{1},}$

${\displaystyle {\text{For }}n>1\!:(x_{1},\ldots ,x_{n-1},x_{n})=((x_{1},\ldots ,x_{ n-1}),x_{n}).}$

Axiomes d'existence de classe et axiome de régularité

Des axiomes d'existence de classe seront utilisés pour prouver le théorème d'existence de classe : Pour chaque formule dans des variables d'ensembles libres qui ne quantifie que sur des ensembles, il existe une classe de -uplets qui la satisfont. L'exemple suivant commence par deux classes qui sont des fonctions et crée une fonction composite . Cet exemple illustre les techniques nécessaires pour prouver le théorème d'existence de classe, ce qui conduit aux axiomes d'existence de classe nécessaires. ${\style d'affichage n}$ ${\style d'affichage n}$

Exemple 1 :  Si les classes et sont des fonctions, alors la fonction composée est définie par la formule : Puisque cette formule a deux variables libres, et que le théorème d'existence de classe construit la classe des paires ordonnées :${\style d'affichage F}$${\style d'affichage G}$${\displaystyle G\circ F}$${\displaystyle \exists t[(x,t)\in F\,\land \,(t,y)\in G].}$${\style d'affichage x}$${\style d'affichage y,}$${\displaystyle G\circ F\,=\,\{(x,y):\existe t[(x,t)\in F\,\land \,(t,y)\in G]\}. }$ Parce que cette formule est construite à partir de formules plus simples utilisant la conjonction et la quantification existentielle , des opérations de classe sont nécessaires qui prennent des classes représentant les formules les plus simples et produisent des classes représentant les formules avec et . Pour produire une classe représentant une formule avec , intersection utilisée depuis Pour produire une classe représentant une formule avec , le domaine est utilisé depuis${\displaystyle \land }$ ${\style d'affichage \existe }$${\displaystyle \land }$${\style d'affichage \existe }$${\displaystyle \land }$${\displaystyle x\in A\cap B\iff x\in A\land x\in B.}$${\style d'affichage \existe }$${\displaystyle x\in Dom(A)\iff \existe t[(x,t)\in A].}$ Avant de prendre l'intersection, les tuples et besoin d' un composant supplémentaire afin qu'ils aient les mêmes variables. Le composant est ajouté aux tuples de et est ajouté aux tuples de : ${\style d'affichage F}$${\style d'affichage G}$${\style d'affichage y}$${\style d'affichage F}$${\style d'affichage x}$${\style d'affichage G}$ ${\displaystyle F'=\{(x,t,y):(x,t)\in F\}\,}$ et ${\displaystyle \,G'=\{(t,y,x):(t,y)\in G\}}$ Dans la définition de la variable n'est pas restreinte par la déclaration donc s'étend sur la classe de tous les ensembles. De même, dans la définition de la variable s'étend sur Donc, un axiome est nécessaire qui ajoute un composant supplémentaire (dont les valeurs s'étendent sur ) aux tuples d'une classe donnée. ${\style d'affichage F',}$${\style d'affichage y}$${\style d'affichage (x,t)\in F,}$${\style d'affichage y}$${\style d'affichage V}$${\style d'affichage G',}$${\style d'affichage x}$${\style d'affichage V.}$${\style d'affichage V}$ Ensuite, les variables sont mises dans le même ordre pour préparer l'intersection : ${\displaystyle F''=\{(x,y,t):(x,t)\in F\}\,}$ et ${\displaystyle \,G''=\{(x,y,t):(t,y)\in G\}}$ Pour aller de à et de à nécessite deux permutations différentes , des axiomes prenant en charge les permutations de composants de tuple sont donc nécessaires. ${\style d'affichage F'}$${\style d'affichage F''}$${\style d'affichage G'}$${\style d'affichage G''}$ L'intersection de et des poignées : ${\style d'affichage F''}$${\style d'affichage G''}$${\displaystyle \land }$ ${\displaystyle F''\cap G''=\{(x,y,t):(x,t)\in F\,\land \,(y,t)\in G\}}$ Puisque est défini comme , prend le domaine des poignées et produit la fonction composite : ${\style d'affichage (x,y,t)}$${\style d'affichage ((x,y),t)}$${\displaystyle F''\cap G''}$${\displaystyle \existe t}$ ${\displaystyle G\circ F=Dom(F''\cap G'')=\{(x,y):\existe t((x,t)\in F\,\land \,(t,y )\dans G)\}}$ Il faut donc des axiomes d'intersection et de domaine.

Les axiomes d'existence de classe sont divisés en deux groupes : les axiomes gérant les primitives de langage et les axiomes gérant les tuples. Il y a quatre axiomes dans le premier groupe et trois axiomes dans le deuxième groupe.

Axiomes pour la gestion des primitives de langage :

Adhésion.  Il existe une classe contenant toutes les paires ordonnées dont le premier composant est membre du deuxième composant. ${\style d'affichage E}$

${\displaystyle \exists E\,\forall x\,\forall y\,[(x,y)\in E\iff x\in y]\!}$ 

Intersection (conjonction).  Pour deux classes et , il existe une classe constituée précisément des ensembles qui appartiennent à la fois à et . ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage C}$${\style d'affichage A}$${\style d'affichage B}$

${\displaystyle \forall A\,\forall B\,\existe C\,\forall x\,[x\in C\iff (x\in A\,\land \,x\in B)]}$ 

Complément (négation).  Pour toute classe, il existe une classeconstituée précisément des ensembles n'appartenant pas à. ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage A}$

${\displaystyle \forall A\,\existe B\,\forall x\,[x\in B\iff \neg (x\in A)]}$ 

Domaine (quantificateur existentiel).  Pour toute classe , il existe une classe constituée précisément des premiers composants des paires ordonnées de . ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage A}$

${\displaystyle \forall A\,\exists B\,\forall x\,[x\in B\iff \exists y((x,y)\in A)]}$ 

Par l'axiome d'extensionnalité, la classe dans l'axiome d'intersection et la classe dans les axiomes du complément et du domaine sont uniques. Ils seront notés par : et respectivement. D'un autre côté, l'extensionnalité n'est pas applicable à l'axiome d'appartenance puisqu'il ne spécifie que les ensembles qui sont des paires ordonnées. ${\style d'affichage C}$${\style d'affichage B}$${\style d'affichage A\cap B,}$ ${\displaystyle \complément A,}$${\displaystyle Dom(A),}$${\style d'affichage E}$${\style d'affichage E}$

Les trois premiers axiomes impliquent l'existence de la classe vide et de la classe de tous les ensembles : L'axiome d'appartenance implique l'existence d'une classe Les axiomes d'intersection et de complément impliquent l'existence de , qui est vide. Par l'axiome d'extensionnalité, cette classe est unique ; il est noté Le complément de est la classe de tous les ensembles, qui est également unique par extensionalité. Le prédicat d'ensemble , qui était défini comme , est maintenant redéfini pour éviter de quantifier sur des classes. ${\style d'affichage E.}$${\displaystyle E\cap \complément E}$${\displaystyle \emptyset .}$${\displaystyle \emptyset }$${\style d'affichage V}$${\style d'affichage M(A)}$${\displaystyle \existe C(A\in C)}$${\style d'affichage A\dans V}$

Axiomes pour la gestion des tuples :

Produit par . ${\style d'affichage V}$ Pour toute classe, il existe une classeconstituée des paires ordonnées dont le premier composant appartient. ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage A}$

${\displaystyle \forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A) ]}$

Permutation circulaire .  Pour toute classe, il existe une classedont les 3-uplets sont obtenus en appliquant la permutation circulaireaux 3-uplets de. ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage (y,z,x)\mapsto (x,y,z)}$${\style d'affichage A}$

${\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (y,z,x)\in UNE]}$

Transposition .  Pour toute classe, il existe une classedont les 3-uplets sont obtenus en transposant les deux dernières composantes des 3-uplets de. ${\style d'affichage A}$${\style d'affichage B}$${\style d'affichage A}$

${\displaystyle \forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (x,z,y)\in UNE]}$

Par extensionalité, le produit par axiome implique l'existence d'une classe unique, qui est notée par Cet axiome est utilisé pour définir la classe de tous les -uplets : et Si est une classe, l'extensionnalité implique que l'unique classe constituée des -uplets de Par exemple, l'axiome d'appartenance produit une classe qui peuvent contenir des éléments qui ne sont pas des paires ordonnées, alors que l'intersection ne contient que les couples de . ${\style d'affichage V}$${\displaystyle A\fois V.}$${\displaystyle V^{n}}$${\style d'affichage n}$${\style d'affichage V^{1}=V}$${\displaystyle V^{n+1}=V^{n}\times V.\,}$${\style d'affichage A}$${\displaystyle A\cap V^{n}}$${\style d'affichage n}$${\style d'affichage A.}$${\style d'affichage E}$${\displaystyle E\cap V^{2}}$${\style d'affichage E}$

Les axiomes de permutation circulaire et de transposition n'impliquent pas l'existence de classes uniques car ils ne spécifient que les 3-uplets de classe En spécifiant les 3-uplets, ces axiomes spécifient également les -uplets pour puisque : Les axiomes de gestion des tuples et l'axiome de domaine impliquent le lemme suivant, qui est utilisé dans la preuve du théorème d'existence de classe. ${\style d'affichage B.}$${\style d'affichage n}$${\style d'affichage n\geq 4}$${\displaystyle (x_{1},\ldots ,x_{n-2},x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-2}), x_{n-1},x_{n}).}$

Lemme du tuple.

1. ${\displaystyle \,\forall A\,\existe B_{1}\,\forall x\,\forall y\,\forall z\,[(z,x,y)\in B_{1}\iff ( x,y)\dans A]}$
2. ${\displaystyle \,\forall A\,\existe B_{2}\,\forall x\,\forall y\,\forall z\,[(x,z,y)\in B_{2}\iff ( x,y)\dans A]}$
3. ${\displaystyle \,\forall A\,\existe B_{3}\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B_{3}\iff ( x,y)\dans A]}$
4. ${\displaystyle \,\forall A\,\existe B_{4}\,\forall x\,\forall y\,\forall z\,[(y,x)\in B_{4}\iff (x, y)\dans A]}$

Preuve :   Classe : Appliquer le produit à pour produire Classe : Appliquer la transposition à pour produire Classe : Appliquer la permutation circulaire à pour produire Classe : Appliquer la permutation circulaire à , puis appliquer le domaine à produire${\style d'affichage B_{3}}$${\style d'affichage V}$${\style d'affichage A}$${\style d'affichage B_{3}.}$
            ${\style d'affichage B_{2}}$${\style d'affichage B_{3}}$${\style d'affichage B_{2}.}$
            ${\style d'affichage B_{1}}$${\style d'affichage B_{3}}$${\style d'affichage B_{1}.}$
            ${\style d'affichage B_{4}}$${\style d'affichage B_{2}}$${\style d'affichage B_{4}.}$

Un autre axiome est nécessaire pour prouver le théorème d'existence de classe : l' axiome de régularité . Puisque l'existence de la classe vide a été prouvée, l'énoncé habituel de cet axiome est donné.

Axiome de régularité .  Tout ensemble non vide a au moins un élément avec lequel il n'a aucun élément en commun.

${\displaystyle \forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].}$

Cet axiome implique qu'un ensemble ne peut appartenir à lui - même: Supposons que et laisser ensuite depuis ce qui contredit l'axiome de régularité , car est le seul élément Par conséquent, l'axiome de régularité interdit également les suites infinies d'adhésion descendante de jeux:${\style d'affichage x\dans x}$${\displaystyle a=\{x\}.}$${\displaystyle x\cap a\neq \emptyset }$${\displaystyle x\in x\cap a.}$${\style d'affichage x}$${\style d'affichage a.}$${\style d'affichage x\notin x.}$${\displaystyle \;\;\cdots \in x_{n+1}\in x_{n}\in \cdots \in x_{1}\in x_{0}.}$

Gödel a déclaré la régularité pour les classes plutôt que pour les ensembles dans sa monographie de 1940, qui était basée sur des conférences données en 1938. En 1939, il a prouvé que la régularité pour les ensembles implique la régularité pour les classes.

Théorème d'existence de classe

Théorème d'existence de classe.  Soit une formule qui quantifie uniquement sur des ensembles et ne contient pas de variables libres autres que (pas nécessairement toutes). Alors pour tout , il existe une unique classe de -uplets telle que : La classe est notée${\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}$${\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}$${\displaystyle Y_{1},\dots ,Y_{m}}$${\style d'affichage A}$${\style d'affichage n}$${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots , x_{n},Y_{1},\dots ,Y_{m})].}$${\style d'affichage A}$${\displaystyle \{(x_{1},\dots ,x_{n}):\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})\ }.}$

La preuve du théorème se fera en deux étapes :

1. Les règles de transformation sont utilisées pour transformer la formule donnée en une formule équivalente qui simplifie la partie inductive de la preuve. Par exemple, les seuls symboles logiques dans la formule transformée sont , , et , donc l'induction gère les symboles logiques avec seulement trois cas.${\style d'affichage \phi }$${\style d'affichage \neg }$${\displaystyle \land }$${\style d'affichage \existe }$
2. Le théorème d'existence de classe est prouvé inductivement pour les formules transformées. Guidés par la structure de la formule transformée, les axiomes d'existence de classe sont utilisés pour produire la classe unique de -uplets satisfaisant la formule.${\style d'affichage n}$

Règles de transformation.  Dans les règles 1 et 2 ci-dessous, et désignent des variables d'ensemble ou de classe. Ces deux règles éliminent toutes les occurrences de variables de classe avant un et toutes les occurrences d'égalité. Chaque fois que la règle 1 ou 2 est appliquée à une sous-formule, est choisie de manière à ce qu'elle diffère des autres variables de la formule actuelle. Les trois règles sont répétées jusqu'à ce qu'il n'y ait plus de sous-formules auxquelles elles puissent être appliquées. Cela produit une formule qui est construite uniquement avec , , , , set variables et class variables où n'apparaît pas avant un . ${\style d'affichage \Delta }$${\style d'affichage \Gamma }$${\style d'affichage \in }$${\style d'affichage i}$${\style d'affichage z_{i}}$${\style d'affichage \neg }$${\displaystyle \land }$${\style d'affichage \existe }$${\style d'affichage \in }$${\displaystyle Y_{k}}$${\displaystyle Y_{k}}$${\style d'affichage \in }$

1. ${\displaystyle \,Y_{k}\in \Gamma }$ se transforme en ${\displaystyle \exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma ).}$
2. L'extensionnalité est utilisée pour se transformer en${\displaystyle \Delta =\Gamma }$${\displaystyle \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ).}$
3. Les identités logiques sont utilisées pour transformer des sous-formules contenant et en sous-formules qui n'utilisent et${\displaystyle \lor ,\implies ,\iff ,}$${\displaystyle \forall }$${\displaystyle \neg ,\land ,}$${\displaystyle \exists .}$

Règles de transformation : variables liées .  Considérons la formule de fonction composée de l' exemple 1 avec ses variables libres remplacées par et : La preuve inductive enlèvera , ce qui produit la formule Cependant, puisque le théorème d'existence de classe est énoncé pour les variables indicées, cette formule n'a pas la forme attendue par hypothèse d'induction . Ce problème est résolu en remplaçant la variable par des variables liées au sein des quantificateurs imbriqués qui sont traités en augmentant l'indice de un pour chaque quantificateur successif. Cela conduit à la règle 4, qui doit être appliquée après les autres règles puisque les règles 1 et 2 produisent des variables quantifiées. ${\style d'affichage x_{1}}$${\style d'affichage x_{2}}$${\displaystyle \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G].}$${\displaystyle \existe t}$${\displaystyle (x_{1},t)\dans F\land (t,x_{2})\dans G.}$${\style d'affichage t}$${\style d'affichage x_{3}.}$

4. Si une formule ne contient aucune variable d'ensemble libre autre que les variables liées qui sont imbriquées dans les quantificateurs sont remplacées par . Ces variables ont une profondeur d'imbrication (quantificateur) .${\displaystyle x_{1},\dots ,x_{n},}$${\style d'affichage q}$${\style d'affichage x_{n+q}}$ ${\style d'affichage q}$

Exemple 2 : la   règle 4 est appliquée à la formule qui définit la classe constituée de tous les ensembles de la forme C'est-à-dire des ensembles qui contiennent au moins et un ensemble contenant — par exemple, où et sont des ensembles. ${\style d'affichage \phi (x_{1})}$${\displaystyle \{\emptyset ,\{\emptyset ,\dots \},\dots \}.}$${\displaystyle \emptyset }$${\displaystyle \emptyset }$${\displaystyle \{\emptyset ,\{\emptyset ,a,b,c\},d,e\}}$${\style d'affichage a,b,c,d,}$${\style d'affichage e}$ ${\displaystyle {\begin{aligned}\phi (x_{1})\,&=\,\exists u\;\,[\,u\in x_{1}\,\land \,\neg \exists v\;\,(\;v\,\in \,u\,)]\,\land \,\,\existe w\;{\bigl (}w\in x_{1}\,\land \ ,\existe y\;\,[(\;y\,\in w\;\land \;\neg \exists z\;\,(\;z\,\in \,y\,)]{\ bigr )}\\\phi _{r}(x_{1})\,&=\,\exists x_{2}[x_{2}\!\in \!x_{1}\,\land \, \neg \exists x_{3}(x_{3}\!\in \!x_{2})]\,\land \,\,\exists x_{2}{\bigl (}x_{2}\! \in \!x_{1}\,\land \,\exists x_{3}[(x_{3}\!\in \!x_{2}\,\land \,\neg \exists x_{4} (x_{4}\!\in \!x_{3})]{\bigr )}\end{aligned}}}$ Puisque c'est la seule variable libre, la variable quantifiée apparaît deux fois à la profondeur d'imbrication 2. Son indice est 3 car si deux portées de quantificateur sont à la même profondeur d'imbrication, elles sont soit identiques, soit disjointes. Les deux occurrences de sont dans des portées de quantificateur disjointes, elles n'interagissent donc pas les unes avec les autres. ${\style d'affichage x_{1}}$${\style d'affichage n=1.}$${\style d'affichage x_{3}}$${\displaystyle x_{3}\in x_{2}}$${\style d'affichage n+q=1+2=3.}$${\style d'affichage x_{3}}$

Démonstration du théorème d'existence de classe.  La preuve commence par appliquer les règles de transformation à la formule donnée pour produire une formule transformée. Puisque cette formule est équivalente à la formule donnée, la preuve est complétée en prouvant le théorème d'existence de classe pour les formules transformées.

Preuve du théorème d'existence de classe pour les formules transformées

Le lemme suivant est utilisé dans la preuve. ${\displaystyle {\mathsf {Expansion\;lemme.}}\,}$Soit et laissez être une classe contenant toutes les paires ordonnées satisfaisant C'est-à-dire que Then peut être développé dans la classe unique de -uplets satisfaisant . C'est-à-dire,${\style d'affichage 1\leq i<j\leq n,}$${\style d'affichage P}$${\style d'affichage (x_{i},x_{j})}$${\style d'affichage R(x_{i},x_{j}).}$${\displaystyle P\supseteq \{(x_{i},x_{j}):R(x_{i},x_{j})\}.}$${\style d'affichage P}$${\style d'affichage Q}$${\style d'affichage n}$${\style d'affichage R(x_{i},x_{j})}$${\displaystyle Q=\{(x_{1},\ldots ,x_{n}):R(x_{i},x_{j})\}.}$ ${\displaystyle {\mathsf {Preuve\!:}}}$ ${\displaystyle {\mathsf {Classe\;existence\;théorème\;pour\;transformé\;formules.}}\,}$ Soit une formule qui : ${\displaystyle \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})}$ Alors pour tout , il existe une classe unique de -uplets telle que : ${\displaystyle Y_{1},\dots ,Y_{m}}$${\style d'affichage A}$${\style d'affichage n}$ ${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots , x_{n},Y_{1},\ldots ,Y_{m})].}$ ${\displaystyle {\mathsf {Preuve\!:\,Base\;étape.}}\,}$ ${\style d'affichage \phi }$a 0 symboles logiques. L'hypothèse du théorème implique que est une formule atomique de la forme ou${\style d'affichage \phi }$${\displaystyle x_{i}\in x_{j}}$${\displaystyle x_{i}\in Y_{k}.}$ ${\displaystyle {\mathsf {Inductif\;step.}}\;\phi }$a des symboles logiques où . Supposons l'hypothèse d'induction que le théorème est vrai pour tous avec moins de symboles logiques. Démontrons maintenant le théorème pour avec des symboles logiques. Dans cette preuve, la liste des variables de classe est abrégée par , donc une formule - telle que - peut être écrite sous la forme${\style d'affichage k}$${\style d'affichage k>0}$${\style d'affichage \psi }$${\style d'affichage k}$${\style d'affichage \phi }$${\style d'affichage k}$${\displaystyle Y_{1},\dots ,Y_{m}}$${\displaystyle {\vec {Y}}}$${\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}$${\displaystyle \phi (x_{1},\dots ,x_{n},{\vec {Y}}).}$

Gödel a souligné que le théorème d'existence de classe "est un métathéorème , c'est-à-dire un théorème sur le système [NBG], pas dans le système …" C'est un théorème sur NBG car il est prouvé dans la métathéorie par induction sur les formules NBG. En outre, sa preuve - au lieu d'invoquer un nombre fini d'axiomes NBG - décrit de manière inductive comment utiliser les axiomes NBG pour construire une classe satisfaisant une formule donnée. Pour chaque formule, cette description peut être transformée en une preuve d'existence constructive qui se trouve dans NBG. Par conséquent, ce métathéorème peut générer les preuves NBG qui remplacent les utilisations du théorème d'existence de classe de NBG.

Un programme informatique récursif capture succinctement la construction d'une classe à partir d'une formule donnée. La définition de ce programme ne dépend pas de la preuve du théorème d'existence de classe. Cependant, la preuve est nécessaire pour prouver que la classe construite par le programme satisfait la formule donnée et est construite en utilisant les axiomes. Ce programme est écrit en pseudocode qui utilise une instruction case de style Pascal .

${\displaystyle \mathbf {function} \;{\text{Class}}(\phi ,\,n)}$
${\displaystyle {\begin{aligned}\mathbf {input} \!:\;\,&\phi {\text{ est une formule transformée de la forme }}\phi (x_{1},\ldots ,x_{ n},Y_{1},\ldots ,Y_{m});\\&n{\text{ spécifie qu'une classe de }}n{\text{-tuples est renvoyée.}}\\\;\;\ ;\;\mathbf {sortie} \!:\;\,&{\text{class }}A{\text{ of }}n{\text{-tuples satisfaisant }}\\&\,\forall x_{ 1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n},Y_{ 1},\ldots ,Y_{m})].\end{aligned}}}$

${\displaystyle \mathbf {commencer} }$

${\displaystyle \mathbf {cas} \;\phi \;\mathbf {of} }$

${\displaystyle {\begin{alignedat}{2}x_{i}\in x_{j}:\;\;&\mathbf {return} \;\,E_{i,j,n};&&{\text {// }}E_{i,j,n}\;\,=\{(x_{1},\dots ,x_{n}):x_{i}\in x_{j}\}\\x_ {i}\in Y_{k}:\;\;&\mathbf {return} \;\,E_{i,Y_{k},n};&&{\text{// }}E_{i,Y_ {k},n}=\{(x_{1},\dots ,x_{n}):x_{i}\in Y_{k}\}\\\neg \psi :\;\;&\mathbf {retour} \;\,\complément _{V^{n}}{\text{Class}}(\psi ,\,n);&&{\text{// }}\complément _{V^{n }}{\text{Class}}(\psi ,\,n)=V^{n}\setminus {\text{Class}}(\psi ,\,n)\\\psi _{1}\land \psi _{2}:\;\;&\mathbf {return} \;\,{\text{Class}}(\psi _{1},\,n)\cap {\text{Class}}( \psi _{2},\,n);&&\\\;\;\;\;\,\exists x_{n+1}(\psi ):\;\;&\mathbf {return} \; \,Dom({\text{Class}}(\psi ,\,n+1));&&{\text{// }}x_{n+1}{\text{ est libre dans }}\psi ; {\text{ Class}}(\psi ,\,n+1)\\&\ &&{\text{// renvoie une classe de }}(n+1){\text{-tuples}}\end{ aligné}}}$

${\displaystyle \mathbf {fin} }$

${\displaystyle \mathbf {fin} }$

Soit la formule de l' exemple 2 . L'appel de fonction génère la classe qui est comparée ci-dessous avec Cela montre que la construction de la classe reflète la construction de sa formule de définition${\style d'affichage \phi }$${\displaystyle A=Classe(\phi ,1)}$${\style d'affichage A,}$${\style d'affichage \phi .}$${\style d'affichage A}$${\style d'affichage \phi .}$

${\displaystyle {\begin{alignedat}{2}&\phi \;&&=\;\;\existe x_{2}\,(x_{2}\!\in \!x_{1}\land \; \;\neg \;\;\;\;\existe x_{3}\;(x_{3}\!\in \!x_{2}))\,\land \;\;\,\existe x_ {2}\,(x_{2}\!\in \!x_{1}\land \;\;\,\existe x_{3}\,(x_{3}\!\in \!x_{2 }\,\land \;\;\neg \;\;\;\;\existe x_{4}\;(x_{4}\!\in \!x_{3})))\\&A\; &&=Dom\,(\;E_{2,1,2}\;\cap \;\complément _{V^{2}}\,Dom\,(\;E_{3,2,3}\; ))\,\cap \,Dom\,(\;E_{2,1,2}\;\cap \,Dom\,(\;\,E_{3,2,3}\;\cap \; \complement _{V^{3}}\,Dom\,(\;E_{4,3,4}\;)))\end{alignedat}}}$

Extension du théorème d'existence de classe

Gödel a étendu le théorème d'existence de classe aux formules contenant des relations sur des classes (telles que et la relation unaire ), des classes spéciales (telles que ) et des opérations (telles que et ). Pour étendre le théorème d'existence de classe, les formules définissant les relations, les classes spéciales et les opérations doivent quantifier uniquement sur des ensembles. Alors peut être transformé en une formule équivalente satisfaisant l' hypothèse du théorème d'existence de classe . ${\style d'affichage \phi }$${\displaystyle Y_{1}\subseteq Y_{2}}$ ${\style d'affichage M(A_{1})}$${\displaystyle Ordre}$ ${\style d'affichage (x_{1},x_{2})}$${\displaystyle x_{1}\cap Y_{1}}$${\style d'affichage \phi }$

Les définitions suivantes spécifient comment les formules définissent les relations, les classes spéciales et les opérations :

1. Une relation est définie par :${\style d'affichage R}$${\displaystyle R(Z_{1},\dots ,Z_{k})\iff \psi _{R}(Z_{1},\dots ,Z_{k}).}$
2. Une classe spéciale est définie par :${\style d'affichage C}$${\displaystyle u\in C\iff \psi _{C}(u).}$
3. Une opération est définie par :${\style d'affichage P}$${\displaystyle u\in P(Z_{1},\dots ,Z_{k})\iff \psi _{P}(u,Z_{1},\dots ,Z_{k}).}$

Un terme est défini par :

1. Les variables et les classes spéciales sont des termes.
2. Si est une opération avec des arguments et sont des termes, alors est un terme.${\style d'affichage P}$${\style d'affichage k}$${\displaystyle \Gamma _{1},\dots ,\Gamma _{k}}$${\style d'affichage P(\Gamma _{1},\dots ,\Gamma _{k})}$

Les règles de transformation suivantes éliminent les relations, les classes spéciales et les opérations. Chaque fois que la règle 2b, 3b ou 4 est appliquée à une sous-formule, est choisie de manière à ce qu'elle diffère des autres variables de la formule actuelle. Les règles sont répétées jusqu'à ce qu'il n'y ait plus de sous-formules auxquelles elles peuvent être appliquées. et désigne des termes. ${\style d'affichage i}$${\style d'affichage z_{i}}$${\displaystyle \,\Gamma _{1},\dots ,\Gamma _{k},\Gamma ,}$${\style d'affichage \Delta }$

Exemple 3 :  Transformation${\displaystyle Y_{1}\subseteq Y_{2}.}$ ${\displaystyle Y_{1}\subseteq Y_{2}\iff \forall z_{1}(z_{1}\in Y_{1}\implies z_{1}\in Y_{2})\quad {\text {(règle 1)}}}$

Exemple 4 :  Transformation${\displaystyle x_{1}\cap Y_{1}\in x_{2}.}$ ${\displaystyle {\begin{alignedat}{2}x_{1}\cap Y_{1}\in x_{2}&\iff \exists z_{1}[z_{1}=x_{1}\cap Y_ {1}\,\land \,z_{1}\in x_{2}]&&{\text{(règle 3b)}}\\&\iff \exists z_{1}[\forall z_{2}( z_{2}\in z_{1}\iff z_{2}\in x_{1}\cap Y_{1})\,\land \,z_{1}\in x_{2}]&&{\text {(règle 4)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\land z_{2}\in Y_{1})\,\land \,z_{1}\in x_{2}]\quad &&{\text{(règle 3a)}}\\\end{alignedat}}}$ Cet exemple illustre comment les règles de transformation fonctionnent ensemble pour éliminer une opération.

Théorème d'existence de classe (version étendue).  Soit une formule qui quantifie uniquement sur des ensembles, ne contient aucune variable libre autre que , et peut contenir des relations, des classes spéciales et des opérations définies par des formules qui quantifient uniquement sur des ensembles. Alors pour tout il existe une classe unique de -uplets tels que${\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}$${\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}$${\displaystyle Y_{1},\dots ,Y_{m},}$${\style d'affichage A}$${\style d'affichage n}$${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots , x_{n},Y_{1},\dots ,Y_{m})].}$

Preuve :  appliquez les règles de transformation à pour produire une formule équivalente ne contenant aucune relation, classe spéciale ou opération. Cette formule satisfait l'hypothèse du théorème d'existence de classe. Par conséquent, pour tous, il existe une classe unique de -uplets satisfaisant${\style d'affichage \phi }$${\displaystyle Y_{1},\dots ,Y_{m},}$${\style d'affichage A}$${\style d'affichage n}$${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots , x_{n},Y_{1},\dots ,Y_{m})].}$

Définir des axiomes

Les axiomes d'appariement et de régularité, qui étaient nécessaires pour la preuve du théorème d'existence de classe, ont été donnés ci-dessus. NBG contient quatre autres axiomes d'ensemble. Trois de ces axiomes traitent des opérations de classe appliquées aux ensembles.

Définition.   est une fonction si${\style d'affichage F}$${\displaystyle F\subseteq V^{2}\land \forall x\,\forall y\,\forall z\,[(x,y)\in F\,\land \,(x,z)\in F\implique y=z].}$

En théorie des ensembles, la définition d'une fonction ne nécessite pas de spécifier le domaine ou le codomaine de la fonction (voir Fonction (théorie des ensembles) ). La définition de fonction de NBG généralise la définition de ZFC d'un ensemble de paires ordonnées à une classe de paires ordonnées.

Les définitions de ZFC des opérations ensemblistes de image , union et power set sont également généralisées aux opérations de classe. L'image de classe sous la fonction est Cette définition ne nécessite pas que L'union de classe est La classe de puissance de est La version étendue du théorème d'existence de classe implique l'existence de ces classes. Les axiomes de remplacement, d' union et d' ensemble de puissance impliquent que lorsque ces opérations sont appliquées à des ensembles, elles produisent des ensembles. ${\style d'affichage A}$${\style d'affichage F}$${\displaystyle F[A]=\{y:\existe x(x\in A\,\land \,(x,y)\in F)\}.}$${\displaystyle A\subseteq Dom(F).}$${\style d'affichage A}$${\displaystyle \cup A=\{x:\exists y(x\in y\,\,\land \,y\in A)\}.}$${\style d'affichage A}$${\displaystyle {\mathcal {P}}(A)=\{x:x\subseteq A\}.}$

Axiome de remplacement.  Si est une fonction et est un ensemble, alors , l' image de under , est un ensemble. ${\style d'affichage F}$${\style d'affichage a}$${\style d'affichage F[a]}$${\style d'affichage a}$${\style d'affichage F}$

${\displaystyle \forall F\,\forall a\,[F{\text{ is a function}}\implies \exists b\,\forall y\,(y\in b\iff \exists x(x\in a\,\land \,(x,y)\in F))].}$

Ne pas avoir l'exigence dans la définition de produit un axiome de remplacement plus fort, qui est utilisé dans la preuve suivante. ${\displaystyle A\subseteq Dom(F)}$${\style d'affichage F[A]}$

Théorème ( axiome de séparation de NBG ).  Si est un ensemble et est une sous-classe de alors est un ensemble. Preuve : Le théorème d'existence de classe construit la restriction de la fonction identité à : Puisque l'image de under est , l'axiome de remplacement implique que est un ensemble. Cette preuve dépend de la définition d'image n'ayant pas l'exigence puisque plutôt que${\style d'affichage a}$${\style d'affichage B}$${\style d'affichage a,}$${\style d'affichage B}$
 ${\style d'affichage B}$${\displaystyle I{\upharpoonright _{B}}=\{(x_{1},x_{2}):x_{1}\in B\land x_{2}=x_{1}\}.}$${\style d'affichage a}$${\displaystyle I{\upharpoonright _{B}}}$${\style d'affichage B}$${\style d'affichage B}$${\displaystyle a\subseteq Dom(F)}$${\displaystyle Dom(I{\upharpoonright _{B}})=B\subseteq a}$${\displaystyle a\subseteq Dom(I{\upharpoonright _{B}}).}$

Axiome d'union.  Si est un ensemble, alors il existe un ensemble contenant${\style d'affichage a}$${\displaystyle \cup a.}$

${\displaystyle \forall a\,\exists b\,\forall x\,[\,\exists y(x\in y\,\,\land \,y\in a)\implies x\in b\, ].}$

Ensemble d'axiomes de puissance.  Si est un ensemble, alors il existe un ensemble contenant${\style d'affichage a}$${\displaystyle {\mathcal {P}}(a).}$

${\displaystyle \forall a\,\exists b\,\forall x\,(x\subseteq a\implies x\in b).}$

Théorème.  Si est un ensemble, alors et sont des ensembles. Preuve : L'axiome de l'union indique qu'il s'agit d'une sous-classe d'un ensemble , donc l'axiome de séparation implique qu'il s'agit d'un ensemble. De même, l'axiome de l'ensemble de puissance indique qu'il s'agit d'une sous-classe d'un ensemble , donc l'axiome de séparation implique qu'il s'agit d'un ensemble. ${\style d'affichage a}$${\displaystyle \cup a}$${\displaystyle {\mathcal {P}}(a)}$
 ${\displaystyle \cup a}$${\style d'affichage b}$${\displaystyle \cup a}$${\displaystyle {\mathcal {P}}(a)}$${\style d'affichage b}$${\displaystyle {\mathcal {P}}(a)}$

Axiome de l'infini.  Il existe un ensemble non vide tel que pour tout in , il existe un in tel qui soit un sous-ensemble propre de . ${\style d'affichage a}$${\style d'affichage x}$${\style d'affichage a}$${\style d'affichage y}$${\style d'affichage a}$${\style d'affichage x}$${\style d'affichage y}$

${\displaystyle \exists a\,[\exists u(u\in a)\,\land \,\forall x(x\in a\implies \exists y(y\in a\,\land \,x\ sous-ensemble y))].}$

Les axiomes de l'infini et du remplacement prouvent l'existence de l' ensemble vide . Dans la discussion des axiomes d'existence de classe , l'existence de la classe vide a été prouvée. Nous montrons maintenant que c'est un ensemble. Soit fonction et soit l'ensemble donné par l'axiome de l'infini. Par remplacement, l'image de under , qui vaut , est un ensemble. ${\displaystyle \emptyset }$${\displaystyle \emptyset }$${\displaystyle F=\emptyset }$${\style d'affichage a}$${\style d'affichage a}$${\style d'affichage F}$${\displaystyle \emptyset }$

L'axiome de l'infini de NBG est impliqué par l' axiome de l'infini de ZFC : Le premier conjoint de l'axiome de ZFC, , implique le premier conjoint de l'axiome de NBG. La deuxième conjonction de l'axiome de ZFC, , implique la deuxième conjonction de l'axiome de NBG puisque Pour prouver l'axiome de l'infini de ZFC à partir de l'axiome de l'infini de NBG, il faut certains des autres axiomes de NBG (voir Axiome faible de l'infini ). ${\displaystyle \,\existe a\,[\emptyset \in a\,\land \,\forall x(x\in a\implies x\cup \{x\}\in a)].\,}$${\displaystyle \emptyset \in a}$${\displaystyle \forall x(x\in a\implies x\cup \{x\}\in a)}$${\displaystyle x\sous-ensemble x\cup \{x\}.}$

Axiome du choix global

Le concept de classe permet à NBG d'avoir un axiome de choix plus fort que ZFC. Une fonction de choix est une fonction définie sur un ensemble d' ensembles non vides telle que pour tous les états d'axiome de choix de ZFC, il existe une fonction de choix pour chaque ensemble d'ensembles non vides. Une fonction de choix global est une fonction définie sur la classe de tous les ensembles non vides telle que pour tout ensemble non vide L'axiome du choix global énonce qu'il existe une fonction de choix global. Cet axiome implique l'axiome de choix de ZFC puisque pour chaque ensemble d' ensembles non vides, (la restriction de à ) est une fonction de choix pour En 1964, William B. Easton a prouvé que le choix global est plus fort que l'axiome de choix en utilisant le forçage pour construire un modèle qui satisfait l'axiome de choix et tous les axiomes de NBG sauf l'axiome de choix global. L'axiome de choix global est équivalent à chaque classe ayant un bon ordre, tandis que l'axiome de choix de ZFC est équivalent à chaque ensemble ayant un bon ordre. ${\style d'affichage f}$${\style d'affichage s}$${\style d'affichage f(x)\dans x}$${\displaystyle x\in s.}$${\style d'affichage G}$${\style d'affichage G(x)\dans x}$${\style d'affichage x.}$${\style d'affichage s}$${\displaystyle G\vert _{s}}$${\style d'affichage G}$${\style d'affichage s}$${\style d'affichage s.}$

Axiome du choix global.  Il existe une fonction qui choisit un élément dans chaque ensemble non vide.

${\displaystyle \exists G\,[G{\text{ is a function}}\,\land \forall x(x\neq \emptyset \implies \exists y(y\in x\land (x,y)\ en G))].}$

Histoire

Le système d'axiomes de Von Neumann de 1925

Von Neumann a publié un article d'introduction sur son système d'axiome en 1925. En 1928, il a fourni un traitement détaillé de son système. Von Neumann a basé son système d'axiomes sur deux domaines d' objets primitifs : les fonctions et les arguments. Ces domaines se chevauchent : les objets qui se trouvent dans les deux domaines sont appelés fonctions d'argument. Les fonctions correspondent à des classes dans NBG, et les fonctions-arguments correspondent à des ensembles. L'opération primitive de Von Neumann est l'application de fonction , notée [ a ,  x ] plutôt que a ( x ) où a est une fonction et x est un argument. Cette opération produit un argument. Von Neumann a défini des classes et des ensembles en utilisant des fonctions et des fonctions-arguments qui ne prennent que deux valeurs, A et B . Il a défini x  ∈  a si [ a ,  x ]  A .

Le travail de Von Neumann en théorie des ensembles a été influencé par les articles de Georg Cantor , les axiomes d'Ernst Zermelo pour la théorie des ensembles de 1908 et les critiques de 1922 de la théorie des ensembles de Zermelo qui ont été données indépendamment par Abraham Fraenkel et Thoralf Skolem . Fraenkel et Skolem ont tous deux souligné que les axiomes de Zermelo ne peuvent prouver l'existence de l'ensemble { Z ₀ ,  Z ₁ ,  Z ₂ , ...} où Z ₀ est l'ensemble des nombres naturels et Z _{n +1} est l' ensemble des puissances de Z _n . Ils ont alors introduit l'axiome de remplacement, qui garantirait l'existence de tels ensembles. Cependant, ils étaient réticents à adopter cet axiome : Fraenkel a déclaré « que le remplacement était un axiome trop fort pour la « théorie générale des ensembles » », tandis que « Skolem a seulement écrit que « nous pourrions introduire » le remplacement ».

Von Neumann a travaillé sur les problèmes de la théorie des ensembles de Zermelo et a apporté des solutions à certains d'entre eux :

• Une théorie des ordinaux
  • Problème : La théorie des nombres ordinaux de Cantor ne peut pas être développée dans la théorie des ensembles de Zermelo car il lui manque l'axiome du remplacement.
  • Solution : Von Neumann a récupéré la théorie de Cantor en définissant les ordinaux en utilisant des ensembles bien ordonnés par la relation ∈, et en utilisant l'axiome de remplacement pour prouver les théorèmes clés sur les ordinaux, tels que chaque ensemble bien ordonné est isomorphe d'ordre avec un ordinal. Contrairement à Fraenkel et Skolem, von Neumann a souligné l'importance de l'axiome de remplacement pour la théorie des ensembles : « En fait, je crois qu'aucune théorie des ordinaux n'est possible sans cet axiome.
• Un critère identifiant les classes trop grandes pour être définies
  • Problème : Zermelo n'a pas fourni un tel critère. Sa théorie des ensembles évite les grandes classes qui conduisent aux paradoxes , mais elle laisse de côté de nombreux ensembles, comme celui mentionné par Fraenkel et Skolem.
  • Solution : Von Neumann a introduit le critère : Une classe est trop grande pour être un ensemble si et seulement si elle peut être mappée sur la classe V de tous les ensembles. Von Neumann s'est rendu compte que les paradoxes de la théorie des ensembles pouvaient être évités en ne permettant pas à de si grandes classes d'être membres d'une classe. En combinant cette restriction avec son critère, il a obtenu son axiome de limitation de taille : Une classe C n'est membre d'aucune classe si et seulement si C peut être mappé sur V .
• Axiomatisation finie
  • Problème : Zermelo avait utilisé le concept imprécis de « fonction propositionnelle définie » dans son axiome de séparation .
  • Solutions : Skolem a introduit le schéma axiome de séparation qui a ensuite été utilisé dans ZFC, et Fraenkel a introduit une solution équivalente. Cependant, Zermelo a rejeté les deux approches "en particulier parce qu'elles impliquent implicitement le concept de nombre naturel qui, selon Zermelo, devrait être basé sur la théorie des ensembles". Von Neumann a évité les schémas d'axiomes en formalisant le concept de « fonction propositionnelle définie » avec ses fonctions, dont la construction ne nécessite qu'un nombre fini d'axiomes. Cela a conduit à sa théorie des ensembles ayant un nombre fini d'axiomes. En 1961, Richard Montague a prouvé que ZFC ne peut pas être axiomatisé de manière finie.
• L'axiome de régularité
  • Problème : la théorie des ensembles de Zermelo commence avec l'ensemble vide et un ensemble infini, et réitère les axiomes d'appariement, d'union, d'ensemble de puissance, de séparation et de choix pour générer de nouveaux ensembles. Cependant, il ne limite pas les ensembles à ceux-ci. Par exemple, il autorise des ensembles qui ne sont pas bien fondés , comme un ensemble x satisfaisant x  ∈  x .
  • Solutions : Fraenkel a introduit un axiome pour exclure ces ensembles. Von Neumann a analysé l'axiome de Fraenkel et a déclaré qu'il n'était pas « précisément formulé », mais il dirait approximativement : « En plus des ensembles... dont l'existence est absolument requise par les axiomes, il n'y a pas d'autres ensembles ». Von Neumann a proposé l'axiome de régularité comme moyen d'exclure les ensembles non fondés, mais ne l'a pas inclus dans son système d'axiomes. En 1930, Zermelo est devenu le premier à publier un système d'axiomes incluant la régularité.

Le système d'axiomes de Von Neumann de 1929

En 1929, von Neumann a publié un article contenant les axiomes qui conduiraient à NBG. Cet article était motivé par son souci de cohérence de l'axiome de limitation de taille. Il a déclaré que cet axiome « ​​fait beaucoup, en fait trop ». En plus d'impliquer les axiomes de séparation et de remplacement, et le théorème de bon ordre , cela implique également que toute classe dont le cardinal est inférieur à celui de V est un ensemble. Von Neumann pense que cette dernière implication va au-delà de la théorie des ensembles cantorienne et conclut : « Nous devons donc discuter si sa cohérence [de l'axiome] n'est pas encore plus problématique qu'une axiomatisation de la théorie des ensembles qui ne dépasse pas le cadre cantorien nécessaire.

Von Neumann a commencé son enquête sur la cohérence en introduisant son système d'axiomes de 1929, qui contient tous les axiomes de son système d'axiomes de 1925 à l'exception de l'axiome de limitation de taille. Il a remplacé cet axiome par deux de ses conséquences, l'axiome de remplacement et un axiome de choix. L'axiome de choix de Von Neumann énonce : « Chaque relation R a une sous-classe qui est une fonction avec le même domaine que R .

Soit S le système d'axiomes de von Neumann de 1929. Von Neumann a introduit le système d'axiome S + Régularité (qui se compose de S et de l'axiome de régularité) pour démontrer que son système de 1925 est cohérent par rapport à S . Il a prouvé :

1. Si S est cohérent, alors S + Régularité est cohérent.
2. S + Régularité implique l'axiome de limitation de taille. Comme c'est le seul axiome de son système d'axiomes de 1925 que S + Régularité n'a pas, S + Régularité implique tous les axiomes de son système de 1925.

Ces résultats impliquent : Si S est cohérent, alors le système d'axiomes de von Neumann de 1925 est cohérent. Preuve : Si S est cohérent, alors S + Régularité est cohérent (résultat 1). En utilisant la preuve par contradiction , supposons que le système d'axiomes de 1925 est incohérent, ou de manière équivalente : le système d'axiomes de 1925 implique une contradiction. Puisque S + Régularité implique les axiomes du système de 1925 (résultat 2), S + Régularité implique également une contradiction. Cependant, cela contredit la cohérence de S + Régularité. Par conséquent, si S est cohérent, alors le système d'axiomes de von Neumann de 1925 est cohérent.

Puisque S est son système d'axiome de 1929, le système d'axiome de von Neumann de 1925 est cohérent par rapport à son système d'axiome de 1929, qui est plus proche de la théorie des ensembles de Cantor. Les principales différences entre la théorie des ensembles cantorienne et le système d'axiomes de 1929 sont les classes et l'axiome du choix de von Neumann. Le système d'axiome S + Régularité a été modifié par Bernays et Gödel pour produire le système d'axiome NBG équivalent.

Système d'axiome de Bernays

En 1929, Paul Bernays a commencé à modifier le nouveau système d'axiomes de von Neumann en prenant des classes et des ensembles comme primitifs. Il a publié son travail dans une série d'articles parus de 1937 à 1954. Bernays a déclaré que :

Le but de la modification du système de von Neumann est de rester plus proche de la structure du système original de Zermelo et d'utiliser en même temps certains des concepts de la théorie des ensembles de la logique de Schröder et des Principia Mathematica qui sont devenus familiers aux logiciens. Comme on le verra, une simplification considérable résulte de cette disposition.

Bernays a géré les ensembles et les classes dans une logique à deux tris et a introduit deux primitives d'appartenance : une pour l'appartenance à des ensembles et une pour l'appartenance à des classes. Avec ces primitives, il a réécrit et simplifié les axiomes de von Neumann de 1929. Bernays a également inclus l'axiome de régularité dans son système d'axiomes.

Système d'axiome de Gödel (NBG)

En 1931, Bernays envoya une lettre contenant sa théorie des ensembles à Kurt Gödel . Gödel a simplifié la théorie de Bernays en faisant de chaque ensemble une classe, ce qui lui a permis d'utiliser une seule sorte et une seule primitive d'appartenance. Il a également affaibli certains des axiomes de Bernays et remplacé l'axiome du choix de von Neumann par l'axiome équivalent du choix global. Gödel a utilisé ses axiomes dans sa monographie de 1940 sur la cohérence relative du choix global et l'hypothèse du continuum généralisé.

Plusieurs raisons ont été avancées pour que Gödel ait choisi NBG pour sa monographie :

• Gödel a donné une raison mathématique : le choix global de NBG produit un théorème de cohérence plus fort : « Cette forme plus forte de l'axiome [du choix], si elle est cohérente avec les autres axiomes, implique, bien sûr, qu'une forme plus faible est également cohérente. »
• Robert Solovay a conjecturé: "Je suppose qu'il [Gödel] a souhaité éviter une discussion sur les aspects techniques impliqués dans le développement des rudiments de la théorie des modèles au sein de la théorie des ensembles axiomatiques."
• Kenneth Kunen a donné une raison pour que Gödel évite cette discussion : « Il y a aussi une approche beaucoup plus combinatoire de L [l' univers constructible ], développée par... [Gödel dans sa monographie de 1940] dans une tentative d'expliquer son travail à des non- logiciens. ... Cette approche a le mérite d'éliminer tout vestige de logique du traitement de L ."
• Charles Parsons a fourni une raison philosophique pour le choix de Gödel : « Cette vue [que la 'propriété de l'ensemble' est une primitive de la théorie des ensembles] peut se refléter dans le choix de Gödel d'une théorie avec des variables de classe comme cadre pour ... [sa monographie] ."

La réalisation de Gödel ainsi que les détails de sa présentation ont conduit à la proéminence dont NBG bénéficiera au cours des deux prochaines décennies. En 1963, Paul Cohen a prouvé ses preuves d' indépendance pour ZF à l'aide de certains outils que Gödel avait développés pour ses preuves de cohérence relative pour NBG. Plus tard, ZFC est devenu plus populaire que NBG. Cela a été causé par plusieurs facteurs, y compris le travail supplémentaire requis pour gérer le forçage dans NBG, la présentation du forçage par Cohen en 1966, qui utilisait ZF, et la preuve que NBG est une extension conservatrice de ZFC.

NBG, ZFC et MK

NBG n'est pas logiquement équivalent à ZFC car son langage est plus expressif : il peut faire des déclarations sur les classes, ce qui ne peut pas être fait dans ZFC. Cependant, NBG et ZFC impliquent les mêmes déclarations sur les ensembles. Par conséquent, NBG est une extension conservatrice de ZFC. NBG implique des théorèmes que ZFC n'implique pas, mais puisque NBG est une extension conservatrice, ces théorèmes doivent impliquer des classes appropriées. Par exemple, c'est un théorème de NBG que l'axiome global du choix implique que la classe appropriée V peut être bien ordonnée et que chaque classe appropriée peut être mise en correspondance biunivoque avec V .

Une conséquence de l'extension conservatrice est que ZFC et NBG sont équicohérents . Le prouver utilise le principe de l'explosion : à partir d'une contradiction , tout est prouvable. Supposons que ZFC ou NBG soit incohérent. Alors la théorie inconsistante implique les déclarations contradictoires ∅ = ∅ et ∅ ≠ ∅, qui sont des déclarations sur les ensembles. Par la propriété d'extension conservatrice, l'autre théorie implique également ces déclarations. Par conséquent, il est également incohérent. Ainsi, bien que NBG soit plus expressif, il est équicohérent avec ZFC. Ce résultat ainsi que la preuve de cohérence relative de von Neumann de 1929 implique que son système d'axiomes de 1925 avec l'axiome de limitation de taille est équicohérent avec ZFC. Cela résout complètement la préoccupation de von Neumann concernant la cohérence relative de cet axiome puissant puisque ZFC est dans le cadre cantorien.

Même si NBG est une extension conservatrice de ZFC, un théorème peut avoir une preuve plus courte et plus élégante dans NBG que dans ZFC (ou vice versa). Pour une étude des résultats connus de cette nature, voir Pudlák 1998 .

La théorie des ensembles de Morse-Kelley a un schéma d'axiome de compréhension de classe qui inclut des formules dont les quantificateurs s'étendent sur des classes. MK est une théorie plus forte que NBG car MK prouve la cohérence de NBG, tandis que le deuxième théorème d'incomplétude de Gödel implique que NBG ne peut pas prouver la cohérence de NBG.

Pour une discussion de certaines questions ontologiques et autres questions philosophiques posées par NBG, en particulier lorsqu'elles sont comparées à ZFC et MK, voir l'annexe C de Potter 2004 .

Des modèles

ZFC, NBG et MK ont des modèles descriptible en termes de hiérarchie cumulative V _α  et la hiérarchie constructible L _α  . Soit V incluant un cardinal inaccessible κ, soit X ⊆ V _κ , et soit Def( X ) la classe des sous -ensembles définissables de premier ordre de X avec des paramètres. Dans les symboles où " " désigne le modèle avec domaine et relation , et " " désigne la relation de satisfaction : ${\style d'affichage (X,\in )}$ ${\style d'affichage X}$${\style d'affichage \in }$${\displaystyle \models }$

${\displaystyle \operatorname {Def} (X):={\Bigl \{}\{x\mid x\in X{\text{ et }}(X,\in )\models \phi (x,y_{ 1},\ldots ,y_{n})\} :\phi {\text{ est une formule du premier ordre et }}y_{1},\ldots ,y_{n}\in X{\Bigr \}} .}$

Puis:

• ( V _κ , ∈) et ( L _κ , ∈) sont des modèles de ZFC .
• ( V _κ ,  V _{κ + 1} , ∈) est un modèle de MK où V _κ se compose des ensembles de modèle et V _{κ + 1} est constitué par les classes du modèle. Puisqu'un modèle de MK est un modèle de NBG, ce modèle est également un modèle de NBG.
• ( V _κ , Def( V _κ ), ∈) est un modèle de la version de Mendelson de NBG, qui remplace l'axiome de choix global de NBG par l'axiome de choix de ZFC. Les axiomes de ZFC sont vrais dans ce modèle car ( V _κ , ∈) est un modèle de ZFC. En particulier, l'axiome du choix de ZFC est valable, mais le choix global de NBG peut échouer. Les axiomes d'existence de classe de NBG sont vrais dans ce modèle car les classes dont ils affirment l'existence peuvent être définies par des définitions de premier ordre. Par exemple, l'axiome d'appartenance est vrai puisque la classe est définie par :${\style d'affichage E}$

${\displaystyle E=\{x\in V_{\kappa }:(V_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v] \}.}$

• ( L _κ , L _{κ ⁺} , ∈), où κ ⁺ est le cardinal successeur de κ, est un modèle de NBG. Les axiomes d'existence de classe de NBG sont vrais dans ( L _κ ,  L _{κ ⁺} , ∈). Par exemple, l'axiome d'appartenance est vrai puisque la classe est définie par :${\style d'affichage E}$

${\displaystyle E=\{x\in L_{\kappa }:(L_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v] \}.}$

Donc E  𝒫( L _κ ). Dans sa preuve que GCH est vrai dans L , Gödel a prouvé que 𝒫( L _κ ) ⊆  L _{κ ⁺} . Par conséquent, E  de  la L _{κ ⁺} , donc l'axiome d'appartenance est vrai ( L _κ ,  L _{κ ⁺} , ∈). De même, les autres axiomes d'existence de classe sont vrais. L'axiome du choix global est vrai parce que L _κ est bien ordonné par la restriction de la fonction de Gödel (qui mappe la classe des ordinaux aux ensembles constructibles) aux ordinaux moins de κ. Par conséquent, ( L _κ ,  L _{κ ⁺} , ∈) est un modèle de NBG.

Théorie des catégories

L'ontologie de NBG fournit un échafaudage pour parler de « grands objets » sans risquer le paradoxe. Par exemple, dans certains développements de la théorie des catégories , une « grande catégorie » est définie comme celle dont les objets et les morphismes constituent une classe propre. D'autre part, une « petite catégorie » est celle dont les objets et les morphismes sont membres d'un ensemble. Ainsi, on peut parler de « catégorie de tous les ensembles » ou de « catégorie de toutes les petites catégories » sans risquer de paradoxe puisque NBG supporte les grandes catégories.

Cependant, NBG ne prend pas en charge une "catégorie de toutes les catégories" car les grandes catégories en seraient membres et NBG ne permet pas aux classes appropriées d'être membres de quoi que ce soit. Une extension ontologique qui nous permet de parler formellement d'une telle « catégorie » est le conglomérat , qui est une collection de classes. Alors la « catégorie de toutes les catégories » est définie par ses objets : le conglomérat de toutes les catégories ; et ses morphismes : le conglomérat de tous les morphismes de A à B où A et B sont des objets. Pour savoir si une ontologie incluant des classes ainsi que des ensembles est adéquate pour la théorie des catégories, voir Muller 2001 .

Remarques

Les références

Bibliographie

• Adámek, Jiří; Herrlich, Horst; Strecker, George E. (1990), Catégories abstraites et concrètes (La joie des chats) (1ère éd.), New York : Wiley & Sons, ISBN 978-0-471-60922-3.
  • Adámek, Jiří; Herrlich, Horst; Strecker, George E. (2004) [1990], Catégories abstraites et concrètes (La joie des chats) (éd. Douvres), New York : Dover Publications, ISBN 978-0-486-46934-8.
• Bernays, Paul (1937), "A System of Axiomatic Set Theory—Part I", The Journal of Symbolic Logic , 2 (1) : 65-77, doi : 10.2307/2268862 , JSTOR  2268862.
• Bernays, Paul (1941), "A System of Axiomatic Set Theory—Part II", The Journal of Symbolic Logic , 6 (1) : 1–17, doi : 10.2307/2267281 , JSTOR  2267281.
• Bernays, Paul (1991), Axiomatic Set Theory (2e édition révisée), Dover Publications, ISBN 978-0-486-66637-2.
• Bourbaki, Nicolas (2004), Éléments de mathématiques : théorie des ensembles , Springer, ISBN 978-3-540-22525-6.
• Chuaqui, Rolando (1981), Axiomatic Set Theory: Impredicative Theories of Classes , North-Holland, ISBN 0-444-86178-5.* Cohen, Paul (1963), "The Independence of the Continuum Hypothesis", Actes de la National Academy of Sciences des États-Unis d'Amérique , 50 (6) : 1143–1148, Bibcode : 1963PNAS...50.1143C , doi : 10.1073/pnas.50.6.1143 , PMC  221287 , PMID  16578557.
• Cohen, Paul (1966), La théorie des ensembles et l'hypothèse du continu , WA Benjamin.
  • Cohen, Paul (2008), La théorie des ensembles et l'hypothèse du continu , Dover Publications, ISBN 978-0-486-46921-8.
• Dawson, John W. (1997), Dilemmes logiques : La vie et l'œuvre de Kurt Gödel , Wellesley, MA : AK Peters.
• Easton, William B. (1964), Pouvoirs des cardinaux réguliers (thèse de doctorat), Université de Princeton.
• Felgner, Ulrich (1971), "Comparaison des axiomes du choix local et universel" (PDF) , Fundamenta Mathematicae , 71 : 43-62, doi : 10.4064/fm-71-1-43-62.
• Ferreirós, José (2007), Labyrinth of Thought: A History of Set Theory and Its Role in Mathematical Thought (2e édition révisée), Bâle, Suisse : Birkhäuser, ISBN 978-3-7643-8349-7.
• Gödel, Kurt (1940), La cohérence de l'axiome du choix et de l'hypothèse du continuum généralisé avec les axiomes de la théorie des ensembles (éd. révisé), Princeton University Press, ISBN 978-0-691-07927-1.
  • Gödel, Kurt (2008), La cohérence de l'axiome du choix et de l'hypothèse du continuum généralisé avec les axiomes de la théorie des ensembles , avec une préface de Laver, Richard (éd. broché), Ishi Press, ISBN 978-0-923891-53-4.
• Gödel, Kurt (1986), Collected Works, Volume 1: Publications 1929-1936 , Oxford University Press, ISBN 978-0-19-514720-9.
• Gödel, Kurt (1990), Collected Works, Volume 2: Publications 1938-1974 , Oxford University Press, ISBN 978-0-19-514721-6.
• Gödel, Kurt (2003), Collected Works, Volume 4 : Correspondance A–G , Oxford University Press, ISBN 978-0-19-850073-5.
• Gray, Robert (1991), "Programmes informatiques et preuves mathématiques", The Mathematical Intelligencer , 13 (4) : 45-48, doi : 10.1007/BF03028342 , S2CID  121229549.
• Hallett, Michael (1984), Cantorian Set Theory and Limitation of Size (édition à couverture rigide), Oxford: Clarendon Press, ISBN 978-0-19-853179-1.
  • Hallett, Michael (1986), Cantorian Set Theory and Limitation of Size (édition de poche), Oxford: Clarendon Press, ISBN 978-0-19-853283-5.
• Kanamori, Akihiro (2009b), The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings , Springer, ISBN 978-3-540-88867-3.
• Kanamori, Akihiro (2009), "Bernays and Set Theory" (PDF) , Bulletin of Symbolic Logic , 15 (1) : 43–69, doi : 10.2178/bsl/1231081769 , JSTOR  25470304 , S2CID  15567244.
• Kanamori, Akihiro (2012), "In Praise of Replacement" (PDF) , Bulletin of Symbolic Logic , 18 (1) : 46-90, doi : 10.2178/bsl/1327328439 , JSTOR  41472440 , S2CID  18951854.
• Kunen, Kenneth (1980), Set Theory: An Introduction to Independence Proofs (édition à couverture rigide), North-Holland, ISBN 978-0-444-86839-8.
  • Kunen, Kenneth (2012), Set Theory: An Introduction to Independence Proofs (édition de poche), North-Holland, ISBN 978-0-444-56402-3.
• Mendelson, Elliott (1997), An Introduction to Mathematical Logic (4e éd.), Londres : Chapman et Hall/CRC, ISBN 978-0-412-80830-2. - Pp. 225-86 contiennent le traitement classique du NBG, montrant comment il fait ce que nous attendons de la théorie des ensembles, en fondant les relations , la théorie de l'ordre , les nombres ordinaux , les nombres transfinis , etc.
• Mirimanoff, Dmitry (1917), "Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles", L'Enseignement Mathématique , 19 : 37-52.
• Montague, Richard (1961), "Semantic Closure and Non-Finite Axiomatizability I", dans Buss, Samuel R. (éd.), Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics , Pergamon Press, pp. 45-69.
• Mostowski, Andrzej (1950), "Some impredicative definitions in the axiomatic set theory" (PDF) , Fundamenta Mathematicae , 37 : 111–124, doi : 10.4064/fm-37-1-111-124.
• Muller, FA (1er septembre 2001), "Sets, classes, and categories" (PDF) , British Journal for the Philosophy of Science , 52 (3) : 539–73, doi : 10.1093/bjps/52.3.539.
• Müller, Gurt, éd. (1976), Sets and Classes: On the Work of Paul Bernays , Studies in Logic and the Foundations of Mathematics Volume 84, Amsterdam: North Holland, ISBN 978-0-7204-2284-9.
• Potter, Michael (2004), Set Theory and Its Philosophy: A Critical Introduction (édition à couverture rigide), Oxford University Press, ISBN 978-0-19-926973-0.
  • Potter, Michael (2004p), Set Theory and Its Philosophy: A Critical Introduction (édition de poche), Oxford University Press, ISBN 978-0-19-927041-5.
• Pudlák, Pavel (1998), "The Lengths of Proofs" (PDF) , dans Buss, Samuel R. (éd.), Handbook of Proof Theory , Elsevier, pp. 547-637, ISBN 978-0-444-89840-1.
• Smullyan, Raymond M. ; Fitting, Melvin (2010) [Édition révisée et corrigée : publiée pour la première fois en 1996 par Oxford University Press], Set Theory and the Continuum Problem , Dover, ISBN 978-0-486-47484-7.
• Solovay, Robert M. (1990), "Note d'introduction à 1938 , 1939 , 1939a et 1940 ", Kurt Gödel Collected Works, Volume 2: Publications 1938-1974 , Oxford University Press, pp. 1-25, ISBN 978-0-19-514721-6.
• von Neumann, John (1923), "Zur Einführung der transfiniten Zahlen" , Acta Litt. Acad. Sc. Szeged X. , 1 : 199-208.
  • Traduction anglaise : van Heijenoort, Jean (2002a) [1967], "Sur l'introduction des nombres transfinis" , De Frege à Gödel: A Source Book in Mathematical Logic, 1879-1931 (quatrième édition), Harvard University Press, pp 346-354, ISBN 978-0-674-32449-7.
  • Traduction anglaise : van Heijenoort, Jean (2002b) [1967], "An axiomatization of set theory" , From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (quatrième édition d'impression), Harvard University Press, pp. 393-413, ISBN 978-0-674-32449-7.
• von Neumann, John (1925), "Eine Axiomatisierung der Mengenlehre" , Journal für die Reine und Angewandte Mathematik , 154 : 219-240.
• von Neumann, John (1928), "Die Axiomatisierung der Mengenlehre" , Mathematische Zeitschrift , 27 : 669–752, doi : 10.1007/bf01171122 , S2CID  123492324.
• von Neumann, John (1929), "Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre" , Journal für die Reine und Angewandte Mathematik , 160 : 227-241.

Liens externes

• "Théorie des ensembles de von Neumann-Bernays-Gödel" . PlanèteMath .
• Szudzik, Matthieu. "Théorie des ensembles de von Neumann-Bernays-Gödel" . MathWorld .