En lógica matemática , Nuevos Fundamentos ( NF ) es una teoría de conjuntos no bien fundamentada y finitamente axiomatizable concebida por Willard Van Orman Quine como una simplificación de la teoría de tipos de Principia Mathematica .
Las fórmulas bien formadas de NF son las fórmulas estándar del cálculo proposicional con dos predicados primitivos: igualdad [ ancla rota ] ( ) y pertenencia ( ). NF se puede presentar con solo dos esquemas axiomáticos:
Se dice que una fórmula está estratificada si existe una función f a partir de fragmentos de la sintaxis de hasta los números naturales, tal que para cualquier subfórmula atómica de tenemos f ( y ) = f ( x ) + 1, mientras que para cualquier subfórmula atómica de , tenemos f ( x ) = f ( y ).
La NF puede axiomatizarse finitamente . [1] Una ventaja de esta axiomatización finita es que elimina la noción de estratificación . Los axiomas en una axiomatización finita corresponden a construcciones básicas naturales, mientras que la comprensión estratificada es poderosa pero no necesariamente intuitiva. En su libro introductorio, Holmes optó por tomar la axiomatización finita como básica y demostrar la comprensión estratificada como un teorema. [2] El conjunto preciso de axiomas puede variar, pero incluye la mayoría de los siguientes, y los demás se pueden demostrar como teoremas: [3] [1]
New Foundations está estrechamente relacionada con la teoría de conjuntos tipados no ramificados de Russell ( TST ), una versión simplificada de la teoría de tipos de Principia Mathematica con una jerarquía lineal de tipos. En esta teoría de múltiples tipos , a cada variable y conjunto se le asigna un tipo. Es habitual escribir los índices de tipo como superíndices: denota una variable de tipo n . El tipo 0 consta de individuos no descritos de otro modo. Para cada número (meta) natural n , los objetos de tipo n +1 son conjuntos de objetos de tipo n ; los objetos conectados por identidad tienen tipos iguales y los conjuntos de tipo n tienen miembros de tipo n -1. Los axiomas de la TST son extensionalidad, en conjuntos del mismo tipo (positivo), y comprensión, es decir, que si es una fórmula, entonces el conjunto existe. En otras palabras, dada cualquier fórmula , la fórmula es un axioma donde representa el conjunto y no es libre en . Esta teoría de tipos es mucho menos complicada que la inicialmente planteada en los Principia Mathematica , que incluía tipos para relaciones cuyos argumentos no eran necesariamente todos del mismo tipo.
Existe una correspondencia entre New Foundations y TST en términos de agregar o borrar anotaciones de tipo. En el esquema de comprensión de NF, una fórmula se estratifica exactamente cuando se le pueden asignar tipos de acuerdo con las reglas de TST. Esto se puede ampliar para asignar cada fórmula de NF a un conjunto de fórmulas TST correspondientes con varias anotaciones de índice de tipo. La asignación es de uno a muchos porque TST tiene muchas fórmulas similares. Por ejemplo, aumentar cada índice de tipo en una fórmula TST en 1 da como resultado una fórmula TST nueva y válida.
La teoría de tipos enredados (TTT) es una extensión de la TST, en la que cada variable se tipifica mediante un número ordinal en lugar de un número natural. Las fórmulas atómicas bien formadas son y donde . Los axiomas de la TTT son los de la TST, en los que cada variable de tipo se asigna a una variable donde es una función creciente.
La TTT se considera una teoría "extraña" porque cada tipo está relacionado con cada tipo inferior de la misma manera. Por ejemplo, los conjuntos de tipo 2 tienen miembros de tipo 1 y de tipo 0, y los axiomas de extensionalidad afirman que un conjunto de tipo 2 está determinado únicamente por sus miembros de tipo 1 o por sus miembros de tipo 0. Mientras que la TST tiene modelos naturales donde cada tipo es el conjunto potencia del tipo , en la TTT cada tipo se interpreta como el conjunto potencia de cada tipo inferior simultáneamente. Independientemente de ello, un modelo de NF se puede convertir fácilmente en un modelo de TTT, porque en NF todos los tipos ya son uno y el mismo. A la inversa, con un argumento más complicado, también se puede demostrar que la consistencia de la TTT implica la consistencia de NF. [34]
La NF con urelementos ( NFU ) es una variante importante de la NF debida a Jensen [35] y aclarada por Holmes. [3] Los urelementos son objetos que no son conjuntos y no contienen ningún elemento, pero pueden estar contenidos en conjuntos. Una de las formas más simples de axiomatización de NFU considera a los urelementos como conjuntos vacíos múltiples y desiguales, debilitando así el axioma de extensionalidad de la NF a:
En esta axiomatización, el esquema de comprensión no cambia, aunque el conjunto no será único si está vacío (es decir, si es insatisfacible).
Sin embargo, para facilitar su uso, es más conveniente tener un conjunto vacío único y "canónico". Esto se puede hacer introduciendo un predicado de conjunto para distinguir los conjuntos de los átomos. Los axiomas son entonces: [36]
NF 3 es el fragmento de NF con extensionalidad completa (sin urelementos) y aquellas instancias de comprensión que pueden estratificarse utilizando como máximo tres tipos. NF 4 es la misma teoría que NF.
La lógica matemática (ML) es una extensión de la NF que incluye clases propias y conjuntos. La ML fue propuesta por Quine y revisada por Hao Wang, quien demostró que la NF y la ML revisada son equiconsistentes.
En esta sección se analizan algunas construcciones problemáticas en NF. Para un mayor desarrollo de las matemáticas en NFU, con una comparación con el desarrollo de las mismas en ZFC, véase implementación de las matemáticas en la teoría de conjuntos .
Las relaciones y funciones se definen en TST (y en NF y NFU) como conjuntos de pares ordenados de la forma habitual. A los efectos de la estratificación, es deseable que una relación o función sea simplemente un tipo superior al tipo de los miembros de su cuerpo. Esto requiere definir el par ordenado de modo que su tipo sea el mismo que el de sus argumentos (lo que da como resultado un par ordenado a nivel de tipo ). La definición habitual del par ordenado, es decir , da como resultado un tipo dos veces superior al tipo de sus argumentos a y b . Por lo tanto, a los efectos de determinar la estratificación, una función es tres tipos superior a los miembros de su cuerpo. NF y teorías relacionadas suelen emplear la definición de Quine de par ordenado en teoría de conjuntos , que produce un par ordenado a nivel de tipo. Sin embargo, la definición de Quine se basa en operaciones de conjunto sobre cada uno de los elementos a y b , y por lo tanto no funciona directamente en NFU.
Como enfoque alternativo, Holmes [3] toma el par ordenado (a, b) como una noción primitiva , así como sus proyecciones izquierda y derecha y , es decir, funciones tales que y (en la axiomatización de Holmes de NFU, el esquema de comprensión que afirma la existencia de para cualquier fórmula estratificada se considera un teorema y solo se demuestra más tarde, por lo que expresiones como no se consideran definiciones adecuadas). Afortunadamente, si el par ordenado es de nivel de tipo por definición o por suposición (es decir, se toma como primitivo) generalmente no importa.
La forma usual del axioma de infinito se basa en la construcción de von Neumann de los números naturales , que no es adecuada para la NF, ya que la descripción de la operación sucesora (y muchos otros aspectos de los numerales de von Neumann) es necesariamente no estratificada. La forma usual de los números naturales utilizada en la NF sigue la definición de Frege , es decir, el número natural n está representado por el conjunto de todos los conjuntos con n elementos. Bajo esta definición, 0 se define fácilmente como , y la operación sucesora se puede definir de manera estratificada: Bajo esta definición, uno puede escribir una afirmación análoga a la forma usual del axioma de infinito. Sin embargo, esa afirmación sería trivialmente verdadera, ya que el conjunto universal sería un conjunto inductivo .
Como los conjuntos inductivos siempre existen, el conjunto de los números naturales puede definirse como la intersección de todos los conjuntos inductivos. Esta definición permite la inducción matemática para enunciados estratificados , porque el conjunto puede construirse y, cuando satisface las condiciones para la inducción matemática, este conjunto es un conjunto inductivo.
Los conjuntos finitos pueden definirse entonces como conjuntos que pertenecen a un número natural. Sin embargo, no es trivial demostrar que no es un "conjunto finito", es decir, que el tamaño del universo no es un número natural. Supóngase que . Entonces (se puede demostrar inductivamente que un conjunto finito no es equinumeroso con ninguno de sus subconjuntos propios), , y cada número natural subsiguiente también lo sería , lo que haría que la aritmética dejara de funcionar. Para evitarlo, se puede introducir el axioma de infinito para NF: [37]
Puede parecer intuitivamente que uno debería ser capaz de probar el Infinito en NF(U) construyendo cualquier secuencia "externamente" infinita de conjuntos, como . Sin embargo, tal secuencia solo podría construirse mediante construcciones no estratificadas (evidenciado por el hecho de que la propia TST tiene modelos finitos), por lo que tal prueba no podría llevarse a cabo en NF(U). De hecho, el Infinito es lógicamente independiente de NFU: existen modelos de NFU donde es un número natural no estándar . En tales modelos, la inducción matemática puede probar afirmaciones sobre , haciendo imposible "distinguirlo" de los números naturales estándar.
Sin embargo, hay algunos casos en los que se puede demostrar el infinito (en cuyos casos se puede hacer referencia al teorema del infinito ):
Existen axiomas más fuertes de infinito, como que el conjunto de números naturales es un conjunto fuertemente cantoriano, o NFUM = NFU + Infinito + Ordinales Grandes + Ordinales Pequeños , que es equivalente a la teoría de conjuntos de Morse-Kelley más un predicado sobre clases propias que es un ultrafiltro no principal κ -completo sobre el ordinal de clase propia κ . [39]
NF (y NFU + Infinito + Elección , descritos a continuación y conocidos como consistentes) permiten la construcción de dos tipos de conjuntos que ZFC y sus extensiones propias no permiten porque son "demasiado grandes" (algunas teorías de conjuntos admiten estas entidades bajo el título de clases propias ):
La categoría cuyos objetos son los conjuntos de NF y cuyas flechas son las funciones entre esos conjuntos no es cartesianamente cerrada ; [40] Dado que NF carece de cierre cartesiano, no todas las funciones cursan como uno podría esperar intuitivamente, y NF no es un topos .
Puede parecer que la NF se enfrenta a problemas similares a los de la teoría de conjuntos ingenua , pero no es así. Por ejemplo, la existencia de la clase imposible de Russell no es un axioma de la NF, porque no se puede estratificar. La NF evita las tres paradojas bien conocidas de la teoría de conjuntos de maneras drásticamente diferentes a cómo se resuelven esas paradojas en teorías de conjuntos bien fundamentadas como la ZFC. Muchos conceptos útiles que son exclusivos de la NF y sus variantes se pueden desarrollar a partir de la resolución de esas paradojas.
La resolución de la paradoja de Russell es trivial: no es una fórmula estratificada, por lo que la existencia de no se afirma en ninguna instancia de Comprensión . Quine dijo que construyó NF con esta paradoja en mente. [41]
La paradoja de Cantor se reduce a la cuestión de si existe un número cardinal más grande o, equivalentemente, si existe un conjunto con la cardinalidad más grande . En NF, el conjunto universal es obviamente un conjunto con la cardinalidad más grande. Sin embargo, el teorema de Cantor dice (dada ZFC) que el conjunto potencia de cualquier conjunto es más grande que (no puede haber inyección (aplicación biunívoca) de en ), lo que parece implicar una contradicción cuando .
Por supuesto, hay una inyección de en ya que es el conjunto universal, por lo que debe ser que el teorema de Cantor (en su forma original) no se cumple en NF. De hecho, la prueba del teorema de Cantor utiliza el argumento de diagonalización al considerar el conjunto . En NF, y se les debe asignar el mismo tipo, por lo que la definición de no está estratificada. De hecho, si es la inyección trivial , entonces es el mismo conjunto (mal definido) en la paradoja de Russell.
Este error no es sorprendente, ya que no tiene sentido en TST: el tipo de es uno mayor que el tipo de . En NF, es una oración sintáctica debido a la combinación de todos los tipos, pero es poco probable que funcione cualquier prueba general que involucre Comprensión .
La forma habitual de corregir un problema de tipo de este tipo es reemplazar con , el conjunto de subconjuntos de un elemento de . De hecho, la versión tipificada correctamente del teorema de Cantor es un teorema en TST (gracias al argumento de diagonalización), y por lo tanto también un teorema en NF. En particular, : hay menos conjuntos de un elemento que conjuntos (y por lo tanto menos conjuntos de un elemento que objetos generales, si estamos en NFU). La biyección "obvia" del universo a los conjuntos de un elemento no es un conjunto; no es un conjunto porque su definición no está estratificada. Nótese que en todos los modelos de NFU + Choice es el caso que ; Choice permite no solo probar que hay urelementos sino que hay muchos cardinales entre y .
Sin embargo, a diferencia de TST, es una oración sintáctica en NF(U), y como se muestra arriba, uno puede hablar sobre su valor de verdad para valores específicos de (por ejemplo, cuando es falso). Un conjunto que satisface la intuitivamente atractiva se dice que es cantoriano : un conjunto cantoriano satisface la forma usual del teorema de Cantor . Un conjunto que satisface la condición adicional de que , la restricción de la función singleton a A , es un conjunto no es solo un conjunto cantoriano sino fuertemente cantoriano . [42]
La paradoja de Burali-Forti del mayor número ordinal se resuelve de manera opuesta: en NF, tener acceso al conjunto de ordinales no permite construir un "mayor número ordinal". Se puede construir el ordinal que corresponde al buen orden natural de todos los ordinales, pero eso no significa que sea mayor que todos esos ordinales.
Para formalizar la paradoja de Burali-Forti en NF, es necesario formalizar primero el concepto de números ordinales. En NF, los ordinales se definen (de la misma manera que en la teoría de conjuntos ingenua ) como clases de equivalencia de buenos ordenamientos bajo isomorfismo . Esta es una definición estratificada, por lo que el conjunto de ordinales se puede definir sin problema. La inducción transfinita funciona en enunciados estratificados, lo que permite demostrar que el orden natural de los ordinales ( si y solo si existen buenos ordenamientos tales que es una continuación de ) es un buen ordenamiento de . Por definición de ordinales, este buen ordenamiento también pertenece a un ordinal . En la teoría de conjuntos ingenua, se procedería a demostrar por inducción transfinita que cada ordinal es el tipo de orden del orden natural en los ordinales menores que , lo que implicaría una contradicción ya que por definición es el tipo de orden de todos los ordinales, no cualquier segmento inicial propio de ellos.
Sin embargo, la afirmación " es el tipo de orden del orden natural en los ordinales menores que " no está estratificada, por lo que el argumento de inducción transfinita no funciona en NF. De hecho, " el tipo de orden del orden natural en los ordinales menores que " es al menos dos tipos mayor que : La relación de orden es un tipo mayor que suponiendo que es un par ordenado a nivel de tipo, y el tipo de orden (clase de equivalencia) es un tipo mayor que . Si es el par ordenado de Kuratowski habitual (dos tipos mayores que y ), entonces sería cuatro tipos mayor que .
Para corregir este problema de tipo, se necesita la operación T , , que "elevó el tipo" de un ordinal , de la misma manera que "elevó el tipo" del conjunto . La operación T se define de la siguiente manera: Si , entonces es el tipo de orden del orden . Ahora el lema sobre los tipos de orden puede reformularse de manera estratificada:
Ambas versiones de esta afirmación pueden demostrarse por inducción transfinita; a continuación, suponemos el par de niveles de tipo. Esto significa que siempre es menor que , el tipo de orden de todos los ordinales. En particular, .
Otra afirmación (estratificada) que se puede demostrar por inducción transfinita es que T es una operación estrictamente monótona (que preserva el orden) sobre los ordinales, es decir, si y solo si . Por lo tanto, la operación T no es una función: la colección de ordinales no puede tener un miembro mínimo y, por lo tanto, no puede ser un conjunto. Más concretamente, la monotonía de T implica , una "secuencia descendente" en los ordinales que tampoco puede ser un conjunto.
Se podría afirmar que este resultado demuestra que ningún modelo de NF(U) es " estándar ", puesto que los ordinales en cualquier modelo de NFU no están bien ordenados externamente. Esta es una cuestión filosófica, no una cuestión de lo que se puede probar dentro de la teoría formal. Nótese que incluso dentro de NFU se puede probar que cualquier modelo de conjunto de NFU tiene "ordinales" no bien ordenados; NFU no concluye que el universo es un modelo de NFU, a pesar de ser un conjunto, porque la relación de pertenencia no es una relación de conjunto.
Algunos matemáticos han cuestionado la consistencia de la NF, en parte porque no está claro por qué evita las paradojas conocidas. Una cuestión clave fue que Specker demostró que la NF combinada con el axioma de elección es inconsistente. La prueba es compleja e involucra operaciones T. Sin embargo, desde 2010, Holmes ha afirmado haber demostrado que la NF es consistente en relación con la consistencia de la teoría de conjuntos estándar (ZFC). En 2024, Sky Wilshaw confirmó la prueba de Holmes utilizando el asistente de prueba Lean . [43]
Aunque la NFU resuelve las paradojas de manera similar a la NF, tiene una prueba de consistencia mucho más simple. La prueba se puede formalizar dentro de la Aritmética de Peano (PA), una teoría más débil que la ZF que la mayoría de los matemáticos aceptan sin cuestionamientos. Esto no entra en conflicto con el segundo teorema de incompletitud de Gödel porque la NFU no incluye el Axioma de Infinito y, por lo tanto, la PA no se puede modelar en la NFU, evitando una contradicción. La PA también demuestra que la NFU con Infinito y la NFU con Infinito y Elección son equiconsistentes con la TST con Infinito y la TST con Infinito y Elección, respectivamente. Por lo tanto, una teoría más fuerte como la ZFC, que demuestra la consistencia de la TST, también demostrará la consistencia de la NFU con estas adiciones. [35] En términos más simples, la NFU generalmente se considera más débil que la NF porque, en la NFU, la colección de todos los conjuntos (el conjunto de potencia del universo) puede ser más pequeña que el universo mismo, especialmente cuando se incluyen urelementos, como lo requiere la NFU con Elección.
La prueba de Jensen proporciona un método bastante simple para producir modelos de NFU en masa. Utilizando técnicas bien conocidas de la teoría de modelos , se puede construir un modelo no estándar de la teoría de conjuntos de Zermelo (no se necesita nada tan sólido como ZFC completo para la técnica básica) en el que hay un automorfismo externo j (no un conjunto del modelo) que se mueve un rango [nota 1] de la jerarquía acumulativa de conjuntos. Podemos suponer sin pérdida de generalidad que .
El dominio del modelo de NFU será el rango no estándar . La idea básica es que el automorfismo j codifica el "conjunto potencia" de nuestro "universo" en su copia externamente isomórfica dentro de nuestro "universo". Los objetos restantes que no codifican subconjuntos del universo se tratan como urelements . Formalmente, la relación de pertenencia del modelo de NFU será
Ahora se puede demostrar que este es realmente un modelo de NFU. Sea una fórmula estratificada en el lenguaje de NFU. Elija una asignación de tipos a todas las variables en la fórmula que atestigua el hecho de que está estratificada. Elija un número natural N mayor que todos los tipos asignados a las variables por esta estratificación. Expanda la fórmula en una fórmula en el lenguaje del modelo no estándar de la teoría de conjuntos de Zermelo con automorfismo j usando la definición de membresía en el modelo de NFU. La aplicación de cualquier potencia de j a ambos lados de una ecuación o enunciado de membresía preserva su valor de verdad porque j es un automorfismo. Haga tal aplicación a cada fórmula atómica en de tal manera que cada variable x asignada al tipo i ocurra con exactamente aplicaciones de j . Esto es posible gracias a la forma de los enunciados de membresía atómica derivados de los enunciados de membresía de NFU, y a que la fórmula está estratificada. Cada oración cuantificada se puede convertir a la forma (y de manera similar para los cuantificadores existenciales ). Realice esta transformación en todas partes y obtenga una fórmula en la que j nunca se aplica a una variable ligada. Elija cualquier variable libre y en el tipo asignado i . Aplique uniformemente a toda la fórmula para obtener una fórmula en la que y aparece sin ninguna aplicación de j . Ahora existe (porque j aparece aplicado solo a variables libres y constantes), pertenece a , y contiene exactamente aquellos y que satisfacen la fórmula original en el modelo de NFU. tiene esta extensión en el modelo de NFU (la aplicación de j corrige la diferente definición de membresía en el modelo de NFU). Esto establece que la Comprensión Estratificada se cumple en el modelo de NFU.
Es sencillo ver que la extensionalidad débil se cumple: cada elemento no vacío hereda una extensión única del modelo no estándar, el conjunto vacío hereda también su extensión habitual y todos los demás objetos son urelementos.
Si es un número natural n , se obtiene un modelo de NFU que afirma que el universo es finito (es externamente infinito, por supuesto). Si es infinito y la Elección se cumple en el modelo no estándar de ZFC, se obtiene un modelo de NFU + Infinito + Elección .
Por razones filosóficas, es importante señalar que no es necesario trabajar en ZFC o cualquier sistema relacionado para llevar a cabo esta prueba. Un argumento común contra el uso de NFU como fundamento de las matemáticas es que las razones para confiar en él tienen que ver con la intuición de que ZFC es correcto. Es suficiente aceptar TST (de hecho, TSTU). En resumen: tome la teoría de tipos TSTU (que permite urelementos en cada tipo positivo) como una metateoría y considere la teoría de modelos de conjuntos de TSTU en TSTU (estos modelos serán secuencias de conjuntos (todos del mismo tipo en la metateoría) con incrustaciones de cada uno en incrustaciones de codificación del conjunto potencia de into de una manera que respete el tipo). Dada una incrustación de into (que identifica elementos del "tipo" base con subconjuntos del tipo base), las incrustaciones pueden definirse a partir de cada "tipo" en su sucesor de una manera natural. Esto se puede generalizar a secuencias transfinitas con cuidado.
Nótese que la construcción de tales secuencias de conjuntos está limitada por el tamaño del tipo en el que se construyen; esto evita que TSTU demuestre su propia consistencia (TSTU + Infinity puede demostrar la consistencia de TSTU; para demostrar la consistencia de TSTU + Infinity se necesita un tipo que contenga un conjunto de cardinalidad , cuya existencia no se puede demostrar en TSTU + Infinity sin suposiciones más sólidas). Ahora los mismos resultados de la teoría de modelos se pueden utilizar para construir un modelo de NFU y verificar que es un modelo de NFU de la misma manera, utilizando 's en lugar de en la construcción habitual. El movimiento final es observar que, dado que NFU es consistente, podemos abandonar el uso de tipos absolutos en nuestra metateoría, lo que hace que la metateoría se vuelva de TSTU a NFU.
El automorfismo j de un modelo de este tipo está estrechamente relacionado con ciertas operaciones naturales en NFU. Por ejemplo, si W es un buen ordenamiento en el modelo no estándar (suponemos aquí que utilizamos pares de Kuratowski para que la codificación de funciones en las dos teorías concuerde hasta cierto punto) que también es un buen ordenamiento en NFU (todos los buenos ordenamientos de NFU son buenos ordenamientos en el modelo no estándar de la teoría de conjuntos de Zermelo, pero no al revés, debido a la formación de urelementos en la construcción del modelo), y W tiene tipo α en NFU, entonces j ( W ) será un buen ordenamiento de tipo T (α) en NFU.
De hecho, j está codificado por una función en el modelo de NFU. La función en el modelo no estándar que envía el singleton de cualquier elemento de a su único elemento, se convierte en NFU en una función que envía cada singleton { x }, donde x es cualquier objeto en el universo, a j ( x ). Llame a esta función Endo y déjela que tenga las siguientes propiedades: Endo es una inyección del conjunto de singletons en el conjunto de conjuntos, con la propiedad de que Endo ( { x } ) = { Endo ( { y } ) | y ∈ x } para cada conjunto x . Esta función puede definir una relación de "pertenencia" a nivel de tipo en el universo, una que reproduce la relación de pertenencia del modelo no estándar original.
En 1914, Norbert Wiener mostró cómo codificar el par ordenado como un conjunto de conjuntos, haciendo posible eliminar los tipos de relación de Principia Mathematica a favor de la jerarquía lineal de conjuntos en TST. La definición habitual del par ordenado fue propuesta por primera vez por Kuratowski en 1921. Willard Van Orman Quine propuso por primera vez la NF como una forma de evitar las "consecuencias desagradables" de la TST en un artículo de 1937 titulado New Foundations for Mathematical Logic ; de ahí el nombre. Quine amplió la teoría en su libro Mathematical Logic , cuya primera edición se publicó en 1940. En el libro, Quine introdujo el sistema "Mathematical Logic" o "ML", una extensión de la NF que incluía clases propias así como conjuntos . La teoría de conjuntos de la primera edición casó la NF con las clases propias de la teoría de conjuntos NBG e incluyó un esquema axiomático de comprensión irrestricta para las clases propias. Sin embargo, J. Barkley Rosser demostró que el sistema estaba sujeto a la paradoja de Burali-Forti. [44] Hao Wang mostró cómo modificar los axiomas de Quine para ML a fin de evitar este problema. [45] Quine incluyó la axiomatización resultante en la segunda y última edición, publicada en 1951.
En 1944, Theodore Hailperin demostró que la comprensión es equivalente a una conjunción finita de sus instancias, [1] En 1953, Ernst Specker demostró que el axioma de elección es falso en la NF (sin urelementos ). [38] En 1969, Jensen demostró que añadir urelementos a la NF produce una teoría (NFU) que es demostrablemente consistente. [35] Ese mismo año, Grishin demostró que la NF 3 es consistente. [46] Specker demostró además que la NF es equiconsistente con la TST más el esquema axiomático de "ambigüedad típica". [ cita requerida ] La NF también es equiconsistente con la TST aumentada con un "automorfismo de cambio de tipo", una operación (externa a la teoría) que aumenta el tipo en uno, mapeando cada tipo sobre el siguiente tipo superior y preserva las relaciones de igualdad y pertenencia. [ cita requerida ]
En 1983, Marcel Crabbé demostró la coherencia de un sistema que llamó NFI, cuyos axiomas son la extensionalidad sin restricciones y aquellas instancias de comprensión en las que a ninguna variable se le asigna un tipo superior al del conjunto que se afirma que existe. Esta es una restricción de predicatividad , aunque la NFI no es una teoría predicativa: admite suficiente impredicatividad para definir el conjunto de números naturales (definido como la intersección de todos los conjuntos inductivos; nótese que los conjuntos inductivos cuantificados sobre son del mismo tipo que el conjunto de números naturales que se está definiendo). Crabbé también discutió una subteoría de la NFI, en la que solo se permite que los parámetros ( variables libres ) tengan el tipo del conjunto que se afirma que existe por una instancia de comprensión. Llamó al resultado "NF predicativa" (NFP); por supuesto, es dudoso que cualquier teoría con un universo auto-miembro sea verdaderamente predicativa. [¿ según quién?] ] Holmes ha demostrado [ fecha faltante ] que el PFN tiene la misma fuerza de consistencia que la teoría predicativa de tipos de Principia Mathematica sin el axioma de reducibilidad .
La base de datos Metamath implementó la axiomatización finita de Hailperin para New Foundations. [47] Desde 2015, varias pruebas candidatas de Randall Holmes de la consistencia de NF relativa a ZF estaban disponibles tanto en arXiv como en la página de inicio del lógico. Sus pruebas se basaban en demostrar la equiconsistencia de una variante "extraña" de TST, "teoría de tipos enredados con λ-tipos" (TTT λ ), con NF, y luego demostrar que TTT λ es consistente en relación con ZF con átomos pero sin elección (ZFA) mediante la construcción de un modelo de clase de ZFA que incluye "redes enredadas de cardinales" en ZF con átomos y elección (ZFA+C). Estas pruebas eran "difíciles de leer, increíblemente complejas e implicaban el tipo de contabilidad elaborada que facilita la introducción de errores". En 2024, Sky Wilshaw formalizó una versión de la prueba de Holmes utilizando el asistente de prueba Lean , resolviendo finalmente la cuestión de la consistencia de NF. [48] Timothy Chow caracterizó el trabajo de Wilshaw como una demostración de que la renuencia de los revisores pares a involucrarse con una prueba difícil de entender se puede abordar con la ayuda de asistentes de prueba. [49]