Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Resumen Técnico: Unificación de Sistemas de Secuentes para la Lógica de la Provabilidad de Gödel-Löb

Planteamiento del Problema
El artículo aborda una brecha significativa en la teoría de la prueba de la lógica de la provabilidad de Gödel-Löb (GL). Si bien GL posee una rica variedad de formalismos de tipo secuente libres de corte, las relaciones entre ellos no se habían establecido completamente. Específicamente, trabajos previos habían establecido correspondencias proof-teóricas entre:

1. Sistemas estructurales: el sistema de secuentes etiquetados de Negri ($G3KGL$) y el sistema de hipersecuentes de árbol de Poggiolesi ($CSGL^*$), a través de Goré y Ramanayake.
2. Generalizaciones de la estructura de la prueba: el sistema de Gentzen de Sambin y Valentini ($GL_{seq}$), el sistema no bien fundado de Shamkanov ($GL_\infty$) y el sistema cíclico de Shamkanov ($GL_{circ}$), a través de Shamkanov.

Sin embargo, la inter-translatabilidad de las pruebas entre los sistemas estructurales ($G3KGL$, $CSGL^*$) y las generalizaciones de la estructura de la prueba ($GL_{seq}$, $GL_\infty$, $GL_{circ}$) seguía siendo un problema abierto. La dificultad inherente radica en transformar pruebas que utilizan secuentes estructurales complejos (grafos o árboles de secuentes de Gentzen) en pruebas que utilizan secuentes de Gentzen estándar, un proceso que requiere "despojarse" de este dato estructural adicional.

Metodología
El autor, Tim S. Lyon, resuelve este problema abierto construyendo una cadena de transformaciones sintácticas de pruebas que cierran la brecha entre estos distintos formalismos. La metodología procede en tres fases principales:

1. Reestructuración a la Forma End-Active: El artículo demuestra primero cómo reestructurar las pruebas en el sistema de hipersecuentes de árbol $CSGL^*$ en una forma "end-active" (activa al final). En una prueba end-active, las fórmulas principal y auxiliares de las reglas de inferencia ocurren únicamente en las (pre-)hojas de la estructura de árbol-secuente. Esto se logra permutando las reglas no end-active hacia abajo a través del árbol de la prueba, aprovechando la invertibilidad preservadora de la altura de las reglas en $CSGL^*$.

2. Linealización: Se introduce una novedosa "técnica de linealización" para transformar estas pruebas de árbol-secuente end-active en pruebas utilizando secuentes anidados lineales. Esta técnica implica identificar caminos específicos desde la raíz hasta una hoja en el árbol-secuente y "podar" los sub-árboles, efectivamente colapsando la estructura de árbol en una secuencia lineal de secuentes de Gentzen. Este proceso produce un nuevo cálculo, LNGL (Cálculo de Secuentes Anidados Lineales para GL).

3. Forma Normal y Traducción a Gentzen: El artículo muestra que las pruebas en LNGL pueden transformarse en una forma normal específica. En esta forma, las pruebas proceden en etapas repetitivas: reglas locales, seguidas de reglas de propagación ($4L$ y $\Box L$), y finalmente la regla modal ($\Box R$). Esta estructura de prueba es luego traducida al sistema de Gentzen de Sambin y Valentini ($GL_{seq}$). Finalmente, transformaciones estándar mapean las pruebas de $GL_{seq}$ de vuelta al sistema etiquetado $G3KGL$ y a los sistemas cíclicos/no bien fundados ($GL_{circ}$, $GL_\infty$).

Contribuciones Clave

• Nuevo Cálculo (LNGL): El artículo introduce LNGL, el primer cálculo de secuentes anidados lineales libre de corte para la lógica de Gödel-Löb. Este sistema opera sobre líneas de secuentes de Gentzen y retiene propiedades fundamentales como la invertibilidad y la admisibilidad del corte.
• Novedosa Técnica de Linealización: El autor presenta un método general para extraer sistemas de secuentes anidados lineales a partir de sistemas de hipersecuentes de árbol. Se conjetura que esta técnica es aplicable a otras lógicas modales y relacionadas para generar nuevos sistemas anidados lineales.
• Correspondencia Proof-Teórica Completa: El trabajo establece una completa correspondencia sintáctica de seis vías entre los siguientes sistemas: $G3KGL$, $CSGL^*$, $LNGL$, $GL_{seq}$, $GL_\infty$ y $GL_{circ}$.
• Mapeos Constructivos: El trabajo proporciona la primera correspondencia de mapeo constructivo entre sistemas estructurales (etiquetados, hipersecuentes de árbol, anidados lineales) y el sistema de secuentes cíclicos ($GL_{circ}$).

Resultos
El resultado principal es la demostración de que las pruebas en cualquiera de los seis sistemas de secuentes principales para GL pueden transformarse sintácticamente en pruebas en cualquiera de los otros. Específicamente:

• Las pruebas en $CSGL^*$ pueden transformarse en pruebas end-active, y luego linealizarse en LNGL.
• Las pruebas en LNGL pueden normalizarse y transformarse en $GL_{seq}$.
• Las pruebas en $GL_{seq}$ pueden transformarse en $G3KGL$ y en los sistemas cíclicos ($GL_{circ}$, $GL_\infty$).
• El artículo confirma que $LNGL$ es sólido y completo para GL, y que las pruebas en $LNGL$ pueden ponerse en una forma normal donde las aplicaciones de reglas modales y locales se repiten por etapas.

Significancia
El artículo afirma "completar el panorama" de las correspondencias proof-teóricas para la lógica de Gödel-Löb. Al establecer estas transformaciones sintácticas, el trabajo permite la transferencia de resultados (como propiedades de interpolación o límites de complejidad) entre sistemas sin requerir pruebas independientes en cada formalismo. Además, la introducción de LNGL proporciona una nueva herramienta para la búsqueda de pruebas con propiedades de complejidad óptimas, mientras que la técnica de linealización ofrece una vía potencial para generar sistemas anidados lineales para otras lógicas. El trabajo también proporciona el primer mapeo constructivo entre sistemas estructurales y pruebas cíclicas, cerrando una brecha entre diferentes enfoques para el manejo del razonamiento inductivo/coinductivo en la lógica modal.