Demostraciones y tableaux semánticos

1. Qué es una demostración

Un argumento es la afirmación de que cierta conclusión se sigue de ciertas premisas. Una demostración es lo que zanja esa afirmación: un objeto finito y comprobable que cualquiera puede leer línea a línea y aceptar, sin tener que fiarse de su palabra. Lo valioso de una demostración no es que convenza - un buen discurso también lo hace -, sino que cada uno de sus pasos no podía haber sido de otro modo.

Es una exigencia más estricta de lo que parece. «Llueve, así que el suelo está mojado» es algo razonable de decir, pero se apoya en lo que usted sabe sobre la lluvia y el suelo. La lógica formal deja eso de lado y plantea una pregunta más estrecha: dada solo la forma de las oraciones, ¿hay alguna manera de que las premisas sean verdaderas y la conclusión falsa? Si no la hay, el argumento es válido, y la demostración es el registro de por qué no la hay.

Esta guía trata de una manera de producir ese registro: el método de los tableaux semánticos, también llamados árboles de verdad. Es el método que este sitio emplea cada vez que usted escribe un argumento en la calculadora, y una vez seguido, basta un bolígrafo para comprobar un argumento sobre papel.

2. Válido, y cómo saberlo

Escriba un argumento con un signo de consecuencia: las premisas a la izquierda, la conclusión a la derecha. La afirmación p → q, ¬q ⊨ ¬p dice que de un condicional y la negación de su consecuente se sigue la negación de su antecedente. El signo de consecuencia no es un conectivo más. Es una afirmación sobre las fórmulas que lo flanquean, y es correcta o incorrecta.

La definición de validez apunta directamente a una forma de comprobarla: recorra cada asignación de verdadero y falso a las variables y vea si alguna hace verdaderas todas las premisas y falsa la conclusión. Eso es lo que hace una tabla de verdad, y con dos o tres variables va perfectamente bien. El problema es que la tabla crece como 2ⁿ. Diez variables necesitan mil filas, veinte necesitan un millón, y la tabla no dice nada sobre qué filas importaban.

Un tableau ataca la misma pregunta por el otro extremo. En vez de enumerar todas las posibilidades y buscar una mala, supone que existe una mala e intenta construirla. Si el intento se derrumba en contradicción por todas las rutas posibles, no existe tal asignación y el argumento es válido. Si el intento tiene éxito, lo construido es un contraejemplo que usted puede leer directamente.

3. El método de los tableaux

Un tableau es un árbol de fórmulas signadas. Cada línea es una fórmula precedida de una T o una F, y el signo dice qué supone la rama sobre esa fórmula: no cuál es su valor de verdad, sino cuál haría falta para que el argumento fallara. Todo el método son cuatro pasos:

1. Escriba cada premisa con una T. Está suponiendo que todas las premisas del argumento se cumplen.
2. Escriba la conclusión con una F. Está suponiendo que aun así falla: esa es la suposición que quiere refutar.
3. Tome cualquier línea que no sea todavía un átomo y aplique la regla de su conectivo principal y su signo, añadiendo lo que esa regla produce al final de cada rama que la atraviesa.
4. Cierre una rama en cuanto contenga a la vez T A y F A para la misma fórmula A. Deténgase cuando todas las ramas estén cerradas o no quede ninguna línea por descomponer.

Nada de ese bucle exige ingenio ni elegir una estrategia. Cada línea tiene exactamente una regla, y aplicarlas en cualquier orden da el mismo veredicto: por eso puede hacerlo una máquina, y por eso puede fiarse del resultado cuando lo hace.

4. Las reglas

Hay una regla por conectivo y por signo: diez en total. Se dividen en dos clases, y la diferencia entre ellas es toda la razón de que un tableau sea un árbol y no una lista. Una regla α dice que varias cosas deben cumplirse a la vez, de modo que apila sus resultados rama abajo. Una regla β dice que debe cumplirse una de dos cosas, de modo que parte la rama en dos y deja que cada caso siga su camino.

Cada regla no es más que la condición de verdad de su conectivo, leída al revés. Una conjunción solo es verdadera cuando lo son ambos lados, así que T (A ∧ B) apila T A y T B. Una conjunción es falsa cuando al menos un lado lo es, pero la fórmula no dice cuál, así que F (A ∧ B) tiene que probar los dos: ramifica. La misma asimetría corre al revés para la disyunción, y un condicional falso significa que el antecedente se cumplió y el consecuente falló, el único caso en que una implicación se rompe.

Fíjese en lo que las reglas nunca hacen: nunca inventan una fórmula. Todo lo que una regla produce es un trozo de la línea de la que salió. Esa propiedad - la propiedad de la subfórmula - es lo que hace finito el método, y volvemos a ella más abajo.

5. Cerrar una rama

Una rama es un único hilo de razonamiento: lea desde la raíz hasta una hoja y tendrá un conjunto completo de suposiciones. Una rama se cierra cuando esas suposiciones se contradicen de plano, es decir, cuando lleva a la vez T A y F A para una misma fórmula. Da igual lo complicada que sea A o lo lejos que estén las dos líneas: si una rama necesita que una fórmula sea verdadera y falsa a la vez, nada la satisface.

Marque una rama cerrada con ×, nombrando las dos líneas que la cerraron, y deje de trabajar en ella. Nada más puede aprenderse de una suposición que ya era imposible.

Cuando todas las ramas se cierran, el tableau está cerrado, y eso es la demostración. Muestra que la suposición de partida - todas las premisas verdaderas, la conclusión falsa - lleva a contradicción por cada ruta que podía tomar. Como no quedó ninguna ruta, no existe tal asignación, y el argumento es válido. Es una demostración por reducción al absurdo, dispuesta de modo que ningún caso pueda pasarse por alto.

6. Una demostración, línea a línea

Tomemos el modus tollens: p → q, ¬q ⊨ ¬p. Las líneas 1 y 2 son las premisas, supuestas verdaderas. La línea 3 es la conclusión, supuesta falsa; y como la conclusión es ¬p, suponerla falsa es suponer p verdadera, que es lo que registra la línea 5. La línea 4 procede de la regla de negación aplicada a la línea 2: si ¬q es verdadera, q es falsa. El condicional de la línea 1 es la única línea que conserva un conectivo, y es una regla β, así que el árbol se bifurca:

La rama izquierda supone que el condicional se cumplió porque falló su antecedente, pero la línea 5 ya tiene p verdadera, de modo que la rama se contradice y se cierra. La rama derecha supone que se cumplió porque su consecuente era verdadero, pero la línea 4 ya tiene q falsa, de modo que también se cierra.

Ambas ramas se cerraron, así que no hay manera de tener p → q y ¬q verdaderas con ¬p falsa. El argumento es válido, y el árbol es la razón. Observe que la demostración no menciona la lluvia, el suelo ni qué representan p y q. No le hizo falta.

7. Cuando una rama queda abierta

No todos los argumentos son válidos, y aquí es donde el método se gana el sueldo. Si trabaja una rama hasta que nada en ella pueda descomponerse más - solo quedan átomos y átomos negados - y aun así no se ha cerrado, esa rama está saturada y abierta. No se ha cerrado, y no porque usted parara demasiado pronto: no queda nada que probar.

Una rama abierta es más que un veredicto de «inválido». Lea los signos de sus átomos y tendrá una asignación: todo átomo marcado con T es verdadero, todo átomo marcado con F es falso. Esa asignación hace verdaderas todas las premisas y falsa la conclusión, que es exactamente lo que es un contraejemplo. Los lógicos lo llaman un contramodelo, y es una respuesta concreta a «¿por qué no?» en lugar de una negativa.

La afirmación del consecuente, p → q, q ⊨ p, es el caso de manual. Su tableau deja una rama abierta con p falsa y q verdadera: una situación en la que el condicional se cumple y su consecuente se cumple, y sin embargo el antecedente no. Esa única asignación refuta el argumento por sí sola.

8. Por qué siempre termina

Cada regla sustituye una fórmula por sus propias subfórmulas, y toda subfórmula es estrictamente más corta que la fórmula de la que vino. Ninguna rama puede crecer para siempre: cada paso baja una escalera finita de piezas del argumento original, y la escalera tiene fondo. Antes o después, cada línea de una rama es un átomo o la negación de uno, y no queda nada por hacer.

Es una garantía real, no una esperanza. Significa que el método es un procedimiento de decisión para la lógica proposicional: aplíquelo a cualquier argumento y se detendrá, con un árbol cerrado o con una rama abierta, y nunca encogiéndose de hombros. El demostrador de este sitio impone además un presupuesto de nodos, pero solo como protección frente a que una fórmula patológica agote una pestaña del navegador; las matemáticas no necesitan tal límite.

9. Otros sistemas de demostración

Los tableaux son uno de varios sistemas de demostración, y son el que tiene forma de refutación: funcionan descartando el fallo. La deducción natural va al revés y construye la conclusión hacia adelante desde las premisas, con reglas como el modus ponens y la prueba condicional, y se parece mucho más a como argumenta un matemático en prosa. Una demostración por deducción natural suele ser más corta; encontrarla suele exigir más inventiva.

El cálculo de secuentes formaliza el propio signo de consecuencia y trata las afirmaciones de consecuencia como objetos, lo que lo convierte en la herramienta preferida para demostrar cosas sobre demostraciones. La resolución lo reduce todo a cláusulas y a una única regla, lo que resulta poco vistoso de leer y extremadamente rápido de ejecutar: sobre ella se construyen la mayoría de los demostradores automáticos y los solucionadores SAT.

Todos coinciden en qué argumentos proposicionales son válidos; difieren en el aspecto de una demostración y en qué resulta fácil de encontrar. Los tableaux son los más amables para aprender, porque una demostración fallida no es un callejón sin salida: le entrega el contraejemplo.

10. Practicar

La forma más rápida de aprender el método es ejecutarlo. Escriba un argumento en la calculadora con ⊨, ⊢ o |= y el tableau se dibuja junto a la tabla de verdad, de modo que puede contrastar el árbol con las filas. Después trabaje algunas demostraciones sobre papel antes de mirar.