Sobre la representación de S4.3

Abstract

En 1935 Gerhard Gentzen introdujo un formalismo sintáctico para representar lógicas llamado Cálculo de Secuentes. El mismo es adecuado para analizar propiedades de la lógica, facilita un conocimiento más profundo del comportamiento individual de cada uno de los operadores de la misma y en muchos casos se puede usar para implementar un demostrador de teoremas para la misma, todo esto a través del estudio de las pruebas que en ese sistema deductivo pueden construirse. Una de las reglas de inferencia del Cálculo de Secuentes es de particular importancia en el estudio de propiedades metalógicas, la regla de Corte. Esta incorpora dentro del cálculo el uso de lemas. Los lemas son útiles para demostrar nuevos teoremas rápidamente, pero desde un punto de vista metalógico estamos interesados en estudiar pruebas sin elementos redundantes. Es fundamental entonces que un cálculo permita la construcción de una prueba sin aplicaciones de la regla de Corte para cada teorema. Esta propiedad se conoce como Propiedad de Eliminación de la Regla de Corte y trae como corolario propiedades tan importantes como consistencia, decidibilidad, interpolación, etc. Así, cualquier estudio relativo a una lógica tiene en cuenta la formulación de un Cálculo de Secuentes asociado como metodología básica para la comprensión de la misma. Las lógicas modales no constituyen una excepción. En este trabajo analizamos el Cálculo de Secuentes de S4.3, una lógica modal particular. Esta lógica también es una lógica temporal en el sentido que puede usarse para razonar sobre aserciones basadas en el tiempo, lineal y continuo. En la literatura encontramos un solo Cálculo de Secuentes (al estilo Gentzen, o a la Gentzen) para S4.3. Este cálculo presenta ciertas diferencias significativas respecto a aquellos formulados originalmente por Gentzen (llámense representaciones standard). Específicamente, una de las reglas de inferencia correspondiente al operador necesidad es complicada y su escritura en el formalismo resulta intrincada. Sin embargo, es importante destacar que esta representación goza de la Propiedad de Elimi- nación de la Regla de Corte. Surge entonces la siguiente pregunta. ¿ Habrá una representación standard para S4.3 que goce de la Propiedad de Eliminación de la Regla de Corte ? Formalizando la noción de representación standard dentro de las representaciones a la Gentzen, veremos que si aceptamos cierta conjetura que se expone en el capítulo 3, tal cálculo es imposible de obtener. Esto nos lleva a estudiar un formalismo alternativo para representar lógicas modales que altera la definición de secuente en el sentido que incorpora la noción de verdad relativa dentro de las reglas. Este formalismo fue originalmente definido para representar lógicas modales intuicionistas de modo que debemos alterar las definiciones básicas de forma de poder trabajar en un marco clásico. Usando este formalismo obtenemos un cálculo para S4.3 que goza de la Propiedad de Eliminación de la Regla de Corte y cuyas reglas son intuitivamente sencillas. Es importante notar que la demostración de la Propiedad de eliminación de la Regla de Corte es sintáctica. Además, el formalismo tiene otras ventajas. El uso del cálculo es ameno y natural, en numerosos ejemplos se verá que la construcción de pruebas en el cálculo es muy sencilla e intuitiva. Además se logra una independencia de las reglas de introducción de los operadores modales. De hecho, de el cálculo para S4.3 se puede extraer un cálculo para S4 sin modificar las reglas de introducción para los operadores modales. Sencillamente se quita del cálculo una regla que "exige" la propiedad de conexión sobre la relación de accesibilidad de los modelos de Kripke de la lógica.