7.4: Tableaux

Template:MathJaxZach

Si bien muchos sistemas de derivación operan con arreglos de oraciones, los tableaux operan con fórmulas firmadas. Una fórmula firmada es un par que consiste en un signo de valor de verdad (\(\True\)o\(\False\)) y\[\sFmla{\True}{A} \text{ or } \sFmla{\False}{A}.\nonumber\] una oración Un cuadro consiste en fórmulas firmadas dispuestas en un árbol de ramificación descendente. Comienza con una serie de supuestos y continúa con fórmulas firmadas que resultan de una de las fórmulas firmadas por encima de ella aplicando una de las reglas de inferencia. Cada regla nos permite agregar una o más fórmulas firmadas al final de una rama, o dos fórmulas firmadas una al lado de la otra, en este caso una rama se divide en dos, con las dos fórmulas firmadas agregadas formando los extremos de las dos ramas.

Una regla aplicada a una fórmula firmada compleja da como resultado la adición de fórmulas firmadas que son subfórmulas inmediatas. Vienen en parejas, una regla para cada uno de los dos signos. Por ejemplo, la\(\TRule{\True}{\land}\) regla se aplica a\(\sFmla{\True}{A \land B}\), y permite la adición tanto de las dos fórmulas\(\sFmla{\True}{A}\) firmadas como\(\sFmla{\True}{B}\) al final de cualquier rama que contenga\(\sFmla{\True}{A \land B}\), y la regla\(\TRule{\False}{A \land B}\) permite que una rama sea dividir agregando\(\sFmla{\False}{A}\) y\(\sFmla{\False}{B}\) lado a lado. Un cuadro se cierra si cada una de sus ramas contiene un par coincidente de fórmulas firmadas\(\sFmla{\True}{A}\) y\(\sFmla{\False}{A}\).

La\(\Proves\) relación basada en tableaux se define de la siguiente manera\(\Gamma \Proves A\): si hay algún conjunto finito\(\Gamma_0 = \{B_1, \dots, B_n\} \subseteq \Gamma\) tal que hay un cuadro cerrado para los supuestos\[\{\sFmla{\False}{A}, \sFmla{\True}{B_1}, \dots, \sFmla{\True}{B_n}\}\nonumber\] Por ejemplo, aquí hay un cuadro cerrado que muestra que\(\Proves (A \land B) \lif A\) :

\[\begin{array}{lcl} 1. & \False\,(A \land B) \lif A & \text { Assumption } \\ 2 . & \True\, A \land B & \lif \False\, 1 \\ 3 . & \False\, A & \lif \False\, 1 \\ 4 . & \True\, A & \lif \True\, 2 \\ 5 . & \True\, B & \lif \True\, 2 \\ & \otimes & \end{array}\nonumber\]

Un conjunto\(\Gamma\) es inconsistente en el cálculo de tableau si hay un cuadro cerrado para suposiciones\[\{\sFmla{\True}{B_1}, \dots, \sFmla{\True}{B_n}\}\nonumber\] para algunos\(B_i \in \Gamma\).

Los tableaux fueron inventados en la década de 1950 independientemente por Evert Beth y Jaakko Hincikka, y simplificados y popularizados por Raymond Smullyan. Son muy fáciles de usar, ya que construir un cuadro es un procedimiento muy sistemático. Debido a la naturaleza sistemática de los tableaux, también se prestan a la implementación por computadora. Sin embargo, un cuadro suele ser difícil de leer y su conexión con las pruebas a veces no es fácil de ver. El enfoque también es bastante general, y muchas lógicas diferentes tienen sistemas tableau. Tableaux también nos ayuda a encontrar estructuras que satisfagan (conjuntos de) oraciones dadas: si el conjunto es satisfacible, no tendrá un cuadro cerrado, es decir, cualquier tableau tendrá una rama abierta. La estructura satisfactoria puede ser “leída” de una rama abierta, siempre que cada regla que sea posible aplicar se haya aplicado en esa rama. También hay una conexión muy estrecha con el cálculo secuente: esencialmente, un cuadro cerrado es una derivación condensada en el cálculo secuente, escrita al revés.