Teoria dos conjuntos de Von Neumann-Bernays-Gödel

As classes têm vários usos em NBG:

• Elas produzem uma axiomatização finita da teoria dos conjuntos.^[4]
• Elas são usadas para formular uma "forma muito forte do axioma da escolha"^[5] — a saber, o axioma da escolha global: Existe uma função de escolha global ${\displaystyle G}$ definida na classe de todos os conjuntos não vazios tal que ${\displaystyle G(x)\in x}$ para todo conjunto não vazio ${\displaystyle x.}$ Isso é mais forte do que o axioma da escolha de ZFC: Para todo conjunto ${\displaystyle s}$ de conjuntos não vazios, existe uma função de escolha ${\displaystyle f}$ definida em ${\displaystyle s}$ tal que ${\displaystyle f(x)\in x}$ para todo ${\displaystyle x\in s.}$^[a]
• Os paradoxos da teoria dos conjuntos são contornados ao reconhecer que algumas classes não podem ser conjuntos. Por exemplo, suponha que a classe ${\displaystyle Ord}$ de todos os ordinais seja um conjunto. Então ${\displaystyle Ord}$ é um conjunto transitivo bem ordenado por ${\displaystyle \in }$. Logo, por definição, ${\displaystyle Ord}$ é um ordinal. Consequentemente, ${\displaystyle Ord\in Ord}$, o que contradiz o fato de ${\displaystyle \in }$ ser uma boa ordem para ${\displaystyle Ord.}$ Portanto, ${\displaystyle Ord}$ não é um conjunto. Uma classe que não é um conjunto é chamada de classe própria; ${\displaystyle Ord}$ é uma classe própria.^[6]
• Classes próprias são úteis em construções. Em sua prova da consistência relativa do axioma da escolha global e da hipótese do contínuo generalizada, Gödel usou classes próprias para construir o universo construtível. Ele construiu uma função sobre a classe de todos os ordinais que, para cada ordinal, constrói um conjunto construtível aplicando uma operação de construção de conjuntos a conjuntos previamente construídos. O universo construtível é a imagem dessa função.^[7]

Uma vez que as classes são adicionadas à linguagem de ZFC, é fácil transformar ZFC em uma teoria dos conjuntos com classes. Primeiro, o esquema de axiomas da compreensão de classes é adicionado. Este esquema de axiomas afirma: Para toda fórmula ${\displaystyle \phi (x_{1},\ldots ,x_{n})}$ que quantifica apenas sobre conjuntos, existe uma classe ${\displaystyle A}$ consistindo nas ${\displaystyle n}$-tuplas que satisfazem a fórmula — isto é, ${\displaystyle \forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n})].}$ Em seguida, o esquema de axiomas da substituição é substituído por um único axioma que usa uma classe. Finalmente, o axioma da extensionalidade de ZFC é modificado para lidar com classes: Se duas classes têm os mesmos elementos, então elas são idênticas. Os outros axiomas de ZFC não são modificados.^[8]

Esta teoria não é finitamente axiomatizada. O esquema de substituição de ZFC foi substituído por um único axioma, mas o esquema de axiomas de compreensão de classes foi introduzido.

Para produzir uma teoria com uma quantidade finita de axiomas, o esquema de axiomas da compreensão de classes é primeiro substituído por finitos axiomas de existência de classe. Em seguida, esses axiomas são usados para provar o teorema da existência de classe, que implica cada instância do esquema de axiomas.^[8] A prova deste teorema requer apenas sete axiomas de existência de classe, que são usados para converter a construção de uma fórmula na construção de uma classe que satisfaça a fórmula.

Os axiomas de existência de classe serão usados para provar o teorema de existência de classe: Para toda fórmula com ${\displaystyle n}$ variáveis de conjunto livres que quantifica apenas sobre conjuntos, existe uma classe de ${\displaystyle n}$-tuplas que a satisfaz. O exemplo a seguir começa com duas classes que são funções e constrói uma função composta. Este exemplo ilustra as técnicas necessárias para provar o teorema de existência de classe, as quais levam aos axiomas de existência de classe que são necessários.

Exemplo 1:  Se as classes ${\displaystyle F}$ e ${\displaystyle G}$ são funções, então a função composta ${\displaystyle G\circ F}$ é definida pela fórmula: ${\displaystyle \exists t[(x,t)\in F\,\land \,(t,y)\in G].}$ Como esta fórmula tem duas variáveis de conjunto livres, ${\displaystyle x}$ e ${\displaystyle y,}$ o teorema de existência de classe constrói a classe de pares ordenados: ${\displaystyle G\circ F\,=\,\{(x,y):\exists t[(x,t)\in F\,\land \,(t,y)\in G]\}.}$ Como esta fórmula é construída a partir de fórmulas mais simples usando a conjunção ${\displaystyle \land }$ e a quantificação existencial ${\displaystyle \exists }$, são necessárias operações de classe que tomam classes representando as fórmulas mais simples e produzem classes representando as fórmulas com ${\displaystyle \land }$ e ${\displaystyle \exists }$. Para produzir uma classe representando uma fórmula com ${\displaystyle \land }$, usa-se a interseção, uma vez que ${\displaystyle x\in A\cap B\iff x\in A\land x\in B.}$ Para produzir uma classe representando uma fórmula com ${\displaystyle \exists }$, usa-se o domínio, uma vez que ${\displaystyle x\in Dom(A)\iff \exists t[(x,t)\in A].}$ Antes de realizar a interseção, as tuplas em ${\displaystyle F}$ e ${\displaystyle G}$ precisam de um componente extra para terem as mesmas variáveis. O componente ${\displaystyle y}$ é adicionado às tuplas de ${\displaystyle F}$ e ${\displaystyle x}$ é adicionado às tuplas de ${\displaystyle G}$: $${\displaystyle F'=\{(x,t,y):(x,t)\in F\}\,}$$ e ${\displaystyle \,G'=\{(t,y,x):(t,y)\in G\}.}$ Na definição de ${\displaystyle F',}$ a variável ${\displaystyle y}$ não é restrita pela declaração ${\displaystyle (x,t)\in F,}$ então ${\displaystyle y}$ varia sobre a classe ${\displaystyle V}$ de todos os conjuntos. Similarmente, na definição de ${\displaystyle G',}$ a variável ${\displaystyle x}$ varia sobre ${\displaystyle V.}$ Assim, é necessário um axioma que adicione um componente extra (cujos valores variem sobre ${\displaystyle V}$) às tuplas de uma dada classe. A seguir, as variáveis são colocadas na mesma ordem para prepará-las para a interseção: $${\displaystyle F''=\{(x,y,t):(x,t)\in F\}\,}$$ e ${\displaystyle \,G''=\{(x,y,t):(t,y)\in G\}.}$ Para ir de ${\displaystyle F'}$ para ${\displaystyle F''}$ e de ${\displaystyle G'}$ para ${\displaystyle G''}$, são necessárias duas permutações diferentes, portanto, são necessários axiomas que suportem permutações de componentes de tuplas. A interseção de ${\displaystyle F''}$ e ${\displaystyle G''}$ lida com ${\displaystyle \land }$: $${\displaystyle F''\cap G''=\{(x,y,t):(x,t)\in F\,\land \,(t,y)\in G\}.}$$ Como ${\displaystyle (x,y,t)}$ é definido como ${\displaystyle ((x,y),t)}$, obter o domínio de ${\displaystyle F''\cap G''}$ lida com ${\displaystyle \exists t}$ e produz a função composta: $${\displaystyle G\circ F=Dom(F''\cap G'')=\{(x,y):\exists t((x,t)\in F\,\land \,(t,y)\in G)\}}$$ Logo, são necessários os axiomas de interseção e domínio.

Os axiomas de existência de classe estão divididos em dois grupos: axiomas para lidar com primitivas da linguagem e axiomas para lidar com tuplas. Existem quatro axiomas no primeiro grupo e três axiomas no segundo grupo.^[b]

Axiomas para lidar com primitivas da linguagem:

Pertinência.  Existe uma classe ${\displaystyle E}$ contendo todos os pares ordenados cujo primeiro componente é um membro do segundo componente.

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

Interseção (conjunção).  Para quaisquer duas classes ${\displaystyle A}$ e ${\displaystyle B}$, existe uma classe ${\displaystyle C}$ consistindo precisamente dos conjuntos que pertencem tanto a ${\displaystyle A}$ quanto a ${\displaystyle B}$.

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

Complemento (negação).  Para qualquer classe ${\displaystyle A}$, existe uma classe ${\displaystyle B}$ consistindo precisamente dos conjuntos que não pertencem a ${\displaystyle A}$.

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

Domínio (quantificador existencial).  Para qualquer classe ${\displaystyle A}$, existe uma classe ${\displaystyle B}$ consistindo precisamente dos primeiros componentes dos pares ordenados de ${\displaystyle A}$.

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

Pelo axioma da extensionalidade, a classe ${\displaystyle C}$ no axioma da interseção e a classe ${\displaystyle B}$ nos axiomas do complemento e domínio são únicas. Elas serão denotadas por: ${\displaystyle A\cap B,}$ ${\displaystyle \complement (A),}$ e ${\displaystyle Dom(A),}$ respectivamente.^[c]

Os três primeiros axiomas implicam a existência da classe vazia e da classe de todos os conjuntos: O axioma da pertinência implica a existência de uma classe ${\displaystyle E.}$ Os axiomas de interseção e complemento implicam a existência de ${\displaystyle E\cap \complement (E)}$, que é vazia. Pelo axioma da extensionalidade, esta classe é única; ela é denotada por ${\displaystyle \emptyset .}$ O complemento de ${\displaystyle \emptyset }$ é a classe ${\displaystyle V}$ de todos os conjuntos, que também é única por extensionalidade. O predicado de conjunto ${\displaystyle M(A)}$, que foi definido como ${\displaystyle \exists C(A\in C)}$, agora é redefinido como ${\displaystyle A\in V}$ para evitar quantificar sobre classes.

Axiomas para lidar com tuplas:

Produto por ${\displaystyle V}$.  Para qualquer classe ${\displaystyle A}$, existe uma classe ${\displaystyle B}$ consistindo dos pares ordenados cujo primeiro componente pertence a ${\displaystyle A}$.

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

Permutação circular.  Para qualquer classe ${\displaystyle A}$, existe uma classe ${\displaystyle B}$ cujas 3-tuplas são obtidas aplicando a permutação circular ${\displaystyle (y,z,x)\mapsto (x,y,z)}$ às 3-tuplas de ${\displaystyle A}$.

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

Transposição.  Para qualquer classe ${\displaystyle A}$, existe uma classe ${\displaystyle B}$ cujas 3-tuplas são obtidas transpondo os dois últimos componentes das 3-tuplas de ${\displaystyle A}$.

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

Por extensionalidade, o axioma do produto por ${\displaystyle V}$ implica a existência de uma classe única, que é denotada por ${\displaystyle A\times V.}$ Este axioma é usado para definir a classe ${\displaystyle V^{n}}$ de todas as ${\displaystyle n}$-tuplas: ${\displaystyle V^{1}=V}$ e ${\displaystyle V^{n+1}=V^{n}\times V.\,}$ Se ${\displaystyle A}$ é uma classe, a extensionalidade implica que ${\displaystyle A\cap V^{n}}$ é a classe única consistindo nas ${\displaystyle n}$-tuplas de ${\displaystyle A.}$ Por exemplo, o axioma da pertinência produz uma classe ${\displaystyle E}$ que pode conter elementos que não são pares ordenados, enquanto a interseção ${\displaystyle E\cap V^{2}}$ contém apenas os pares ordenados de ${\displaystyle E}$.

Os axiomas da permutação circular e transposição não implicam a existência de classes únicas porque especificam apenas as 3-tuplas da classe ${\displaystyle B.}$ Ao especificar as 3-tuplas, esses axiomas também especificam as ${\displaystyle n}$-tuplas para ${\displaystyle n\geq 4}$ já que: $${\displaystyle (x_{1},\ldots ,x_{n-2},x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-2}),x_{n-1},x_{n}).}$$ Os axiomas para lidar com tuplas e o axioma do domínio implicam o seguinte lema, que é usado na prova do teorema de existência de classe.

Lema da tupla:

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

Prova do lema:

• Classe ${\displaystyle B_{3}}$: Aplique produto por ${\displaystyle V}$ a ${\displaystyle A}$ para produzir ${\displaystyle B_{3}.}$
• Classe ${\displaystyle B_{2}}$: Aplique transposição a ${\displaystyle B_{3}}$ para produzir ${\displaystyle B_{2}.}$
• Classe ${\displaystyle B_{1}}$: Aplique permutação circular a ${\displaystyle B_{3}}$ para produzir ${\displaystyle B_{1}.}$
• Classe ${\displaystyle B_{4}}$: Aplique permutação circular a ${\displaystyle B_{2}}$, em seguida aplique o domínio para produzir ${\displaystyle B_{4}.}$ ∎

Mais um axioma é necessário para provar o teorema de existência de classe: o axioma da regularidade. Como a existência da classe vazia foi provada, é dada a declaração usual desse axioma.^[d]

Axioma da regularidade.  Todo conjunto não vazio tem pelo menos um elemento com o qual não tem nenhum elemento em comum. $${\displaystyle \forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].}$$

Este axioma implica que um conjunto não pode pertencer a si mesmo: Suponha que ${\displaystyle x\in x}$ e seja ${\displaystyle a=\{x\}.}$ Então ${\displaystyle x\cap a\neq \emptyset }$ já que ${\displaystyle x\in x\cap a.}$ Isso contradiz o axioma da regularidade porque ${\displaystyle x}$ é o único elemento em ${\displaystyle a.}$ Portanto, ${\displaystyle x\notin x.}$ O axioma da regularidade também proíbe sequências de pertinência descendentes infinitas de conjuntos: $${\displaystyle \cdots \in x_{n+1}\in x_{n}\in \cdots \in x_{1}\in x_{0}.}$$

Gödel declarou a regularidade para classes em vez de para conjuntos em sua monografia de 1940, que foi baseada em palestras dadas em 1938.^[18] Em 1939, ele provou que a regularidade para conjuntos implica a regularidade para classes.^[19]

Teorema de existência de classe: Seja ${\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}$ uma fórmula que quantifica apenas sobre conjuntos e não contém variáveis livres além de ${\displaystyle x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}}$ (não necessariamente todas elas). Então, para todo ${\displaystyle Y_{1},\dots ,Y_{m}}$, existe uma classe única ${\displaystyle A}$ de ${\displaystyle n}$-tuplas tal que: $${\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})].}$$ A classe ${\displaystyle A}$ é denotada por ${\displaystyle \{(x_{1},\dots ,x_{n}):\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})\}.}$^[e]

A prova do teorema será feita em dois passos:

1. Regras de transformação são usadas para transformar a fórmula dada ${\displaystyle \phi }$ numa fórmula equivalente que simplifica a parte indutiva da prova. Por exemplo, os únicos símbolos lógicos na fórmula transformada são ${\displaystyle \neg }$, ${\displaystyle \land }$, e ${\displaystyle \exists }$, de modo que a indução lida com símbolos lógicos em apenas três casos.
2. O teorema de existência de classe é provado indutivamente para fórmulas transformadas. Guiado pela estrutura da fórmula transformada, os axiomas de existência de classe são usados para produzir a classe única de ${\displaystyle n}$-tuplas que satisfaz a fórmula.

Regras de transformação.  Nas regras 1 e 2 abaixo, ${\displaystyle \Delta }$ e ${\displaystyle \Gamma }$ denotam variáveis de conjunto ou de classe. Essas duas regras eliminam todas as ocorrências de variáveis de classe antes de um ${\displaystyle \in }$ e todas as ocorrências de igualdade. Cada vez que a regra 1 ou 2 é aplicada a uma subfórmula, ${\displaystyle i}$ é escolhido de forma que ${\displaystyle z_{i}}$ difira das outras variáveis na fórmula atual. As três regras são repetidas até que não haja mais subfórmulas às quais elas possam ser aplicadas. Isso produz uma fórmula que é construída apenas com ${\displaystyle \neg }$, ${\displaystyle \land }$, ${\displaystyle \exists }$, ${\displaystyle \in }$, variáveis de conjunto, e variáveis de classe ${\displaystyle Y_{k}}$ onde ${\displaystyle Y_{k}}$ não aparece antes de um ${\displaystyle \in }$.

1. ${\displaystyle \,Y_{k}\in \Gamma }$ é transformada em ${\displaystyle \exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma ).}$
2. A extensionalidade é usada para transformar ${\displaystyle \Delta =\Gamma }$ em ${\displaystyle \forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ).}$
3. Identidades lógicas são usadas para transformar subfórmulas contendo ${\displaystyle \lor ,\implies ,\iff ,}$ e ${\displaystyle \forall }$ em subfórmulas que usam apenas ${\displaystyle \neg ,\land ,}$ e ${\displaystyle \exists .}$

Regras de transformação: variáveis ligadas.  Considere a fórmula da função composta do exemplo 1 com suas variáveis de conjunto livres substituídas por ${\displaystyle x_{1}}$ e ${\displaystyle x_{2}}$: ${\displaystyle \exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G].}$ A prova indutiva removerá ${\displaystyle \exists t}$, o que produz a fórmula ${\displaystyle (x_{1},t)\in F\land (t,x_{2})\in G.}$ No entanto, como o teorema de existência de classe é declarado para variáveis com subscritos, esta fórmula não tem a forma esperada pela hipótese de indução. Este problema é resolvido substituindo a variável ${\displaystyle t}$ por ${\displaystyle x_{3}.}$ As variáveis ligadas dentro de quantificadores aninhados são tratadas aumentando o subscrito em um para cada quantificador sucessivo. Isto leva à regra 4, que deve ser aplicada após as outras regras, já que as regras 1 e 2 produzem variáveis quantificadas.

4. Se uma fórmula não contém variáveis de conjunto livres além de ${\displaystyle x_{1},\dots ,x_{n},}$ então as variáveis ligadas que estão aninhadas dentro de ${\displaystyle q}$ quantificadores são substituídas por ${\displaystyle x_{n+q}}$. Essas variáveis têm profundidade de aninhamento (de quantificador) ${\displaystyle q}$.

Exemplo 2:  A regra 4 é aplicada à fórmula ${\displaystyle \phi (x_{1})}$ que define a classe consistindo de todos os conjuntos da forma ${\displaystyle \{\emptyset ,\{\emptyset ,\dots \},\dots \}.}$ Ou seja, conjuntos que contêm pelo menos ${\displaystyle \emptyset }$ e um conjunto contendo ${\displaystyle \emptyset }$ — por exemplo, ${\displaystyle \{\emptyset ,\{\emptyset ,a,b,c\},d,e\}}$ onde ${\displaystyle a,b,c,d,}$ e ${\displaystyle e}$ são conjuntos. $${\displaystyle {\begin{aligned}\phi (x_{1})\,&=\,\exists u\;\,[\,u\in x_{1}\,\land \,\neg \exists v\;\,(\;v\,\in \,u\,)]\,\land \,\,\exists w\;{\bigl (}w\in x_{1}\,\land \,\exists 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}}}$$ Como ${\displaystyle x_{1}}$ é a única variável livre, ${\displaystyle n=1.}$ A variável quantificada ${\displaystyle x_{3}}$ aparece duas vezes em ${\displaystyle x_{3}\in x_{2}}$ na profundidade de aninhamento 2. Seu subscrito é 3 porque ${\displaystyle n+q=1+2=3.}$ Se dois escopos de quantificador estão na mesma profundidade de aninhamento, eles são idênticos ou disjuntos. As duas ocorrências de ${\displaystyle x_{3}}$ estão em escopos de quantificadores disjuntos, então elas não interagem entre si.

Prova do teorema de existência de classe para fórmulas transformadas: O seguinte lema é usado na prova.

Lema de expansão: Seja ${\displaystyle 1\leq i<j\leq n,}$ e seja ${\displaystyle P}$ uma classe contendo todos os pares ordenados ${\displaystyle (x_{i},x_{j})}$ satisfazendo ${\displaystyle R(x_{i},x_{j}).}$ Ou seja, ${\displaystyle P\supseteq \{(x_{i},x_{j}):R(x_{i},x_{j})\}.}$ Então ${\displaystyle P}$ pode ser expandido para a classe única ${\displaystyle Q}$ de ${\displaystyle n}$-tuplas satisfazendo ${\displaystyle R(x_{i},x_{j})}$. Ou seja, ${\displaystyle Q=\{(x_{1},\ldots ,x_{n}):R(x_{i},x_{j})\}.}$

Prova do lema de expansão:

1. Se ${\displaystyle i=1,}$ seja ${\displaystyle P_{1}=P.}$
   Caso contrário, ${\displaystyle i>1,}$ então componentes são adicionados antes de ${\displaystyle x_{i}{\text{:}}}$ aplique a declaração 1 do lema da tupla a ${\displaystyle P}$ com ${\displaystyle z=(x_{1},\dots ,x_{i-1}).}$ Isso produz uma classe ${\displaystyle P_{1}}$ contendo todas as ${\displaystyle (i+1)}$-tuplas $${\displaystyle ((x_{1},\dots ,x_{i-1}),x_{i},x_{j})=(x_{1},\dots ,x_{i-1},x_{i},x_{j})}$$ satisfazendo ${\displaystyle R(x_{i},x_{j}).}$
2. Se ${\displaystyle j=i+1,}$ seja ${\displaystyle P_{2}=P_{1}.}$
   Caso contrário, ${\displaystyle j>i+1,}$ então componentes são adicionados entre ${\displaystyle x_{i}}$ e ${\displaystyle x_{j}{\text{:}}}$ adicione os componentes ${\displaystyle x_{i+1},\dots ,x_{j-1}}$ um por um usando a declaração 2 do lema da tupla. Isso produz uma classe ${\displaystyle P_{2}}$ contendo todas as ${\displaystyle j}$-tuplas $${\displaystyle (((\cdots ((x_{1},\dots ,x_{i}),x_{i+1}),\cdots ),x_{j-1}),x_{j})=(x_{1},\dots ,x_{j})}$$ satisfazendo ${\displaystyle R(x_{i},x_{j}).}$
3. Se ${\displaystyle j=n,}$ seja ${\displaystyle P_{3}=P_{2}.}$
   Caso contrário, ${\displaystyle j<n,}$ então componentes são adicionados depois de ${\displaystyle x_{j}{\text{:}}}$ adicione os componentes ${\displaystyle x_{j+1},\dots ,x_{n}}$ um por um usando a declaração 3 do lema da tupla. Isso produz uma classe ${\displaystyle P_{3}}$ contendo todas as ${\displaystyle n}$-tuplas $${\displaystyle ((\cdots ((x_{1},\dots ,x_{j}),x_{j+1}),\cdots ),x_{n})=(x_{1},\dots ,x_{n})}$$ satisfazendo ${\displaystyle R(x_{i},x_{j}).}$
4. Seja ${\displaystyle Q=P_{3}\cap V^{n}.}$ A extensionalidade implica que ${\displaystyle Q}$ é a classe única de ${\displaystyle n}$-tuplas satisfazendo ${\displaystyle R(x_{i},x_{j}).}$ ∎

Teorema de existência de classe para fórmulas transformadas: Seja ${\displaystyle \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})}$ uma fórmula que:

1. não contém variáveis livres além de ${\displaystyle x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m}}$;
2. contém apenas ${\displaystyle \in }$, ${\displaystyle \neg }$, ${\displaystyle \land }$, ${\displaystyle \exists }$, variáveis de conjunto, e as variáveis de classe ${\displaystyle Y_{k}}$ onde ${\displaystyle Y_{k}}$ não aparece antes de um ${\displaystyle \in }$ ;
3. apenas quantifica variáveis de conjunto ${\displaystyle x_{n+q}}$ onde ${\displaystyle q}$ é a profundidade de aninhamento de quantificador da variável.

Então, para todo ${\displaystyle Y_{1},\dots ,Y_{m}}$, existe uma classe única ${\displaystyle A}$ de ${\displaystyle n}$-tuplas tal que: $${\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})].}$$

Prova do teorema: Passo base: ${\displaystyle \phi }$ tem 0 símbolos lógicos. A hipótese do teorema implica que ${\displaystyle \phi }$ é uma fórmula atômica da forma ${\displaystyle x_{i}\in x_{j}}$ ou ${\displaystyle x_{i}\in Y_{k}.}$

Passo indutivo: ${\displaystyle \phi }$ tem ${\displaystyle k}$ símbolos lógicos onde ${\displaystyle k>0}$. Assuma a hipótese de indução de que o teorema é verdadeiro para todo ${\displaystyle \psi }$ com menos de ${\displaystyle k}$ símbolos lógicos. Provaremos agora o teorema para ${\displaystyle \phi }$ com ${\displaystyle k}$ símbolos lógicos. Nesta prova, a lista de variáveis de classe ${\displaystyle Y_{1},\dots ,Y_{m}}$ é abreviada por ${\displaystyle {\vec {Y}}}$, de modo que uma fórmula — como ${\displaystyle \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})}$ — possa ser escrita como ${\displaystyle \phi (x_{1},\dots ,x_{n},{\vec {Y}}).}$

∎

Gödel apontou que o teorema de existência de classe "é um metateorema, ou seja, um teorema sobre o sistema [NBG], não no sistema..."^[22] É um teorema sobre o NBG porque é provado na metateoria por indução em fórmulas NBG. Além disso, sua prova — em vez de invocar um número finito de axiomas NBG — descreve indutivamente como usar os axiomas NBG para construir uma classe que satisfaça uma determinada fórmula. Para cada fórmula, esta descrição pode ser transformada em uma prova construtiva de existência que está no NBG. Portanto, este metateorema pode gerar as provas NBG que substituem os usos do teorema de existência de classe de NBG.

Um programa de computador recursivo captura de forma sucinta a construção de uma classe a partir de uma dada fórmula. A definição deste programa não depende da prova do teorema de existência de classe. Contudo, a prova é necessária para demonstrar que a classe construída pelo programa satisfaz a fórmula dada e é construída usando os axiomas. Este programa é escrito em pseudocódigo que usa uma estrutura de case no estilo Pascal.^[g] $${\displaystyle {\begin{array}{l}\mathbf {function} \;{\text{Class}}(\phi ,\,n)\\\quad {\begin{array}{rl}\mathbf {input} \!:\;\,&\phi {\text{ é uma fórmula transformada da forma }}\phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m});\\&n{\text{ especifica que uma classe de }}n{\text{-tuplas é retornada.}}\\\;\;\;\;\mathbf {output} \!:\;\,&{\text{classe }}A{\text{ de }}n{\text{-tuplas satisfazendo }}\\&\,\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{array}}\\\mathbf {begin} \\\quad \mathbf {case} \;\phi \;\mathbf {of} \\\qquad {\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 {return} \;\,\complement _{V^{n}}{\text{Class}}(\psi ,\,n);&&{\text{// }}\complement _{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{ é livre em }}\psi ;{\text{ Class}}(\psi ,\,n+1)\\&\ &&{\text{// retorna uma classe de }}(n+1){\text{-tuplas}}\end{alignedat}}\\\quad \mathbf {end} \\\mathbf {end} \end{array}}}