Proof Identity and Categorical Models of BV

1. Declaração do Problema

A lógica BV (uma extensão conservativa da Lógica Linear Multiplicativa com um conectivo não comutativo autodual $\text{seq}$, denotado $\text{seq}$) possui sintaxe e teoria de provas bem desenvolvidas, mas carece de uma semântica categórica clara e sólida.

• A Lacuna: Tentativas anteriores de definir modelos categóricos (chamados categorias-BV) por Acclavio et al. e outros não foram provadas como sólidas em relação à lógica.
• A Questão Central: Não há uma noção acordada de identidade de prova para BV. Em cálculos de sequente padrão, a identidade de prova é frequentemente definida via eliminação de corte. No entanto, a BV é formulada em um contexto de Inferência Profunda (especificamente o sistema SBV), onde as regras podem ser aplicadas em qualquer lugar dentro de uma fórmula. Isso torna difícil traduzir as provas padrão de eliminação de corte (baseadas em lemas de divisão) em condições de coerência categórica.
• A Consequência: Sem uma definição precisa de quando duas provas BV são "iguais", é impossível verificar se um modelo categórico identifica corretamente provas equivalentes (solidez). As definições existentes de categorias-BV não se alinham bem com as propriedades estruturais necessárias para lidar com o conectivo não comutativo $\text{seq}$ de uma maneira que respeite a inferência profunda.

2. Metodologia

Os autores preenchem a lacuna entre a teoria de provas e a teoria das categorias através das seguintes etapas metodológicas:

A. Fluxos Atômicos como Identidade de Prova

Em vez de confiar na normalização sintática (que é complexa na inferência profunda), os autores introduzem Fluxos Atômicos para BV.

• Definição: Um fluxo atômico é um diagrama 2D (uma forma específica de diagrama de corda) que rastreia as ocorrências de átomos (literais) em uma derivação, abstraindo os conectivos lógicos.
• Mapeamento: Cada regra de inferência no sistema BV (por exemplo, $\text{ai}\downarrow$, $\text{s}$, $\text{q}\downarrow$) é mapeada para um gerador específico de fluxo atômico. As derivações são mapeadas para a composição desses fluxos.
• Equivalência: Duas provas são consideradas equivalentes se seus fluxos atômicos forem iguais.

B. Eliminação de Corte como Puxada (Yanking)

Os autores estabelecem uma correspondência crucial entre a operação global de eliminação de corte na BV e uma regra de reescrita local em fluxos atômicos chamada Puxada (Yanking).

• Puxada ($\text{Y}$): Uma regra de reescrita em fluxos atômicos que corresponde ao "puxar" topológico de um fio em um diagrama de corda (removendo um par copela-tampa).
• Teorema: Os autores provam que o Lema de Divisão (o mecanismo central para eliminação de corte na BV) preserva fluxos atômicos. Consequentemente, eliminar regras "para cima" ($\text{ai}\uparrow$, $\text{q}\uparrow$) de uma derivação corresponde exatamente à aplicação da reescrita de Puxada ao fluxo atômico até que uma forma normal seja alcançada.
• Resultado: Se duas provas se reduzem à mesma forma normal sob Puxada, elas são equivalentes. Isso fornece uma definição concreta e gráfica de identidade de prova para BV.

C. Categorias-BV Fortes

Para fornecer um modelo categórico sólido, os autores propõem uma nova definição: a Categoria-BV Forte.

• Estrutura: Uma Categoria-BV Forte é uma tupla $\langle \mathcal{C}, \otimes, \text{seq}, I, \perp, U \rangle$ onde:
  1. $\mathcal{C}$ é uma categoria $*$-autônoma com uma estrutura isomix.
  2. $\mathcal{C}$ possui uma estrutura monoidal para $\text{seq}$.
  3. Condição Crucial: Existe um functor $*$-autônomo estrito fiel $U$ de $\mathcal{C}$ para uma Categoria Compactamente Fechada Estrita $\mathcal{D}$.
• Racional: Como os fluxos atômicos são conhecidos por serem a linguagem interna das categorias compactamente fechadas estritas, incorporar o modelo BV em tal categoria através de um functor fiel permite aos autores "elevar" as propriedades de coerência conhecidas das categorias compactamente fechadas (especificamente em relação a diagramas de corda) para o modelo BV. Isso garante que, se duas provas tiverem o mesmo fluxo atômico, elas mapeiam para o mesmo morfismo no modelo.

3. Principais Contribuições

1. Definição de Identidade de Prova para BV: O artigo define a equivalência de prova para BV baseada em Fluxos Atômicos, resolvendo a ambiguidade da identidade de prova em sistemas de inferência profunda.
2. Eliminação de Corte = Puxada: Os autores provam que a eliminação de corte na BV corresponde à regra de reescrita Puxada em fluxos atômicos. Isso estabelece que os fluxos atômicos são invariantes sob eliminação de corte.
3. Categorias-BV Fortes: A introdução de Categorias-BV Fortes, que exigem uma incorporação em uma categoria compactamente fechada estrita. Esta definição é mais forte do que propostas anteriores, mas é necessária para garantir a solidez.
4. Teorema de Solidez: O artigo prova que as Categorias-BV Fortes são sólidas em relação à lógica BV: se duas provas são equivalentes (têm o mesmo fluxo atômico), elas têm a mesma interpretação denotacional no modelo.
5. Modelos Concretos: Os autores demonstram que várias categorias não triviais são Categorias-BV Fortes, incluindo:
   • O esqueleto de espaços vetoriais de dimensão finita.
   • Espaços de Operadores de dimensão finita (usando produtos tensoriais projetivos, injetivos e de Haagerup), ligando a BV à teoria quântica (dualidade Heisenberg-Schrödinger).
   • A construção Caus[-] em mapas completamente positivos (computação quântica de ordem superior).
   • Espaços de Coerência Probabilísticos (computação probabilística clássica).

4. Resultados

• Teorema 14: Se uma derivação $\Phi$ se reduz a $\Phi'$ via eliminação de corte, então o fluxo atômico de $\Phi'$ é a forma normal de Puxada do fluxo atômico de $\Phi$.
• Teorema 23 (Solidez): Para qualquer Categoria-BV Forte, se duas derivações $\Phi$ e $\Phi'$ são equivalentes (isto é, $\Phi \sim \Phi'$), então suas interpretações na categoria são idênticas ($\llbracket \Phi \rrbracket = \llbracket \Phi' \rrbracket$).
• Teorema 18: Toda Categoria-BV Forte é uma categoria-BV no sentido da literatura anterior, mas o inverso provavelmente é falso (a condição de incorporação é um requisito estrito).

5. Significado

• Unificação de Comunidades: O artigo conecta com sucesso a comunidade de Inferência Profunda/Teoria de Provas (focada em BV e fluxos atômicos) com a comunidade de Semântica Categórica (focada em computação quântica e espaços de operadores).
• Fundamentos para Lógica Quântica: Ao validar Espaços de Operadores e construções Caus[-] como modelos sólidos, o artigo fornece uma base lógica rigorosa para o uso da BV para modelar causalidade quântica e sequencialidade na computação quântica.
• Nova Semântica para Lógica Não Comutativa: Resolve questões de longa data sobre a semântica do conectivo não comutativo $\text{seq}$, mostrando que ele pode ser modelado solidamente usando a interação entre estruturas $*$-autônomas e categorias compactamente fechadas.
• Direções Futuras: O trabalho abre caminhos para investigar teoremas de coerência para categorias-BV, estender esses resultados para BV Intuicionista e explorar a relação entre fluxos atômicos BV e redes de prova da Lógica Pomset.

Em resumo, este artigo resolve o problema crítico de definir a identidade de prova para BV e usa essa definição para construir uma semântica categórica robusta e sólida, validando assim o uso da BV na modelagem de estruturas sequenciais e causais complexas em sistemas quânticos e probabilísticos.