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

Problema
A lógica linear (LL) possui uma noção de consequência sensível a recursos que exige diversos frameworks semânticos, variando de modelos algébricos como a semântica de fases até abordagens de teoria da prova como a semântica de extensão de base (B-eS). Enquanto a semântica de fases interpreta fórmulas sobre espaços de fase (monoide comutativo com relações de ortogonalidade) e a B-eS define validade via relações de suporte indutivo sobre regras de inferência (bases), a relação entre esses dois frameworks distintos não havia sido formalmente estabelecida. Especificamente, não estava claro se essas semânticas, apesar de suas formulações distintas (algébrica vs. inferencial), capturam o mesmo comportamento prova-teórico subjacente da consequência linear, particularmente em relação às modalidades exponenciais (! e ?).

Metodologia
O artigo estabelece uma equivalência entre a semântica de fases e a B-eS para a lógica linear clássica através de uma construção sistemática de mapas bidirecionais entre os dois domínios:

1. Fase para Base: Dado um espaço de fase $P$, os autores constroem uma base $P_B$ onde o conjunto de átomos corresponde ao conjunto de fatos em $P$. As regras de inferência em $P_B$ são definidas para espelhar as propriedades de ortogonalidade e fechamento do espaço de fase, incluindo regras específicas para reductio ad absurdum e comportamento estrutural.
2. Base para Fase: Dada uma base $B$, os autores constroem um espaço de fase $B_P$ onde o monoide consiste em multiconjuntos de fórmulas sobre os átomos da base. O subconjunto fixo $\bot$ é definido como o conjunto de multiconjuntos que suportam uma contradição ($\Gamma \Vdash_B \bot$).
3. Morfismos e Isomorfismo: Os autores definem mapas preservadores de estrutura (morfismos) entre bases e espaços de fase. Eles demonstram que a composição dos mapas bidirecionais resulta em um mapa identidade (ou uma identidade até "intersuporte" no contexto da base), provando que as duas estruturas são isomórficas.
4. Extensão para Exponenciais: Um passo metodológico significativo envolve a definição das cláusulas semânticas para as modalidades exponenciais (! e ?) dentro do framework B-eS, que não haviam sido previamente formalizadas para a lógica linear clássica neste contexto. Essas cláusulas utilizam "átomos estruturais" na base para mimetizar as propriedades de enfraquecimento e contração das exponenciais.

Principais Contribuições

• Prova de Equivalência: A principal contribuição é a prova rigorosa de que a semântica de fases e a semântica de extensão de base são equivalentes para a lógica linear clássica. Isso é alcançado mostrando que um espaço de fase pode ser convertido em uma base e vice-versa, de tal forma que as estruturas resultantes sejam isomórficas.
• Novas Cláusulas Semânticas: O artigo introduz as primeiras cláusulas formais de B-eS para as modalidades exponenciais (! e ?) na lógica linear clássica. Essas cláusulas dependem do conceito de átomos estruturais para lidar com os aspectos de gerenciamento de recursos (enfraquecimento e contração) inerentes às exponenciais.
• Formalização da Correspondência: O trabalho formaliza a relação entre a estrutura algébrica dos espaços de fase e a estrutura inferencial das bases, definindo morfismos específicos que preservam a validade e as relações de suporte.

Resultos

• Teoremas 25 & 29: O artigo prova que a composição dos mapas de Fase para Base e de volta para Fase resulta em um mapa identidade nos espaços de fase. Da mesma forma, a composição de Base para Fase e de volta para Base resulta em uma identidade até o intersuporte (equivalência lógica dentro da base).
• Soundness (Correção) e Completude: O artigo afirma que a lógica linear é correta e completa em relação às novas cláusulas de B-eS para exponenciais. Provas para essas propriedades são fornecidas no Apêndice A, baseando-se na interação entre átomos estruturais e a relação de suporte.
• Lema 16: É demonstrado que, em uma base derivada de um espaço de fase, um átomo é estrutural se, e somente se, ele corresponde à interpretação de uma fórmula exponencial ($! \alpha$). Isso une a lacuna entre a definição algébrica de exponenciais na semântica de fases e a definição inferencial de átomos estruturais na B-eS.

Significância
O artigo afirma que estabelecer esta equivalência serve a vários propósitos:

1. Verificação de Correção: Valida ambos os frameworks ao mostrar que uma semântica formulada via indução sobre provas (B-eS) e uma formulada sobre espaços de fase expressam exatamente as mesmas inferências.
2. Transferência de Resultados: Permite que resultados obtidos em um cenário (por exemplo, provas de decidibilidade ou admissibilidade de corte na semântica de fases) sejam reformulados e transferidos para o outro (B-eS), e vice-versa.
3. Integração: Coloca a relativamente recente semântica de extensão de base dentro da teoria semântica estabelecida da lógica linear, permitindo a comparação sistemática com outros frameworks padrão.
4. Potencial Categórico: Os autores observam que os morfismos definidos sugerem que bases e espaços de fase podem ser vistos como categorias, abrindo as portas para uma interpretação mais abstrata e categórica da equivalência, potencialmente ligando-a à existência de semântica prova-teórica categórica.

O artigo conclui observando modestamente que, embora a equivalência seja estabelecida, sutis diferenças permanecem entre as cláusulas propostas de B-eS clássica para exponenciais e as versões intuicionistas existentes, o que justifica investigações futuras. Também sugere que um resultado de equivalência semelhante provavelmente se aplica à lógica linear intuicionista, dada a similaridade estrutural entre as versões clássica e intuicionista de ambas as semânticas.