Una regla es un movimiento permitido; un axioma es una oración que podés citar. Mismo contenido, distinto estatus.
En la nota de la Guía 3 armaste pruebas con tres reglas. Mirabas la forma de una meta, elegías la que encajaba, y la meta se partía en pedazos más chicos hasta que cada pedazo suelto era un hecho citable. Funcionaba, y en ningún momento hizo falta preguntar de dónde salían las tres.
La Guía 6 lo contesta, y lo dice sin ningún rodeo:
Muchas de las pruebas dadas en la Guía 3 pueden adaptarse naturalmente para ser pruebas elementales de reticulados cuaterna… el axioma A≤A puede ser usado en lugar de aplicar la Regla Igualdad en Posets, y similarmente los axiomas As≤C y Ai≥C se pueden usar en lugar de las reglas Superar un Supremo y Ser ≤ que un Ínfimo.
En lugar de. Las tres reglas no eran un método aparte que la cátedra te prestó para la Guía 3: eran tres de los siete axiomas que definen un reticulado cuaterna, usados antes de que la palabra «axioma elemental» existiera en el curso.
La diferencia entre una regla y un axioma no está en lo que dicen — dicen exactamente lo mismo. Está en dónde viven.
«Para probar , probá y » es una oración sobre pruebas: te dice qué movimiento tenés permitido hacer. No se puede escribir con , , , y , porque no habla de reticulados, habla de vos.
sí. Es una oración del lenguaje, sin variables libres, verdadera en todo reticulado cuaterna — y por eso la podés citar en el medio de una prueba, como quien cita un dato.
La consecuencia es más grande de lo que parece. Si cada paso es una cita, la prueba entera se escribe adentro del lenguaje y deja de necesitar instrucciones de afuera. Eso es lo que la Guía 6 llama una prueba elemental, y es el programa que la Guía 8 va a bautizar.
Abajo está el mismo árbol de la nota anterior: las mismas metas, las mismas tres reglas, la misma mecánica. Lo único nuevo es la columna de la derecha — cada vez que hacés un movimiento aparece al lado la oración que ese movimiento cita, ya instanciada con los términos de tu meta.
Tocá una meta abierta de la columna izquierda para elegirla y después tocá una regla — o usá el teclado: las metas abiertas entran en el orden de tabulación. Si la regla no encaja con la forma de esa meta, el widget te lo dice y no pasa nada.
No cambiaste de método. Es el mismo árbol, las mismas metas, el mismo orden de decisiones; lo único que cambió es cómo se escribe cada paso. Y la columna derecha no es una traducción libre: la fórmula que aparece es el axioma mismo, con los cuantificadores pelados y sus variables reemplazadas por los términos de tu meta. No hay ninguna tabla de equivalencias escrita a mano — la instancia se calcula, y si falla no aparece.
Las hojas también. En la Guía 3, cerrar una hoja era citar uno de cinco hechos: reflexividad, , , y . Los cinco son axiomas. El primero es A≤R; los dos del supremo son las dos mitades de una sola sentencia, AsesC, y los dos del ínfimo las dos mitades de AiesC — por eso son cinco hechos y tres axiomas.
Ninguna prueba sola los usa a todos: cada lema pide los que su forma pide, y hay lemas que se arreglan con menos. Pero recorré el catálogo entero —el widget no olvida lo que ya citaste— y contá los que quedan encendidos: seis. Tres los usaste como reglas, tres como hechos, y en ningún momento del cuatrimestre nadie los llamó axiomas.
Un axioma no es un truco ni un atajo de escritura. Es una sentencia: cerrada, sin nombres de elementos fijos, que en una estructura dada o vale o no vale — y eso se puede preguntar. «Ser un reticulado cuaterna» no es más que cumplir las siete.
Elegí uno y mirá dónde vale. El banco tiene cuatro estructuras: tres reticulados de divisores —D12, D30, D36, con la divisibilidad— y una cuarta que no es un reticulado, aunque su orden sea un orden parcial impecable.
Las dos que se rompen en la anticadena son As≤C y Ai≥C: dos de tus tres reglas. Y no se rompen porque el orden esté mal — los tres axiomas del orden valen ahí, es un orden parcial de verdad. Se rompen porque e devuelven una cota y no la mínima ni la máxima: AsesC y AiesC, que sólo piden ser cota, siguen valiendo.
O sea que Superar un Supremo nunca fue evidente. Era una afirmación con contenido, que en esa estructura tiene un contraejemplo con nombre y apellido — el testigo que el widget te muestra. Lo que pasaba es que la Guía 3 trabajaba siempre adentro de reticulados, donde es verdadera, y una verdad que nunca falla no se distingue de una regla del juego.
Quedó uno apagado: A≤T, la transitividad. Y esa ausencia ya la habías sentido.
En la nota de la Guía 3 la asociatividad no cerraba, y el motivo era que la hoja no admitía ninguna de las tres reglas: la izquierda no es un supremo, la derecha no es un ínfimo, y no es una igualdad. Lo que hacía falta era encadenar, pasar por un término del medio. Encadenar es transitividad, y con A≤T sobre la mesa esa hoja se cierra en tres citas:
Y ahí se ve por qué A≤T no podía ser una regla como las otras tres. Las tres reglas salen solas: la forma de la meta determina cuáles son las submetas, y por eso el árbol se puede armar sin pensar. La transitividad no. Su conclusión es , que encaja con cualquier meta de la forma , y deja la sin determinar: el término del medio no sale de la meta, lo elegís vos.
Eso es literalmente lo que pasa en el widget de arriba. La misma rutina que encuentra el axioma de cada hoja rechaza A≤T siempre, porque exige que la cita determine todas sus variables y ésta deja una libre. No es una excepción que haya que programar aparte: es la definición de citar, aplicada.
Así que lo que quedó de la Guía 3 no es una tabla de equivalencias entre dos vocabularios. Es que estuviste trabajando adentro de un sistema axiomático completo —seis de sus siete sentencias, en un orden que vos elegías— sin que el sistema tuviera nombre todavía. La Guía 6 no te enseña a probar: le pone el nombre a lo que ya venías haciendo, y al ponérselo te deja preguntar cosas que antes no se podían formular, como si un axioma vale en tal estructura o cuál te falta.
La nota anterior es Producir la prueba, donde estos árboles aparecen por primera vez. Los siete axiomas de esta nota no son texto: son fórmulas que se evalúan, y por eso los números —los siete valen en D12, D30 y D36; en la anticadena fallan exactamente As≤C y Ai≥C— salen de evaluarlas y no de afirmarlas.