A Proof-Theoretic Approach to the Semantics of Classical Linear Logic

Resumo Técnico: Uma Abordagem Prova-Téorica para a Semântica da Lógica Linear Clássica

Autores: Victor Barroso-Nascimento, Ekaterina Piotrovskaya e Elaine Pimentel.
Contexto: Proceedings of MFPS 2025 (Electronic Notes in Theoretical Informatics and Computer Science).

1. O Problema

A semântica da Lógica Linear (LL) é tradicionalmente apresentada de duas formas principais:

1. Semântica de Modelos: Associando fórmulas a conjuntos de contextos que as provam (ex: semântica de fases) ou a estruturas matemáticas (ex: espaços de coerência).
2. Semântica Prova-Téorica (PtS): Atribui significado diretamente às provas, focando na inferência em vez de na verdade em modelos.

Dentro da PtS, a Semântica de Extensão de Base (Base-Extension Semantics - BeS) tem sido bem-sucedida em lógica intuicionista e em lógicas subestruturais intuicionistas. No entanto, estender a BeS para a Lógica Linear Clássica (especificamente o fragmento multiplicativo-aditivo, MALL) apresenta desafios significativos:

• A Natureza da Falsidade ($\bot$): Em semânticas de modelos, a falsidade é frequentemente definida como "nunca válida". Em PtS, definir $\bot$ de forma que capture a refutabilidade sintática sem recorrer a uma noção bivalente de verdade é complexo.
• Validade Clássica vs. Construtiva: Sistemas de dedução natural clássicos muitas vezes exigem regras não harmônicas ou dependem excessivamente da dualidade de conectivos para simular comportamentos de múltiplas conclusões. A questão central é: como descrever a validade clássica (que permite o reductio ad absurdum) dentro de um framework construtivo baseado em bases de regras atômicas?
• Subestruturalidade: A LL remove regras estruturais (contração e enfraquecimento), exigindo o uso de multiconjuntos em vez de conjuntos, o que complica a definição de bases e a relação entre suporte e derivabilidade.

2. Metodologia

Os autores propõem uma extensão da Semântica de Extensão de Base (BeS) para o MALL clássico. A metodologia baseia-se nos seguintes pilares:

• Bases e Derivabilidade Atômica: Define-se uma "base" ($B$) como um conjunto de regras que governam apenas fórmulas atômicas (incluindo $\bot$ tratado como um átomo fixo). A derivabilidade ($\vdash_B$) é definida indutivamente sobre essas regras.
• Relação de Suporte ($\Vdash$): O conceito central é a relação de suporte $\Vdash^\Delta_{B} \phi$, que indica que a base $B$ suporta a inferência de $\phi$ relativo a um contexto $\Delta$.
• A Restrição Uniforme (O "Truque" Clássico): A inovação principal é a aplicação de uma restrição uniforme às condições de prova intuicionistas. Em vez de exigir que uma fórmula seja suportada se ela implicar qualquer átomo arbitrário $p$, o sistema clássico exige que ela implique apenas $\bot$.
  • Exemplo para Conjunção Multiplicativa ($\otimes$):
    • Intuicionista: $\Vdash \phi \otimes \psi$ se, para todo $C \supseteq B$ e átomo $p$, se $\phi, \psi \Vdash p$, então $\Gamma \Vdash p$.
    • Clássico (Proposto): $\Vdash \phi \otimes \psi$ se, para todo $C \supseteq B$, se $\phi, \psi \Vdash \bot$, então $\Gamma \Vdash \bot$.
• Tratamento de $\bot$: Ao contrário de abordagens anteriores que excluíam $\bot$ das bases ou o tratavam como um conectivo lógico complexo, aqui $\bot$ é tratado como um átomo fixo manipulável pelas regras da base. A cláusula para átomos atômicos ($p$) é reformulada para garantir que o suporte de $p$ seja equivalente a dizer que qualquer coisa derivável de $p$ é derivável do suporte de $p$, mas com o alvo sendo $\bot$.

3. Principais Contribuições

1. Primeira BeS para Sistemas Subestruturais Clássicos: O artigo apresenta a primeira semântica de extensão de base completa para o fragmento multiplicativo-aditivo da lógica linear clássica (MALL).
2. Caracterização da Validade Clássica via Restrição: Demonstra-se que as condições de prova clássicas podem ser obtidas através de uma restrição muito pequena e uniforme sobre as condições de prova intuicionistas (substituindo o alvo de quantificação atômica por $\bot$). Isso sugere que a prova clássica é uma "restrição" da prova construtiva.
3. Sistema de Dedução Natural para MALL: Definição formal de um sistema de dedução natural para MALL com regras de inferência adequadas, incluindo regras para negação clássica via $\bot$ (Reductio ad Absurdum - Raa).
4. Provas de Corretude (Soundness) e Completude (Completeness):
   • Soundness: Prova-se que se $\Gamma \vdash_{MALL} \phi$, então $\Gamma \Vdash \phi$.
   • Completeness: Prova-se que se $\Gamma \Vdash \phi$, então existe uma derivação $\Gamma \vdash_{MALL} \phi$. A prova de completude utiliza uma base de simulação ($U$) que mapeia subfórmulas para átomos únicos, simulando o comportamento lógico dentro da base.

4. Resultados Chave

• Equivalência entre Suporte e Derivabilidade em Bases de Simulação: O Lema 5.3 estabelece que, em uma base de simulação construída especificamente para um conjunto de fórmulas, a relação de suporte semântico ($\Vdash$) coincide exatamente com a derivabilidade sintática ($\vdash$) dos átomos mapeados.
• Propriedade de Normalização Semântica (Corolário 5.5): Uma consequência direta da prova de completude é a demonstração de que qualquer prova válida em MALL pode ser transformada em uma prova onde todas as aplicações das regras de eliminação ($\otimes E, \oplus E, 0 E, ` E$) têm premissas menores com a forma de $\bot$. Isso é um resultado puramente semântico sobre a estrutura sintática das provas.
• Interpretação de Conectivos Clássicos:
  • O conectivo par () e a conjunção aditiva (&) têm condições de prova clássicas que podem ser lidas diretamente de suas regras de introdução e eliminação, sem necessidade de restrições adicionais complexas, sugerindo que é essencialmente clássico.
  • A conjunção aditiva (&) compartilha as mesmas condições de prova em lógica clássica e intuicionista, apoiando a ideia de ecumenismo lógico.

5. Significado e Implicações

• Reconciliação entre Clássico e Construtivo: O trabalho oferece uma justificativa intuitiva para resultados que mostram que conteúdo algorítmico pode ser extraído de provas clássicas. A diferença entre prova clássica e construtiva é apresentada não como qualitativa (existência vs. não-existência de prova), mas quantitativa (a quantidade de informação necessária para estabelecer a prova). A prova clássica exige menos informação (apenas consistência com $\bot$) do que a construtiva.
• Lógica Linear como Construtiva: A ausência de regras estruturais na LL aumenta o conteúdo informacional necessário para provar fórmulas a tal ponto que, mesmo com o uso de reductio ad absurdum, a lógica linear clássica pode ser vista como construtiva.
• Generalidade do Método: A estrutura das provas sugere que a metodologia é geral e pode ser aplicada a outras lógicas para derivar semânticas clássicas a partir de versões intuicionistas.
• Futuro: Os autores propõem extensões para a lógica linear completa (com exponenciais ! e ?), conjecturando cláusulas semânticas que respeitam a restrição de $\bot$ para os modais exponenciais.

Em suma, o artigo fornece uma ponte robusta entre a semântica de modelos e a prova-teórica para lógicas clássicas subestruturais, demonstrando que a complexidade da validade clássica pode ser capturada elegantemente através de restrições simples no suporte de provas baseadas em recursos.