Hola, argentinator. Gracias por tus comentarios.
Pienso que para tener el derecho de usar siglas en castellano, necesitamos tener una teoría desarrollada por un matemático hispanoparlante.
Y luego, claro, que esas siglas o nomenclatura se usen en todo el planeta uniformemente.
En realidad la falta de uniformidad es algo que me pone los pelos de punta, porque si hay un lugar donde debe haber acuerdo y falta de ambigüedad es en la matemática.
P.D.: Obviamente que este asunto es el menos importante de todos los que se puedan discutir.
Ciertamente, es lo menos importante. Mi opinión es que, igual que decimos "conjunto" y no "set" y decimos "átomo" y no "urelement" podemos decir NFA y no NFU. No veo por qué toda palabra es traducible pero las sílabas no pueden serlo. NFA no es sino el nombre de una teoría, y no nombras en alemán la teoría de la relatividad porque Einstein fuera alemán.
Axioma de los átomos:

En palabras: Si un objeto tiene elementos, entonces es un conjunto o, equivalentemente, los átomos son objetos sin elementos.
Tengo dudas sobre cómo está enunciado esto.
Yo diria que: "un objeto es un conjunto si EXISTE otro objeto que pertenece a él".
Así, escribiría:

.
Las dos fórmulas son lógicamente equivalentes. Una implica la otra y viceversa. No sé si cuestionas esto o sólo dices que psicológicamente es más clara la forma que propones.
Por contrarrecíproco sale que un no-conjunto (o átomo) no tiene elementos.
Cierto. Ése es el contenido del axioma de los átomos: que no hay relaciones de pertenencia entre ellos.
¿Y el

? ¿Conjunto o átomo?
Es un conjunto. No creo que haga falta aclarar mucho porque tú mismo dices más abajo que ya lo tienes claro. El axioma de los átomos dice que los átomos no tienen elementos, pero no que todo objeto que no tenga elementos sea un átomo. Por el contrario, el axioma de formación de conjuntos implica la existencia de un conjunto sin elementos y el axioma de extensionalidad (que sólo afecta a conjuntos) implica que el conjunto vacío es el único conjunto sin elementos.
A decir verdad, no vamos a tomar el axioma de los átomos como axioma de NFA por una razón muy simple: aunque lo hiciéramos, jamás tendríamos ocasión de usarlo.
Entonces no entiendo dónde se produce la distinción de Jensen entre una teoría que sí tiene átomos.
El uso del operador "cto" en las fórmulas y axiomas debiera ser suficiente, pero deja la puerta abierta a una teoría muy general, que no se sabe si tiene o no tiene algún átomo.
Creo que aquí te confundes: el axioma de los átomos no dice nada sobre que existan o no existan átomos. Sólo dice que, en caso de que haya átomos, no se dan relaciones de pertenencia entre ellos.
El axioma que afirma que no existen átomos es el que he llamado NA y ese sí que es crucial. Aún no he llegado ahí, pero veremos que el axioma de elección implica que existen átomos, luego, si queremos usarlo, no podemos permitirlos el lujo de suponer que no existen.
Quizá la confusión se debe a que implícitamente estás identificando "átomo" con objeto sin elementos (distinto del conjunto vacío). El axioma de los átomos justifica esa identificación, si es que quieres hacerla, pero no es necesario. Oficialmente un "átomo" es simplemente un objeto que no es un conjunto, por lo que el axioma de extensionalidad no dice nada sobre sus posibles elementos y dichos "posibles elementos" son irrelevantes en la teoría, hasta el punto de que puedes suponer sin cambiar nada esencial que los átomos no tienen elementos (y es lo más natural, aunque en la práctica no te aporta nada relevante).
Más claramente: ¿puede ocurrir que

y

sean dos átomos y se cumpla

. Pues, sin el axioma de los átomos puede ocurrir, pero no significa nada, porque, como el axioma de extensionalidad no afecta a los átomos, no puedes considerar a éstos como conjuntos. Aunque sucediera que

es el único objeto que pertenece al objeto

, eso no haría a

igual al conjunto

. Digamos que

sería el autétntico conjunto que tiene a

por único elemento y el átomo

sería un objeto que anecdoticamente contiene a

.
Otra forma de verlo: imagina que tienes un modelo de NFA (tú llámala NFU si quieres, que me parece muy bien) en el que se cumple el axioma de los átomos, es decir, los átomos no tienen elementos. Ahora imagina que modificas el modelo modificando la relación de pertenencia de modo que un determinado átomo pase a ser elemento de otro átomo. ¿Qué sucede entonces? Pues nada, que sigues teniendo un modelo de NFA en el que ya no se cumple el axioma de los átomos, pero los demás axiomas se siguen cumpliendo, porque ningún axioma de NFA afirma nada sobre posibls elementos de átomos.
En palabras: Dos pares ordenados son iguales si y sólo si tienen la misma primera componente y la misma segunda componente.
De este modo, por el mero hecho de introducir el nuevo signo, estamos diciendo que, para cada par de objetos

e

, existe un tercer objeto (no especificamos si es un átomo o un conjunto)
Tomo nota de este hecho de que los pares ordenados no se sabe si son conjuntos o no.
Más adelante demostraremos que muchos pares ordenados son necesariamente átomos (aunque es consistente exigir que un par ordenado de conjuntos sea un conjunto).
También se pone en evidencia que siempre se necesita en matemática usar pares o n-uplas ordenadas, aún en las fases más elementales de cualquier teoría, pues se necesitan relaciones y funciones.
Eso es indudable.
Por consiguiente, la paradoja de Russell no puede demostrarse en NFA, sus axiomas no afirman que exista el conjunto

, ya que la fórmula que (supuestamente) lo define no está estratificada.
Es interesante notar que, mientras en ZFC se prohíben
desde los axiomas conjuntos que den lugar a paradojas,
en NFU (o sea NFA, o sea NFU, o sea...

) en cambio la prohibición se hace directamente
desde el lenguaje.
No sé si a alguien se le había ocurrido antes esto de "meterse con el lenguaje".
Bueno, NFA es el último paso en una cadena de simplificaciones de la teoría de los Principia Mathematica.
A simple vista parece también que la
estratificación impide conjuntos que cumplan algo como X = {X}, o sea, se impiden aquellos casos patológicos que en ZFC se suprimen por medio del
axioma de regularidad.
¿Estoy acertado en esto? Pues a mí me da que si X tiene cierto tipo

, necesariamente {X} tiene un tipo mayor

, pero entonces por el primer axioma y por ser X = {X}, se obtiene que X tiene tipo

, pero X no puede tener asociados dos tipos distintos

.
Aquí creo que empiezas a mostrar dos errores que a medida que avanza el mensaje se van agravando:
1) En la teoría original de Russell y en algunas de sus simplificaciones, cada objeto tiene un tipo asignado, pero en NFA los tipos sólo se asignan a los términos del lenguaje, es decir, a los nombres de los objetos, lo cual permite que un mismo objeto aparezca con tipos distintos si se le nombra con nombres distintos.
El caso más trivial es el siguiente: Tú puedes nombrar el conjunto vacío con el término

, paro también con el término

, donde

e

son variables distintas, y nada te impide estratificar una fórmula asignando tipos distintos a las variables

e

, con lo que puedes hacer que el conjunto vacío aparezca en ellas con tipos distintos, correspondientes a nombres distintos.
Luego tienes el caso de los parámetros. En uno de los mensajes pongo un ejemplo con la unión. El axioma de formación de conjuntos te asegura, en particular que

,
porque esta fórmula está estratificada. Una vez cuentas con esta fórmula, nada te impide aplicarla a un conjunto

cualquiera y al conjunto

, con lo que obtienes la existencia del conjunto

, sin que importe que este término no esté estratificado.
2) Nunca debes olvidar que el axioma de formación de conjuntos es únicamente una
condición suficiente para que exista un conjunto, pero no necesaria.
Tienes razón en que el axioma de formación de conjuntos no te permite asegurar que exista un conjunto tal que

, pero tampoco te dice que no exista. Ahora mismo no sabría decirte si es consistente con NFA que exista un conjunto así. Ya pensaré en ello.
Otra duda técnica: ¿queda claro de entrada este hecho de que un cierto objeto
no tiene permitido tener asociados dos tipos distintos en una misma fórmula?
Ojo, un objeto no, una variable. Y sólo en una fórmula estratificada, es decir, una fórmula a la que pretendas aplicar el axioma de formación de conjuntos. Por lo demás, puedes demostrar fórmulas no estratificadas, como

Esto es un teorema (no estratificado) de NFA. Si no queda claro con las explicaciones que he dado antes dilo e insisto en ello. (Lo mismo vale para cualquier otra cosa que haya dicho o diga luego, claro.)
Otra cosa que llama la atención enseguida es que
los pares ordenados tienen el mismo tipo que sus componentes.
Eso es algo inesperado para mí, porque uno está acostumbrado a poner en ZFC los pares ordenados como conjuntos que contienen de alguna forma algo enrevesada a sus componentes (

por ejemplo). El objeto

tiene tipo 2 veces mayor que el de

.
Explico la situación en el mensaje #13. No sé si lo has visto. Si no lo has visto será más fácil que lo mires antes de que yo repita lo dicho allí, si lo has visto y no queda claro, dilo y lo hablamos.
¿Implica necesariamente esto que los pares ordenados en NFU no son conjuntos?
En NF se pueden definir pares ordenados nivelados que son conjuntos, pero con una definición bastante más complicada que la usual que indicas. En NFU dicha definición vale para definir pares ordenados nivelados de conjuntos cuyos elementos sean todos conjuntos, pero para definir pares ordenados nivelados de objetos cualesquiera resulta que muchos de ellos tienen que ser necesariamente átomos. Eso lo demostraré un poco más adelante.
En cuanto a los ordinales de Von Newmann ya lo hemos comentado al principio, que no andan muy bien, pues no ellos necesitarían fórmulas no estratificadas como

.
Pero eso no impide que puedan definirse. Se pueden definir exactamente igual que en ZFC (una definición rápida sería definirlos como conjuntos transitivos bien ordenados por la inclusión, lo cual no requiere el axioma de formación de conjuntos, y nada te impide demostrar que

es un ordinal de von Neumann, y que

también lo es, y

, etc. pero poco más puedes probar. En cuanto quieres definir conjuntos de ordinales, te encuentras con que no puedes aplicar el axioma de formación de conjuntos), aunque no puedes demostrar que exista el ordinal

(como en ZFC sin el axioma de infinitud).
La verdad es que en ZFC uno "echa de menos" el enfoque de los cardinales a través de "clases de equivalencia".
Je, je. Eso está entre las virtudes de NFA.
En NGB o en MK uno puede definir los cardinales como clases de equivalencia, pero no los puede usar, porque no puede formar "conjuntos cuyos elementos son números cardinales".
Exacto.
Más aún, Carlos ha respondido en parte lo siguiente:
El concepto de ordinal de von Neumann se puede definir en toda teoría de conjuntos entre cuyos teoremas se encuentren el axioma de extensionalidad, la existencia de la unión de dos conjuntos, del complemento de dos conjuntos, del par desordenado de dos conjuntos y del conjunto vacío. No hace falta nada más, en particular no hace falta ningún axioma de formación de conjuntos o subconjuntos a partir de fórmulas.
Todos estos resultados son teoremas de NFA, luego en NFA puedes definir el concepto de ordinal (de von Neumann) e incluso el de número natural (de von Neumann, de modo que , etc.)
Ahora bien, las fórmulas "x es un ordinal" o "x es un número natural" (en este sentido de von Neumann) no están estratificadas y, por ello dan muy poco juego. En NFA no es posible demostrar que exista el conjunto de los números naturales en este sentido (pero sí que se pueden definir de otro modo, estratificado, y todo va bien).
Esta respuesta contiene un hecho interesante.
Es sabido que en el tema de la incompletitud de Godel, la incompletitud surge al pretender utilizar una fórmula que diga algo como "x es un número natural".
Esto no lo entiendo. En toda teoría de conjuntos tienes una fórmula que dice "x es un número natural", a saber, la definición de "número natural".
Según lo dicho por Carlos, esta frase no existe para ordinales de Von Neumann en NFU.
No te sigo. En el párrafo que citas digo expresamente que en NFA puedes definir la fórmula "x es un número natural (en el sentido de von Neumann)", pero que la fórmula no es estratificada y eso hace que se pueda hacer poca cosa con los números naturales de von Neumann. Ni siquiera puedes demostrar que para todo número natural n (de los definidos en NFA como clases de equivalencia) existe un número natural de von Neumann

tal que

.
Me pregunto si hay alguna relación entre estos temas de la estratificación y la incompletitud de Godel.
Como ya digo, no he entendido lo que has dicho sobre la incompletitud y los números naturales.
Mi olfato dice que la incompletitud de Godel sigue firme en NFU, pero bueno, no sé.
Por supuesto. Los teoremas de incompletitud se aplican a toda teoría recursiva (es decir, en los que esté claro qué es un axioma y qué no lo es, como es el caso de NFA) en la que se pueda definir de algún modo el concepto de "número natural" con el único requisito de que se puedan demostrar los axiomas de Peano, y en NFA se pueden definir los números naturales (no como en ZFC, sino como clases de equivalencia) y demostrar los axiomas de Peano. Esto basta para asegurar que los teoremas de incompletitud son aplicables a NFA.
En realidad los números naturales y los infinitos siempre traen incomodidades.
No sé si te has fijado en que en NFA se construyen los números naturales sin necesidad de un axioma de infinitud. ¿A que es curioso?
Son lo más básico de la matemática, y sin embargo nunca se encuentra una teoría que sea del todo "cómoda" o que exprese o refleje todo lo que hace falta o se desea.
Como yo lo veo, esto es indicio de un problema más profundo, y es que nadie entiende qué son los números naturales ni mucho menos los transfinitos,
por lo cual no puedo admitir que se los utilice despreocupadamente al construir una teoría axiomática.
Bueno, si entramos otra vez en eso no saldremos nunca.

Creo que no puedo decirte nada al respecto que no te haya dicho ya.
Este asunto de la estratificación es una idea interesante, pero a mí lo que no me gusta es el hecho de asignarle un número natural o entero a una expresión.
Estaba esperando esto desde el primer día. Mucho has tardado en decirlo.

Podría admitirla sin problemas, en cambio, si la cantidad de tipos aceptadas fuera finita, y no todo el rango de los enteros.
Lo de admitir tipos enteros es sólo por comodidad, porque si a una fórmula estratificada le sumas un mismo número natural a todos los tipos, obtienes una nueva estratificación, por lo que no pierdes generalidad si supones que los tipos son naturales. Por otra parte, para estratificar una fórmula concreta sólo necesitas una cantidad finita de tipos, que podrías incluso acotar a priori a partir de la estructura de la fórmula. Te digo esto porque es importante para ti. Para mí no tiene la importancia que tú le das.
Según ví en Wikipedia, NF es equivalente a

, en que se admiten 4 grados de estratificación como máximo. (Si es que he entendido bien el asunto

).
¿Se puede convertir NFU en algo como un

, digamos?
Pues no sé si cuatro concretamente, pero sí sé que NFA es finitamente axiomatizable, es decir, que puedes sustituir los infinitos casos particulares del esquema de formación de conjuntos por unos pocos casos particulares concretos (te los podría enumerar, si quieres, pero ahora mismo no los tengo a mano). De ese modo, puedes eliminar por completo el concepto de fórmula estratificada de los axiomas de NFA. Basta con que digas: estas fórmulas concretas (casos particulares del esquema de formación de conjuntos) son axiomas, y ya está. Luego puedes demostrar como teorema el axioma de formación de conjuntos para cualquier fórmula estratificada (sin límite para el número de tipos admisibles). Esto es más fuerte que lo que tú pedías. No sé si estarás de acuerdo y si te resolverá tu objeción de principios.
En cuanto a lo que pregunté arriba sobre el conjunto vacío, creo que está muy bien explicado acá:
Alguien podría pensar que podríamos haber incorporado el axioma de los átomos a la teoría a la vez que eliminábamos el signo primitivo cto definiendo un átomo como un objeto sin elementos y un conjunto como un objeto con elementos. Eso no es conveniente porque nos interesa que la teoría tenga un conjunto vacío, es decir, un objeto que no tiene elementos y, a pesar de ello, no es un átomo, sino un conjunto. El axioma de extensionalidad implica que el conjunto vacío es el único conjunto sin elementos, pues dos conjuntos vacíos serían dos conjuntos con los mismos elementos (ninguno) y no puede haber dos conjuntos distintos con los mismos elementos. En cambio, el axioma de extensionalidad no afecta a los átomos, por lo que nada impide que haya muchos átomos distintos y que ninguno tenga elementos.
Vale
Lo siguiente no lo tengo claro:
Cabe destacar algunas relaciones obvias que pueden "chirriar" a una mente clásica:

Yo no tengo una "mente clásica" y sin embargo me chirría igual, porque creí que la fórmula

no está estratificada. Entonces, ¿cómo es posible escribir eso?
Por "clasica" quería decir simplemente "que piensa en términos de ZFC". Aquí volvemos a lo que te señalaba antes: el axioma de formación de conjuntos prohibe usar fórmulas no estratificadas para definir conjuntos (y no en el sentido de asegurar que las fórmulas no estratificadas no definen conjuntos, sino únicamente en el de no asegurar que lo hacen), pero eso no significa que no puedas demostrar teoremas no estratificados.
Pese a todo, estos ejemplos no serían realmente un ejemplo. La fórmula

Sí que está estratificada, y es equivalente a

. Aquí es esencial lo que te decía de que los tipos no se asignan a objetos, sino a nombres de objetos, y podemos jugar con que un mismo objeto admite nombres distintos.
No obstante, ya te he puesto antes un ejemplo de teorema genuinamente no estratificado, como

.
Insisto: en NFU no están prohibidos los teoremas no estratificados, sino únicamente no tenemos garantías de que las fórmulas no estratificadas definan conjuntos, lo cual no significa que no los definan. Por ejemplo, la fórmula

sí que define un conjunto, aunque no está estratificada. El conjunto

existe, lo cual no se deduce de aplicar directamente el axioma de formación de conjuntos (sería incorrecto), pero sí de aplicarlo a la fórmula estratificada

y luego particularizar el axioma es decir, la fórmula

al caso

.
Si esto te parece "trampa" insiste, porque es fundamental que quede claro.
Lo mismo en esto:
(...) el tipo de

y

es siempre una unidad inferior al tipo de

(...)
en contraste con esto otro:
¿Entonces el vacío y el universo no tienen tipo? ¿Cómo se entiende esto?
Ningún objeto tiene tipo. Sólo los nombres de objetos tienen tipo. Los casos que citas se pueden ver como fórmulas estratificadas con el truco que ya te he explicado:

,
pero, aunque no fuera así, insisto en que hay muchos teoremas de NFA que no están estratificados. No pasa nada por ello. La única restricción concerniente a la estratificación es que no es lítico tomar como axioma de NFA un caso particular del axioma de formación de conjuntos cuya fórmula no esté estratificada, y hemos visto un ejemplo de un caso particular de dicho axioma con una fórmula no estratificada que, a pesar de no ser un axioma de NFA, resulta ser un teorema de NFA. Ojo con eso.
He llegado hasta el tema de definir funciones en NFU (y de ojeada lo de los ordinales y cardinales).
En cuanto a las funciones, me parece natural preguntar si es posible definir funciones de un conjunto

en

, pues dominio e imagen tienen tipos distintos en la estratificación.
Es muy natural en álgebra definir un isomorfismo que haga algo como esto:

.
¿Se puede hacer esto en NFU? ¿Es muy complicado?
Por ejemplo, tú puedes probar que

,
que es una fórmula estratificada, y luego puedes particularizar este teorema al caso

y tienes probada la existencia de una aplicación

dada por

.
Ahora bien, puede probarse (está probado más allá del mensaje hasta el que has llegado) que no existe ninguna aplicación

tal que

.
Aún no hemos llegado a ello, pero veremos más adelante que los conjuntos

tales que existe una aplicación

dada por

se llaman estrictamente cantorianos, y es consistente añadir a NFA un axioma que asegure que los conjuntos "normales" como

son estrictamente cantorianos, mientras que los conjuntos "raros" como

no lo son.
¿Hay algo importante que no estoy entendiendo?
Sí, hay un par de cosas importantes que no estás entendiendo: 1) que los tipos se asignan a nombres y no a conjuntos y 2) que no hay ningún problema en demostrar en NFA fórmulas no estratificadas. La estratificación sólo es un requisito para tomar como axioma la existencia de un conjunto definido por una fórmula. Nada más.
He tratado de ser lo más claro posible, pero lo cierto es que todo esto está lleno de sutilezas. No dudes en preguntar todo lo que no veas claro (y lo mismo vale para cualquier otro lector). El único interés que tiene que publique esto así y no como un pdf para que cada cual lo entienda como pueda es la oportunidad de resolver todas las dudas conceptuales (o no conceptuales) que puedan surgir.