En lógica matemática , el marco hipersecuente es una extensión del marco teórico de prueba de los cálculos secuenciales utilizado en la teoría de prueba estructural para proporcionar cálculos analíticos para lógicas que no se capturan en el marco secuencial. Un hypersequent lo general se toma para ser una finita conjunto múltiple de corrientes secuentes , escrito
Los secuentes que componen un hipersecuente se denominan componentes. La expresividad adicional del marco hipersecuente es proporcionada por reglas que manipulan diferentes componentes, como la regla de comunicación para la lógica intermedia LC (abajo a la izquierda) o la regla de división modal para la lógica modal S5 (abajo a la derecha): [1]
Los cálculos hipersecuentes se han utilizado para tratar lógicas modales , lógicas intermedias y lógicas subestructurales . Los hipersecuentes suelen tener una interpretación de fórmula, es decir, se interpretan mediante una fórmula en el lenguaje del objeto, casi siempre como una especie de disyunción. La interpretación precisa de la fórmula depende de la lógica considerada.
Definiciones formales y reglas proposicionales
Formalmente, un hypersequent lo general se toma para ser una finita conjunto múltiple de corrientes secuentes , escrito
Los secuentes que componen un hipersecuente consisten en tuplas de conjuntos múltiples de fórmulas y se denominan componentes del hipersecuente. También se consideran las variantes que definen hipersecuentes y secuentes en términos de conjuntos o listas en lugar de multijuegos, y dependiendo de la lógica considerada, los secuentes pueden ser clásicos o intuicionistas. Las reglas para los conectivos proposicionales generalmente son adaptaciones de las reglas secuenciales estándar correspondientes con un lado adicional hipersecuente, también llamado contexto hipersecuente. Por ejemplo, un conjunto común de reglas para el conjunto funcionalmente completo de conectivos.para la lógica proposicional clásica viene dada por las siguientes cuatro reglas:
Debido a la estructura adicional en la configuración hipersecuente, las reglas estructurales se consideran en sus variantes internas y externas. Las reglas de debilitamiento interno y contracción interna son las adaptaciones de las reglas secuenciales correspondientes con un contexto hipersecuente agregado:
Las reglas de debilitamiento externo y contracción externa son las reglas correspondientes en el nivel de componentes hipersecuentes en lugar de fórmulas:
La solidez de estas reglas está estrechamente relacionada con la interpretación de la fórmula de la estructura hipersecuente, casi siempre como alguna forma de disyunción . La interpretación precisa de la fórmula depende de la lógica considerada; consulte algunos ejemplos a continuación.
Ejemplos principales
Lógicas modales
Se han utilizado hipersecuentes para obtener cálculos analíticos para lógicas modales , para lo cual los cálculos secuenciales analíticos resultaron elusivos. En el contexto de la lógica modal, la interpretación de la fórmula estándar de un hipersecuente
es la formula
Aquí si es el multiset nosotros escribimos por el resultado de prefijar cada fórmula en con , es decir, el multiset . Tenga en cuenta que los componentes individuales se interpretan utilizando la interpretación de la fórmula estándar para los secuentes y la barra hipersecuentese interpreta como una disyunción de cajas. El mejor ejemplo de una lógica modal para la que las hipersecuentes proporcionan un cálculo analítico es la lógica S5 . En un cálculo hipersecuente estándar para esta lógica [1], la interpretación de la fórmula es la anterior, y las reglas proposicionales y estructurales son las de la sección anterior. Además, el cálculo contiene las reglas modales
La admisibilidad de una versión adecuadamente formulada de la regla de corte puede demostrarse mediante un argumento sintáctico sobre la estructura de las derivaciones o mostrando la completitud del cálculo sin la regla de corte utilizando directamente la semántica de S5. De acuerdo con la importancia de la lógica modal S5, se han formulado varios cálculos alternativos. [2] [3] [1] [4] [5] [6] [7] También se han propuesto cálculos hipersecuentes para muchas otras lógicas modales. [6] [7] [8] [9]
Lógicas intermedias
Los cálculos hipersecuentes basados en secuencias intuicionistas o sucesivas únicas se han utilizado con éxito para capturar una gran clase de lógicas intermedias , es decir, extensiones de la lógica proposicional intuicionista . Dado que las hipersecuentes en esta configuración se basan en secuencias sucesivas únicas, tienen la siguiente forma:
La interpretación de la fórmula estándar para tal hipersecuente es
La mayoría de los cálculos hipersecuentes para lógicas intermedias incluyen las versiones de un solo sucesor de las reglas proposicionales dadas anteriormente, una selección de las reglas estructurales. Las características de una lógica intermedia particular se capturan principalmente mediante una serie de reglas estructurales adicionales . Por ejemplo, el cálculo estándar para LC lógica intermedia , a veces también llamado lógica de Gödel-Dummett, contiene además la llamada regla de comunicación: [1]
Se han introducido cálculos hipersecuentes para muchas otras lógicas intermedias, [1] [10] [11] [12] y hay resultados muy generales sobre la eliminación de cortes en dichos cálculos. [13]
Lógicas subestructurales
En cuanto a las lógicas intermedias, las hipersecuentes se han utilizado para obtener cálculos analíticos para muchas lógicas subestructurales y lógicas difusas . [1] [13] [14]
Historia
La estructura hipersecuente parece haber aparecido primero en [2] bajo el nombre de cortege para obtener un cálculo para la lógica modal S5 . Parece haber sido desarrollado independientemente en, [3] también para el tratamiento de lógicas modales, y en las influyentes, [1] donde se consideran los cálculos para lógicas modales, intermedias y subestructurales, y se introduce el término hipersecuente.
Referencias
- ↑ a b c d e f g Avron, Arnon (1996). El método de las hipersecuentes en la teoría de la prueba de la lógica proposicional no clásica . Lógica: de los cimientos a las aplicaciones . págs. 1-32. ISBN 978-0-19-853862-2.
- ^ a b Mentas, Grigori (1971). "Sobre algunos cálculos de lógica modal". Proc. Steklov Inst. De Matemáticas . 98 : 97-122.
- ^ a b Pottinger, Garrell (1983). "Formulaciones uniformes y sin cortes de T, S4 y S5 (resumen)". J. Symb. Entrar . 48 (3): 900.
- ^ Poggiolesi, Francesca (2008). "Un cálculo secuencial simple sin cortes para la lógica modal S5" (PDF) . Rev. Symb. Entrar . 1 : 3-15. doi : 10.1017 / S1755020308080040 .
- ^ Restall, Greg (2007). Dimitracopoulos, Costas; Newelski, Ludomir; Normann, Dag; Steel, John R (eds.). "Proofnets para S5: Secuencias y circuitos para lógica modal". Coloquio de lógica 2005 . Notas de clase en lógica. 28 : 151-172. doi : 10.1017 / CBO9780511546464.012 . hdl : 11343/31712 . ISBN 9780511546464.
- ^ a b Kurokawa, Hidenori (2014). "Cálculos hipersecuentes para lógicas modales que extienden S4". Nuevas fronteras en inteligencia artificial . Apuntes de conferencias en informática. 8417 . págs. 51–68. doi : 10.1007 / 978-3-319-10061-6_4 . ISBN 978-3-319-10060-9.
- ^ a b Lahav, Ori (2013). "De las propiedades del marco a las reglas hipersecuentes en lógicas modales". 2013 28º Simposio Anual ACM / IEEE sobre Lógica en Ciencias de la Computación . págs. 408–417. doi : 10.1109 / LICS.2013.47 . ISBN 978-1-4799-0413-6. S2CID 221813 .
- ^ Indrzejczak, Andrzej (2015). "Eliminabilidad de corte en cálculos hipersecuentes para algunas lógicas modales de marcos lineales". Cartas de procesamiento de información . 115 (2): 75–81. doi : 10.1016 / j.ipl.2014.07.002 .
- ^ Lellmann, Björn (2016). "Reglas hipersecuentes con contextos restringidos para lógicas modales proposicionales" . Theor. Computación. Sci . 656 : 76-105. doi : 10.1016 / j.tcs.2016.10.004 .
- ^ Ciabattoni, Agata ; Ferrari, Mauro (2001). "Cálculos hipersecuentes para algunas lógicas intermedias con modelos de Kripke acotados". J. Log. Computación . 11 (2): 283-294. doi : 10.1093 / logcom / 11.2.283 .
- ^ Ciabattoni, Agata ; Maffezioli, Paolo; Spendier, Lara (2013). Galmiche, Didier; Larchey-Wendling, Dominique (eds.). "Cálculos hipersecuentes y etiquetados para lógicas intermedias". Tableaux 2013 : 81–96.
- ^ Baaz, Matthias; Ciabattoni, Agata ; Fermüller, Christian G. (2003). "Cálculos hipersecuentes para las lógicas de Gödel - una encuesta". J. Log. Computación . 13 (6): 835–861. doi : 10.1093 / logcom / 13.6.835 .
- ^ a b Ciabattoni, Agata ; Galatos, Nikolaos; Terui, Kazushige (2008). "De axiomas a reglas analíticas en lógicas no clásicas". 2008 23º Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación . págs. 229-240. CiteSeerX 10.1.1.405.8176 . doi : 10.1109 / LICS.2008.39 . ISBN 978-0-7695-3183-0. S2CID 7456109 .
- ^ Metcalfe, George; Olivetti, Nicola; Gabbay, Dov (2008). Teoría de la prueba para lógicas difusas . Springer, Berlín.