A non-uniform view of Craig interpolation in modal logics with linear frames

Resumen Técnico: Una visión no uniforme de la interpolación de Craig en lógicas modales con marcos lineales

Planteamiento del problema
La Propiedad de Interpolación de Craig (CIP, por sus siglas en inglés) es una propiedad fundamental en la lógica que establece que para cualquier implicación válida $\phi \to \psi$, existe un interpolante $\iota$ que utiliza solo el vocabulario compartido de $\phi$ y $\psi$ tal que $\phi \to \iota$ y $\iota \to \psi$ también son válidas. Es un hecho "negativo" bien establecido que muchas lógicas modales normales que extienden K4.3 (la lógica de los marcos transitivos lineales) carecen de la CIP, particularmente aquellas con profundidades no acotadas. Tradicionalmente, la ausencia de la CIP ha terminado con la investigación de interpolantes para una lógica dada.

Este artículo replantea la ausencia de la CIP como una pregunta de investigación investigando el Problema de Existencia de Interpolantes (IEP): dado dos fórmulas $\phi$ y $\psi$ tales que $\phi \to \psi$ es válida en una lógica $L$, ¿existe un interpolante de Craig en $L$? A diferencia de la CIP uniforme, el IEP no se reduce a una simple comprobación de validez porque la validez de la implicación no garantiza la existencia de un interpolante. La cuestión central abordada es si el IEP es computacionalmente más difícil que el problema de validez (entailment) para estas lógicas. Resultados previos en otras lógicas (por ejemplo, lógicas modales con nominales, fragmentos de la lógica de primer orden) sugirieron que el IEP podría ser significativamente más difícil (por ejemplo, 3ExpTime). Este artículo investiga si esto se cumple para las lógicas modales proposicionales que contienen K4.3.

Metodología
Los autores emplean un enfoque no uniforme y modelo-teórico basado en bisimulaciones y marcos descriptivos.

1. Caracterización por bisimulación: El artículo utiliza un criterio conocido (Teorema 3.2) que establece que $\phi \to \psi$ carece de un interpolante en $L$ si y solo si existen dos modelos, $M_1$ y $M_2$, basados en marcos descriptivos para $L$, tales que $M_1$ satisface $\phi$, $M_2$ satisface $\neg\psi$, y los puntos raíz de estos modelos son $\sigma$-bisimilares (donde $\sigma$ es la firma compartida).
2. Marcos descriptivos: El análisis depende fuertemente de la estructura de los marcos descriptivos (marcos equipados con un álgebra específica de conjuntos internos que satisfacen condiciones de diferenciación, densidad y compacidad). Esto es crucial porque, para lógicas como GL.3 y Log{(N, <)}, los contraejemplos a la CIP no pueden ser testimoniados por marcos de Kripke estándar, sino que requieren marcos descriptivos infinitos.
3. Descomposición estructural: La innovación técnica central involucra el análisis de la estructura de estos modelos bisimilares. Los autores particionan los modelos en $\sigma$-bloques (intervalos de puntos con propiedades de bisimulación específicas) y demuestran que cualquier par de modelos bisimilares que testifique la falta de un interpolante puede transformarse en un par de modelos "cuasi-finitos". Estos modelos se construyen como sumas ordenadas de modelos simples basados en marcos atómicos específicos (cadenas finitas, cúmulos finitos o estructuras de "tadpole" como $C(\bigcirc_k, \bullet)$).
4. Propiedad de cuasi-tamaño polinómico: Para lógicas finitamente axiomatizables, los autores demuestran que estos modelos testigos pueden ser acotados en tamaño por un polinomio en el tamaño de las fórmulas de entrada y los axiomas de la lógica. Esto se denomina la propiedad de modelo bisimilar de cuasi-tamaño polinómico.

Contribuciones clave y resultados

• Decidibilidad y complejidad: El artículo demuestra que para todas las lógicas modales normales finitamente axiomatizables que contienen K4.3, el IEP es decidible y coNP-completo.

  • Este resultado es significativo porque muestra que el IEP no es más difícil que el problema de validez (que también está en coNP para estas lógicas). Esto contrasta fuertemente con los resultados recientes de interpolación no uniforme en otros marcos lógicos donde el IEP es estrictamente más difícil.
  • La prueba involucra un algoritmo no determinista que adivina modelos de tamaño polinómico que satisfacen el criterio de bisimulación y verifica los axiomas de la lógica.

• Propiedad de modelo bisimilar de cuasi-tamaño polinómico: Los autores establecen que todas las extensiones de K4.3 finitamente axiomatizables poseen la "propiedad de modelo bisimilar de cuasi-tamaño polinómico". Esto significa que, si un interpolante no existe, existe un par de modelos bisimilares que testimonian este hecho donde los modelos son sumas ordenadas de un número polinómico de modelos simples basados en marcos atómicos de tamaño polinómico.

  • Para las lógicas de submarco cofinal d-persistentes (una subclase), la propiedad es aún más fuerte: poseen la propiedad de modelo bisimilar de tamaño polinómico, donde los modelos son marcos de Kripke estándar de tamaño polinómico.

• Extensión a lógicas temporales prioreanas: La metodología se extiende a las lógicas temporales prioreanas (que contienen tanto modalidades de futuro como de pasado) sobre flujos de tiempo estándar:

  • Lin (todos los marcos lineales), LinQ (racionales) y LinR (reales): Se demuestra que estas lógicas poseen la propiedad de modelo bisimilar de tamaño polinómico, y su IEP es coNP-completo.
  • Lin<ω (órdenes lineales estrictos finitos) y LinZ (enteros): Estas lógicas no poseen la propiedad de tamaño polinómico pero poseen la propiedad de modelo bisimilar de cuasi-tamaño polinómico. Su IEP también se demuestra como coNP-completo.
  • La prueba para las lógicas temporales requiere el manejo de cadenas bidireccionales y cúmulos límite en ambas direcciones, lo que requiere nuevas construcciones de marcos (por ejemplo, marcos "tadpole" simétricos $C(\bullet, \bigcirc_k, \bullet)$).

Significado y afirmaciones
El artículo afirma proporcionar el primer resultado general sobre la existencia de interpolantes de Craig que cubre una gran familia de lógicas modales (extensiones de K4.3) que carecen de la CIP. Al demostrar que el IEP es coNP-completo para estas lógicas, los autores desafían la intuición de que la ausencia de la CIP conduce necesariamente a una clase de complejidad superior para el problema de existencia.

El trabajo sugiere que la complejidad del IEP no está intrínsecamente ligada al fallo de la CIP, sino que depende de las propiedades estructurales de los modelos requeridos para testimoniar dicho fallo. Los autores posicionan esto como un paso hacia una clasificación de las lógicas modales basadas en la complejidad de su IEP.

El artículo señala explícitamente que su prueba no es constructiva respecto al cálculo de los interpolantes; proporciona un procedimiento de decisión para la existencia, pero no ofrece un algoritmo eficiente para calcular el interpolante en sí mismo o los límites superiores de su tamaño. Los autores también destacan que los marcos descriptivos son esenciales para sus pruebas, planteando la pregunta abierta de si los marcos de Kripke bastan para el IEP en lógicas que no son d-persistentes pero que son fuertemente completas en Kripke (como LinR).