Las tres reglas no sirven para entender el lema: sirven para partir la meta hasta que cada pedazo sea un axioma.
Los lemas de la Guía 3 no son difíciles de entender. Leés la absorción —x s (x i y) = x— y te convencés en diez segundos: el ínfimo de x con cualquier cosa está por debajo de x, así que juntarlo con x no agrega nada.
Lo difícil es producir la prueba con la hoja en blanco. Y ahí la guía te da tres reglas que no parecen gran cosa:
Parecen triviales porque lo son. Lo que no es trivial es hasta dónde alcanzan: aplicadas una y otra vez, parten casi todos los lemas de la guía hasta que cada pedazo suelto es un axioma que podés citar. Casi todos — y el que se resiste tiene algo para enseñar. Abajo lo hacés vos.
La meta está arriba. Tocá una meta abierta 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.
Dos reglas. Eso fue todo. Y fijate que en ningún momento hiciste algo inteligente: miraste la forma de la meta —una igualdad, un supremo a la izquierda— y aplicaste la regla que encajaba con esa forma. La creatividad que parecía hacer falta no estaba.
Eso es lo que la guía quiere que automatices, y por eso el Ejercicio 13 te pide completar pruebas en vez de inventarlas. Abajo tenés el catálogo entero: siete lemas, la misma mecánica.
Elegí un lema y armá su prueba. Si te trabás, el botón te dice qué hojas quedaron abiertas y qué forma tienen — que es exactamente la pregunta que hay que hacerse frente a una hoja en blanco.
Son siete, y uno no va a salir. Cuando lo encuentres, no insistas: apretá el botón y mirá qué te dice de las hojas que quedaron.
Los seis que salen, salen con la misma mecánica, y ninguno pidió una idea. Por eso el consejo de la guía —automatizar el patrón— no es pereza: es que el patrón es la prueba.
El que no salía era la asociatividad, y no es un defecto del catálogo: con estas tres reglas no cierra. Vale la pena ver por qué.
Cuando lo intentaste, te quedaron cuatro hojas — entre ellas z ≤ (x s (y s z)). Ninguna de las tres reglas encaja: la izquierda no es un supremo, la derecha no es un ínfimo, y no es una igualdad. Y sin embargo la meta es verdadera — z está por debajo de y s z, que está por debajo de x s (y s z).
Lo que falta es encadenar: pasar por un término del medio. Y encadenar no es partir. Las tres reglas toman una meta y la parten en pedazos que ya estaban adentro; la transitividad, en cambio, te pide traer un término que no estaba — y elegir cuál es justamente el paso donde vuelve a hacer falta pensar.
Por eso la guía trata la asociatividad aparte y con más trabajo (Ejercicios 17 y 18), y por eso el formulario tiene además el Director de Cine Generoso y Pertenecer a la Imagen: son reglas que introducen un actor en vez de partir la meta. Saber cuál de las dos cosas te hace falta es la mitad del oficio.
Sirve para los ejercicios 13 a 21 de la Guía 3. Las resoluciones están en parcial-1/soluciones/practico-3-reticulados-par.pdf del repo de Lógica, y las cinco reglas completas en parcial-1/preparacion/plan-de-estudio.pdf.