Most Properties are Undecidable for Transitive Tense Logics

Resumen Técnico: La mayoría de las propiedades son indecidibles para las lógicas de tiempo transitivas

Planteamiento del problema
El artículo aborda la decidibilidad algorítmica de las propiedades lógicas dentro del retículo de las lógicas de tiempo transitivas, denotado como $NExtK4t$. Si bien la decidibilidad de las propiedades (tales como la completitud de Kripke, la propiedad del modelo finito y la decidibilidad misma) está bien estudiada para las lógicas unimodales y las lógicas de tiempo lineales, el estatus de estas propiedades en la clase intermedia de las lógicas de tiempo transitivas sigue siendo una cuestión abierta crítica. Específicamente, los autores investigan si la interacción natural entre las modalidades del futuro ($\Box$) y del pasado ($\blacksquare$) en los marcos transitivos vuelve indecidible el problema de decisión para estas propiedades. Trabajos previos de Chagrov y Shehtman establecieron la indecidibilidad de la tabularidad y la consistencia en $NExtK4t$, pero la decidibilidad de la completitud de Kripke, la propiedad del modelo finito (FMP) y la decidibilidad general permanecían sin resolver.

Metodología
Los autores adaptan una técnica de reducción originalmente desarrollada por Chagrov para lógicas unimodales, extendiéndola al entorno bimodal de las lógicas de tiempo. El método central consiste en construir una reducción computable de un problema de alcanzabilidad de máquinas de Minsky (un problema conocido como indecidible equivalente al problema de la parada para máquinas de Turing) al problema de decisión para propiedades lógicas específicas.

1. Codificación de la máquina de Minsky: Los autores utilizan una máquina de Minsky $M$ con dos registros y una configuración específica $c_0 = \langle s, n, m \rangle$ tal que el conjunto de configuraciones alcanzables es indecidible.
2. Construcción del marco general: Se construye un marco general específico $\mathcal{F} = (W, R, A)$. El dominio $W$ codifica las configuraciones alcanzables de $M$ junto con puntos auxiliares ($a_i, b_i, c_i$) que representan los valores de los registros y una estructura de "contador". La relación de accesibilidad $R$ se define para simular las transiciones de la máquina de Minsky y las operaciones de incremento/decremento en los registros.
3. Construcción de fórmulas: Los autores definen un conjunto de fórmulas sin variables ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$) que identifican de manera única puntos específicos en el marco $\mathcal{F}$. Además, definen fórmulas $\psi_A, \psi_B$ y sus sucesores para simular las operaciones $+1$ y $-1$ en los registros.
4. Construcción de la lógica: Para cualquier configuración $c = \langle t, k, l \rangle$, se define una lógica $L(c)$ como una extensión de $K4t$. Esta lógica incluye:
   • Axiomas ($Ax_M$) que codifican las reglas de transición de la máquina de Minsky.
   • Un axioma condicional que vincula la configuración inicial con la configuración objetivo $c$.
   • Una fórmula específica $\alpha$ (derivada de una lógica tabular) y una fórmula "trampa" $\phi_0$ diseñada para asegurar que, si la configuración objetivo no es alcanzable, la lógica resultante sea incompleta de Kripke e indecidible.

Contribuciones clave y resultados
El artículo establece un criterio general (Teorema 3.5) para la indecidibilidad de las propiedades en $NExtK4t$. El teorema establece que si una propiedad $P$ está contenida dentro de la unión de la completitud de Kripke ($KC$) y la decidibilidad ($DEC$), y existe una fórmula $\alpha$ tal que $K4t \oplus \alpha \in P$ pero el marco construido $\mathcal{F}$ no valida $\alpha$, entonces $P$ es indecidible.

Aplicando este teorema, los autores demuestran los siguientes resultados (Corolario 3.13):

• Los siguientes conjuntos de fórmulas son indecidibles en $NExtK4t$:
  1. Completitud de Kripke.
  2. Canonicidad.
  3. Definibilidad de primer orden.
  4. La propiedad del modelo finito (FMP).
  5. Tabularidad local.
  6. Tabularidad.
  7. Decidibilidad (de la lógica misma).
  8. Coincidencia con una lógica tabular fija.
  9. Consistencia (específicamente, el complemento, la inconsistencia, es indecidible).

Además, mediante la Proposición 2.2, los autores señalan que, dado que $K4t$ es una extensión de $Kt$ (la lógica de tiempo mínima), estos resultados de indecidibilidad se extienden al retículo $NExtKt$.

Significado y Reivindicaciones
El artículo afirma resolver el estatus de decidibilidad de las principales propiedades para las lógicas de tiempo transitivas, demostrando que "la mayoría de las propiedades son indecidibles" en esta clase. La importancia radica en cómo la interacción de las modalidades afecta la decidibilidad:

• Contraste con el tiempo lineal: Mientras que las propiedades son decidibles en el retículo de los flujos de tiempo lineales ($NExtLint$), la introducción de la transitividad sin linealidad ($NExtK4t$) conduce a la indecidibilidad.
• Contraste con las lógicas unimodales: Los resultados resaltan que el mapa de extensión de tiempo mínimo no preserva propiedades como la completitud de Kripke o la FMP, haciendo que el caso bimodal sea fundamentalmente diferente y más complejo que el caso unimodal ($NExtK4$).
• Esquema General: El artículo proporciona un esquema de prueba general para establecer la indecidibilidad en lógicas de tiempo mediante la reducción de la alcanzabilidad de la máquina de Minsky a las propiedades lógicas, llenando un vacío dejado por trabajos previos que no podían transferir directamente los resultados de indecidibilidad unimodal al entorno de tiempo debido a la no inyectividad del mapa de extensión de tiempo.

Los autores concluyen que las interacciones de las modalidades en las lógicas de tiempo transitivas hacen que el problema de decisión para las propiedades sea estrictamente más difícil que en las lógicas de tiempo lineales y sugieren que, para propiedades como la completitud de Kripke, la indecidibilidad en un retículo unimodal probablemente implica la indecidibilidad en su extensión de tiempo mínima, aunque esto sigue siendo una conjetura para trabajos futuros.