El axioma promete una conexión y no dice para qué lado. Cerrarle todas las salidas a un vértice no lo deja aislado: lo obliga a recibir.
El Ejercicio 15 de la Guía 8, pág. 25, trabaja sobre una firma con una sola relación, binaria: . Sin operaciones y sin constantes: lo único que hay es una flecha que va de un elemento a otro, o sea un grafo dirigido.
La teoría elemental tiene un único axioma propio:
Nadie queda suelto: para cada hay algún con una flecha entre los dos. En algún sentido — el axioma pone una disyunción justamente para no comprometerse con cuál. Y lo que hay que probar en es esto:
En castellano: si de un vértice no sale ninguna flecha, entonces alguna le entra. Cerrarle todas las salidas no lo aísla.
El formato de prueba elemental —las líneas numeradas, las justificaciones, qué puede citar cada una— está en La mariposa y el escarabajo. Esta nota usa una sola de sus reglas hasta el hueso: la que dice cuándo una constante es arbitraria y cuándo no.
Tomá un vértice cualquiera y llamalo . El axioma, leído en , promete algún con : hay una flecha entre los dos, y el axioma no dice para qué lado.
Ahora suponé lo que supone la tesis: que de no sale ninguna flecha, o sea . El disyunto de la izquierda queda muerto, y queda muerto para todos los a la vez. Pero la promesa sigue en pie — es un axioma de , no una opción del dibujo —, así que lo que se cumple es el otro lado: hay un con . Alguien apunta a .
Ése es todo el argumento. Abajo está caminado: apagás las salidas de una por una y mirás en qué momento la promesa se queda sin lado izquierdo con qué cumplirse.
Mientras conserva una salida no hay nada que mirar: el axioma se cumple por izquierda y nadie está obligado a apuntarle. Con la última apagada, la flecha punteada que aparece no es una que el dibujo tuviera escondida — es la que el axioma obliga a que exista. Los cuatro vértices sin ella no son un modelo de .
Y el vértice del que sale esa flecha tiene un nombre que pusimos nosotros: . Ese nombre es el asunto de las dos secciones que siguen.
La misma mariposa, escrita como pide la Guía 6: una línea por paso, con su justificación y las líneas que cita. El prefijo TESIS1 lo lleva una sola línea de las siete del bloque: la 7, que es la que consigue la tesis que el bloque promete. Las otras seis son camino.
HIPOTESIS1AXIOMAPROPIOPARTICULARIZACION(2)ELECCION(3)PARTICULARIZACION(1)DISJUNCIONELIMINACION(5, 4)TESIS1EXISTENCIA(6)CONCLUSIONGENERALIZACION(8)La barra al costado es el bloque que abre la hipótesis de la línea 1 y que la CONCLUSION de la 8 cierra. Todo lo de adentro vale bajo esa hipótesis, y por eso la 8 no afirma sino la implicación entera.
Mirá dos líneas de esa lista: la 4 y la 7.
La línea 4 inventa un nombre. El existencial de la 3 promete que hay alguno, y ELECCION lo bautiza . Ese nombre no está en el enunciado, no está en el axioma y no está en la hipótesis: nace ahí, y lo único que se sabe de él es lo que la línea 4 dice.
La línea 7 lo borra. De pasa a , que es exactamente lo que se sabía antes de bautizar a nadie: alguien apunta a . no vuelve a aparecer en el resto de la prueba, y ése es el punto.
Recién por eso la línea 9 puede generalizar. GENERALIZACION pone un sobre una constante arbitraria, y lo es: entró como un vértice cualquiera y nunca se le pidió nada. , en cambio, no es arbitraria — la eligió la línea 4 justamente entre los que cumplían la promesa.
Si en lugar de descargarlo se generalizara sobre él, pasando de la línea 6 a , la prueba estaría diciendo que todos los vértices apuntan a . Es falso y no es lo que se probó, y a simple vista el paso parece tan legal como los otros ocho. Es el error que hace fallar el Teorema de Corrección; La mariposa y el escarabajo deja hacerlo y ver dónde se cae.
Esto no está en la guía. Sale de evaluar las dos sentencias —el axioma de y la tesis del ejercicio— sobre todos los grafos dirigidos chicos, uno por uno.
Sobre las 512 relaciones binarias de tres elementos —las que salen de decidir casilla por casilla cada uno de los nueve pares ordenados— el axioma vale en 469, y la tesis vale en esas mismas 469. Las 43 donde falla una son las 43 donde falla la otra. Repetido sobre las 65 536 de cuatro elementos: coinciden en las 65 536, con 63 577 modelos.
Son dos sentencias distintas y podrían haber diferido en cualquiera de esas 66 048 estructuras. No difieren en ninguna, y hay una razón: leída en un , la promesa del axioma es y la tesis es . La misma disyunción, escrita como implicación.
Lo cual dice qué es exactamente el trabajo de estas nueve líneas: reescribir una disyunción como una implicación, sin tener esa equivalencia a mano como axioma. Los cuantificadores hay que sacarlos y volverlos a poner, y ahí es donde entra el testigo y donde hay que sacárselo de encima.
Y la hipótesis no es vacía: de los 469 modelos de tres elementos, 126 tienen algún vértice sin ninguna salida — algo más de la cuarta parte. En cuatro elementos son 12 952 de 63 577. En todos ellos la implicación se cumple con el antecedente verdadero, que es la única forma de que diga algo.
Sirve para el Ejercicio 15 de la Guía 8, pág. 25. El enunciado está en parcial-2/practicos/Guia 8 de Logica.pdf y el formato de prueba elemental, con la lista completa de justificaciones, en parcial-2/preparacion/apunte-pruebas-elementales.pdf del repo de Lógica.
La nota anterior es Un color obliga al de al lado, donde la disyunción también se descarta pero sin ningún testigo de por medio. La siguiente es El testigo lo construís vos, donde el testigo no se elige: se fabrica, y por eso no hay nada que descargar.