Uniform Interpolation of Basic Tense Logic

Resumen Técnico: Interpolación Uniforme de la Lógica de Tiempos Básica

Planteamiento del Problema
El artículo aborda el problema abierto de establecer la propiedad de interpolación uniforme para la lógica de tiempos básica (también conocida como lógica modal de dos vías o lógica modal con conversos), denotada como $K_t$. Si bien la propiedad de interpolación de Craig para $K_t$ está bien establecida mediante métodos tanto de la teoría de la prueba como semánticos, la propiedad de interpolación uniforme —que requiere la existencia de un "interpolante uniforme" $\exists p.\phi$ para cualquier fórmula $\phi$ y variable $p$ tal que $\exists p.\phi$ sea independiente de $p$ y preserve las relaciones de demostrabilidad con todas las fórmulas libres de $p$— no había sido plenamente demostrada para esta lógica. El autor señala que, aunque Visser (1996) proporcionó un argumento semántico para la interpolación uniforme de la lógica modal básica $K$ utilizando bisimulaciones por capas, este resultado no se había extendido a la expansión de tiempos que involucra la modalidad conversa.

Metodología
El artículo emplea un enfoque semántico, extendiendo el argumento modelo-teórico de Visser basado en bisimulaciones por capas (o acotadas) al contexto de la lógica de tiempos. La metodología procede a través de los siguientes pasos:

1. Definiciones y Marco de Trabajo: El autor define la sintaxis y semántica de la lógica de tiempos básica, introduciendo el sistema de Hilbert estándar $H(K_t)$ y la semántica de Kripke con modalidades hacia adelante ($\square$) y hacia atrás ($\blacksquare$). El concepto de bisimulación por capas se adapta para la lógica de tiempos, incorporando condiciones para las transiciones tanto hacia adelante (Forth, Back) como hacia atrás (Forth$^{-1}$, Back$^{-1}$), indexadas por la profundidad modal $n$.
2. Propiedad de Expansión de Bisimulación: Se formula una condición suficiente para que una lógica de tiempos normal $\Lambda_{\mathcal{F}}$ (asociada a una clase de marcos) posea la propiedad de interpolación uniforme. Esta condición, denominada propiedad de expansión de bisimulación, requiere que para cualquier par de modelos señalados $(M_1, w_1)$ y $(M_2, w_2)$ en $\mathcal{F}$, que sean bisimilares hasta la profundidad $n$ sobre un conjunto compartido de variables, exista un modelo intermedio $(N, x)$ en $\mathcal{F}$ que los conecte mediante bisimulaciones sobre los respectivos conjuntos de variables.
3. Construcción del Modelo Intermedio: La contribución técnica central implica demostrar que la clase de todos los marcos ($\mathcal{F}_{all}$) posee la propiedad de expansión de bisimulación. El autor construye un modelo intermedio $N$ tomando la unión disjunta de los dos modelos de entrada y añadiendo un nuevo estado "universal" $T$ conectado a todos los estados. La relación en $N$ se define sobre un espacio producto que involucra los estados de los modelos originales y un índice de "capa", simulando efectivamente los pasos de bisimulación requeridos para satisfacer la propiedad de expansión.
4. Resultados de Transferencia: El artículo investiga la preservación de la propiedad de interpolación uniforme bajo diversas extensiones:
   • Imágenes Espejo: Si una lógica $\Lambda$ es invariante bajo la operación de imagen espejo (intercambio de $\square$ y $\blacksquare$), la propiedad se transfiere a las extensiones por axiomas de imagen espejo.
   • Axiomas Constantes: La propiedad se preserva al añadir fórmulas constantes (fórmulas sin variables proposicionales).
   • Traducción Boxdot: Se muestra que la propiedad se transfiere a la contraparte reflexiva de una lógica a través de la traducción boxdot.
5. Construcción de Contraejemplos: Para demostrar los límites de la propiedad, el artículo analiza la expansión de tiempos de la lógica modal $S4$ (denotada como $S4_t$). Utilizando una construcción de modelo específica (un camino infinito con valores de verdad alternos para una proposición $r$) y un argumento de bisimulación por capas, el autor demuestra que $S4_t$ carece de la propiedad de interpolación uniforme.

Contribuciones y Resultados Clave

• Teorema Principal: El artículo establece que la lógica de tiempos básica mínima $K_t$ posee la propiedad de interpolación uniforme. Esto se logra demostrando que la clase de todos los marcos satisface la propiedad de expansión de bisimulación.
• Caracterización Semántica: Se demuestra que el interpolante uniforme en $K_t$ coincide con un cuantificador de bisimulación. Específicamente, una fórmula $\exists p.\phi$ se cumple en un estado si y solo si existe un modelo bisimilar (donde $p$ se interpreta de forma distinta) en el cual $\phi$ se cumple.
• Extensión a Sublógicas: Se muestra que la propiedad de interpolación uniforme se mantiene para varias extensiones de $K_t$, incluyendo aquellas definidas por axiomas constantes (por ejemplo, la existencia de momentos iniciales/finales) y extensiones invariantes de imagen espejo.
• Fallo en $S4_t$: El artículo demuestra que la expansión de tiempos de $S4$ ($S4_t$) no posee la propiedad de interpolación uniforme. Este resultado extiende los hallazgos previos de Ghilardi y Zawadowski sobre $S4$ al entorno de los tiempos, mostrando que la adición de los axiomas de reflexividad y transitividad rompe la propiedad de interpolación uniforme.
• Mecanismos de Transferencia: El autor proporciona pruebas formales para la transferencia de la propiedad de interpolación uniforme mediante imágenes espejo, extensiones constantes y la traducción boxdot, permitiendo la derivación de resultados para lógicas como $K_t \oplus T_\square$ y $K_t \oplus 4_\square$ (bajo condiciones específicas).

Significancia
El artículo afirma resolver una brecha significativa en la literatura respecto a las propiedades metalógicas de la lógica de tiempos básica. Al extender el argumento semántico de Visser al entorno de la modalidad de dos vías, el autor confirma que $K_t$ goza de la propiedad de interpolación uniforme, un resultado que era previamente desconocido a pesar del uso generalizado de esta lógica en la filosofía, la informática y la semántica formal. El trabajo clarifica la frontera entre las lógicas que poseen esta fuerte propiedad de interpolación (como $K_t$) y aquellas que no la poseen (como $S4_t$), proporcionando un marco semántico robusto (bisimulaciones por capas) para analizar la interpolación en lógicas de tiempos. Además, el artículo sugiere que el interpolante uniforme en $K_t$ puede entenderse semánticamente como una versión temporal de un cuantificador de bisimulación, ofreciendo una comprensión conceptual más profunda de su poder expresivo. Los resultados también sientan las bases para futuras investigaciones sobre la interpolación de Lyndon uniforme y la aplicación de estas técnicas a las lógicas de tiempos multimodales e híbridas.