El axioma ofrece dos alternativas. Saber el color de una punta tacha una de las dos, y la otra punta ya no elige.
Dos pruebas elementales prueba que un grafo bicoloreado no tiene ningún triángulo, y para eso usa tres veces el mismo paso: de una arista y el color de una punta sale el color de la otra. Allá ese paso se usa; acá se prueba. Es el Ejercicio 25 (a) de la Guía 7, pág. 16, y es la pieza más chica del práctico.
La regla de corrección del parcial es explícita: «si usa un resultado de alguna de las guías debe enunciarlo y probarlo por separado». La prueba del triángulo usa este lema tres veces, así que enunciarlo y probarlo aparte no es prolijidad — es la mitad del puntaje. Esta nota es exactamente ese trabajo.
La sentencia, textual:
dice que hay una arista entre e ; dice que es rojo. En castellano: si hay una arista y la punta de salida no es roja, la otra punta es roja.
El único axioma que hace falta es el de bicoloreo, Aprop:
Es una disyunción, y la sentencia del ejercicio es una implicación. Toda la prueba consiste en convertir una en la otra, y lo que hace el trabajo es saber el color de un vértice.
Dos vértices, y , unidos por una arista. El axioma, instanciado en ese par, dice «uno de los dos, no los dos»: o se da , o se da .
Supongamos ahora que no es rojo. La primera alternativa pide que sí lo sea, así que se cae: no puede ser ésa. Queda la otra, y la otra trae adentro. No hubo elección en ningún momento — el color de obliga al de .
Eso es toda la mariposa, y cabe en tres renglones. Lo que cuesta es escribirla como escarabajo: descartar una alternativa no es un paso del formato de la cátedra, y hay que fabricarlo con un absurdo — suponer la alternativa mala, chocarla contra lo que ya sabemos, y negarla.
Abajo, el mismo paso a mano. Pintá y mirá qué le pasa a .
Con hueco pasa lo que dice el ejercicio, y se encienden ocho de los dieciocho renglones: la espina del argumento, del supuesto al cierre. Con lleno el axioma también obliga a —al otro color—, pero ése no es este ejercicio: la hipótesis pide . Ahí quedan encendidos tres renglones, y son los del axioma: el 4, el 5 y el 6 se escriben antes de suponer nada, así que son los únicos que no se caen cuando el caso del ejercicio no se da.
Cada renglón es una sentencia y su justificación. Los rieles de la izquierda son los bloques: el de afuera abre en la línea 1 suponiendo la hipótesis del ejercicio y cierra en la 16; el de adentro, en la 8, abre el absurdo que descarta la alternativa mala y cierra en la 12. Adentro de un bloque cerrado no se puede volver a entrar: de la línea 9 no queda nada disponible después de la 12, y por eso la 13 tiene que citar a la 12 y no a la 11.
De las dieciocho líneas, dos llevan el prefijo TESISk: la 11 y la 15. No es que a las otras se les haya olvidado. El prefijo lo lleva la línea que consigue la tesis del bloque, una sola por bloque: la 11 es la contradicción que el absurdo salió a buscar, y la 15 es , que es lo que el ejercicio pide. Todo lo demás —las eliminaciones de conjunción, el modus ponens, la evocación— es camino, y va pelado. La prueba de la unicidad del máximo de la Guía 8, pág. 25, se lee igual: nueve renglones adentro del bloque y exactamente uno con prefijo.
Las dos generalizaciones del final —la 17 y la 18— son el paso que la cátedra marca como el más fácil de romper. Acá pasan porque y son arbitrarias de verdad: no salieron de ninguna elección, y la única hipótesis que las nombraba se cerró en la línea 16. Si se generalizara antes de esa línea, con la hipótesis todavía abierta, no sería arbitraria: sería «un vértice del que ya sabemos algo».
La prueba no cita más que Aprop: ni Airr ni Asim aparecen. Y eso se puede contar de un lado y del otro. Sobre las 4096 estructuras de tres elementos con y arbitrarias —las mismas 4096 que cuenta Dos pruebas elementales—, 98 cumplen Aprop, y en esas 98 la sentencia no falla ni una vez. Que no falle es lo que la prueba afirma; contarlo es otro camino al mismo hecho, y sirve justamente porque no comparte ni una línea con el primero.
El axioma hace falta. De las 4096, la sentencia falla en 2719 —dos de cada tres—, y las 2719 caen todas entre las 3998 que no cumplen Aprop. Sin el axioma, la implicación no es ninguna verdad general: es falsa casi siempre.
Y no es una reformulación del axioma, es una consecuencia estrictamente más débil. La sentencia vale en 1377 de las 4096, de las cuales 1279 no cumplen Aprop. Hay muchísimas estructuras donde el vecino queda obligado y sin embargo el bicoloreo no vale: la implicación no alcanza para recuperar la disyunción de la que salió.
Con esto en la mano, el Ejercicio 25 (b) es corto: en un triángulo , , , el color de obliga el de ; el de obliga el de ; y el de vuelve a obligar el de , al otro color. Los dos colores de a la vez, y ahí está la contradicción. Ese recorrido está escrito entero en Dos pruebas elementales.
Sirve para el Ejercicio 25 (a) de la Guía 7, pág. 16. El formato de la prueba, con las veintiuna justificaciones y el paso que parece legal y no lo es, está en La mariposa y el escarabajo. Las resoluciones están en parcial-2/soluciones/practico-7-lenguaje-elemental.pdf del repo de Lógica, y el formato de prueba elemental en parcial-2/preparacion/apunte-pruebas-elementales.pdf.