Finalmente estamos en condiciones de presentar la teoría NFA completa, con todos sus axiomas. Para evitar que quede esparcida en varios mensajes incluyo aquí todo lo anterior:
Definición: Llamaremos NFA a la teoría axiomática cuyo lenguaje formal consta de los signos lógicos más los signos \( \text{cto} \), \( \in \) y \( (\ ,\ ) \), y cuyos axiomas son los siguientes (en los que empleamos el convenio de que las mayúsculas representan conjuntos):
Extensionalidad: \( \forall XY(\forall u(u\in X\leftrightarrow u\in Y)\leftrightarrow X=Y) \)
Pares ordenados: \( \forall xyuv((x,y)=(u,v)\rightarrow x=u\land y=v) \)
Formación de conjuntos: Para cada
fórmula estratificada \( \phi(x,x_1,\ldots, x_n) \) del lenguaje de NFA, \( \forall x_1\cdots x_n\exists A\forall x(x\in A\leftrightarrow \phi(x,x_1,\ldots, x_n)) \).
Para que esto tenga sentido, sólo nos falta definir qué hemos de entender por "fórmula estratificada". La finalidad ya la hemos explicado: la estratificación es una propiedad que exigimos a las fórmulas para que definan conjuntos, de modo que así excluimos las fórmulas que dan lugar a contradicciones, como \( x\notin x \), pero permitimos muchas otras, incluso algunas que otras teorías de conjuntos prohiben.
Antes de entrar en la definición de fórmula estratificada, interpretamos el axioma de formación de conjuntos: Lo que afirma es que, para toda propiedad \( \phi(x,x_1,\ldots, x_n) \) que cumpla la propiedad técnica que tenemos pendiente definir, existe un conjunto \( A \) cuyos elementos son los objetos \( x \) (conjuntos o átomos) que cumplen la propiedad (las otras variables representan parámetros que pueden aparecer en la propiedad, como los conjuntos arbitrarios \( A \) y \( B \) cuando consideramos la propiedad \( x\in A\lor x\in B \) que define la unión de conjuntos.
El conjunto \( A \) es único por el mismo motivo explicado en el mensaje anterior, luego podemos nombrarlo con una descripción:
\( \{x\mid \phi(x,x_1,\ldots, x_n)\}\equiv A\mid \forall x(x\in A\leftrightarrow \phi(x,x_1,\ldots, x_n)) \)
En estos términos, el axioma de formación de conjuntos dice que podemos hablar del conjunto \( \{x\mid \phi(x,x_1,\ldots, x_n)\} \) siempre que la propiedad \( \phi \) que aparece en ella esté estratificada, pero en caso contrario nada nos asegura a priori que exista semejante conjunto.
En lugar de definir el concepto de fórmula estratificada definiremos algo ligeramente más general. Para ello debemos distinguir entre
fórmulas, que son cadenas de signos que constituyen una afirmación, y
términos, que son cadenas de signos que nombran objetos.
Por ejemplo, los axiomas de NFA son fórmulas, al igual que \( x\in Y \) o \( X\subset Y \), mientras que \( x \), \( (x,y) \), \( \{x\mid x=x\} \) son términos, pues son expresiones que nombran objetos.
Para referirnos indistintamente a términos o fórmulas usaremos la palabra
expresiones. Cada expresión puede contener varias subexpresiones. Por ejemplo, la expresión (fórmula en este caso) \( (x,y)\in A\lor A\subset B \) contiene las subfórmulas \( (x,y)\in A \) y \( A\subset B \), y la primera de ellas contiene los subtérminos \( (x,y) \) y \( A \), y el primer término contiene como subtérminos a \( x \) y a \( y \), etc.
Definición de expresión estratificada Una expresión del lenguaje de NFA está
estratificada si admite una estratificación, donde una
estratificación es cualquier criterio que asigne un número entero a cada subtérmino de la expresión dada, al que llamaremos su
tipo, de modo que se cumplan las propiedades siguientes:
1) Si un mismo término aparece repetido varias veces en la expresión, el tipo que se le asigne debe ser siempre el mismo.
2) En cada subfórmula \( t_1=t_2 \), los términos \( t_1 \) y \( t_2 \) deben tener el mismo tipo.
3) En cada subfórmula \( t_1\in t_2 \), el tipo del término \( t_1 \) debe ser exactamente una unidad menor que el del término \( t_2 \).
4) En cada subtérmino \( (t_1,t_2) \) los dos términos \( t_1 \) y \( t_2 \) deben tener el mismo tipo, que a su vez debe coincidir con el tipo de \( (t_1,t_2) \).
5) En cada subtérmino \( x\mid \phi(x,x_1,\ldots, x_n) \) su tipo debe ser el mismo que el tipo de la variable \( x \).
Como es fácil comprender, el concepto de estratificación es crucial en la teoría, así que dedicamos el resto del mensaje a familiarizarnos con él a través de ejemplos y algunas observaciones. A partir del próximo mensaje empezaremos ¡por fin! a trabajar con (o en) NFA.
El ejemplo crucial:
La fórmula \( x\notin x \) no está estratificada.Demostración:
Spoiler
Tenemos que \( x\notin x\equiv \lnot x\in x \). Para estratificar esta fórmula tendríamos que asignar un tipo a la variable \( x \), que tendría que ser el mismo en sus dos apariciones por la regla 1, pero tendría que ser distinto por la regla 3. Así pues, es imposible asignar tipos en las condiciones que exige la definición de estratificación.
Por consiguiente, la paradoja de Russell no puede demostrarse en NFA, sus axiomas no afirman que exista el conjunto \( \{x\mid x\notin x\} \), ya que la fórmula que (supuestamente) lo define no está estratificada.
Sólo con el propósito de practicar con el concepto de estratificación, vamos a ver que los axiomas de NFA están estratificados.
ExtensionalidadSpoiler
Indicaremos los tipos mediante subíndices:
\( \forall XY(\forall u(u_0\in X_1\leftrightarrow u_0\in Y_1)\leftrightarrow X_1=Y_1) \)
Tenemos una estratificación que respeta todas las reglas: la \( u \) tiene tipo 0 en todas sus apariciones, la \( X \) tiene tipo 1 en todas sus apariciones, al igual que la \( Y \), las igualdades igualan términos del mismo tipo, mientras que las pertenencias aumentan una unidad el tipo.
Notemos que el uso de mayúsculas oculta dos subfórmulas, a saber, \( \text{cto}\,X \) y \( \text{cto}\,Y \), pero no debemos preocuparnos por ello, porque la definición de estratificación no impone ninguna condición sobre el signo \( \text{cto} \), por lo que la fórmula \( \text{cto}\,X \) está estratificada y no importa si no la escribimos explícitamente al chequear la estratificación.
Spoiler
El axioma de los pares ordenados se estratifica asignando tipo cero a todas las variables:
\( \forall xyuv((x_0,y_0)_0=(u_0,v_0)_0\rightarrow x_0=u_0\land y_0=v_0) \)
Observemos que, como asignamos tipo \( 0 \) a \( x \) y a \( y \), la regla 4) exige que asignemos también tipo \( 0 \) al par \( (x,y) \). Similarmente, el par \( (u,v) \) tiene también tipo \( 0 \), por lo que la igualdad entre los dos pares cumple la condición de que sus dos términos (los dos pares) tengan el mismo tipo.
Spoiler
Supongamos que la fórmula \( \phi(x) \) (con posibles parámetros) admite una estratificación en la que la variable \( x \) tiene tipo \( n \). Entonces una estratificación del axioma correspondiente es
\( \exists A\forall x(x_n\in A_{n+1}\leftrightarrow \phi(x_n)) \).
En realidad, para que esta fórmula sea un axioma hay que pedir que la variable \( A \) sea una variable "nueva", es decir, una variable que no aparezca ya en la fórmula \( \phi \). En caso contrario, ni la estratificación que acabamos de construir tendría por qué ser correcta, ni el "axioma" tendría el sentido que pretende tener.
Un último ejemplo:
Una fórmula \( t_1\subset t_2 \) está estratificada si y sólo si los dos términos admiten una estratificación (conjunta, es decir, que los subtérminos de uno que también estén en el otro tengan el mismo tipo en ambos) en la que ambos tengan el mismo tipo.Spoiler
Por definición
\( t_1\subset t_2\equiv \text{cto}\,t_1\land \text{cto}\,t_2\land \forall u(u\in t_1\leftrightarrow u\in t_2) \)
Si \( t_1 \) y \( t_2 \) admiten estratificaciones, entonces las fórmulas \( \text{cto}\,t_1 \) y \( \text{cto}\,t_2 \) estarán estratificadas, porque el signo \( \text{cto} \) no impone ninguna restricción. Incluso podríamos haber omitido esta parte de la fórmula. Respecto a la parte final, si ambos términos admiten una estratificación conjunta que les asigne tipo \( n \), basta asignar tipo \( n-1 \) a la variable \( u \) y tenemos la fórmula completamente estratificada.
Recíprocamente, si la fórmula se puede estratificar, entonces \( t_1 \) y \( t_2 \) admiten una estratificación conjunta en la que ambos tienen tipo una unidad mayor que el asignado a la variable \( u \), luego ambos tienen el mismo tipo.
Algunas observaciones finales:
Como vemos, NFA tiene únicamente tres axiomas, si bien ya hemos advertido que el segundo es redundante (un poco más adelante explicaré la situación) y el tercero es en realidad un esquema de infinitos axiomas (pero se puede probar que a partir de un número finito de casos particulares se pueden demostrar todos los demás, es decir, que NFA es finitamente axiomatizable). Recordemos también que, por puro perfeccionismo, podríamos añadir consistentemente el axioma de los átomos (el que afirma que los átomos no tienen elementos).
Si hemos insistido en los detalles técnicos de cómo se escriben formalmente los enunciados de NFA es por la necesidad continua que tendremos de comprobar que cada propiedad que usemos para definir un conjunto sea estratificada. Salvo por esta cuestión, a partir de aquí podremos aligerar considerablemente las cuestiones de lógica y pasar a razonar en términos ligeramente más informales.
En cuanto a la noción de estratificación, es preciso que todo aquel que quiera seguir estas explicaciones se familiarice en la práctica con el concepto. En la práctica uno tiene que ser capaz de ver una fórmula y decidir si está o no está estratificada. Siempre es posible hacerlo mediante un proceso finito, pero costaría más explicar un algoritmo general que enfrentarse directamente a cada caso particular. Estratificar es más o menos como resolver un sudoku.
No es necesario que uno adquiera la práctica ya mismo, sino que basta con que estudie atentamente los muchos ejemplos que vamos a ver y que, en cuanto uno se crea capaz de estratificar por sí mismo, que se abstenga de mirar las "soluciones" hasta que considere que ya no merece la pena pararse a hacer cuentas porque las domine sobradamente.
Algunas observaciones generales:
Notemos que todo término de NFA es una variable, un par ordenado o una descripción, por lo que, a la hora de estratificar, sólo tenemos (relativa) libertad para asignar tipos a las variables de la expresión. Una vez cada variable tiene un tipo asignado, todos los demás términos tienen asignado un único tipo por las condiciones 4 y 5.
Si en una estratificación sumamos un mismo número entero a todas las asignaciones de tipos obtenemos otra estratificación igualmente correcta. Esto es porque los términos que tenían el mismo tipo seguirán teniéndolo (luego se seguirá cumpliendo la regla 1), las igualdades que igualaban términos del mismo tipo seguirán haciéndolo (regla 2), las pertenencias seguirán manteniendo una unidad de diferencia entre sus términos, etc.
En particular, a la hora de estratificar una expresión, siempre podemos empezar por asignar un tipo arbitrario a una variable arbitraria, y a partir de ahí ir calculando tipos "obligados" de otras variables por las relaciones que hay entre ellas en la expresión estudiada.
Otra consecuencia del hecho de que podemos elevar simultáneamente todos los tipos en la misma cantidad es que podríamos haber definido el concepto de estratificación admitiendo únicamente tipos naturales en lugar de enteros, puesto que si una estratificación llega a asignar, por ejemplo, hasta el tipo \( -4 \), basta sumar \( 4 \) a todos los tipos para tener otra en la que todos los tipos son naturales. No obstante, el admitir enteros flexibilizará ciertos razonamientos.
