Guía 9 · las atómicas, los niveles, el menú, el mordisqueo y la lectura única
Una fórmula de tipo es una palabra, igual que un término: se arma por niveles a partir de las atómicas, y se lee de una sola manera. Lo que la separa de los términos es una asimetría. Una fórmula nunca es el principio de otra, pero sí puede ser su final: termina en . Y cuando eso pasa, lo que sobra adelante es siempre una cadena de negaciones y cuantificadores. De ese hecho salen la lectura única y todas las pruebas que comparan dos fórmulas por atrás.
La Guía 9, en la página 9, las define así. Dado un tipo , las fórmulas atómicas de tipo son las palabras de alguna de estas dos formas:
Son palabras armadas por concatenación, no expresiones que denotan algo: es el resultado de concatenar las palabras
Por eso la longitud sale de sumar las piezas, como la de un término:
El 3 de la primera son los dos paréntesis y el ; en la segunda, cuenta las comas y el 2 los paréntesis. Con el tipo de la guía , con , y : tiene longitud ; , , porque la variable son dos símbolos; y , .
Tres detalles de la definición que deciden ejercicios. La igualdad va siempre entre paréntesis: es atómica y no es nada. No hay relaciones de aridad 0, así que toda atómica lleva paréntesis. Y es un símbolo del alfabeto, no un nombre del tipo: está en todas las fórmulas de todos los tipos, y ningún nombre de constante, función o relación lo puede usar.
Con las atómicas como piso, la guía arma los conjuntos por recursión en :
y es más tres clases de palabras nuevas, todas hechas con fórmulas de :
Las fórmulas de tipo son los elementos de . Otra vez, todo es concatenación: es la concatenación de las cinco palabras , y la de las tres palabras .
Hay que mirar dónde van los paréntesis. Sólo los nexos binarios los agregan, uno de cada lado. y se pegan adelante y no agregan nada atrás: es una fórmula y no. Ese detalle es toda la asimetría de la sección 06.
Como , una fórmula está en todos los niveles a partir de uno; el nivel de una fórmula es el mínimo. Los ejemplos de la guía (página 10), leídos de afuera hacia adentro: los cinco de (E1) con el tipo de arriba, y los seis de (E2) con .
| Fórmula | De afuera | Nivel |
|---|---|---|
| 2 | ||
| 1 | ||
| 2 | ||
| 4 | ||
| 4 | ||
| atómica | 0 | |
| atómica | 0 | |
| 1 | ||
| 2 | ||
| 1 | ||
| 5 |
El nivel no mide el largo. La cuarta fórmula tiene 37 símbolos y la quinta 61, y las dos son de nivel 4. Lo que cuenta es la cadena más larga de construcciones: en la quinta, es atómica, pero del otro lado del hay tres cuantificadores apilados sobre una igualdad, y . Y la conjunción de (E2) tiene 27 símbolos y es de nivel 1: sus dos miembros son atómicos.
La guía cierra con un contraejemplo: no es una fórmula de ese tipo, aunque . Los nombres de relación van adelante, como los de función: la fórmula es . Leída de afuera, empieza con , así que sólo podría ser o ; y adentro del paréntesis de afuera no hay ningún ni ningún nexo. La guía avisa que probarlo «no es trivial de la definición»: cómo se escribe esa prueba está en Probar que una palabra no es término ni fórmula.
Las fórmulas de tipo son el modelo matemático de las fórmulas elementales puras de tipo , las que no usan nombres de elementos fijos. La diferencia es de estatuto: «fórmula elemental» era una idea que se reconocía al verla; es un conjunto de palabras definido con precisión, del que se pueden probar cosas.
Lema 5 (Menú para fórmulas). Sea . Si , entonces se da alguna de las siguientes:
Parece la definición repetida, y no lo es. La definición dice que es unión las palabras nuevas; una fórmula de puede venir de , y ésa a su vez de , y así hasta abajo. El lema dice que no importa: igual tiene una de las cinco formas, con piezas un nivel más abajo.
Se prueba con la Regla de Inducción desde 0, tomando como el enunciado mismo. sale directo de la definición de . Para el paso, si vale y , hay dos casos. Si , da una de las cinco formas con piezas en , que es la conclusión de . Si no, es , o con piezas en , y eso ya es la conclusión. El molde de esta inducción, y por qué el va cuantificado adentro de , está en Inducción en la construcción.
Lo que el lema no dice es que la forma sea una sola, ni que las piezas sean únicas: «alguna de las siguientes». Eso es el Teorema 7, y para llegar hace falta el mordisqueo.
Dos palabras se solapan cuando el final de una es el principio de la otra. La guía, en la página 12, acepta sin prueba lo que pasa cuando las dos son fórmulas:
Proposición 6 (Mordisqueo de fórmulas). Si y son palabras tales que , e , entonces y
En particular, ningún tramo inicial propio de una fórmula es una fórmula, y ningún tramo final propio de una fórmula atómica es una fórmula.
Leída despacio: si el final de se superpone con el principio de , la superposición se traga a entera (, así que es tramo final de ), y lo que queda de adelante es una tira de bloques, cada uno un o un cuantificador con su variable. Por ejemplo, con y , el corte es , , : dos bloques, y . Con en cambio, : un bloque.
Las dos consecuencias «en particular» salen de elegir bien las tres palabras. Si fuera tramo inicial propio de , sería e , y la conclusión diría que . Si fuera tramo final propio de una atómica , el no vacío tendría que empezar con , o , y una atómica empieza con o con un nombre de relación.
La guía no la prueba. El apunte sí, borrando de las palabras todo lo que no es paréntesis. Lo que queda de una fórmula es una palabra balanceada, como lo que queda de y de ; y como termina en , lo que queda de no es vacío. El balanceo obliga a que se quede con todos los paréntesis de y de : y no tienen ninguno. Como termina en , eso fuerza . Y una palabra sin paréntesis que puesta delante de una fórmula da otra fórmula sólo puede ser una cadena de y , que se ve por inducción en el nivel de .
La mitad fácil es el Ejercicio 16:
Pruebe que si , entonces no puede ser tramo inicial propio de (Hint: elija bien y y aplique la proposición anterior).
Prueba. Supongamos que es tramo inicial propio de : con . Tomemos , , . Entonces , e , porque ninguna fórmula es vacía. Por la Proposición 6, , o sea . Absurdo. ∎
Con esto se cancela por adelante, que es el Ejercicio 18: si con las cuatro fórmulas, y son tramos iniciales de la misma palabra, así que uno es tramo inicial del otro; por el Ejercicio 16 ninguno lo es propio, y entonces . Sacando ese tramo de las dos escrituras, . Es la misma cancelación que con términos, y la que va a usar el Teorema 7 en su forma (3).
Con los términos, el mordisqueo es simétrico. El Lema 2 de la guía da , salvo el caso de dos constantes que se mordisquean: un término no es tramo inicial ni tramo final propio de otro. La Proposición 6 da sólo , y puede no ser vacía. es tramo final propio de , y de , y de . La razón está en la sección 02: y construyen agregando sólo adelante, así que la fórmula de la que se partió queda intacta al final de la nueva. Los nexos binarios, en cambio, la encierran entre paréntesis.
Lo que la Proposición 6 agrega es que ésa es la única manera. Si una fórmula es tramo final propio de otra, lo que sobra adelante es exactamente una cadena de esos prefijos. Medido sobre 3370 fórmulas distintas del tipo , armadas desde las atómicas , , , , y con dos capas de , , , y , y hasta 26 símbolos: de los 11 356 900 pares ordenados, en 3712 el final de la primera coincide con el principio de la segunda, con . Así se reparten:
| Lo que pasa | Casos |
|---|---|
| la misma fórmula dos veces () | 3370 |
| tramo final propio, sobra un bloque: , o | 288 |
| tramo final propio, sobran dos bloques: , , … | 54 |
| tramo inicial propio (, ) | 0 |
| solapamiento parcial ( y ) | 0 |
Los 288 son 96 de cada bloque, y los 54 son 6 de cada uno de los nueve pares de bloques: con dos capas no hay más. En los 342 tramos finales propios lo que sobra adelante se parte en negaciones y cuantificadores, y ninguno de los 3712 contradice la Proposición 6. La primera fila es el control: cualquier fórmula se solapa consigo misma, y si no apareciera, la cuenta estaría mal.
Esa forma de lo que sobra es lo que se usa para comparar por atrás. El Ejercicio 19 pide probar que si , entonces . Como empieza con y tiene un , el Teorema 7 la da de la forma (3): con , y sacando los paréntesis de afuera, . Lo que se sabe fórmula es , así que se compara por el final: y son tramos finales de la misma palabra, y uno es tramo final del otro. Acá el Ejercicio 16 no sirve, porque por atrás una fórmula sí puede ser tramo final propio de otra. Pero si lo fuera, lo que sobra adelante sería una cadena de y , y una cadena así termina en o en el numeral negrita de una variable. Y su último símbolo es el que va justo antes del tramo final más corto en la otra escritura: el de si lo que sobra está adelante de , el de si está adelante de . Los dos son nexos. Así que no sobra nada, , y cancelando, y . La prueba entera, con sus dos casos, está en Una fórmula puede ser el final de otra, nunca el principio.
La hipótesis no es decorativa. El Ejercicio 13 pregunta si de sale que , y es falso: en , que es de nivel 2, tomar el primer como separador da , con dos paréntesis que abren y uno que cierra, que no es fórmula. Es el corte equivocado de Un corte equivocado rompe las dos piezas, y está resuelto en Contar paréntesis no alcanza.
Teorema 7 (Lectura única de fórmulas). Dada se da una y sólo una de las siguientes:
Más aún, si , cuando se da (3) las fórmulas y están en , y cuando se da (4) o (5) la fórmula está en .
Que se dé alguna es el Lema 5 (y, para las atómicas, la definición de ). Lo nuevo son el «sólo una» y los «únicos», y la guía deja completarlos en el Ejercicio 17.
Las formas se excluyen por el primer símbolo:
| Forma | Primer símbolo |
|---|---|
| (1) | |
| (2) | el primer símbolo de |
| (3) | |
| (4) | |
| (5) | o |
Ningún nombre del tipo usa , , ni , así que (2), (4) y (5) se separan entre sí y de las otras dos. Sólo el deja dos formas abiertas, y las separa un nexo: en no ocurre ninguno, porque los términos no los tienen, y en ocurre . Cómo este cuadro se vuelve un procedimiento que decide si una palabra es fórmula está en El primer símbolo ya dice qué forma tiene.
Las piezas son únicas, forma por forma:
Los niveles. Si es de la forma (3), el Lema 5 la escribe como alguna de (a) a (e) con piezas en ; como las formas se excluyen, tiene que ser la (c), con ; y por la unicidad en (3), y . Las formas (4) y (5) van igual, con (d) y (e).
Lo que habilita el teorema es definir funciones sobre por recursión en la forma: dar el valor en las atómicas y decir cómo se calcula en , y a partir del valor en las piezas. Sin la unicidad, una misma fórmula podría recibir dos valores, uno por cada manera de leerla. Así se definen la ocurrencia libre y , en Variables libres, y más adelante la verdad de una fórmula en una estructura.