Wider systems for linear logic with fixed points: proof theory and complexity

1. El Problema

La lógica lineal con puntos fijos ($\mu$MALL) es fundamental para formalizar inducción y recursión. Investigaciones anteriores se centraron en sistemas con ramificación $\omega$ (infinita pero numerable), adecuados para modelos continuos donde los operadores alcanzan sus puntos fijos en $\le \omega$ pasos.

Sin embargo, modelos generales (como el cálculo modal $\mu$ o lógicas de primer orden) pueden admitir ordinales de cierre arbitrarios (transfinitos). El problema central abordado en este trabajo es:

• ¿Cuál es la complejidad algorítmica de la demostrabilidad en sistemas de lógica lineal con puntos fijos parametrizados por un ordinal computable arbitrario $\alpha$?
• ¿Cómo se comportan estos sistemas cuando las reglas de inferencia tienen ramificación indexada por ordinales $\beta \le \alpha$?

El objetivo es clasificar la complejidad de la demostrabilidad en el sistema $\mu\text{MALL}_{\alpha,\alpha}$ dentro de la jerarquía hiperaritmética.

2. Metodología

Los autores emplean una combinación de fundamentos de teoría de la prueba y teoría de la complejidad efectiva:

• Sistemas Infinitarios Bien Fundados: Definen el sistema $\mu\text{MALL}_{\alpha,\alpha}$, que extiende la lógica lineal multiplicativa-aditiva (MALL) con reglas de punto fijo $\mu_\beta$ y $\nu_\beta$ para $\beta \le \alpha$. Estas reglas permiten inferencias con un número de premisas indexado por ordinales menores que $\beta$.
• Eliminación de Cortes (Cut-Elimination): Demuestran que cualquier prueba en el sistema puede transformarse en una prueba sin cortes. Esto es crucial para establecer cotas superiores de complejidad, ya que restringe la búsqueda de pruebas a pasos no cortantes.
• Enfoque (Focussing): Desarrollan un sistema enfocado ($\mu\text{MALL}^F_{\alpha,\alpha}$) que organiza la búsqueda de pruebas en fases síncronas (no invertibles, positivas) y asíncronas (invertibles, negativas). Esto reduce drásticamente el espacio de búsqueda de pruebas al imponer una disciplina estricta sobre el orden de aplicación de las reglas.
• Rango de Fórmulas (Formula Rank): Introducen una nueva noción de "rango" para las fórmulas basada en operaciones naturales de ordinales (suma natural $\oplus$ y producto natural $\otimes$). A diferencia de enfoques anteriores que usaban máximos, el uso de sumas naturales permite acotar estrictamente la altura del espacio de búsqueda de pruebas sin cortes.
• Codificación de Computación: Para la cota inferior, codifican máquinas de Minsky (para funciones computables) y sentencias infinitarias computables dentro del sistema lógico, utilizando el mecanismo de "bloqueo" (locking) con proposiciones especiales para simular la evaluación de verdad.

3. Contribuciones Clave

1. Fundamentos de Teoría de la Prueba:

   • Prueban la eliminación de cortes para $\mu\text{MALL}_{\alpha,\alpha}$ para cualquier ordinal $\alpha$.
   • Establecen un teorema de enfoque (focussing) que garantiza que toda prueba tiene una forma normal enfocada.
   • Definen un rango de fórmula preciso que acota la altura de las pruebas sin cortes, demostrando que la búsqueda de pruebas termina.

2. Clasificación de Complejidad:

   • Demuestran que la demostrabilidad en $\mu\text{MALL}_{\alpha,\alpha}$ es completa para el nivel $\omega^{\alpha^\omega}$ de la jerarquía hiperaritmética (bajo reducciones de Turing).
   • Esto generaliza resultados anteriores que solo cubrían el caso $\alpha = \omega$ (que corresponde a $\Sigma^0_{\omega^\omega}$).

3. Análisis de Ordinales Computables:

   • Utilizan la notación de Kleene ($O$) para manejar ordinales computables y definen cómo las operaciones lógicas interactúan con la estructura de estos ordinales, mostrando que la complejidad crece exponencialmente con el ordinal de cierre.

4. Resultados Principales

• Teorema 2.8 (Resultado Principal): Para cualquier ordinal computable $\alpha \ge \omega$, el problema de decisión de demostrabilidad en $\mu\text{MALL}_{\alpha,\alpha}$ es $\Sigma^0_{\omega^{\alpha^\omega}}$-completo.

  • Cota Superior: Se deriva de la propiedad del rango de las fórmulas. La búsqueda de pruebas sin cortes puede modelarse como una definición inductiva de longitud $\omega^{\alpha^\omega}$, lo que sitúa el problema en la clase $\Sigma^0_{\omega^{\alpha^\omega}}$.
  • Cota Inferior: Se logra reduciendo el conjunto de sentencias infinitarias computables verdaderas (completas para cada nivel de la jerarquía hiperaritmética) a la demostrabilidad en el sistema. Se utiliza el teorema de enfoque para demostrar la adecuación de esta codificación.

• Corolario 8.1: Si $\omega \le \alpha < \omega^\omega$, la demostrabilidad es $\Sigma^0_{\omega^{\omega^\omega}}$-completa. Esto implica que todos los sistemas con ordinales de cierre en este rango son Turing-equivalentes en complejidad.

5. Significado e Impacto

• Unificación de Modelos: El trabajo proporciona un marco unificado para entender la complejidad de la lógica con puntos fijos más allá de los modelos continuos ($\omega$), abarcando modelos discretos y transfinitos generales.
• Herramientas de Teoría de Prueba: La introducción de rangos basados en operaciones naturales de ordinales ofrece una herramienta técnica potente para analizar sistemas infinitarios, superando las limitaciones de los métodos basados en tamaño de fórmula o máximos.
• Límites de la Computabilidad: El resultado establece un límite preciso de la complejidad lógica asociada con la recursión transfinita. Muestra que la capacidad de expresar puntos fijos con ordinales de cierre $\alpha$ eleva la complejidad de la lógica al nivel $\omega^{\alpha^\omega}$ en la jerarquía hiperaritmética.
• Comparación con Otros Sistemas: El artículo destaca que la lógica lineal con puntos fijos es significativamente más expresiva (en términos de complejidad) que otras lógicas de acción infinitaria con multiplicación, que pueden estar en niveles mucho más bajos de la jerarquía.

En resumen, este artículo establece la teoría de la prueba y la complejidad computacional completa para una familia amplia de lógicas lineales con puntos fijos, demostrando que la complejidad de la demostrabilidad escala directamente con el ordinal de cierre de los puntos fijos, alcanzando niveles profundos de la jerarquía hiperaritmética.