Caracterización deductiva de los árboles de forzamiento semántico

Deductive characterization of semantic forcing trees.

El cálculo proposicional clásico está caracterizado por una herramienta de inferencia visual llamada árboles de forzamiento semántico. Con esta herramienta se marcan los nodos del árbol asociado a una fórmula dada, con base en estas marcas se determina si la formula es valida o no. En caso de invalidez, la valuación que refuta la validez de la fórmula está determinada por las marcas de las hojas en su árbol de forzamiento. En caso de validez, se puede construir una deducción formal de la fórmula asociada a la raíz del árbol; esto se logra debido a que cada regla utilizada para marcar los nodos en el árbol está asociada a una regla de inferencia en el sistema deductivo.

Introducción

El método de los tableros semánticos, presentado por E. Beth en [1] y popularizado como árboles de opciones semánticas por R. Smullyan en [2], consiste básicamente en examinar, de manera sistemática, todas las posibilidades que podrían hacer falsa una proposición dada y buscar si una de estas posibilidades es lógicamente viable, es decir, que no genera contradicciones; en éste caso se tiene un contraejemplo que refuta la validez de la proposición dada; si no es posible generar un contraejemplo, esto es, ninguna posibilidad resulta lógicamente viable, entonces la proposición analizada es válida. Este método ha encontrado gran aceptación y se ha extendido a muchos sistemas de lógicas no clásicas, además, es fácil de implementar con un programa de computador.

Los árboles de forzamiento semántico, a diferencia de los árboles de opciones semánticas, no exploran todas las opciones posibles cuando se busca el contraejemplo, se limitan a las opciones que son deductivamente forzadas por las reglas del sistema. Por esta razón, el análisis de validez con árboles de forzamiento es en principio más sencillo y natural que con los árboles de opciones.

En este trabajo se presentan los árboles de forzamiento semántico a nivel proposicional para la lógica clásica (CL). Se prueba detalladamente la equivalencia entre la presentación semántica con valuaciones y la presentación con árboles de forzamiento. Esta caracterización permite, por un lado, si una fórmula es inválida, lo cual se concluye si el árbol de la fórmula está bien marcado, entonces la lectura de las marcas de los nodos asociados a las fórmulas atómicas proporciona una valuación que refuta la validez de la fórmula, y, por otro lado, si una fórmula es válida, lo cual se concluye si el árbol está mal marcado o si la raíz forzosamente está marcada con 1, entonces es posible construir una deducción formal con la cual se prueba que la fórmula asociada a la raíz del árbol es un teorema; para lograr esto se cambia cada regla para el forzamiento de marcas por la regla deductiva a la que está asociada.

2 Lenguaje de CL

El lenguaje de la Lógica Clásica (CL) consta de los operadores binarios →, ∧, ∨ y ↔, y del operador monádico ∼, además del paréntesis izquierdo y el paréntesis derecho. El conjunto de fórmulas de CL es generado por las siguientes reglas y sólo por ellas:

R1. Se tiene un conjunto enumerable de fórmulas atómicas.