Full Definability in a Profunctorial Model

1. Formulação do Problema

O artigo aborda o problema da definibilidade total (ou completude total) em modelos semânticos para a Lógica Linear Multiplicativa com MIX (MLL + Mix).

• Contexto: Um modelo é totalmente definível se todo elemento semântico no modelo corresponder à denotação de alguma prova (ou termo $\lambda$). Embora modelos totalmente definíveis existam para o modelo relacional (por exemplo, espaços de totalidade de Loader) e para semântica de jogos, estender esses resultados a modelos mais expressivos é um desafio.
• A Lacuna: Os autores focam na (bi)categoria de profuntores em grupoides. Profuntores são uma "categorificação" de relações; ao contrário das relações, que apenas indicam se dois elementos estão relacionados, os profuntores codificam como eles estão relacionados (incluindo o número de maneiras e as relações entre essas maneiras).
• O Desafio: Embora modelos de profuntores capturem informações quantitativas e combinatórias ricas (úteis para expansões de Taylor e tipos de interseção), eles são significativamente mais complexos do que modelos relacionais. A questão central é: Quais propriedades intrínsecas caracterizam os profuntores que são denotações de provas válidas de MLL + Mix? Os autores visam construir um modelo totalmente definível baseado em profuntores e caracterizar os elementos definíveis.

2. Metodologia

Os autores constroem um novo modelo semântico combinando dois conceitos estabelecidos na literatura: Totalidade (do modelo relacional de Loader) e Estabilidade (da teoria de domínios e do trabalho de Fiore et al. sobre profuntores).

A. Fundamentos Teóricos

1. Profuntores em Grupoides: O modelo é construído sobre a categoria Prof, onde os objetos são grupoides e os morfismos são classes de isomorfismo de profuntores ($P: A^{op} \times B \to \mathbf{Set}$). Esta categoria é fechada compactamente, tornando-se um modelo para MLL onde o tensor ($\otimes$) e o par ($\parr$) coincidem.
2. Ortogonalidade: Os autores utilizam o arcabouço da ortogonalidade (Hyland e Schalk) para definir subcategorias de profuntores "bons".
3. Creeds e Kits: Eles empregam creeds (famílias de subconjuntos de endomorfismos) e kits (famílias de subgrupos) para restringir a estrutura dos profuntores. Esses conceitos, originalmente introduzidos por Taylor e Fiore et al., servem como o mecanismo para definir estabilidade.

B. Construção Central: Ortogonalidade Total Estável

Os autores definem uma nova relação de ortogonalidade, a ortogonalidade total estável ($\between$), que combina:

• Estabilidade: Garante que o profuntor se comporte bem em relação à estrutura lógica (relacionado ao critério "creed-kit").
• Totalidade: Garante uma forma de "unicidade de órbita" ou maximalidade, impedindo que a soma de duas provas distintas seja um único elemento definível (um problema comum em modelos relacionais).

A categoria resultante, STProf (Profuntores Totais Estáveis), é uma subcategoria plena da categoria de ortogonalidade apertada derivada dessa nova ortogonalidade.

C. Técnicas de Prova

• Critério de Corretude: Eles provam que a estabilidade serve como um critério de corretude para estruturas de prova. Uma estrutura de prova é correta (uma rede de prova) se e somente se sua interpretação for estável em relação a todos os creeds/kits booleanos.
• Sistemas de Fatoração Estrita: Uma percepção técnica chave é que a interação entre estabilidade e totalidade em grupoides de objeto único (grupos) gera naturalmente sistemas de fatoração estrita. Isso oferece uma nova perspectiva sobre por que sistemas de fatoração aparecem na semântica de profuntores.
• Famílias Lógicas: Para lidar com a dependência de atribuições de variáveis, os autores definem famílias lógicas de profuntores, garantindo que a interpretação respeite a estrutura fonctorial da lógica (usando categorias duplas).

3. Contribuições Principais

1. Um Modelo de Profuntores Totalmente Definível:
   O artigo constrói um modelo STProf baseado em profuntores que é totalmente definível em relação ao MLL + Mix. Este é o primeiro resultado desse tipo para um modelo baseado em profuntores que captura o poder expressivo total da lógica.

2. Caracterização de Profuntores Definíveis:
   Os autores fornecem uma caracterização completa: Uma família de profuntores é definível por uma prova de MLL + Mix se e somente se for lógica (respeita a estrutura fonctorial da lógica) e totalmente estável.

   • A Lógica garante que a família se comporte corretamente sob substituição e renomeação de variáveis.
   • A Totalidade Estável garante que o profuntor corresponda a uma única estrutura de prova sem elementos "espúrios" (como somas de provas disjuntas).

3. Estabilidade como Critério de Corretude:
   Eles provam o Teorema 17: Uma estrutura de prova sem cortes é correta (uma rede de prova) se e somente se satisfizer o critério creed-kit (uma condição de estabilidade). Isso estabelece a estabilidade como um critério semântico de corretude análogo ao critério de coerência de Retoré para o modelo relacional, mas adaptado para a estrutura mais rica dos profuntores.

4. Emergência de Sistemas de Fatoração Estrita:
   O artigo demonstra que sistemas de fatoração estrita surgem naturalmente da combinação de estabilidade e totalidade em grupoides. Especificamente, para um grupo $G$, um profuntor é totalmente estável se e somente se seus subgrupos associados formarem um sistema de fatoração estrito. Isso oferece uma justificativa teórica nova para o papel dos sistemas de fatoração na semântica de profuntores.

4. Resultados

• Teorema 38 (Resultado Principal): Uma família de profuntores é definível por uma prova de MLL + Mix (até isomorfismo natural) se e somente se for uma família lógica e totalmente estável.
• Teorema 17: O critério creed-kit é necessário e suficiente para a corretude de estruturas de prova de MLL + Mix.
• Proposição 29: Em grupoides de objeto único, a ortogonalidade totalmente estável coincide com a existência de um sistema de fatoração estrito.
• Lema 35 (Propriedade de Órbita Única): Todo profuntor totalmente estável possui uma propriedade de "órbita única", o que significa que quaisquer dois elementos na mesma classe de isomorfismo de objetos estão relacionados por uma ação única dos morfismos do groido. Isso previne o problema da "soma de provas" encontrado em modelos mais simples.

5. Significado

• Ponte entre Semântica de Jogos e Profuntores: A semântica de jogos é conhecida pela definibilidade total, mas é complexa. Modelos de profuntores são frequentemente vistos como uma variante simplificada da semântica de jogos (ao descartar certas estruturas). Este artigo demonstra que o raciocínio semântico de jogos (especificamente a definibilidade total) pode ser realizado com sucesso no cenário simplificado dos profuntores, desde que a ortogonalidade correta (totalmente estável) seja utilizada.
• Semântica Quantitativa: Ao usar profuntores, o modelo retém informações "quantitativas" ou "combinatórias" (por exemplo, o número de maneiras pelas quais uma prova pode ser construída) que são perdidas em modelos relacionais padrão. Isso torna o resultado altamente relevante para o estudo de expansões de Taylor e computação sensível a recursos.
• Nova Perspectiva sobre Sistemas de Fatoração: A derivação de sistemas de fatoração estrita a partir de estabilidade e totalidade fornece um elo teórico fresco entre conceitos da teoria de domínios (estabilidade) e estruturas combinatórias (sistemas de fatoração) no contexto da lógica linear.
• Fundamental para Extensões Futuras: Os autores observam que, embora este trabalho cubra MLL + Mix, a abordagem oferece um caminho para estender a definibilidade total a lógicas com exponenciais (que modelam gerenciamento de recursos), um problema aberto importante na lógica categórica.

Em resumo, o artigo eleva com sucesso o conceito de definibilidade total do mundo relacional para o mundo mais rico dos profuntores, usando uma combinação inovadora de estabilidade e totalidade para caracterizar exatamente quais elementos semânticos correspondem a provas válidas.