A Proof-theoretic Semantics for Intuitionistic Linear Logic

Problema
A semântica prova-teórica (P-tS) visa conferir significado às expressões lógicas através da noção de prova em vez de verdade. Enquanto Sandqvist estabeleceu com sucesso uma semântica de base-extensão (B-eS) para a Lógica Proposicional Intuicionista (IPL), e Gheorghiu, Gu e Pym estenderam isso para o fragmento multiplicativo da Lógica Linear Intuicionista (IMLL), uma P-tS completa para a lógica linear intuicionista (ILL) completa permanecia elusiva. O desafio primordial reside na natureza subestrutural da ILL, que proíbe a enfraquecimento e contração gerais, e sua inclusão de conectivos aditivos e a modalidade exponencial (!). Abordagens existentes lutam para lidar com a interação entre esses recursos dentro de um arcabouço de base-extensão. Especificamente, definir uma relação de suporte que respeite a natureza sensível a recursos da ILL enquanto captura corretamente o conteúdo inferencialista do conectivo "bang" (!) — um operador modal que exige derivações estritas — apresenta dificuldades significativas. Além disso, sistemas de dedução natural padrão para ILL frequentemente dependem de condições laterais ad-hoc em relação ao compartilhamento de contexto (aditividade) e ao número de premissas, que são difíceis de formalizar dentro da estrutura não esquemática rígida exigida para regras atômicas em B-eS.

Metodologia
O artigo propõe uma nova semântica de base-extensão para ILL abordando dois obstáculos técnicos principais: a formalização de regras de dedução natural sem metavariáveis de contexto esquemáticas, e a definição de uma relação de suporte que lide com aditividade e modalidade.

1. Reformulação da Dedução Natural: O autor introduz uma nova sintaxe para o sistema de dedução natural NILL usando "caixas aditivas" (denotadas por chaves {...}) e "caixas modais" (denotadas por colchetes semânticos J...K).

   • Caixas Aditivas: Estas demarcam contextos compartilhados, permitindo que o sistema represente conectivos aditivos (como & e ⊕) e regras com variáveis premissas (como ⊤I e 0E) sem depender de metavariáveis de contexto arbitrárias. Isso permite um tratamento sistemático da aditividade onde as derivações dentro de uma caixa compartilham o mesmo multiconjunto de suposições abertas.
   • Caixas Modais: Estas são usadas para caracterizar a regra de Promoção (Prom). A regra é redefinida para exigir que a conclusão siga de um contexto onde todas as suposições são conclusões de regras contendo apenas caixas modais acima delas. Isso captura o requisito de derivação estrita da modalidade exponencial sem referenciar explicitamente o conectivo ! na definição estrutural da regra.
   • O autor prova que este novo sistema é equivalente à NILL padrão de estilo sequente (Teorema 2.7).

2. Derivabilidade Atômica e Relação de Suporte:

   • Regras Atômicas: A semântica define regras atômicas como triplas consistindo em um multiconjunto de caixas aditivas, uma única caixa aditiva (a conclusão), e um átomo. Isso espelha a estrutura das regras reformuladas de dedução natural.
   • Extensão de Base: Uma base $B$ é um conjunto de tais regras atômicas. A relação de derivabilidade $\vdash_B$ é definida indutivamente, lidando com a divisão multiplicativa de contextos e o compartilhamento aditivo via estrutura de caixa.
   • Relação de Suporte ($\Vdash_B^L$): A definição semântica central estende a relação de suporte para ILL. Crucialmente, a cláusula para a modalidade exponencial !ϕ é definida não meramente como uma regra estrutural, mas como uma condição sobre a validade de $\phi$ através de extensões de base. Especificamente, $\Vdash_B^L !\phi$ ocorre se, para qualquer extensão $C$ de $B$, se $\phi$ é um "teorema" de $C$ (isto é, $\Vdash_D^\emptyset \phi$ para todo $D \supseteq C$), então o recurso pode ser usado.
   • Lidando com a Modalidade: O artigo introduz o conceito de "átomos persistentes" na base, que correspondem a fórmulas da forma !ϕ. Estes átomos desempenham um papel análogo ao conectivo ! na relação de derivabilidade, permitindo que a semântica distinga entre suposições padrão e aquelas que podem ser enfraquecidas ou contraídas.

Contribuições Principais

• Uma B-eS Completa para ILL: O artigo apresenta a primeira semântica de base-extensão que cobre a lógica linear intuicionista completa, incluindo conectivos aditivos e a modalidade exponencial.
• Tratamento Sistemático da Aditividade: Ao introduzir caixas aditivas, o autor fornece um método para lidar com compartilhamento de contexto e regras de premissas variáveis em dedução natural sem condições laterais ad-hoc ou metavariáveis de contexto explícitas. Isso oferece uma representação mais limpa e uniforme de figuras de inferência.
• Caracterização por Caixa Modal: A redefinição da regra de Promoção usando caixas modais fornece uma caracterização estrutural da modalidade exponencial que é independente da sintaxe específica do conectivo, facilitando sua integração no arcabouço de base-extensão.
• Conta Inferencialista de !: O artigo oferece uma discussão detalhada sobre o conteúdo inferencialista do conectivo !. Argumenta que a semântica captura a natureza modal de ! ao tratá-lo como uma condição sobre a validade da fórmula subjacente através de extensões de base, efetivamente internalizando o aspecto de "necessitação" da modalidade.
• Consistência e Completude: O autor prova que a semântica proposta é tanto consistente quanto completa em relação ao sistema de dedução natural NILL. A prova de completude envolve a construção de uma "base de simulação" $N$ onde as regras atômicas mimetizam as regras de inferência de NILL, e um mapeamento de achatamento traduz fórmulas de ILL em átomos.

Resultos

• Teorema 2.7: Estabelece a equivalência entre a derivabilidade padrão de estilo sequente ($\vdash$) e a nova derivabilidade baseada em caixas ($\vdash^*$).
• Teorema 5.1 (Consistência): Prova que se uma sequência é provável em NILL, ela é válida na semântica proposta ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$).
• Teorema 6.1 (Completude): Prova que se uma sequência é válida na semântica, ela é provável em NILL ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$).
• Teorema 4.15: Demonstra que a cláusula (Inf) específica usada para lidar com hipóteses com ! é equivalente a uma cláusula (Gen-Inf) mais geral, validando o tratamento específico de hipóteses modais.
• Corolário 4.11 & 4.12: Estabelecem propriedades estruturais em relação à interação de ! com a relação de suporte, mostrando que se $\phi$ é válido, então !ϕ é válido, e que !Γ suporta !ϕ se suporta ϕ.

Significância
O artigo afirma preencher uma lacuna significativa na semântica prova-teórica ao estender a abordagem de base-extensão da IPL e IMLL para a ILL completa. O autor observa que, embora Gheorghiu, Gu e Pym tenham lidado com sucesso com o fragmento multiplicativo, a adição de aditivos e a modalidade exponencial exigiu um novo maquinário substancial. O trabalho é significativo por sua abordagem prova-teórica intrínseca à modalidade, oferecendo uma maneira de entender o conectivo "bang" não apenas como uma regra estrutural, mas como uma condição sobre a validade de fórmulas dentro do arcabouço de base-extensão. O autor reconhece modestamente que a solução para lidar com a regra de promoção e a aditividade é "um tanto convoluta", mas necessária para alcançar uma representação limpa e sistemática de figuras de inferência. Além disso, o artigo destaca a dificuldade de embutir a semântica de Sandqvist para IPL diretamente neste arcabouço de ILL, deixando a generalização do mapeamento entre os dois como um problema aberto para estudos futuros. O trabalho sugere que a abordagem atual para modalidades em P-tS pode exigir insights metafísicos ou estruturais profundos que estão apenas começando a ser abordados.