Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

Resumen Técnico: Lógica Modal Monótona Intuicionista: Teoría de la Prueba y Semántica

Planteamiento del Problema
El artículo aborda un vacío en el estudio de la lógica modal monotona intuicionista, específicamente la lógica IM introducida recientemente en [27]. Mientras que la lógica monotona clásica ($M$) está bien estudiada y sustenta sistemas como la lógica de juegos y la lógica de coaliciones, sus contrapartes intuicionistas permanecen menos desarrolladas en comparación con los análogos intuicionistas de las lógicas modales normales (como $K$ y $S4$). El trabajo existente sobre lógicas monótonas intuicionistas incluye CM (modalidades completamente independientes), WM (estilo Wijesekera, que permite cero o una conclusión) e IM (derivada mediante traducción a la lógica de primer orden intuicionista). Sin embargo, IM carecía de un tratamiento de teoría de la prueba dedicado, un estudio sistemático de sus extensiones y resultados básicos de decidibilidad. Además, se requería clarificar la relación entre las variantes constructivas (como $WM$) y las variantes intuicionistas (como $IM$) de la lógica monotona.

Metodología
Los autores emplean un enfoque dual que combina la caracterización semántica y el análisis de la teoría de la prueba:

1. Caracterización Semántica: Los autores definen marcos de vecindad constructivos (derivados de [11]) para proporcionar una semántica para IM y sus extensiones. A diferencia de los modelos de vecindad intuicionistas en [27], estos marcos utilizan un preorden y una función de vecindad que mapea mundos a conjuntos de conjuntos de mundos. Introducen el concepto de marcos continuos para capturar las propiedades específicas de IM. Se utiliza una construcción de modelo canónico usando segmentos (pares de teorías primas y colecciones de conjuntos de teorías) para probar la completitud.

2. Análisis de la Teoría de la Prueba: Los autores desarrollan un cálculo de secuentes libre de corte, $C_{IM}$, para IM. Este cálculo es una adaptación del cálculo estructurado $HM$ para la lógica monotona clásica [14]. Las características estructurales clave incluyen:

   • Fórmulas Marcadas: Las fórmulas se marcan con polaridad de entrada ($\bullet$) o de salida ($\circ$).
   • Bloques: Conectivas estructurales $\{ \Delta \}$ que representan conjuntos de vecindad.
   • Poda de Salida ($\downarrow$): Una operación distintiva en la regla de implicación ($\to^\bullet$) que elimina las fórmulas de salida (y vacía los bloques de salida) al pasar de las premisas a las conclusiones. Esta operación es crucial para capturar el axioma $I3$ ($(2\top \to 3\phi) \to 3\phi$).
   • Extensiones: El cálculo se extiende modularmente para manejar los axiomas $N, P, T, D,$ y $K$ mediante la adición de reglas estructurales específicas (por ejemplo, $n, p, d, t, k$) manteniendo inalteradas las reglas lógicas, adhiriéndose al principio de Dösen.

Contribuciones Clave

1. Completitud Semántica: El artículo proporciona una semántica completa y sólida para IM y sus extensiones con respecto a clases de marcos de vecindad constructivos continuos. Esto difiere del enfoque de traducción a la lógica de primer orden de [27] al ofrecer una semántica modal directa que ayuda a comprender el cálculo de secuentes.
2. Cálculo Libre de Corte ($C_{IM}$): Los autores presentan un cálculo de secuentes terminante y libre de corte para IM. El cálculo simula con éxito los axiomas de IM, particularmente la interacción entre las modalidades a través del axioma $I3$, mediante el mecanismo de la poda de salida.
3. Decidibilidad: Al establecer la propiedad de subfórmula y una condición de detección de bucles para la búsqueda de prueba hacia atrás en $C_{IM}$, los autores prueban que IM es decidible.
4. Relación con $WM$: El artículo demuestra una relación estrecha entre IM y WM. Al modificar la operación de poda de salida en $C_{IM}$ por adelgazamiento de salida (que elimina bloques de salida enteros en lugar de solo vaciarlos), los autores derivan un cálculo $C_{WM}$ para WM. Esto permite una re-demostración de que IM y WM tienen fragmentos 2-libres diferentes, mientras comparten el mismo fragmento 3-libre.
5. Extensiones: El marco se extiende para cubrir las extensiones axiomáticas de IM (incluyendo $N, P, T, D, K$). Para el axioma $K$, el cálculo se generaliza para permitir bloques que contengan multiconjuntos de fórmulas, introduciendo una nueva regla $k$ para dividir bloques.

Resultos

• Completitud: El Teorema 2.14 establece que $\vdash_{IM \oplus Ax} \phi$ si y solo si $\Vdash_{IM \oplus Ax} \phi$ para cualquier subconjunto de axiomas $Ax \subseteq \{N, P, T, D, K\}$.
• Eliminación de Corte: El Teorema 3.12 prueba la admisibilidad del corte (y las reglas de sustitución) en $C_{IM}$, asegurando que el cálculo es analítico.
• Decidibilidad: El Teorema 3.14 confirma que el problema de derivabilidad de IM es decidible.
• Distinción de Fragmentos: El artículo re-confirma que IM y WM difieren en sus fragmentos 2-libres (específicamente respecto a la derivabilidad de $((3\bot \to \bot) \to \bot) \to 3\bot$), mientras comparten el mismo fragmento 3-libre.
• Solidez y Completitud para Extensiones: Los Teoremas 4.4 y 4.14 extienden los resultados de solidez y completitud a todas las extensiones axiomáticas consideradas, incluyendo aquellas con el axioma $K$.

Significancia
El artículo afirma llenar el vacío en el estudio de la teoría de la prueba y la semántica de IM. Al proporcionar un cálculo libre de corte, establece a IM como una lógica bien comportada con un problema de derivabilidad decidible. Un hallazgo central es la revelación de una analogía entre las variantes constructivas/intuicionistas de la lógica monotona ($M$) y la lógica normal ($K$):

• Las variantes constructivas (como $WM$) corresponden a restricciones de un solo sucedente de los cálculos de Gentzen estándar.
• Las variantes intuicionistas (como $IM$) corresponden a restricciones de un solo sucedente de cálculos de secuentes estructurados (que involucran bloques y operaciones de poda específicas).

Esta visión estructural justifica a IM como una variante intuicionista fiel de la lógica monotona clásica. Los autores señalan que su trabajo abre interrogantes sobre la generalizabilidad de este patrón a otras lógicas modales y el potencial de extraer contramodelos de derivaciones fallidas, lo cual identifican como direcciones para investigaciones futuras.