Teoría de conjuntos de Von Neumann-Bernays-Gödel

En los fundamentos de las matemáticas, la teoría de conjuntos de von Neumann-Bernays-Gödel (NBG) es una teoría de conjuntos axiomática que es una extensión conservadora de la teoría de conjuntos de elección de Zermelo-Fraenkel (ZFC). NBG introduce la noción de clase, que es una colección de conjuntos definidos por una fórmula cuyos cuantificadores abarcan únicamente conjuntos. NBG puede definir clases que son mayores que los conjuntos, como la clase de todos los conjuntos y la clase de todos los ordinales. La teoría de conjuntos de Morse-Kelley (MK) permite que las clases se definan mediante fórmulas cuyos cuantificadores abarcan clases. NBG es finitamente axiomatizable, mientras que ZFC y MK no lo son.

Un teorema clave de NBG es el teorema de existencia de clases, que establece que para cada fórmula cuyos cuantificadores abarcan solo conjuntos, hay una clase que consta de conjuntos que satisfacen la fórmula. Esta clase se construye reflejando la construcción paso a paso de la fórmula con clases. Dado que todas las fórmulas de la teoría de conjuntos se construyen a partir de dos tipos de fórmulas atómicas (pertenencia e igualdad) y un número finito de símbolos lógicos, sólo se necesita un número finito de axiomas para construir las clases que los satisfagan. Ésta es la razón por la que NBG es finitamente axiomatizable. Las clases también se utilizan para otras construcciones, para manejar las paradojas de la teoría de conjuntos y para enunciar el axioma de elección global, que es más fuerte que el axioma de elección de ZFC.

John von Neumann introdujo las clases en la teoría de conjuntos en 1925. Las nociones primitivas de su teoría eran función y argumento. Utilizando estas nociones, definió clase y conjunto. Paul Bernays reformuló la teoría de von Neumann tomando las nociones de clase y conjunto como primitivas. Kurt Gödel simplificó la idea de Bernays teoría por su consistencia relativa, prueba del axioma de elección y la hipótesis del continuo generalizado.

Clases de teoría de conjuntos

Los usos de las clases

Las clases tienen varios usos en NBG:

• Producen una axiomatización finita de la teoría del conjunto.
• Se utilizan para establecer una "forma muy fuerte del axioma de la elección" —por ejemplo, el axioma de la elección global: Existe una función de elección global ${displaystyle G.$ definido en la clase de todos los conjuntos no vacíos tal que ${displaystyle G(x)in x}$ para cada conjunto no vacío ${displaystyle x.}$ Esto es más fuerte que el axioma de elección de ZFC: Para cada conjunto ${displaystyle s}$ de conjuntos no vacíos, existe una función de elección ${displaystyle f}$ definidas ${displaystyle s}$ tales que ${displaystyle f(x)in x}$ para todos ${displaystyle xin s.}$
• Las paradojas teóricas se manejan reconociendo que algunas clases no pueden ser sets. Por ejemplo, asuma que la clase ${displaystyle Ord.$ de todos los ordinal es un conjunto. Entonces... ${displaystyle Ord.$ es un conjunto transitivo bien ordenado por ${displaystyle in }$. Así que, por definición, ${displaystyle Ord.$ es un ordinal. Por lo tanto, ${displaystyle Ord 'in Ord'$, que contradice ${displaystyle in }$ ser un buen orden de ${displaystyle Ord.$ Por lo tanto, ${displaystyle Ord.$ no es un juego. Una clase que no es un conjunto se llama una clase adecuada, ${displaystyle Ord.$ es una clase adecuada.
• Las clases adecuadas son útiles en construcciones. En su prueba de la consistencia relativa del axioma de la elección global y de la hipótesis continuum generalizada, Gödel utilizó clases adecuadas para construir el universo constructible. Construyó una función en la clase de todos los ordinal que, para cada ordinal, construye un conjunto constructible aplicando una operación de construcción de conjuntos previamente construidos. El universo constructible es la imagen de esta función.

Esquema de axioma versus teorema de existencia de clases

Una vez que las clases se agregan al idioma de ZFC, es fácil transformar ZFC en una teoría de conjunto con las clases. En primer lugar, se añade el esquema de axioma de la comprensión de clase. Este esquema de axioma dice: Por cada fórmula ${displaystyle phi (x_{1},ldotsx_{n}}$ que cuantifica sólo sobre conjuntos, existe una clase ${displaystyle A}$ consistente en ${displaystyle n}$-tuples satisfacción de la fórmula, es decir, ${displaystyle forall x_{1}cdots ,forall x_{n}[(x_{1},ldotsx_{n})in Aiff phi (x_{1},ldotsx_{n}].}$ Luego el esquema axiom de reemplazo es reemplazado por un solo axioma que utiliza una clase. Finalmente, el axioma de extensión de ZFC se modifica para manejar las clases: Si dos clases tienen los mismos elementos, entonces son idénticos. Los otros axiomas de ZFC no son modificados.

Esta teoría no está axiomatizada de forma finita. El esquema de reemplazo de ZFC ha sido reemplazado por un axioma único, pero se ha introducido el esquema de axioma de comprensión de clases.

Para producir una teoría con un número finito de axiomas, el esquema de axiomas de comprensión de clases se reemplaza primero por un número finito de axiomas de existencia de clases. Luego, estos axiomas se utilizan para demostrar el teorema de existencia de clases, que implica todos los casos del esquema del axioma. La demostración de este teorema requiere sólo siete axiomas de existencia de clases, que se utilizan para convertir la construcción de una fórmula en la construcción de una clase que satisfaga la fórmula.

Axiomatización de NBG

Clases y conjuntos

NBG tiene dos tipos de objetos: clases y conjuntos. Intuitivamente, cada conjunto es también una clase. Hay dos maneras de axiomatizar esto. Bernays usó mucha lógica con dos tipos: clases y conjuntos. Gödel evita las clases introduciendo predicados primitivos: ${displaystyle {mathfrak}(A)}$ para "${displaystyle A}$ es una clase ${displaystyle {Mathfrak}(A)}$ para "${displaystyle A}$ es un juego" (en alemán, "set" es Menge). También introdujo axiomas declarando que cada conjunto es una clase y que si clase ${displaystyle A}$ es miembro de una clase, entonces ${displaystyle A}$ es un juego. Usar predicados es la forma estándar de eliminar tipos. Elliott Mendelson modificó el enfoque de Gödel al tener todo ser una clase y definir el predicado conjunto ${displaystyle M(A)}$ como ${displaystyle exists C(Ain C).}$ Esta modificación elimina el predicado de clase de Gödel y sus dos axiomas.

Bernays' El enfoque de dos tipos puede parecer más natural al principio, pero crea una teoría más compleja. En Bernays' En teoría, todo conjunto tiene dos representaciones: una como conjunto y otra como clase. Además, existen dos relaciones de membresía: la primera, denotada por "∈", es entre dos conjuntos; el segundo, denotado por "η", está entre un conjunto y una clase. Esta redundancia es requerida por la lógica multiclasificada porque variables de diferentes tipos abarcan subdominios disjuntos del dominio del discurso.

Las diferencias entre estos dos enfoques no afectan lo que puede probarse, pero sí afectan cómo se escriben las declaraciones. En el enfoque de Gödel, ${displaystyle Ain C}$ Donde ${displaystyle A}$ y ${displaystyle C}$ son clases es una declaración válida. En el enfoque de Bernays esta declaración no tiene sentido. Sin embargo, si ${displaystyle A}$ es un conjunto, hay una declaración equivalente: Define "set ${displaystyle a}$ representa la clase ${displaystyle A}$"si tienen los mismos sets que los miembros, es decir, ${displaystyle forall x(xin aiff x;eta ;A).}$ La declaración ${displaystyle a;eta;C}$ donde se establece ${displaystyle a}$ representa la clase ${displaystyle A}$ es equivalente a la de Gödel ${displaystyle Ain C.}$

El enfoque adoptado en este artículo es el de Gödel con la modificación de Mendelson. Esto significa que NBG es un sistema axiomático en lógica de predicados de primer orden con igualdad, y sus únicas nociones primitivas son clase y relación de membresía.

Definiciones y axiomas de extensionalidad y emparejamiento

Un juego es una clase que pertenece al menos a una clase: ${displaystyle A}$ es un conjunto si y sólo si ${displaystyle exists C(Ain C)}$. Una clase que no es un conjunto se llama una clase adecuada: ${displaystyle A}$ es una clase adecuada si y sólo si ${displaystyle forall C(Anotin C)}$. Por lo tanto, cada clase es un conjunto o una clase adecuada, y ninguna clase es ambas.

Gödel introdujo la convención de que las variables en mayúsculas abarcan las clases, mientras que las variables en minúsculas abarcan los conjuntos. Gödel también usó nombres que comienzan con una letra mayúscula para denotar clases particulares, incluidas funciones y relaciones definidas en la clase de todos los conjuntos. En este artículo se utiliza la convención de Gödel. Nos permite escribir:

Los siguientes axiomas y definiciones son necesarios para demostrar el teorema de existencia de clases.

Axioma de extensionalidad.  Si dos clases tienen los mismos elementos, entonces son idénticas.

${displaystyle forall A,forall B,[forall x(xin Aiff xin B)implies A=B]}$

Este axioma generaliza el axioma de extensionalidad de ZFC a las clases.

Axioma de emparejamiento. Si ${displaystyle x}$ y ${displaystyle y}$ son conjuntos, entonces existe un conjunto ${displaystyle p}$ cuyos únicos miembros son ${displaystyle x}$ y ${displaystyle y}$.

${displaystyle forall x,forall y,exists p,forall z,[zin piff (z=x,lor ,z=y)}$

Como en ZFC, el axioma de la extensión implica la singularidad del conjunto ${displaystyle p}$, que nos permite introducir la notación ${displaystyle {x,y}.}$

Los pares ordenados se definen por:

${displaystyle (x,y)={x},{x,y}}}$

Las tuplas se definen inductivamente usando pares ordenados:

${displaystyle (x_{1}=x_{1}$

${displaystyle {text{ ¡No!$

Axiomas de existencia de clases y axioma de regularidad

Los axiomas de la existencia de clase se utilizarán para probar el teorema de la existencia de clase: Por cada fórmula en ${displaystyle n}$ variables de conjunto libre que cuantifica solamente sobre conjuntos, existe una clase de ${displaystyle n}$-tuples que lo satisfaga. El siguiente ejemplo comienza con dos clases que son funciones y construye una función compuesta. Este ejemplo ilustra las técnicas que se necesitan para probar el teorema de la existencia de clase, que conducen a los axiomas de la existencia de clase que son necesarios.

Example 1:  If the classes ${displaystyle F}$ and ${displaystyle G}$ are functions, then the composite function ${displaystyle Gcirc F}$ is defined by the formula: ${displaystyle exists t[(x,t)in F,land ,(t,y)in G].}$ Since this formula has two free set variables, ${displaystyle x}$ and ${displaystyle y,}$ the class existence theorem constructs the class of ordered pairs: ${displaystyle Gcirc F,=,{(x,y):exists t[(x,t)in F,land ,(t,y)in G]}.}$ Because this formula is built from simpler formulas using conjunction ${displaystyle land }$ and existential quantification ${displaystyle exists }$, class operations are needed that take classes representing the simpler formulas and produce classes representing the formulas with ${displaystyle land }$ and ${displaystyle exists }$. To produce a class representing a formula with ${displaystyle land }$, intersection used since ${displaystyle xin Acap Biff xin Aland xin B.}$ To produce a class representing a formula with ${displaystyle exists }$, the domain is used since ${displaystyle xin Dom(A)iff exists t[(x,t)in A].}$ Before taking the intersection, the tuples in ${displaystyle F}$ and ${displaystyle G}$ need an extra component so they have the same variables. The component ${displaystyle y}$ is added to the tuples of ${displaystyle F}$ and ${displaystyle x}$ is added to the tuples of ${displaystyle G}$: $${displaystyle F'={(x,t,y):(x,t)in F},}$$ and ${displaystyle ,G'={(t,y,x):(t,y)in G}}$ In the definition of ${displaystyle F',}$ the variable ${displaystyle y}$ is not restricted by the statement ${displaystyle (x,t)in F,}$ so ${displaystyle y}$ ranges over the class ${displaystyle V}$ of all sets. Similarly, in the definition of ${displaystyle G',}$ the variable ${displaystyle x}$ ranges over ${displaystyle V.}$ So an axiom is needed that adds an extra component (whose values range over ${displaystyle V}$) to the tuples of a given class. Next, the variables are put in the same order to prepare for the intersection: $${displaystyle F''={(x,y,t):(x,t)in F},}$$ and ${displaystyle ,G''={(x,y,t):(t,y)in G}}$ To go from ${displaystyle F'}$ to ${displaystyle F''}$ and from ${displaystyle G'}$ to ${displaystyle G''}$ requires two different permutations, so axioms that support permutations of tuple components are needed. The intersection of ${displaystyle F''}$ and ${displaystyle G''}$ handles ${displaystyle land }$: $${displaystyle F''cap G''={(x,y,t):(x,t)in F,land ,(t,y)in G}}$$ Since ${displaystyle (x,y,t)}$ is defined as ${displaystyle ((x,y),t)}$, taking the domain of ${displaystyle F''cap G''}$ handles ${displaystyle exists t}$ and produces the composite function: $${displaystyle Gcirc F=Dom(F''cap G'')={(x,y):exists t((x,t)in F,land ,(t,y)in G)}}$$ So axioms of intersection and domain are needed.

Los axiomas de existencia de clases se dividen en dos grupos: axiomas que manejan primitivos del lenguaje y axiomas que manejan tuplas. Hay cuatro axiomas en el primer grupo y tres axiomas en el segundo grupo.

Axiomas para el manejo de primitivos del lenguaje:

Composición. Existe una clase ${displaystyle E}$ conteniendo todos los pares ordenados cuyo primer componente es miembro del segundo componente.

${displaystyle exists E,forall x,forall you,[(x,y)in Eiff xin y]!}$

Intersección (conjunción). Para cualquier clase ${displaystyle A}$ y ${displaystyle B}$, hay una clase ${displaystyle C}$ consiste precisamente en los conjuntos que pertenecen a ambos ${displaystyle A}$ y ${displaystyle B}$.

${displaystyle forall A,forall B,exists C,forall x,[xin Ciff (xin A,land ,xin B)}$

Complemento (negación). Para cualquier clase ${displaystyle A}$, hay una clase ${displaystyle B}$ consiste precisamente en los conjuntos que no pertenecen a ${displaystyle A}$.

${displaystyle forall A,exists B,forall x,[xin Biff neg (xin A)}$

Dominio (cuartificador existencial). Para cualquier clase ${displaystyle A}$, hay una clase ${displaystyle B}$ consiste precisamente en los primeros componentes de los pares ordenados de ${displaystyle A}$.

${displaystyle forall A,exists B,forall x,[xin Biff exists y(x,y)in A)}$

Por el axioma de la extensión, clase ${displaystyle C}$ en la intersección axioma y clase ${displaystyle B}$ en el complemento y los axiomas de dominio son únicos. Serán denotados por: ${displaystyle Acap B,}$ ${displaystyle complement A,}$ y ${displaystyle Dom(A),}$ respectivamente. Por otra parte, la extensión no es aplicable a ${displaystyle E}$ en el axioma de la membresía ya que especifica solamente los conjuntos ${displaystyle E}$ que son pares ordenados.

Los tres primeros axiomas implican la existencia de la clase vacía y la clase de todos los conjuntos: El axioma de la membresía implica la existencia de una clase ${displaystyle E.}$ La intersección y los axiomas complementarios implican la existencia de ${displaystyle Ecap complement E.$, que está vacía. Por el axioma de la extensión, esta clase es única; se denota por ${displaystyle emptyset.}$ El complemento ${displaystyle emptyset }$ es la clase ${displaystyle V}$ de todos los conjuntos, que también es único por la extensión. El predicado establecido ${displaystyle M(A)}$, que se define como ${displaystyle exists C(Ain C)}$, ahora se redefine como ${displaystyle Ain V}$ para evitar cuantificar las clases.

Axiomas para el manejo de tuplas:

Producto por ${displaystyle V}$. Para cualquier clase ${displaystyle A}$, hay una clase ${displaystyle B}$ consistente en los pares ordenados cuyo primer componente pertenece a ${displaystyle A}$.

${displaystyle forall A,exists B,forall you,[uin] Biff exists x,exists y,(u=(x,y)land xin A)]}$

Permutación circular. Para cualquier clase ${displaystyle A}$, hay una clase ${displaystyle B}$ cuyos 3-tuples se obtienen aplicando la permutación circular ${displaystyle (y,z,x)mapsto (x,y,z)}$ a los 3-tuplas de ${displaystyle A}$.

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

Transposición. Para cualquier clase ${displaystyle A}$, hay una clase ${displaystyle B}$ cuyos 3-tuples se obtienen transponiendo los dos últimos componentes de los 3-tuples de ${displaystyle A}$.

${displaystyle forall A,exists B,forall x,forall you,[(x,y,z)in Biff (x,z,y)in A]$

Por extensión, el producto por ${displaystyle V}$ axioma implica la existencia de una clase única, que es denotada por ${displaystyle Atimes V.}$ Este axioma se utiliza para definir la clase ${displaystyle V^{n}$ de todos ${displaystyle n}$-tuples: ${displaystyle V^{1}=V}$ y ${displaystyle V^{n+1}=V^{n}times V.$ Si ${displaystyle A}$ es una clase, la extensión implica que ${displaystyle Acap V^{n}$ es la clase única que consiste en ${displaystyle n}$-tuples de ${displaystyle A.}$ Por ejemplo, el axioma de la membresía produce una clase ${displaystyle E}$ que puede contener elementos que no se ordenan pares, mientras que la intersección ${displaystyle Ecap V^{2}$ contiene sólo los pares ordenados de ${displaystyle E}$.

Los axiomas circulares de permutación y transposición no implican la existencia de clases únicas porque especifican solamente los 3-tuples de clase ${displaystyle B.}$ Al especificar los 3‐tuples, estos axiomas también especifican los ${displaystyle n}$-tuples para ${displaystyle ngeq 4}$ desde:

$${displaystyle (x_{1},ldotsx_{n-2},x_{n-1},x_{n})=(x_{1},ldotsx_{n-2}),x_{n-1},x_{n}}}}}}$$

Se necesita un axioma más para demostrar el teorema de existencia de clases: el axioma de regularidad. Una vez demostrada la existencia de la clase vacía, se da el enunciado habitual de este axioma.

Axioma de regularidad.  Cada conjunto no vacío tiene al menos un elemento con el que no tiene ningún elemento en común.

$${displaystyle forall a,[aneq emptyset implies exists u(uin aland ucap a=emptyset)].}$$

Este axioma implica que un conjunto no puede pertenecer a sí mismo: Supongamos que ${displaystyle xin x}$ y dejar ${displaystyle a={x}}$ Entonces... ${displaystyle xcap aneq emptyset }$ desde entonces ${displaystyle xin xcap a.}$ Esto contradice el axioma de la regularidad porque ${displaystyle x}$ es el único elemento en ${displaystyle a.}$ Por lo tanto, ${displaystyle xnotin x.}$ El axioma de la regularidad también prohíbe infinitas secuencias de miembros descendentes de conjuntos:

$${displaystyle cdots in x_{n+1}in x_{n}in cdots in x_{1}in x_{0}$$

Gödel afirmó la regularidad de las clases en lugar de la de los conjuntos en su monografía de 1940, que se basó en conferencias dadas en 1938. En 1939, demostró que la regularidad de los conjuntos implica regularidad de las clases.

Teorema de existencia de clases

Teorema de existencia de clase—Vamos ${displaystyle phi (x_{1},dotsx_{n},Y_{1},dots Sí.$ ser una fórmula que cuantifica solamente sobre conjuntos y no contiene ninguna variable libre que no sea ${displaystyle x_{1},dotsx_{n},Y_{1},dotsY_{m}$ (no necesariamente todos estos). Entonces para todos ${displaystyle Y_{1},dots Y...$, existe una clase única ${displaystyle A}$ de ${displaystyle n}$-tuples tal que:

$${displaystyle forall x_{1}cdots ,forall x_{n}[(x_{1},dotsx_{n})in Aiff phi (x_{1},dotsx_{n},Y_{1},dotsY_{m}].}$$

La clase ${displaystyle A}$ es denotado por ${displaystyle {(x_{1},dotsx_{n}:phi (x_{1},dotsx_{n},Y_{1},dotsY_{m}}}}$

La demostración del teorema se realizará en dos pasos:

1. Las reglas de transformación se utilizan para transformar la fórmula dada ${displaystyle phi }$ en una fórmula equivalente que simplifica la parte inductiva de la prueba. Por ejemplo, los únicos símbolos lógicos en la fórmula transformada son ${displaystyle neg }$, ${displaystyle land }$, y ${displaystyle exists }$, por lo que la inducción maneja símbolos lógicos con sólo tres casos.
2. El teorema de la existencia de clase se demuestra inductivamente para fórmulas transformadas. Guiados por la estructura de la fórmula transformada, los axiomas de la existencia de clase se utilizan para producir la clase única de ${displaystyle n}$-tuples satisfaciendo la fórmula.

Reglas de transformación. En las reglas 1 y 2 infra, ${displaystyle Delta }$ y ${displaystyle "Gamma"$ denote set o variables de clase. Estas dos reglas eliminan todas las ocurrencias de variables de clase antes de una ${displaystyle in }$ y todos los casos de igualdad. Cada regla 1 o 2 se aplica a una subformula, ${displaystyle i}$ es elegido para que ${displaystyle z_{i}$ difiere de las otras variables de la fórmula actual. Las tres reglas se repiten hasta que no haya subformulas a las que puedan aplicarse. Esto produce una fórmula que se construye sólo con ${displaystyle neg }$, ${displaystyle land }$, ${displaystyle exists }$, ${displaystyle in }$, variables establecidas y variables de clase ${displaystyle Y...$ Donde ${displaystyle Y...$ no aparece antes ${displaystyle in }$.

1. ${displaystyle ,Y_{k}in Gamma }$ se transforma en ${displaystyle exists z_{i}(z_{i}=Y_{k},land ,z_{i}in Gamma). }$
2. La extensión se utiliza para transformar ${displaystyle Delta =Gamma }$ en ${displaystyle forall z_{i}(z_{i}in Delta iff z_{i}in Gamma). }$
3. Las identidades lógicas se utilizan para transformar subformulas que contienen ${displaystyle lorimpliesiff}$ y ${displaystyle forall }$ a subformulas que solo utilizan ${displaystyle negland}$ y ${displaystyle exists.}$

Reglas de transformación: variables vinculadas. Considere la fórmula de función compuesta del ejemplo 1 con sus variables de conjunto libre reemplazadas por ${displaystyle x_{1}}$ y ${displaystyle x_{2}$: ${displaystyle exists t[(x_{1},t)in F,land ,(t,x_{2}in G].}$ La prueba inductiva eliminará ${displaystyle exists t}$, que produce la fórmula ${displaystyle (x_{1},t)in Fland (t,x_{2}in G.}$ Sin embargo, dado que el teorema de la existencia de clase se declara para variables subscriptas, esta fórmula no tiene la forma esperada por la hipótesis de inducción. Este problema se resuelve reemplazando la variable ${displaystyle t}$ con ${displaystyle x_{3}$ Las variables de sonido dentro de cuantificadores anidados se manejan aumentando el subscripto por uno para cada cuantificador sucesivo. Esto conduce a la regla 4, que debe aplicarse después de las otras reglas, ya que las reglas 1 y 2 producen variables cuantificadas.

4. Si una fórmula no contiene variables de conjunto libre que no sean ${displaystyle x_{1},dot Sx_{n},}$ entonces variables ligadas que se anidan dentro ${displaystyle q}$ los cuantificadores son reemplazados por ${displaystyle x_{n+q}$. Estas variables tienen (quantificador) profundidad de anidación ${displaystyle q}$.

Ejemplo 2: La regla 4 se aplica a la fórmula ${displaystyle phi (x_{1}}$ que define la clase que consiste en todos los conjuntos de la forma ${displaystyle {emptyset{emptysetdots },dots }.}$ Es decir, conjuntos que contienen al menos ${displaystyle emptyset }$ y un conjunto que contiene ${displaystyle emptyset }$ - por ejemplo, ${displaystyle {emptyset{emptyseta,b,c},d,e}$ Donde ${displaystyle a,b,c,d,}$ y ${displaystyle e}$ son sets. $$################################################################################################################################################################################################################################################################$$ Desde ${displaystyle x_{1}}$ es la única variable libre, ${displaystyle n=1.}$ La variable cuantificada ${displaystyle x_{3}}$ aparece dos veces ${displaystyle x_{3}in x_{2}$ a profundidad de anidación 2. Su subscripto es 3 porque ${displaystyle n+q=1+2=3.}$ Si dos alcances cuantificadores están a la misma profundidad de anidación, son idénticos o descompuestos. Las dos ocurrencias de ${displaystyle x_{3}}$ están en alcances de cuantificación descomunal, por lo que no interactúan entre sí.

Demostración del teorema de existencia de clases.  La prueba comienza aplicando las reglas de transformación a la fórmula dada para producir una fórmula transformada. Dado que esta fórmula es equivalente a la fórmula dada, la demostración se completa demostrando el teorema de existencia de clases para fórmulas transformadas.

Proof of the class existence theorem for transformed formulas

The following lemma is used in the proof.

Expansion lemma — Let ${displaystyle 1leq i<jleq n,}$ and let ${displaystyle P}$ be a class containing all the ordered pairs ${displaystyle (x_{i},x_{j})}$ satisfying ${displaystyle R(x_{i},x_{j}).}$ That is, ${displaystyle Psupseteq {(x_{i},x_{j}):R(x_{i},x_{j})}.}$ Then ${displaystyle P}$ can be expanded into the unique class ${displaystyle Q}$ of ${displaystyle n}$-tuples satisfying ${displaystyle R(x_{i},x_{j})}$. That is, ${displaystyle Q={(x_{1},ldotsx_{n}):R(x_{i},x_{j})}.}$

Proof:

1. If ${displaystyle i=1,}$ let ${displaystyle P_{1}=P.}$
   Otherwise, ${displaystyle i>1,}$ so components are added in front of ${displaystyle x_{i}{text{:}}}$ apply the tuple lemma's statement 1 to ${displaystyle P}$ with ${displaystyle z=(x_{1},dotsx_{i-1}).}$ This produces a class ${displaystyle P_{1}}$ containing all the ${displaystyle (i+1)}$-tuples
   $${displaystyle ((x_{1},dotsx_{i-1}),x_{i},x_{j})=(x_{1},dotsx_{i-1},x_{i},x_{j})}$$

   
   satisfying ${displaystyle R(x_{i},x_{j}).}$
2. If ${displaystyle j=i+1,}$ let ${displaystyle P_{2}=P_{1}.}$
   Otherwise, ${displaystyle j>i+1,}$ so components are added between ${displaystyle x_{i}}$ and ${displaystyle x_{j}{text{:}}}$ add the components ${displaystyle x_{i+1},dotsx_{j-1}}$ one by one using the tuple lemma's statement 2. This produces a class ${displaystyle P_{2}}$ containing all the ${displaystyle j}$-tuples
   $${displaystyle (((cdots ((x_{1},dotsx_{i}),x_{i+1}),cdots),x_{j-1}),x_{j})=(x_{1},dotsx_{j})}$$

   
   satisfying ${displaystyle R(x_{i},x_{j}).}$
3. If ${displaystyle j=n,}$ let ${displaystyle P_{3}=P_{2}.}$
   Otherwise, ${displaystyle j<n,}$ so components are added after ${displaystyle x_{j}{text{:}}}$ add the components ${displaystyle x_{j+1},dotsx_{n}}$ one by one using the tuple lemma's statement 3. This produces a class ${displaystyle P_{3}}$ containing all the ${displaystyle n}$-tuples
   $${displaystyle ((cdots ((x_{1},dotsx_{j}),x_{j+1}),cdots),x_{n})=(x_{1},dotsx_{n})}$$

   
   satisfying ${displaystyle R(x_{i},x_{j}).}$
4. Let ${displaystyle Q=P_{3}cap V^{n}.}$ Extensionality implies that ${displaystyle Q}$ is the unique class of ${displaystyle n}$-tuples satisfying ${displaystyle R(x_{i},x_{j}).}$

Class existence theorem for transformed formulas — Let ${displaystyle phi (x_{1},ldotsx_{n},Y_{1},ldotsY_{m})}$ be a formula that:

1. contains no free variables other than ${displaystyle x_{1},ldotsx_{n},Y_{1},ldotsY_{m}}$;
   
2. contains only ${displaystyle in }$, ${displaystyle neg }$, ${displaystyle land }$, ${displaystyle exists }$, set variables, and the class variables ${displaystyle Y_{k}}$ where ${displaystyle Y_{k}}$ does not appear before an ${displaystyle in }$ ;
   
3. only quantifies set variables ${displaystyle x_{n+q}}$ where ${displaystyle q}$ is the quantifier nesting depth of the variable.

Then for all ${displaystyle Y_{1},dotsY_{m}}$, there exists a unique class ${displaystyle A}$ of ${displaystyle n}$-tuples such that:

$${displaystyle forall x_{1}cdots ,forall x_{n}[(x_{1},ldotsx_{n})in Aiff phi (x_{1},ldotsx_{n},Y_{1},ldotsY_{m})].}$$

Proof: Basis step: ${displaystyle phi }$ has 0 logical symbols. The theorem's hypothesis implies that ${displaystyle phi }$ is an atomic formula of the form ${displaystyle x_{i}in x_{j}}$ or ${displaystyle x_{i}in Y_{k}.}$

Case 1: If ${displaystyle phi }$ is ${displaystyle x_{i}in x_{j}}$, we build the class ${displaystyle E_{i,j,n}={(x_{1},ldotsx_{n}):x_{i}in x_{j}},}$ the unique class of ${displaystyle n}$-tuples satisfying ${displaystyle x_{i}in x_{j}.}$

Case a: ${displaystyle phi }$ is ${displaystyle x_{i}in x_{j}}$ where ${displaystyle i<j.}$ The axiom of membership produces a class ${displaystyle P}$ containing all the ordered pairs ${displaystyle (x_{i},x_{j})}$ satisfying ${displaystyle x_{i}in x_{j}.}$ Apply the expansion lemma to ${displaystyle P}$ to obtain ${displaystyle E_{i,j,n}={(x_{1},ldotsx_{n}):x_{i}in x_{j}}.}$

Case b: ${displaystyle phi }$ is ${displaystyle x_{i}in x_{j}}$ where ${displaystyle i>j.}$ The axiom of membership produces a class ${displaystyle P}$ containing all the ordered pairs ${displaystyle (x_{i},x_{j})}$ satisfying ${displaystyle x_{i}in x_{j}.}$ Apply the tuple lemma's statement 4 to ${displaystyle P}$ to obtain ${displaystyle P'}$ containing all the ordered pairs ${displaystyle (x_{j},x_{i})}$ satisfying ${displaystyle x_{i}in x_{j}.}$ Apply the expansion lemma to ${displaystyle P'}$ to obtain ${displaystyle E_{i,j,n}={(x_{1},ldotsx_{n}):x_{i}in x_{j}}.}$

Case c: ${displaystyle phi }$ is ${displaystyle x_{i}in x_{j}}$ where ${displaystyle i=j.}$ Since this formula is false by the axiom of regularity, no ${displaystyle n}$-tuples satisfy it, so ${displaystyle E_{i,j,n}=emptyset.}$

Case 2: If ${displaystyle phi }$ is ${displaystyle x_{i}in Y_{k}}$, we build the class ${displaystyle E_{i,Y_{k},n}={(x_{1},ldotsx_{n}):x_{i}in Y_{k}},}$ the unique class of ${displaystyle n}$-tuples satisfying ${displaystyle x_{i}in Y_{k}.}$

Case a: ${displaystyle phi }$ is ${displaystyle x_{i}in Y_{k}}$ where ${displaystyle i<n.}$ Apply the axiom of product by ${displaystyle V}$ to ${displaystyle Y_{k}}$ to produce the class ${displaystyle P=Y_{k}times V={(x_{i},x_{i+1}):x_{i}in Y_{k}}.}$ Apply the expansion lemma to ${displaystyle P}$ to obtain ${displaystyle E_{i,Y_{k},n}={(x_{1},ldotsx_{n}):x_{i}in Y_{k}}.}$

Case b: ${displaystyle phi }$ is ${displaystyle x_{i}in Y_{k}}$ where ${displaystyle i=n>1.}$ Apply the axiom of product by ${displaystyle V}$ to ${displaystyle Y_{k}}$ to produce the class ${displaystyle P=Y_{k}times V={(x_{i},x_{i-1}):x_{i}in Y_{k}}.}$ Apply the tuple lemma's statement 4 to ${displaystyle P}$ to obtain ${displaystyle P'=Vtimes Y_{k}={(x_{i-1},x_{i}):x_{i}in Y_{k}}.}$ Apply the expansion lemma to ${displaystyle P'}$ to obtain ${displaystyle E_{i,Y_{k},n}={(x_{1},ldotsx_{n}):x_{i}in Y_{k}}.}$

Case c: ${displaystyle phi }$ is ${displaystyle x_{i}in Y_{k}}$ where ${displaystyle i=n=1.}$ Then ${displaystyle E_{i,Y_{k},n}=Y_{k}.}$

Inductive step: ${displaystyle phi }$ has ${displaystyle k}$ logical symbols where ${displaystyle k>0}$. Assume the induction hypothesis that the theorem is true for all ${displaystyle psi }$ with less than ${displaystyle k}$ logical symbols. We now prove the theorem for ${displaystyle phi }$ with ${displaystyle k}$ logical symbols. In this proof, the list of class variables ${displaystyle Y_{1},dotsY_{m}}$ is abbreviated by ${displaystyle {vec {Y}}}$, so a formula—such as ${displaystyle phi (x_{1},dotsx_{n},Y_{1},dotsY_{m})}$—can be written as ${displaystyle phi (x_{1},dotsx_{n},{vec {Y}}).}$

Case 1: ${displaystyle phi (x_{1},ldotsx_{n},{vec {Y}})=neg psi (x_{1},ldotsx_{n},{vec {Y}}).}$ Since ${displaystyle psi }$ has ${displaystyle k-1}$ logical symbols, the induction hypothesis implies that there is a unique class ${displaystyle A}$ of ${displaystyle n}$-tuples such that:

$${displaystyle quad (x_{1},ldotsx_{n})in Aiff psi (x_{1},ldotsx_{n},{vec {Y}}).}$$

By the complement axiom, there is a class ${displaystyle complement A}$ such that ${displaystyle forall u,[uin complement Aiff neg (uin A)].}$ However, ${displaystyle complement A}$ contains elements other than ${displaystyle n}$-tuples if ${displaystyle n>1.}$ To eliminate these elements, use ${displaystyle complement _{V^{n}}A=,}$${displaystyle complement Acap V^{n}=,}$${displaystyle V^{n}setminus A,}$ which is the complement relative to the class ${displaystyle V^{n}}$ of all ${displaystyle n}$-tuples. Then, by extensionality, ${displaystyle complement _{V^{n}}A}$ is the unique class of ${displaystyle n}$-tuples such that:

$${displaystyle {begin{alignedat}{2}quad &(x_{1},ldotsx_{n})in complement _{V^{n}}A&&iff neg [(x_{1},ldotsx_{n})in A]\&&&iff neg psi (x_{1},ldotsx_{n},{vec {Y}})\&&&iff phi (x_{1},ldotsx_{n},{vec {Y}}).end{alignedat}}}$$

Case 2: ${displaystyle phi (x_{1},ldotsx_{n},{vec {Y}})=psi _{1}(x_{1},ldotsx_{n},{vec {Y}})land psi _{2}(x_{1},ldotsx_{n},{vec {Y}}).}$ Since both ${displaystyle psi _{1}}$ and ${displaystyle psi _{2}}$ have less than ${displaystyle k}$ logical symbols, the induction hypothesis implies that there are unique classes of ${displaystyle n}$-tuples, ${displaystyle A_{1}}$ and ${displaystyle A_{2}}$, such that:

${displaystyle {begin{aligned}quad &(x_{1},ldotsx_{n})in A_{1}iff psi _{1}(x_{1},ldotsx_{n},{vec {Y}}).\&(x_{1},ldotsx_{n})in A_{2}iff psi _{2}(x_{1},ldotsx_{n},{vec {Y}}).end{aligned}}}$

By the axioms of intersection and extensionality, ${displaystyle A_{1}cap A_{2}}$ is the unique class of ${displaystyle n}$-tuples such that:

$${displaystyle {begin{alignedat}{2}quad &(x_{1},ldotsx_{n})in A_{1}cap A_{2}&&iff (x_{1},ldotsx_{n})in A_{1}land (x_{1},ldotsx_{n})in A_{2}\&&&iff psi _{1}(x_{1},ldotsx_{n},{vec {Y}})land psi _{2}(x_{1},ldotsx_{n},{vec {Y}})\&&&iff phi (x_{1},ldotsx_{n},{vec {Y}}).end{alignedat}}}$$

Case 3: ${displaystyle phi (x_{1},ldotsx_{n},{vec {Y}})=exists x_{n+1}psi (x_{1},ldotsx_{n},x_{n+1},{vec {Y}}).}$ The quantifier nesting depth of ${displaystyle psi }$ is one more than that of ${displaystyle phi }$ and the additional free variable is ${displaystyle x_{n+1}.}$ Since ${displaystyle psi }$ has ${displaystyle k-1}$ logical symbols, the induction hypothesis implies that there is a unique class ${displaystyle A}$ of ${displaystyle (n+1)}$-tuples such that:

$${displaystyle quad (x_{1},ldotsx_{n},x_{n+1})in Aiff psi (x_{1},ldotsx_{n},x_{n+1},{vec {Y}}).}$$

By the axioms of domain and extensionality, ${displaystyle Dom(A)}$ is the unique class of ${displaystyle n}$-tuples such that:

$${displaystyle {begin{alignedat}{2}quad &(x_{1},ldotsx_{n})in Dom(A)&&iff exists x_{n+1}[((x_{1},ldotsx_{n}),x_{n+1})in A]\&&&iff exists x_{n+1}[(x_{1},ldotsx_{n},x_{n+1})in A]\&&&iff exists x_{n+1},psi (x_{1},ldotsx_{n},x_{n+1},{vec {Y}})\&&&iff phi (x_{1},ldotsx_{n},{vec {Y}}).end{alignedat}}}$$