De los tres axiomas de poset, la prueba cita uno. Y sobre las 512 relaciones de tres elementos, la sentencia falla en exactamente una.
Guía 7, Ejercicio 17 (a), pág. 11. Hay que probar, en posets:
En castellano: si hay dos elementos distintos, hay un par ordenado que no está en .
Y conviene leer bien la tesis, porque dice menos de lo que parece. no afirma que haya dos elementos incomparables: afirma que hay un par ordenado afuera de la relación. En una cadena de dos puntos vale y nada más — los dos se comparan, y aun así el par ya alcanza como testigo. Lo que no puede pasar es que se miren los dos, y de ahí sale el título.
El que hace toda la fuerza es un solo axioma, A≤A, la antisimetría:
El Ejercicio 17 ya había aparecido: Maximal no es máximo es el ítem (e) de esta misma lista. Allá la cuenta de axiomas de poset usados dio cero; acá da uno, y la última sección lo mide de la misma forma.
La Guía 6, pág. 12, pide hacer la prueba a lo mariposa —pensando, imaginando— antes de escribirla como escarabajo, y advierte contra volverse un «escarabajo sintáctico mecánico». Así que primero el recorrido, sin una sola línea numerada.
Supongamos que hay dos elementos distintos. Llamémoslos y : no son el mismo. Y preguntémonos si valen las dos comparaciones, y , a la vez.
No pueden. Si valieran las dos, la antisimetría diría , y quedaríamos con que es y no es al mismo tiempo. Ése es el absurdo, y lo que queda al salir de él es : una de las dos comparaciones falla.
Cuál de las dos, no lo sabemos — y no hace falta saberlo. Falle la que falle, ahí está el par ordenado que la tesis pedía. Por eso el final es una división por casos y no una cuenta derecha: los dos casos llegan a la misma conclusión por el mismo camino, con los nombres cambiados de lugar.
Abajo está dibujado. Son dos puntos y dos flechas posibles, y arranca sin ninguna. Poné una, poné la otra, y después poné las dos.
Las cuatro combinaciones de flechas son las cuatro relaciones reflexivas que caben en dos puntos, y en tres de ellas la sentencia vale. La única donde falla es la de las dos flechas — y ésa no es un poset. El colapso tampoco es un truco del dibujo: es lo que la antisimetría manda hacer, y al hacerlo se va el antecedente, porque ya no hay dos elementos distintos de los que hablar.
Ahora sí, línea por línea. Tres cosas del formato, antes de leerlo.
HIPOTESISk abre el bloque k suponiendo algo, y CONCLUSION lo cierra y deja escrita la implicación entera. Entre las dos, TESISk marca una sola línea: la que consigue la tesis del bloque, la de más abajo antes de su CONCLUSION. No la llevan todas las líneas que descienden de la hipótesis — sólo la que llega. Acá son cuatro bloques y cuatro líneas marcadas: la 10, la 17, la 21 y la 23.
La sangría de cada línea es su profundidad de bloque: con eso alcanza para saber qué se puede citar desde dónde.
La técnica nueva son las dos ELECCION seguidas. El antecedente es un existencial doble, , y cada ELECCION saca un cuantificador: la primera nombra , la segunda nombra . Y cada una tiene que nombrar una constante nueva — es eso lo que impide que y terminen siendo el mismo objeto por descuido de notación.
Y el final cierra con CONCLUSION, no con GENERALIZACION. Es la excepción, y tiene su sección más abajo.
La fuente de la que salió esta prueba justificaba el paso de a con un REEMPLAZO de una sola referencia. No cierra, y por dos motivos distintos.
El primero es la aritmética de la regla: REEMPLAZO cambia un término por otro igual, así que necesita dos líneas — la igualdad que autoriza el cambio, y la sentencia donde se cambia. Con una sola referencia le falta la mitad.
El segundo es de fondo, y explica el primero: acá no se está reemplazando ningún término. No hay ninguna igualdad a la vista. Lo que se usa es De Morgan, una ley del cálculo proposicional que reacomoda los conectivos y no toca un solo término. REEMPLAZO no iba a poder justificarlo nunca, con una referencia o con cinco.
La corrección es enunciar De Morgan y usarla, que son dos líneas donde había una: la implicación entra como AXIOMALOGICO, y de ahí sale la disyunción con un MODUSPONENS. Por eso la prueba de arriba tiene 24 líneas y no 23.
Y entra sin prueba aparte, a propósito. La regla de corrección del parcial dice que si una resolución usa un resultado de alguna de las guías hay que enunciarlo y probarlo por separado — pero De Morgan no es un resultado de las guías: es una tautología, verdadera en cualquier teoría y sobre cualquier estructura, que es exactamente lo que AXIOMALOGICO significa. Enunciarla es obligatorio; probarla, no.
Lo que más enseña es lo otro. Con la línea mal, el que se cae no es ese renglón solo: la división por casos del final la cita, y al citar una línea que no vale se cae también. Un error de una línea se lleva la prueba entera — es el mismo mecanismo por el que un bloque cerrado no deja usar lo que quedó adentro.
El error que la cátedra nombra como el error —generalizar sobre una constante que salió de una ELECCION, que es lo que hace fallar el Teorema de Corrección— no puede aparecer en esta prueba. Vale entender por qué.
Porque la tesis es un existencial. Las pruebas que terminan en un —las dos de Dos pruebas elementales, por ejemplo— cierran generalizando sobre las constantes que fueron fijas pero arbitrarias, y ahí sí hay que mirar de dónde salió cada una. Ésta cierra con CONCLUSION y nunca necesita la regla peligrosa: cero GENERALIZACION en veinticuatro líneas.
Lo cual es una suerte, porque no habría podido usarla. Las dos constantes de esta prueba, y , nacieron de sendas ELECCION: son testigos elegidos, no elementos arbitrarios. Si la tesis hubiera sido universal, generalizar sobre cualquiera de las dos habría sido justo el paso prohibido. El mismo ejercicio enseña las dos caras de la regla: no se generaliza sobre un testigo, y acá no hace falta.
Nada de lo que sigue está en la guía. Sale de evaluar la sentencia sobre todas las relaciones chicas, que es lo que este sitio puede hacer y un apunte no.
Sobre las 512 relaciones binarias de tres elementos —las que salen de decidir, casilla por casilla, cada uno de los nueve pares ordenados— la sentencia falla en exactamente una: la relación completa, donde todo par está en . En dos elementos es 1 de 16; en cuatro, 1 de 65 536. Siempre la misma: la que tiene todas las flechas.
De esas 512, 216 son antisimétricas y apenas 19 son posets de verdad. En las 216 antisimétricas la sentencia no falla nunca. Y la única que falla sí es reflexiva y transitiva — o sea que ninguno de esos dos axiomas puede descartarla. La antisimetría es el único de los tres que hace falta, y es el único que la prueba cita. Es la misma cuenta que Maximal no es máximo hizo para el ítem (e), donde dio cero de tres.
Y una sorpresa con el antecedente. De dos elementos para arriba, es verdadero siempre, así que la implicación vale exactamente donde vale su consecuente y el antecedente no descarta nada: una falla contra una falla, en 16, en 512 y en 65 536. El único lugar donde el antecedente hace algo es el universo de un solo elemento, donde es falso: ahí el consecuente solo falla y la implicación entera se salva. Que es, exactamente, el estado del dibujo de arriba después de apretar «Aplicar antisimetría».
Sirve para el Ejercicio 17 (a) de la Guía 7, pág. 11. El formato de la prueba —qué significa cada justificación y por qué una sola línea del bloque lleva el prefijo— está en La mariposa y el escarabajo. La teoría está en parcial-2/preparacion/apunte-pruebas-elementales.pdf del repo de Lógica, y las resoluciones en parcial-2/soluciones/practico-7-lenguaje-elemental.pdf.