En $NF$ no estratificado fórmulas se pueden utilizar en las pruebas. Ellos no están prohibidos, como en la de Russell Teoría de Tipos. Sin embargo, no podemos utilizar no estratificado fórmulas para demostrar la existencia de conjuntos. En general, si recuerdo que probar que los conjuntos de existir por un argumento diferente, en lugar de tratar de apelar a estratificada de la comprensión de lo que sería sin esperanza si la fórmula no es estratificado.
Si estoy en lo correcto, en tu ejemplo, usted tiene $A \cup B = \{x : x \in y \vee y\in x\}$. Usted en lugar de escribir $A \cup B = \{x : x \in z \vee y\in x\}$$A=\{x : y\in x\}$$B=\{x: x\in z\}$, de modo que usted puede asignar de 1 a $y$, 2 $x$ y 3 $z$, esto es estratificado por lo que ahora la unión existe por estratificada de la comprensión. Pero esto no excluye el caso de $z=y$, por lo que tenemos el conjunto de $A \cup B = \{x : x \in y \vee y\in x\}$ aunque $x \in y \vee y\in x$ es no estratificado.
Un ejemplo similar es el hecho en el libro Fundamentos Lógicos de la Matemática y Computacional de la Complejidad: Una Introducción Suave (Springer Monografías en Matemáticas), página 233.
