A Proof-theoretic Semantics for Intuitionistic Linear Logic

Problema
La semántica proof-teórica (P-tS) busca conferir significado a las expresiones lógicas a través de la noción de prueba en lugar de la verdad. Mientras que Sandqvist estableció con éxito una semántica de base-extensión (B-eS) para la Lógica Proposicional Intuicionista (IPL), y Gheorghiu, Gu y Pym extendieron esto al fragmento multiplicativo de la Lógica Lineal Intuicionista (ILL), una P-tS completa para la ILL completa seguía siendo elusiva. El desafío principal reside en la naturaleza substructural de la ILL, que prohíbe la debilidad y la contracción general, y su inclusión de conectivas aditivas y la modalidad exponencial (!). Los enfoques existentes luchan por manejar la interacción entre estas características dentro de un marco de base-extensión. Específicamente, definir una relación de soporte que respete la naturaleza sensible a los recursos de la ILL mientras capture correctamente el contenido inferencial del conectivo "bang" (!) —un operador modal que requiere derivaciones estrictas— presenta dificultades significativas. Además, los sistemas de deducción natural estándar para la ILL a menudo dependen de condiciones laterales ad-hoc respecto al uso compartido de contextos (aditividad) y al número de premisas, las cuales son difíciles de formalizar dentro de la estructura rígida y no esquemática requerida para las reglas atómicas en la B-eS.

Metodología
El artículo propone una nueva semántica de base-extensión para la ILL abordando dos obstáculos técnicos principales: la formalización de las reglas de deducción natural sin metavariables de contexto esquemáticas, y la definición de una relación de soporte que maneje la aditividad y la modalidad.

1. Reformulación de la Deducción Natural: El autor introduce una nueva sintaxis para el sistema de deducción natural NILL utilizando "cajas aditivas" (denotadas por llaves {...}) y "cajas modales" (denotadas por corchetes semánticos J...K).

   • Cajas Aditivas: Estas demarcan contextos compartidos, permitiendo al sistema representar conectivas aditivas (como & y ⊕) y reglas con premisas variables (como ⊤I y 0E) sin depender de metavariables de contexto arbitrarias. Esto permite un tratamiento sistemático de la aditividad donde las derivaciones dentro de una caja comparten el mismo multiset de supuestos abiertos.
   • Cajas Modales: Se utilizan para caracterizar la regla de Promoción (Prom). La regla se redefine para requerir que la conclusión siga de un contexto donde todos los supuestos son conclusiones de reglas que contienen únicamente cajas modales por encima de ellas. Esto captura el requisito de derivación estricta de la modalidad exponencial sin referirse explícitamente al conectivo ! en la definición estructural de la regla.
   • El autor demuestra que este nuevo sistema es equivalente al NILL estándar de estilo secuente (Teorema 2.7).

2. Derivabilidad Atómica y Relación de Soporte:

   • Reglas Atómicas: La semántica define las reglas atómicas como tríos que consisten en un multiset de cajas aditivas, una única caja aditiva (la conclusión), y un átomo. Esto refleja la estructura de las reglas reformuladas de la deducción natural.
   • Extensión de Base: Una base $B$ es un conjunto de tales reglas atómicas. La relación de derivabilidad $\vdash_B$ se define inductivamente, manejando la división multiplicativa de contextos y la compartición aditiva a través de la estructura de la caja.
   • Relación de Soporte ($\Vdash_B^L$): La definición semántica central extiende la relación de soporte a la ILL. Crucialmente, la cláusula para la modalidad exponencial !ϕ se define no meramente como una regla estructural, sino como una condición sobre la validez de $\phi$ a través de las extensiones de base. Específicamente, $\Vdash_B^L !\phi$ se cumple si, para cualquier extensión $C$ de $B$, si $\phi$ es un "teorema" de $C$ (es decir, $\Vdash_D^\emptyset \phi$ para todo $D \supseteq C$), entonces el recurso puede ser utilizado.
   • Manejo de la Modalidad: El artículo introduce el concepto de "átomos persistentes" en la base, que corresponden a fórmulas de la forma !ϕ. Estos átomos juegan un papel análogo al conectivo ! en la relación de derivabilidad, permitiendo a la semántica distinguir entre supuestos estándar y aquellos que pueden ser debilitados o contraídos.

Contribuciones Clave

• Una B-eS Completa para la ILL: El artículo presenta la primera semántica de base-extensión que cubre la totalidad de la Lógica Lineal Intuicionista, incluyendo las conectivas aditivas y la modalidad exponencial.
• Tratamiento Sistemático de la Aditividad: Al introducir cajas aditivas, el autor proporciona un método para manejar el uso compartido de contextos y las reglas de premisa variable en la deducción natural sin condiciones laterales ad-hoc o metavariables de contexto explícitas. Esto ofrece una representación más limpia y uniforme de las figuras de inferencia.
• Caracterización por Caja Modal: La redefinición de la regla de Promoción usando cajas modales proporciona una caracterización estructural de la modalidad exponencial que es independiente de la sintaxis específica del conectivo, facilitando su integración en el marco de base-extensión.
• Cuenta Inferencialista de !: El artículo ofrece una discusión detallada sobre el contenido inferencialista del conectivo !. Argumenta que la semántica captura la naturaleza modal de ! al tratarlo como una condición sobre la validez de la fórmula subyacente a través de las extensiones de base, internalizando efectivamente el aspecto de "necesitación" de la modalidad.
• Corrección y Completitud: El autor demuestra que la semántica propuesta es tanto correcta como completa con respecto al sistema de deducción natural NILL. La prueba de completitud implica la construcción de una "base de simulación" $N$ donde las reglas atómicas imitan las reglas de inferencia de NILL, y un mapa de aplanamiento traduce las fórmulas de ILL en átomos.

Resultados

• Teorema 2.7: Establece la equivalencia entre la derivabilidad de estilo secuente estándar ($\vdash$) y la nueva derivabilidad basada en cajas ($\vdash^*$).
• Teorema 5.1 (Corrección): Demuestra que si una secuencia es demostrable en NILL, es válida en la semántica propuesta ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$).
• Teorema 6.1 (Completitud): Demuestra que si una secuencia es válida en la semántica, es demostrable en NILL ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$).
• Teorema 4.15: Demuestra que la cláusula específica (Inf) utilizada para manejar hipótesis con ! es equivalente a una cláusula más general (Gen-Inf), validando el tratamiento específico de las hipótesis modales.
• Corolario 4.11 & 4.12: Establecen propiedades estructurales respecto a la interacción de ! con la relación de soporte, mostrando que si $\phi$ es válida, entonces !ϕ es válida, y que !Γ soporta a !ϕ si soporta a $\phi$.

Significancia
El artículo afirma llenar un vacío significativo en la semántica de la teoría de la prueba al extender el enfoque de base-extensión desde la IPL y la IMLL hacia la ILL completa. El autor señala que, mientras que Gheorghiu, Gu y Pym manejaron con éxito el fragmento multiplicativo, la adición de los aditivos y la modalidad exponencial requirió una maquinaria sustancialmente nueva. El trabajo es significativo por su enfoque intrínsecamente proof-teórico de la modalidad, ofreciendo una forma de entender el conectivo "bang" no solo como una regla estructural, sino como una condición sobre la validez de las fórmulas dentro del marco de base-extensión. El autor reconoce modestamente que la solución para manejar la regla de promoción y la aditividad es "algo enrevesada", pero necesaria para lograr una representación limpia y sistemática de las figuras de inferencia. Además, el artículo destaca la dificultad de integrar la semántica de Sandqvist para la IPL directamente en este marco de la ILL, dejando la generalización del mapeo entre ambos como un problema abierto para estudios futuros. El trabajo sugiere que el enfoque actual para las modalidades en P-tS puede requerir de profundos conocimientos metafísicos o estructurales que apenas están comenzando a abordarse.