La sentencia no cambió, el texto de la prueba no cambió una letra, y dejó de ser una prueba.
Una prueba elemental es un texto: una lista de renglones donde cada uno se justifica citando un axioma, o dando un paso de lógica que no depende de ninguno. Eso es lo que quedó de la Guía 6, y es una definición cómoda — se la puede revisar renglón por renglón sin entender de qué habla.
El Ejercicio 18 de la Guía 7 agarra esa comodidad y hace la pregunta que a nadie se le ocurre: una prueba, ¿de qué tipo es? Porque si citar es lo único que hace, entonces lo que decide si el texto vale es la lista de lo que hay disponible para citar. Y esa lista viene con el tipo.
El experimento se hace con una sentencia sola, que de acá en más llamamos :
Se lee sin esfuerzo: si el supremo de con es , entonces el ínfimo es . Las dos maneras de decir « está por debajo de » usando operaciones.
Mirale los símbolos, que es lo que importa acá: usa e , y nada más. No menciona . Por eso es una sentencia del lenguaje de los reticulados terna —que tiene e — y también del de los reticulados cuaterna, que tiene , y además . La misma palabra, escrita en dos lenguajes.
Y es verdadera en los dos lados: —. Esos tres reticulados de divisores son estructuras de los dos tipos, y la sentencia no se mueve.
Abajo hay dos pruebas de , las dos correctas, las dos escritas como pide la Guía 6. Una pasa por el orden y tarda seis pasos; la otra usa la absorción y tarda dos. Las dos arrancan suponiendo , que también es un renglón del texto. A la derecha está, para el tipo que elijas, la lista completa de los axiomas que podés citar — sacada del módulo, no escrita a mano.
Empezá como está: la prueba del orden, en cuaterna. No cae ningún renglón, y las cinco citas están en la lista, encendidas en azul. Eso es una prueba.
Ahora, sin tocar la prueba, cambiá el tipo a terna.
Se cayó entera, y por una razón más profunda que la esperable. Cinco de los seis pasos ni siquiera son fórmulas de una terna: mencionan , y en el lenguaje de una terna no existe. El único que sobrevive como fórmula es el último —una igualdad, sin a la vista— y ese cae por el otro motivo: cita A≤A, que no está entre los ocho axiomas de una terna.
Los dos motivos son el mismo motivo, y se ve en la lista de la derecha, que cambió por completo. Los ocho axiomas de una terna no mencionan ni una vez, porque no lo tienen. Los siete de una cuaterna lo mencionan todos. Las dos listas no comparten ni una fórmula: son disjuntas.
Con listas disjuntas, una prueba de cuaterna no puede citar ni un solo axioma de terna. No importa cuán buena sea la prueba, ni que la sentencia sea verdadera. Citar es lo único que una prueba hace, y todo lo que citaba dejó de existir.
Andá al revés, que es igual de brutal y mucho más corto: elegí la prueba de la absorción y ponete en cuaterna. Tres renglones, uno solo cita, y ese cae. Queda un texto donde el paso del medio no se justifica con nada.
Vale la pena anotar todo lo que no cambió mientras esto pasaba. La sentencia es la misma. Sigue siendo sentencia de los dos tipos. Sigue siendo verdadera en los mismos reticulados. Los renglones dicen exactamente las mismas palabras, en el mismo orden. Lo único que se movió fue la lista de la derecha — y con eso alcanzó.
Probá también poset, que enseña otra cosa. Ahí la lectura dice que dos de las cinco citas están permitidas: A≤R y A≤A son axiomas de poset, y la prueba del orden los cita tal cual. Y no sirve de nada, porque los renglones que mencionan o ni siquiera son fórmulas — en el lenguaje de un poset esos símbolos no existen. Ni se puede escribir. Antes de preguntar si una prueba vale hay que preguntar si lo que prueba se puede decir.
Y probá la simetría entera: la prueba de la absorción, en acotado y en complementado, sigue en pie. Un acotado tiene los ocho axiomas de terna y dos más; un complementado, esos diez y dos más. Agregar axiomas no rompe una prueba — la deja igual de válida, y con más cosas para citar la próxima vez. Cambiarlos, en cambio, la borra. Por eso «el tipo decide» no es un eslogan: hay una dirección en la que la prueba se hereda y una en la que no.
¿De dónde sale la lista de la derecha? De algo que veníamos usando sin nombrarlo, y que la Guía 8 nombra al fin. Un tipo es una cuaterna : un conjunto de símbolos de constante, uno de símbolos de función, uno de símbolos de relación, y una función que le da a cada símbolo su aridad — cuántos argumentos recibe.
Eso es todo. Y con eso alcanza para que las ocho estructuras del parcial entren como ocho filas de la misma tabla — incluida la última, las median algebras de la Guía 7, que traen un símbolo de aridad tres y son el único caso donde la aridad no es uno ni dos. Tocá una fila y mirá qué decide.
Ninguna de las cuatro cosas que el panel dice para cada fila es nueva. «Un subuniverso contiene las constantes y cierra bajo las operaciones» fue la nota del Ejercicio 7. «Un homomorfismo respeta las constantes y conmuta con las operaciones» fue la de las tres capas. «Una fórmula sólo puede usar los símbolos del tipo» fue toda la Guía 6. «Una prueba sólo puede citar los axiomas del tipo» es lo que acabás de ver caerse arriba.
Lo nuevo es que las cuatro se leen de la misma fila. Eso es lo que hace la Guía 8: no agrega materia, le pone nombre a lo que las guías venían haciendo caso por caso y lo convierte en un programa. Donde antes había una definición de subuniverso por estructura, ahora hay una sola con el tipo como parámetro.
Queda un hueco, y la guía lo señala ella misma: falta dar un modelo matemático del concepto de prueba elemental. Es lo que llama el plato gordo, y con razón.
Porque fijate qué poco hace el widget de arriba. Chequea una cosa sola —si cada cita está en la lista— y eso está lejísimos de decidir si el texto es una prueba. De los renglones que no citan nada no dice nada: «reemplazando por » es un paso que alguien tiene que justificar, y acá lo justificamos leyéndolo y asintiendo. Mientras «prueba» signifique «texto que convence a quien lo lee», no hay nada que una máquina pueda verificar, ni nada sobre lo que se pueda demostrar un teorema.
Convertir eso en un objeto matemático —reglas explícitas, derivaciones que son árboles y no párrafos, y después el teorema que liga «se puede derivar» con «es verdadera en toda estructura del tipo»— es el contenido de las guías que siguen. Es otro parcial y es otro proyecto.
Lo que sí queda cerrado es la tesis de éste, y es incómoda a propósito. El tipo no es un rótulo administrativo que se elige al principio y después no molesta. Decide qué subconjuntos son subuniversos y qué funciones son homomorfismos; decide qué palabras se pueden escribir y cuáles no significan nada; y decide, como acabás de ver, qué pruebas siguen siendo pruebas. Cambiás el tipo y cambia todo — menos el texto. Eso último es lo que lo vuelve tan fácil de no ver.
Sirve para el Ejercicio 18 de la Guía 7 y para la Guía 8 entera. Los ocho tipos, sus símbolos y sus axiomas no están transcritos a mano: la tabla se arma sola, y que ningún axioma de terna mencione , que los siete de cuaterna lo mencionen todos y que las dos listas sean disjuntas sale de mirarlas, no de afirmarlo. Con esta nota se cierra el segundo parcial de Lógica.