En lógica , un compañero modal de una lógica superintuicionista (intermedia) L es una lógica modal normal que interpreta L mediante una determinada traducción canónica, que se describe a continuación. Los compañeros modales comparten varias propiedades de la lógica intermedia original , lo que permite estudiar la lógica intermedia utilizando herramientas desarrolladas para la lógica modal.
Traducción de Gödel – McKinsey – Tarski
Sea A una fórmula intuicionista proposicional . Una fórmula modal T ( A ) se define por inducción sobre la complejidad de A :
- para cualquier variable proposicional,
Como la negación está en la lógica intuicionista definida por , también tenemos
T se denomina traducción Gödel o Gödel - McKinsey - Tarski traducción . La traducción a veces se presenta de formas ligeramente diferentes: por ejemplo, se puede insertarantes de cada subfórmula. Todas estas variantes son probablemente equivalentes en S4 .
Compañeros modales
Para cualquier lógica modal normal M que extiende S4 , definimos su fragmento si ρM como
El fragmento si de cualquier extensión normal de S4 es una lógica superintuicionista. Una lógica modal M es una compañera modal de una lógica superintuicionista L si.
Toda lógica superintuicionista tiene compañeros modales. El compañero modal más pequeño de L es
dónde denota cierre normal. Se puede demostrar que toda lógica superintuicionista también tiene un compañero modal más grande , que se denota por σL . Una lógica modal M es compañera de L si y solo si.
Por ejemplo, el propio S4 es el compañero modal más pequeño de la lógica intuicionista ( IPC ). El compañero modal más grande del IPC es la Grzegorczyk lógica grz , axiomatizada por el axioma
sobre K . El compañero modal más pequeño de la lógica clásica ( CPC ) es el S5 de Lewis , mientras que su compañero modal más grande es la lógica
Más ejemplos:
L | τL | σL | otros compañeros de L |
---|---|---|---|
IPC | S4 | Grz | S4.1 , Dum , ... |
KC | S4.2 | Grz.2 | S4.1.2 , ... |
LC | S4.3 | Grz.3 | S4.1.3 , S4.3Dum , ... |
CPC | S5 | Triv | vea abajo |
Isomorfismo de Blok-Esakia
El conjunto de extensiones de una lógica superintuitionistic L ordenado por formas de inclusión de un retículo completo , denotado Ext L . Del mismo modo, el conjunto de extensiones normales de una lógica modal M es un enrejado completa Siguiente M . Los operadores acompañantes ρM , τL y σL se pueden considerar como asignaciones entre las celosías Ext IPC y NExt S4 :
Es fácil ver que los tres son monótonos yes la función de identidad en Ext IPC . L. Maksimova y V. Rybakov han demostrado que ρ , τ y σ son homomorfismos reticulares completos , de unión-completa y de reunión-completa, respectivamente. La piedra angular de la teoría de los compañeros modales es el teorema de Blok-Esakia , probado de forma independiente por Wim Blok y Leo Esakia . Afirma
- Las asignaciones ρ y σ son isomorfismos de celosía mutuamente inversos de Ext IPC y NExt Grz .
En consecuencia, σ y la restricción de ρ a NExt Grz se denominan isomorfismo de Blok-Esakia . Un corolario importante del teorema de Blok-Esakia es una descripción sintáctica simple de los compañeros modales más grandes: para cada lógica superintuicionista L ,
Descripción semántica
La traducción de Gödel tiene una contraparte de la teoría del marco. Dejarser un marco general modal transitivo y reflexivo . El preorden R induce la relación de equivalencia
en F , que identifica puntos pertenecientes al mismo grupo. Dejarser el orden parcial del cociente inducido (es decir, ρF es el conjunto de clases de equivalencia de), y pon
Luego es un marco general de intuitionistic, llamado el esqueleto de F . El punto de la construcción del esqueleto es que conserva la validez de la traducción módulo Gödel: para cualquier fórmula intuicionista A ,
- A es válida en ρ F si y sólo si T ( A ) es válida en F .
Por lo tanto, el fragmento si de una lógica modal M se puede definir semánticamente: si M es completo con respecto a una clase C de marcos generales reflexivos transitivos, entonces ρM está completo con respecto a la clase.
Los compañeros modales más grandes también tienen una descripción semántica. Para cualquier marco general intuicionista, sea σV el cierre de V bajo operaciones booleanas ( intersección binaria y complemento ). Se puede demostrar que σV está cerrado bajo, por lo tanto es un marco modal general. El esqueleto de σ F es isomorfo a F . Si L es una lógica superintuicionista completa con respecto a una clase C de marcos generales, entonces su compañera modal más grande σL está completa con respecto a.
El esqueleto de un marco Kripke es en sí mismo un marco Kripke. Por otro lado, σ F nunca es un marco de Kripke si F es un marco de Kripke de profundidad infinita.
Teoremas de preservación
El valor de los compañeros modales y el teorema de Blok-Esakia como herramienta para la investigación de lógicas intermedias proviene del hecho de que muchas propiedades interesantes de las lógicas se conservan mediante algunas o todas las asignaciones ρ , σ y τ . Por ejemplo,
- la decidibilidad se conserva mediante ρ , τ y σ ,
- La propiedad del modelo finito se conserva mediante ρ , τ y σ ,
- la tabularidad se conserva mediante ρ y σ ,
- La integridad de Kripke se conserva mediante ρ y τ ,
- La definibilidad de primer orden en las tramas de Kripke se conserva mediante ρ y τ .
Otras propiedades
Cada lógica intermedia L tiene un número infinito de compañeros modales y, además, el conjuntode compañeros modales de L contiene una cadena descendente infinita . Por ejemplo,consta de S5 , y las lógicaspara cada entero positivo n , dondees el grupo de n elementos. El conjunto de compañeros modales de cualquier L es contable o tiene la cardinalidad del continuo . Rybakov ha demostrado que la celosía Ext L se puede incrustar en; en particular, una lógica tiene un continuo de compañeros modales si tiene un continuo de extensiones (esto es válido, por ejemplo, para todas las lógicas intermedias por debajo de KC ). Se desconoce si lo contrario también es cierto.
La traducción de Gödel se puede aplicar tanto a reglas como a fórmulas: la traducción de una regla
es la regla
Una regla R es admisible en una lógica L si el conjunto de teoremas de L es cerrado bajo R . Es fácil ver que R es admisible en una lógica superintuitionistic L cuando T ( R ) es admisible en un compañero modal de L . Lo contrario no es cierto en general, pero tiene la mayor modal del compañero L .
Referencias
- Alexander Chagrov y Michael Zakharyaschev, Modal Logic , vol. 35 de Oxford Logic Guides, Oxford University Press, 1997.
- Vladimir V. Rybakov, Admisibilidad de las reglas de inferencia lógica , vol. 136 de Estudios de lógica y fundamentos de las matemáticas, Elsevier, 1997.