La mariposa y el escarabajo

Una línea, tres cosas

Una línea del escarabajo es un número, una sentencia y una justificación con las líneas que cita:

La sentencia va escrita entera, sin abreviar y sin variables libres. La justificación es un nombre de una lista cerrada: no se inventa, y no se escribe «por definición» ni «es obvio». Y los números entre paréntesis son las líneas anteriores de las que este paso sale.

El bloque de hipótesis

Para probar una implicación se abre un bloque. HIPOTESISk supone el antecedente y CONCLUSION lo cierra, dejando la implicación armada — lo único del bloque que sobrevive afuera. Adentro se trabaja normalmente, y hay una sola línea con prefijo: la que consigue la tesis del bloque, justo antes del cierre.

El k es el número del bloque, porque los bloques se anidan: adentro de uno puede abrirse otro, y el prefijo es lo que dice a cuál pertenece la línea. Y TESISk no es una justificación: es un prefijo que se le pega adelante a la que sí lo es. La línea que consigue la tesis del bloque 1 por modus ponens se rotula TESIS1MODUSPONENS(6, 9), todo junto.

Lo que más se escribe mal es cuántas líneas lo llevan, así que conviene contarlo sobre un caso de la guía. La Guía 8, págs. 25-26, prueba que en un poset el máximo es único: si $a$ y $b$ son los dos máximos, son el mismo.

Nueve líneas adentro del bloque, y el prefijo aparece una vez. Mirá la línea 2: sale de la hipótesis directamente, por CONJUNCIONELIMINACION(1), y va pelada. Igual la 3, la 5 y la 6, que también descienden de ella. El prefijo no marca «esto depende del supuesto»: marca la línea que consigue lo que el bloque fue a buscar, que acá es la 10, la última antes del CONCLUSION. Todo lo demás lleva su regla sola, aunque esté escrito adentro.

Y las otras dos cosas que este ejemplo deja ver de paso: la línea 7 es un AXIOMAPROPIO citado adentro del bloque —un axioma se puede citar en cualquier lado, el bloque no lo tapa— y la CONCLUSION de la 11 no cita ninguna línea: el bloque entero es su referencia.

Las veintiuna justificaciones

La lista es cerrada, y es corta. Veintiuna, con cuántas líneas cita cada una:

Casi todas piden un número fijo de referencias, y escribir una de menos ya es un error de formato. La excepción es TRANSITIVIDAD, que encadena: con dos referencias es el caso de la guía — de $t=s$ y $s=u$, $t=u$ — y con más es la misma regla aplicada seguido sobre una cadena de igualdades.

Encima de la lista manda la regla de corrección del parcial, textual: «si usa un resultado de alguna de las guías debe enunciarlo y probarlo por separado, salvo que se aclare explícitamente que puede usarse sin demostración». Citar un lema de la guía por su nombre no es una justificación. O el paso está en la lista de arriba, o el lema se enuncia y se prueba aparte.

Las dos trampas de alcance

Lo que el escarabajo se equivoca casi nunca es una regla mal aplicada. Es el alcance: usar un nombre donde ese nombre ya no significa nada, o usar una línea donde esa línea ya no vale. Son dos, y las dos parecen pasos legales.

Primera: generalizar sobre algo que no es arbitrario. GENERALIZACION pone un $\forall$ sobre una constante, y sólo se puede si esa constante era fija pero arbitraria. Dos cosas la ensucian. Una: que haya nacido de una ELECCION — ahí la constante es un testigo, el nombre que le pusimos a uno que existe, y de uno no se deduce nada sobre todos. Otra: que aparezca en una hipótesis todavía abierta — mientras esa hipótesis viva, la constante está diciendo algo particular. Generalizar igual es el paso que hace fallar el Teorema de Corrección: la prueba se sigue leyendo bien y la sentencia que deja probada es falsa.

Segunda: el bloque que ya cerró. Lo que nació adentro de un HIPOTESISk vale mientras el bloque está abierto, y no después. Cuando la CONCLUSION lo cierra, de todo eso queda una sola cosa: la implicación. Las líneas de adentro no se citan más, ni siquiera para algo que parece inocente, porque valían bajo el supuesto y ese supuesto ya se descargó.

Abajo está la prueba del Ejercicio 15 de la Guía 8, entera y correcta. El teorema es $\forall x(\forall y\neg \mathrm{rel}(x,y)\to \exists z\mathrm{rel}(z,x))$, sobre una teoría de un solo axioma, $\forall x\exists y(\mathrm{rel}(x,y)\vee \mathrm{rel}(y,x))$. La mariposa cabe en un renglón: si de $a$ no sale ninguna flecha, la que el axioma promete tiene que entrar.

Y ahí está la tentación. En la línea 6 ya tenemos $\mathrm{rel}(b,a)$, que es lo que queríamos. ¿Para qué el paso 7? Sacalo y mirá dónde se cae la prueba.

Sin el paso 7, la línea 6 dice $\mathrm{rel}(b,a)$ y generalizar sobre $b$ parece la continuación natural. No lo es: $b$ es el nombre que la línea 4 le puso a uno que existe, y no hay nada que autorice a decir lo mismo de todos. El corrector marca la línea y el motivo nombra la ELECCION de la que salió.

El paso 7 no es burocracia, entonces: es lo único que borra el nombre. EXISTENCIA cambia la constante $b$ por un $\exists z$ que ya no la menciona, y recién con la línea 7 adentro la implicación de la 8 queda sin testigos — que es lo que le permite a la 9 generalizar sobre $a$, que sí era arbitraria.

Lo medido

Que el paso prohibido rompe el Teorema de Corrección no es una advertencia de estilo: se puede contar. La sentencia que deja probada el atajo, $\forall x(\forall y\neg \mathrm{rel}(x,y)\to \forall z\mathrm{rel}(z,x))$, tiene un $\forall z$ donde el teorema tiene un $\exists z$. Evaluando las dos sobre todas las relaciones binarias de tres elementos — las 512 que salen de decidir casilla por casilla cada uno de los nueve pares ordenados —, 469 cumplen el axioma de la teoría. En esas 469 el teorema no falla ninguna vez, y la sentencia del atajo falla 126. Repetido sobre las 65 536 relaciones de cuatro elementos: 63 577 modelos, 0 fallas del teorema y 12 952 del atajo.

El contraejemplo más chico tiene dos elementos y una sola flecha, de $a$ a $b$. El axioma se cumple: cada uno de los dos tiene su flecha, en algún sentido. De $b$ no sale ninguna, así que el antecedente vale. Y entra una — la de $a$ —, que es todo lo que el teorema pide. Pero no entran todas: $\mathrm{rel}(b,b)$ no se da. El paso que el corrector rechaza es exactamente el que cruza de «entra una» a «entran todas».

El segundo botón es la otra trampa, y es más sorda. La línea 5 es correcta, está probada, y el corrector no tiene nada contra ella mientras el bloque está abierto. Recién cuando se la cita desde afuera aparece el problema, y el motivo dice de qué bloque venía. En una prueba de treinta líneas con dos bloques anidados esto se hace solo: uno se acuerda de que la línea existe y se olvida de dónde vivía.

Las dos trampas tienen el mismo aire: nada de lo que está escrito es falso. La línea 6 dice la verdad y la línea 5 dice la verdad. Lo que se rompe es dónde se las puede usar, y eso no se ve leyendo la línea sola. Por eso el escarabajo se corrige de atrás para adelante, mirando de dónde vino cada nombre.

Dónde se ve cada técnica

Las cinco notas que siguen son un ejercicio cada una, elegidas por variedad de técnica y no de tema. Todas escriben el escarabajo en este formato, y ninguna vuelve a explicarlo.

El formato está en la Guía 6, pág. 12, y la lista de justificaciones se repite en las Guías 7 y 8. La prueba del ejemplo es el Ejercicio 15 de la Guía 8, pág. 25. Viene después de Maximal no es máximo, salvo que todo par tenga cota, que camina una prueba de la Guía 7 sin llegar a escribirla como escarabajo.