Four intuitionistic modal connectives

Resumen Técnico: Cuatro Conectivas Modales Intuicionistas

Planteamiento del Problema
El artículo aborda la semántica fundacional y la axiomatización de las Lógicas Modales Intuicionistas (LMI). Tradicionalmente, las LMI interpretan las conectivas modales dentro de estructuras relacionales $(W, \leq, R, V)$, donde $\leq$ es un preorden y $R$ es una relación binaria. Existe una tensión central entre dos grandes escuelas de pensamiento respecto al operador de posibilidad:

1. El enfoque de Fischer Servi: Define la posibilidad ($\diamond_{FS}$) tal que $s \models \diamond_{FS} A$ si y solo si existe un $t$ tal que $sRt$y$t \models A$. Este enfoque típicamente requiere restringir la clase de modelos a marcos "confluentes hacia adelante y hacia atrás" para satisfacer la Propiedad de Hereditariedad (monotonicidad con respecto a $\leq$).
2. El enfoque de Wijesekera: Define la posibilidad ($\diamond_{W}$) tal que $s \models \diamond_{W} A$ si y solo si para todo $t \geq s$, existe un $u$ tal que $tRu$y$u \models A$. Este enfoque no requiere estrictamente la confluencia para que la Propiedad de Hereditariedad se cumpla.

Los autores argumentan que limitar la discusión a modelos confluentes (como hace Fischer Servi) es una elección arbitraria que privilegia una variante de la Lógica de Primer Orden Intuicionista sobre otras. Además, señalan que la traducción estándar de las LMI a la lógica de primer orden a menudo falla en capturar la semántica pretendida si se restringe únicamente a modelos confluentes. Por consiguiente, el artículo busca establecer un marco unificado que incorpore cuatro conectivas modales distintas sin restringir la clase de marcos a priori, explorando así todo el panorama de las modalidades intuicionistas.

Metodología
Los autores emplean una combinación rigurosa de semántica relacional, teoría de correspondencia, sistemas de prueba algebraicos y técnicas de modelos:

1. Sintaxis y Semántica:

   • Introducen un lenguaje que contiene las conectivas intuicionistas estándar ($\to, \top, \bot, \lor, \land$) y una implicación/co-implicación dual ($\leftarrow$).
   • Se definen cuatro operadores modales:
     • $\Diamond$ (Posibilidad estilo Přenosil): $s \models \Diamond A$ si y solo si $\exists t \leq s, \exists u (tRu \land u \models A)$.
     • $\Box$ (Necesidad estilo Fischer Servi): $s \models \Box A$ si y solo si $\forall t \geq s, \forall u (tRu \to u \models A)$.
     • $\Diamond$ (Posibilidad estilo Wijesekera): $s \models \Diamond A$ si y solo si $\forall t \geq s, \exists u (tRu \land u \models A)$.
     • $\blacksquare$ (Necesidad dual): $s \models \blacksquare A$ si y solo si $\exists t \leq s, \forall u (tRu \to u \models A)$.
   • La semántica se define sobre la clase de todos los marcos (sin restricciones de confluencia), y se demuestra que la Propiedad de Hereditariedad se cumple para todas las fórmulas bajo estas definiciones.

2. Teoría de Correspondencia:

   • El artículo investiga la definibilidad modal de clases elementales de marcos (ej. serial, reflexivo, simétrico, transitivo, confluente).
   • Utiliza fórmulas con signo y reglas de inferencia para caracterizar propiedades de los marcos.
   • Emplea la "Propiedad de Relativización" de la teoría de modelos para probar la indecidibilidad del problema de definibilidad modal para ciertas clases de marcos.

3. Axiomatización y Completitud:

   • Se presenta un sistema de estilo Hilbert utilizando conjuntos de fórmulas con signo (positivas y negativas), cerrados bajo sustitución uniforme y reglas de inferencia específicas (incluyendo reglas para la implicación dual y la interacción de las modalidades).
   • Los autores construyen un Modelo Canónico utilizando "clips balanceados" (tripletas que consisten en un filtro primo, un ideal primo y fórmulas auxiliares). Esta construcción es necesaria para manejar las complejas interacciones entre las cuatro modalidades y la implicación dual.
   • Se prueban teoremas de completitud para la lógica mínima y sus extensiones correspondientes a clases de marcos específicas (reflexivo, serial, confluencia hacia adelante/hacia abajo).

4. Decidibilidad:

   • Para probar la decidibilidad, los autores embeben la LMI mínima en el Fragmento Guardado Monádico de Dos Variables de la Lógica de Primer Orden Clásica.
   • Definen funciones de traducción que mapean fórmulas intuicionistas a fórmulas de primer orden guardadas, aprovechando la decidibilidad conocida del fragmento guardado.

Contribuciones Clave y Resultados

• Marco Unificado: El artículo integra con éxito cuatro conectivas modales distintas ($\Diamond, \Box, \Diamond, \blacksquare$) en un único marco intuicionista, demostrando que no son interdefinibles sobre la clase de todos los marcos.
• Análisis de Eliminabilidad: Se muestra que, sobre la clase de marcos confluentes hacia adelante y hacia abajo ($C_{fd}$), las cuatro conectivas son eliminables (interdefinibles). Sin embargo, sobre clases más amplias (como $C_{bdu}$), son distintas.
• Resultados de Correspondencia:
  • Las clases de marcos confluentes hacia adelante ($C_f$) y hacia abajo ($C_d$) son positivamente definibles.
  • Las clases de marcos reflexivos ($C_{ref}$), simétricos ($C_{sym}$), transitivos ($C_{tra}$), euclidianos ($C_{Euc}$) y deterministas ($C_{det}$) no son modalmente definibles con respecto a la clase de todos los marcos (o subclases específicas como $C_{fbdu}$).
  • Las clases de marcos confluentes hacia atrás ($C_b$) y hacia arriba ($C_u$) no son modalmente definibles con respecto a $C_{fd}$.
• Axiomatización: El artículo proporciona axiomatizaciones completas para la lógica mínima ($L_{min}$) y sus extensiones correspondientes a las propiedades de reflexividad, serialidad y confluencia. La lógica mínima resulta ser la lógica de todos los marcos.
• Decidibilidad: Se prueba que el problema de membresía para la lógica modal intuicionista mínima ($L_{min}$) y varias de sus extensiones (reflexiva, serial, confluente) es decidible. Esto se logra reduciendo el problema a la satisfacibilidad del Fragmento Guardado Monádico de Dos Variables.
• Indecidibilidad de la Definibilidad: El artículo demuestra que los problemas de decisión para determinar si una clase elemental de marcos es modal, positiva o negativamente definible son indecidibles.

Significancia y Reivindicaciones
Los autores afirman que su trabajo proporciona una base más natural y menos restrictiva para las LMI al evitar la limitación arbitraria a los modelos confluentes. Al introducir la implicación dual y las cuatro conectivas modales, ofrecen un lenguaje simétrico y exhaustivo que captura el rango completo de los comportos modales intuicionistas.

El artículo señala modestamente que, aunque se establece la decidibilidad de la lógica mínima, la clase de complejidad de este problema sigue siendo una cuestión abierta. Además, los autores destacan que, aunque se utilizaron ciertas reglas de inferencia (específicamente $R8+$ y $R8-$) en las pruebas de completitud, actualmente se desconoce si estas reglas pueden ser reemplazadas por un conjunto finito de axiomas. También plantean preguntas abiertas sobre la axiomatizabilidad finita de las lógicas correspondientes a los marcos simétricos y transitivos, así como el potencial de adaptar las técnicas de filtración a este entorno específico.

El trabajo sirve como un paso fundacional para comprender la interacción entre diferentes semánticas modales intuicionistas y sus propiedades de marco correspondientes, yendo más allá de la dicotomía tradicional de Fischer Servi y Wijesekera.