Bitácora · Lógica · Concepto

La prueba elemental

Guías 6, 7 y 8 · qué es, por qué vale en toda estructura del tipo, el esqueleto, lo que la invalida y la versión con justificaciones

Una prueba elemental es una prueba de matemático con tres restricciones. Se parte de una estructura de la que no se sabe nada salvo que cumple los axiomas. Cada paso es tan simple que se justifica en una frase. Y todo lo que se afirma se escribe con sentencias elementales del tipo. Con esas tres cosas, lo que se prueba para esa estructura vale para todas las del tipo, porque la prueba nunca supo en cuál estaba parada.

01 · La definición

La Guía 6 la da para reticulados cuaterna. Una prueba elemental de una sentencia elemental pura de reticulados cuaterna es una prueba con estas características:

  1. Se parte de una estructura (L,s,i,≤) fija pero arbitraria: lo único que se sabe de ella es que L no es vacío, que s e i son operaciones binarias, que ≤ es una relación binaria, y que cumple los siete axiomas A≤R, A≤T, A≤A, AsesC, As≤C, AiesC y Ai≥C. Ésa es la única información particular que se puede usar.
  2. Las deducciones son muy simples y obvias de justificar, con mínimas frases en castellano.
  3. Lo concerniente a la matemática misma se escribe sólo con sentencias elementales del tipo.

La Guía 7 la extiende a cada tipo de estructura —posets, reticulados terna, acotados, complementados, grafos, grafos bicoloreados, median álgebras—, cada uno con su lista de axiomas elementales, y le agrega un punto al principio: lo que se prueba tiene que ser una sentencia elemental pura del tipo. La Guía 8 da el último paso: una teoría elemental (Σ,τ) es un tipo τ con un conjunto Σ de sentencias elementales puras, y una prueba elemental en (Σ,τ) parte de una estructura de tipo τ fija pero arbitraria de la que sólo se sabe que cumple Σ. Las tres versiones son la misma idea; lo que cambia es de dónde salen los axiomas.

Dos cosas que la definición fija sin decirlas fuerte. Primera: la prueba es relativa a los axiomas. Una prueba elemental de reticulados terna no es una prueba elemental de reticulados cuaterna, aunque la sentencia sea de los dos tipos: la absorción es axioma de terna y no de cuaterna, y es el Ejercicio 18 de la Guía 7, desarrollado en La misma prueba, y depende del tipo. Segunda: los nombres de elementos fijos —a, b, c— no aparecen en los axiomas ni en lo que se prueba. Viven sólo adentro de la prueba, para nombrar elementos hipotéticos mientras se razona sobre ellos. Por eso el enunciado tiene que ser una sentencia pura: sin variables libres y sin nombres sueltos, que no tendrían valor de verdad.

02 · Por qué vale en toda estructura del tipo

La Guía 7 lo dice en una oración: como se parte de una estructura de la que sólo se asume que satisface los axiomas, y como cada paso es simple y obvio, la sentencia probada tiene que ser verdadera en todas las estructuras del tipo. Desarmada:

Sea M cualquier estructura que cumpla los axiomas. La prueba se puede releer entera con M en el lugar de la estructura fija, porque de aquélla no usó nada que M no tenga. Los axiomas son verdaderos en M. Cada paso obvio lleva de oraciones verdaderas en M a una oración verdadera en M. Recorriendo la prueba de arriba abajo, la última línea —la sentencia— es verdadera en M. Y M era cualquiera.

El argumento se apoya en las dos condiciones de la definición, y por eso cada una tiene un error que la rompe. Si un paso usa algo de la estructura que no sale de los axiomas —que es finita, que es una cadena, que es la de los divisores de 12—, la relectura con M se traba en las estructuras que no lo cumplen. Si un paso no es obvio, nada garantiza que preserve la verdad. La Guía 8 promete convertir este argumento en un teorema: es el punto «sublime» de su programa, y lo cierran el Teorema de Corrección y el de Completitud en la Guía 14.

03 · No es una prueba matemática cualquiera

La Guía 6 lo muestra con la conmutatividad del supremo, ∀x∀yxsy=ysx. Una prueba matemática correcta y corta: los axiomas AsesC y As≤C garantizan que xsy es sup({x,y}), y obviamente sup({x,y})=sup({y,x}). No es elemental: sup, las llaves y la igualdad de conjuntos no son parte del lenguaje elemental de reticulados cuaterna. Ninguna sentencia elemental dice «el conjunto {x,y}».

La prueba elemental de la misma sentencia es más larga y no usa conjuntos: instancia AsesC con x como b y y como a para tener b≤bsa∧a≤bsa; instancia As≤C con x como a, y como b y z como bsa para sacar asb≤bsa; hace lo mismo con los papeles cambiados para bsa≤asb; y cierra con A≤A. Lo que en la prueba común era «obviamente» acá son instancias de axiomas, una por paso.

La diferencia no es de rigor, es de vocabulario. La prueba común puede ser perfectamente rigurosa y usar conjuntos, funciones, inducción, lo que haga falta. La elemental se ata las manos a propósito: sólo los axiomas, sólo pasos obvios, sólo sentencias elementales. Las reglas de la Guía 3 —Igualdad en Posets, Superar un Supremo, Ser ≤ que un Ínfimo— pasan al formato sin cambiar, porque eran tres de los siete axiomas: A≤A, As≤C y Ai≥C. Y la Guía 6 aconseja hacer primero la prueba como matemático y después «tunearla»: es el método de la mariposa y el escarabajo.

04 · El esqueleto

Casi todas las pruebas elementales de la lista tienen la misma forma. Para una sentencia ∀x∀y(φ→ψ), las jugadas, en orden:

  1. Fijar«Sean a, b elementos fijos pero arbitrarios.» Un nombre nuevo por cada ∀ de afuera.
  2. SuponerSi lo de adentro es una implicación, «supongamos» el antecedente. Desde acá hasta descargarlo, todo vale bajo ese supuesto.
  3. InstanciarCitar un axioma diciendo qué va en lugar de cada variable: «tomando x como a e y como asb». Una variable puede recibir un término entero.
  4. EncadenarDos desigualdades con un extremo en común dan la de los extremos: A≤T, instanciado con los tres.
  5. Cerrar una igualdadLas dos desigualdades por separado y después A≤A. En reticulados cuaterna, casi toda igualdad se prueba así.
  6. Descargar«Como habíamos supuesto el antecedente, probamos la implicación.»
  7. Generalizar«Como a, b eran fijos pero arbitrarios, vale» la sentencia con sus ∀. Va al final, una sola vez, y sólo sobre los nombres del primer paso.

Un ejemplo que usa las siete. En todo reticulado cuaterna vale

∀x∀y∀z((x≤y∧y≤z)→(xsy)sz=z)

(si x está debajo de y y éste debajo de z, sumarle z a xsy da z). Verificada además en los 425 reticulados de hasta cinco elementos, contando con rótulos: vale en todos, y sin el antecedente vale sólo en el de un elemento.

Prueba. Sean a, b, c ∈L elementos fijos pero arbitrarios. Supongamos a≤b∧b≤c. El axioma A≤T, tomando x como a, y como b y z como c, dice (a≤b∧b≤c)→a≤c, así que a≤c.

De la hipótesis, b≤c; junto con lo anterior, a≤c∧b≤c. El axioma As≤C, tomando x como a, y como b y z como c, dice (a≤c∧b≤c)→asb≤c, así que asb≤c.

El axioma A≤R, tomando x como c, da c≤c, y entonces asb≤c∧c≤c. El axioma As≤C otra vez, ahora tomando x como asb, y como c y z como c, da (asb)sc≤c.

El axioma AsesC, tomando x como asb y y como c, da asb≤(asb)sc∧c≤(asb)sc; su segundo conjunto es c≤(asb)sc.

Con las dos desigualdades, (asb)sc≤c∧c≤(asb)sc, y el axioma A≤A, tomando x como (asb)sc y y como c, da (asb)sc=c. Como habíamos supuesto a≤b∧b≤c, probamos (a≤b∧b≤c)→(asb)sc=c. Como a, b, c eran fijos pero arbitrarios, vale la sentencia. ∎

Un ejemplo trabajado más largo, con la parte de pensar antes de escribir, es La distributiva que vale en todo reticulado, el Ejercicio 2 de la lista: ahí la meta se parte de atrás para adelante hasta que cada pedazo es un axioma, y la transitividad aparece dos veces con un intermedio que hay que elegir.

Simulación Encontrá el paso que la invalida — ocho pruebas cortas. Algunas son elementales y otras tienen un paso que no lo es. Tocá la línea que la rompe, o «Ninguna», antes de ver la respuesta.

    revisadas 0 de 8 acertadas 0 esta prueba sin responder

    05 · Lo que la invalida

    Los errores se reparten en dos familias, y la diferencia importa. En la primera, la sentencia que se quería probar es verdadera y la prueba igual no es elemental: falla una de las tres condiciones. En la segunda, el paso ilegal deja «probadas» sentencias falsas, y se puede medir cuántas veces.

    «Análogamente». La Guía 6 escribe la prueba de ∀x∀yxsy=ysx, dice «en forma análoga se puede probar que bsa≤asb», y a renglón seguido aclara que así la prueba no es elemental: esa justificación no es simple y obvia, y hay que poner las líneas. Su Ejercicio 7 pide justamente completarlas. Lo mismo vale para «el otro caso es simétrico».

    Instanciar sin decir con qué. «Por As≤C, asb≤c» deja al lector buscando qué va en x, y y z, y de dónde salen las dos desigualdades del antecedente. El paso puede ser correcto, pero no es obvio de justificar en una frase: la frase falta.

    Salirse del lenguaje. sup({a,b}), conjuntos, cardinales, «la componente conexa de»: nada de eso es una sentencia elemental. Y usar un axioma de otra teoría, aunque la sentencia sea del tipo: es el caso terna y cuaterna.

    Usar lo particular. Razonar sobre un ejemplo —el reticulado de los divisores de 12—, o suponer que la estructura es finita, o que es una cadena. Probó algo de esa estructura, no de todas.

    Generalizar sobre un testigo. Ésta es de la segunda familia. Si ∃yrel(a,y) y uno escribe «sea b tal que rel(a,b)», ese b no es arbitrario: es el que el ∃ entregó. Generalizar sobre él en la teoría de un solo axioma ∀x∃yrel(x,y) —de cada elemento sale una flecha— «prueba» ∀x∀yrel(x,y). Contado sobre las 512 relaciones de tres elementos: 343 cumplen el axioma, y la sentencia «probada» falla en 342 de ellas; vale sólo cuando la relación es todo. Cómo se ve este error en una prueba escrita línea por línea, y el corrector que lo atrapa, está en La mariposa y el escarabajo.

    Reusar un nombre. El testigo es un nombre nuevo. Con la misma teoría: «sea a un elemento; el axioma da ∃yrel(a,y); sea a tal que rel(a,a)» termina en ∃xrel(x,x), que es falsa en 27 de los 343 modelos de tres elementos y en el más chico de todos: dos elementos con una flecha de ida y otra de vuelta.

    Casos que no agotan. «Hay dos casos: a≤b o b≤a» sólo agota en una cadena. Con esos dos casos se «prueba» ∀x∀y(xsy=x∨xsy=y), y en el rombo, con p y q incomparables, psq=1 no es ninguno de los dos. De los 425 reticulados de hasta cinco elementos la sentencia vale en 153, y son exactamente las 153 cadenas.

    06 · La regla de citado

    La cátedra agrega una regla encima de la definición, escrita en las listas de ejercicios de parcial: si en la resolución de un ejercicio se usa un resultado de alguna guía, hay que enunciarlo y probarlo por separado, salvo que la consigna aclare que se puede usar sin demostración.

    No es una regla nueva: es la condición de los pasos obvios aplicada a los teoremas. La Guía 7 lo muestra con una prueba de ∀xxi1=x en reticulados acotados que cita ∀x∀y(xsy=y→xiy=x) como «teorema ya probado», y la descarta: un teorema anterior puede ser muy difícil de probar, así que citarlo no es una justificación simple y obvia. El arreglo es el que da la guía: anteponer la prueba elemental del resultado citado. La prueba queda más larga y es legítima.

    En la lista del parcial 2 hay una sola excepción declarada: el Ejercicio 15, que dice qué dos sentencias se pueden usar como teoremas. Fuera de ésa, citar la ∀x∀y(x≤y↔xsy=y) de la Guía 6, o «la monotonía del supremo», o un ejercicio anterior de la misma lista, es citar sin probar. Lo que no hace falta probar son los axiomas: citarlos instanciados es el paso obvio por excelencia.

    07 · La misma prueba, con justificaciones

    La Guía 8 se propone modelar matemáticamente la prueba elemental —el «plato gordo» de su programa—, y el modelo es la prueba formal: una sucesión de sentencias numeradas, cada una con una justificación de una lista cerrada. AXIOMAPROPIO cita un elemento de Σ. PARTICULARIZACION saca un ∀ poniendo un término en su lugar: es instanciar, una variable por vez. ELECCION nombra un testigo nuevo para un ∃. GENERALIZACION pone un ∀ sobre un nombre arbitrario. HIPOTESISk abre un supuesto y CONCLUSION lo descarga. La lista completa, con cuántas líneas cita cada una y las dos trampas de alcance, está en La mariposa y el escarabajo.

    Abajo está la prueba de la sección 04 escrita así. Cada grupo de líneas lleva arriba, en azul, el paso en castellano del que sale.

    Supongamos a≤b∧b≤c

    1.a≤b∧b≤cHIPOTESIS1

    a≤c, por A≤T

    2.∀x∀y∀z((x≤y∧y≤z)→x≤z)AXIOMAPROPIO
    3.∀y∀z((a≤y∧y≤z)→a≤z)PARTICULARIZACION(2)
    4.∀z((a≤b∧b≤z)→a≤z)PARTICULARIZACION(3)
    5.(a≤b∧b≤c)→a≤cPARTICULARIZACION(4)
    6.a≤cMODUSPONENS(1, 5)

    asb≤c, por As≤C

    7.b≤cCONJUNCIONELIMINACION(1)
    8.a≤c∧b≤cCONJUNCIONINTRODUCCION(6, 7)
    9.∀x∀y∀z((x≤z∧y≤z)→xsy≤z)AXIOMAPROPIO
    10.∀y∀z((a≤z∧y≤z)→asy≤z)PARTICULARIZACION(9)
    11.∀z((a≤z∧b≤z)→asb≤z)PARTICULARIZACION(10)
    12.(a≤c∧b≤c)→asb≤cPARTICULARIZACION(11)
    13.asb≤cMODUSPONENS(8, 12)

    (asb)sc≤c, por A≤R y As≤C

    14.∀xx≤xAXIOMAPROPIO
    15.c≤cPARTICULARIZACION(14)
    16.asb≤c∧c≤cCONJUNCIONINTRODUCCION(13, 15)
    17.∀y∀z((asb≤z∧y≤z)→(asb)sy≤z)PARTICULARIZACION(9)
    18.∀z((asb≤z∧c≤z)→(asb)sc≤z)PARTICULARIZACION(17)
    19.(asb≤c∧c≤c)→(asb)sc≤cPARTICULARIZACION(18)
    20.(asb)sc≤cMODUSPONENS(16, 19)

    c≤(asb)sc, por AsesC

    21.∀x∀y(x≤xsy∧y≤xsy)AXIOMAPROPIO
    22.∀y(asb≤(asb)sy∧y≤(asb)sy)PARTICULARIZACION(21)
    23.asb≤(asb)sc∧c≤(asb)scPARTICULARIZACION(22)
    24.c≤(asb)scCONJUNCIONELIMINACION(23)

    (asb)sc=c, por A≤A

    25.(asb)sc≤c∧c≤(asb)scCONJUNCIONINTRODUCCION(20, 24)
    26.∀x∀y((x≤y∧y≤x)→x=y)AXIOMAPROPIO
    27.∀y(((asb)sc≤y∧y≤(asb)sc)→(asb)sc=y)PARTICULARIZACION(26)
    28.((asb)sc≤c∧c≤(asb)sc)→(asb)sc=cPARTICULARIZACION(27)
    29.(asb)sc=cTESIS1MODUSPONENS(25, 28)

    Descargar el supuesto

    30.(a≤b∧b≤c)→(asb)sc=cCONCLUSION

    Como a, b, c eran arbitrarios

    31.∀z((a≤b∧b≤z)→(asb)sz=z)GENERALIZACION(30)
    32.∀y∀z((a≤y∧y≤z)→(asy)sz=z)GENERALIZACION(31)
    33.∀x∀y∀z((x≤y∧y≤z)→(xsy)sz=z)GENERALIZACION(32)

    Son las mismas jugadas. «Sean a, b, c fijos pero arbitrarios» no tiene línea propia: es que a, b y c aparecen como nombres nuevos, y vuelve al final como las tres GENERALIZACION. «Supongamos» es HIPOTESIS1, y «probamos la implicación» es la CONCLUSION de la línea 30. Y cada «el axioma tal, tomando x como …» se desarma en un AXIOMAPROPIO, una PARTICULARIZACION por variable y un MODUSPONENS.

    Lo que cambia es el tamaño: seis párrafos de castellano son 33 líneas, y catorce de ellas son particularizaciones. Lo que en castellano era una frase —«tomando x como asb, y como c y z como c»— acá son tres líneas, y el axioma As≤C se cita una sola vez, en la 9, y se particulariza dos veces desde ahí. Por eso las pruebas del parcial se escriben en castellano: la versión formal existe para poder demostrar teoremas sobre las pruebas, y el que importa es que lo que se prueba así vale en todos los modelos.

    Para tener a mano

    1. Prueba elemental: estructura fija pero arbitraria de la que sólo se saben los axiomas, pasos simples y obvios justificados en una frase, todo escrito con sentencias elementales. Lo que se prueba es una sentencia elemental pura.
    2. Por eso vale en toda estructura del tipo: la prueba se relee con cualquier modelo en el lugar de la estructura fija.
    3. Es relativa a los axiomas: una prueba de terna no es de cuaterna.
    4. El esqueleto: fijar, suponer, instanciar diciendo con qué, encadenar con A≤T, cerrar igualdades con A≤A, descargar, generalizar al final.
    5. La invalidan: «análogamente», instanciar sin decir con qué, salirse del lenguaje, usar lo particular, citar un teorema sin probarlo. Y dejan probar falsedades: generalizar sobre un testigo, reusar un nombre, casos que no agotan.
    6. Un resultado de una guía se enuncia y se prueba aparte, antes de usarlo. Los axiomas se citan sin probar.
    7. La prueba formal de la Guía 8 es la misma prueba con una justificación por línea: AXIOMAPROPIO, PARTICULARIZACION, MODUSPONENS, HIPOTESISk, CONCLUSION, ELECCION, GENERALIZACION…
    ← Anterior Siguiente → Inicio
    Relacionados La mariposa y el escarabajo La distributiva que vale en todo reticulado La misma prueba, y depende del tipo Fórmulas y sentencias elementales Teorías elementales y modelos La hipótesis elige el puente