From Phase Semantics to Base-extension Semantics (and back)

Problema
La lógica lineal (LL) posee una noción de consecuencia sensible a los recursos que requiere diversos marcos semánticos, que van desde modelos algebraicos como la semántica de fases hasta enfoques de teoría de la prueba como la semántica de extensión de bases (B-eS). Mientras que la semántica de fases interpreta las fórmulas sobre espacios de fase (monoides conmutativos con relaciones de ortogonalidad) y la B-eS define la validez mediante relaciones de soporte inductivo sobre reglas de inferencia (bases), la relación entre estos dos marcos distintos no se había establecido formalmente. Específicamente, no estaba claro si estas semánticas, a pesar de sus diferentes formulaciones (algebraica frente a inferencial), capturan el mismo comportamiento probatorio subyacente de la consecuencia lineal, particularmente respecto a las modalidades exponenciales (! y ?).

Metodología
El artículo establece una equivalencia entre la semántica de fases y la B-eS para la lógica lineal clásica mediante una construcción sistemática de mapas bidireccionales entre los dos dominios:

1. De Fase a Base: Dado un espacio de fase $P$, los autores construyen una base $P_B$ donde el conjunto de átomos corresponde al conjunto de hechos en $P$. Las reglas de inferencia en $P_B$ se definen para reflejar las propiedades de ortogonalidad y clausura del espacio de fase, incluyendo reglas específicas para el reductio ad absurdum y el comportamiento estructural.
2. De Base a Fase: Dado una base $B$, los autores construyen un espacio de fase $B_P$ donde el monoide consiste en multiconjuntos de fórmulas sobre los átomos de la base. El subconjunto fijo $\bot$ se define como el conjunto de multiconjuntos que soportan una contradicción ($\Gamma \Vdash_B \bot$).
3. Morfismos e Isomorfismo: Los autores definen mapas que preservan la estructura (morfismos) entre bases y espacios de fase. Demuestran que la composición de los mapas bidireccionales produce un mapa identidad (o una identidad hasta el "intersoporte" en el entorno de la base), probando así que las dos estructuras son isomorfas.
4. Extensión a los Exponenciales: Un paso metodológico significativo implica definir las cláusulas semánticas para las modalidades exponenciales (! y ?) dentro del marco de la B-eS, las cuales no habían sido formalizadas previamente para la lógica lineal clásica en este contexto. Estas cláusulas utilizan "átomos estructurales" en la base para imitar las propiedades de debilitamiento (weakening) y contracción inherentes a los exponenciales.

Contribuciones Clave

• Prueba de Equivalencia: La contribución principal es la rigurosa prueba de que la semántica de fases y la semántica de extensión de bases son equivalentes para la lógica lineal clásica. Esto se logra demostrando que un espacio de fase puede convertirse en una base y viceversa, de tal manera que las estructuras resultantes sean isomorfas.
• Nuevas Cláusulas Semánticas: El artículo introduce las primeras cláusulas formales de B-eS para las modalidades exponenciales (! y ?) en la lógica lineal clásica. Estas cláusulas se apoyan en el concepto de átomos estructurales para gestionar los aspectos de gestión de recursos (debilitamiento y contracción) propios de los exponenciales.
• Formalización de la Correspondencia: El trabajo formaliza la relación entre la estructura algebraica de los espacios de fase y la estructura inferencial de las bases, definiendo morfismos específicos que preservan la validez y las relaciones de soporte.

Resultados

• Teoremas 25 y 29: El artículo demuestra que la composición de los mapas de Fase a Base y de vuelta a Fase resulta en un mapa identidad sobre los espacios de fase. Del mismo modo, la composición de Base a Fase y de vuelta a Base resulta en una identidad hasta el intersoporte (equivalencia lógica dentro de la base).
• Corrección y Completitud: El artículo afirma que la lógica lineal es sólida y completa con respecto a las cláusulas de B-eS recién definidas para los exponenciales. En el Apéndice A se proporcionan las pruebas para estas propiedades, basándose en la interacción entre los átomos estructurales y la relación de soporte.
• Lema 16: Se demuestra que en una base derivada de un espacio de fase, un átomo es estructural si y solo si corresponde a la interpretación de una fórmula exponencial ($! \alpha$). Esto tiende un puente entre la definición algebraica de los exponenciales en la semántica de fases y la definición inferencial de los átomos estructurales en la B-eS.

Significado
El artículo sostiene que establecer esta equivalencia cumple varios propósitos:

1. Verificación de Corrección: Valida ambos marcos al mostrar que una semántica formulada mediante inducción sobre pruebas (B-eS) y una formulada sobre espacios de fase expresan exactamente las mismas inferencias.
2. Transferencia de Resultados: Permite que los resultados obtenidos en un entorno (por ejemplo, pruebas de decidibilidad o admisibilidad del corte en la semántica de fases) sean reformulados y transferidos al otro (B-eS), y viceversa.
3. Integración: Sitúa la relativamente reciente semántica de extensión de bases dentro de la teoría semántica establecida de la lógica lineal, permitiendo una comparación sistemática con otros marcos estándar.
4. Potencial Categórico: Los autores señalan que los morfismos definidos sugieren que las bases y los espacios de fase pueden verse como categorías, abriendo la puerta a una interpretación más abstracta y categórica de la equivalencia, vinculándola potencialmente con la semántica de prueba categórica existente.

El artículo concluye señalando modestamente que, si bien se establece la equivalencia, persisten diferencias sutiles entre las cláusulas de B-eS propuestas para los exponenciales en la lógica clásica y las versiones intuicionistas existentes, lo que justifica una mayor investigación. También sugiere que un resultado de equivalencia similar probablemente se aplique a la lógica lineal intuicionista, dada la similitud estructural entre las versiones clásica e intuicionista de ambas semánticas.