Resumo Técnico: Provas Não Bem-Fundadas Coalgebraicas: Recursividade e GTC

Declaração do Problema

Sistemas de prova não bem-fundados, incluindo provas cíclicas, são essenciais para lógicas envolvendo (co)indução, como o cálculo modal $\mu$ e lógicas de ponto fixo de ordem superior. Diferentemente de provas finitárias com árvores de derivação finitas, esses sistemas permitem árvores de derivação infinitas. Consequentemente, a correção não pode ser estabelecida via indução estrutural padrão na profundidade da árvore. Em vez disso, esses sistemas impõem uma Condição de Rastreamento Global (GTC), uma restrição sobre caminhos infinitos dentro das árvores de derivação, para garantir a correção.

Apesar de várias abordagens categóricas para provas cíclicas (por exemplo, categorias $\mu$-bicompletas, categorias de rastreamento), fornecer uma caracterização categórica da GTC que garanta a correção permanece um desafio significativo. As principais dificuldades são:

1. Global vs. Local: A GTC impõe restrições sobre árvores de derivação inteiras, o que conflita com a natureza local e composicional do raciocínio categórico padrão.
2. Estrutura Infinitária: Provas não bem-fundadas podem ser infinitas, impedindo o uso da indução estrutural padrão para construir morfismos semânticos.
3. Lacuna na Teoria de Coalgebras Recursivas: Embora coalgebras recursivas e bem-fundadas garantam soluções únicas (interpretações semânticas), as árvores de derivação de provas não bem-fundadas frequentemente resultam em coalgebras não bem-fundadas. Teorias existentes não explicam de forma direta por que soluções únicas existem em casos não bem-fundados específicos (por exemplo, o exemplo da "sequência descendente" de Capretta e Jeannin et al.).

Metodologia

O artigo desenvolve uma estrutura coalgebraica para sistemas de prova não bem-fundados, modelando árvores de derivação como coalgebras e formulando a GTC como uma condição sobre os grafos dessas coalgebras.

1. Coalgebras de Funtores Familiares em Pré-Esquemas

Os autores modelam árvores de derivação como coalgebras $c: C \to FC$ onde $F$ é um funtor familiar em uma categoria de pré-esquemas $\widehat{\mathcal{J}}$.

• Funtores Familiares: São generalizações de funtores polinomiais definidos via polinômios (diagramas de categorias com propriedades específicas de fibrado). Eles permitem que nós sejam rotulados por julgamentos e que estruturas de ramificação sejam determinadas por regras de inferência, acomodando parâmetros e contextos naturalmente.
• Grafos de Coalgebras: Construindo sobre a noção de grafos de coalgebras, o artigo estende a equivalência entre a bem-fundação de coalgebras e a ausência de caminhos infinitos em seus grafos associados para endofuntores em pré-esquemas (Teorema 1.9).

2. Adjunções e Imagens Recursivas

Para abordar a natureza não bem-fundada das provas, a estrutura explora a correspondência de morfismos de coalgebra para álgebra ao longo de adjunções.

• Estratégia: Em vez de exigir que a coalgebra original $c$ seja recursiva, o artigo investiga se sua imagem sob um adjunto esquerdo $L$ adequado (especificamente, um funtor de mudança de base induzido por uma anotação ordinal) é recursiva.
• Mecanismo: Se $Coalg(L)(c)$ for recursiva, e a álgebra semântica alvo $a$ estiver na imagem do adjunto direito $R$ (isto é, $a \cong Alg(R)(a')$), então um morfismo único de coalgebra para álgebra existe para $c$ (Proposição 2.4).
• Intuição: Isso corresponde ao enriquecimento do grafo de derivação com uma dimensão adicional (anotações ordinais) obtida puxando para trás ao longo de uma adjunção. Essa expansão pode tornar o grafo bem-fundado mesmo que o original não seja.

3. Estruturas de Rastreamento e GTC

A GTC é formalizada usando estruturas de rastreamento $(pfml, prog)$:

• Estrutura de Rastreamento: Um morfismo na categoria de polinômios ($VPoly$) que rastreia fórmulas (ou fórmulas marcadas) ao longo das arestas, combinado com um subconjunto de arestas "progressivas" (tipicamente correspondendo a expansões de ponto fixo).
• Definição de GTC: Uma pré-prova satisfaz a GTC se cada caminho infinito em seu grafo rotulado admitir um rastreamento infinitamente progressivo ao longo de um sufixo.
• Anotações Ordinais: A estrutura constrói um sistema de prova abstrato $P^\gamma$ com julgamentos anotados por ordinais. O funtor de esquecimento $u_\gamma: \mathcal{J}dg^\gamma \to \mathcal{J}dg$ induz a adjunção necessária.

Principais Contribuições e Resultados

1. Extensão da Teoria de Grafos para Pré-Esquemas

O artigo estende a equivalência entre a bem-fundação de grafos e a recursividade de coalgebras de endofuntores em $\mathbf{Set}$ para endofuntores em categorias de pré-esquemas (Teorema 1.9). Isso é alcançado definindo grafos de coalgebras para funtores familiares e provando que o funtor preserva interseções e imagens inversas.

2. Correção via Imagens Recursivas

O artigo estabelece um Teorema de Correção (Teorema 4.13): Se uma pré-prova $c$ satisfaz a GTC, então existe um morfismo único de coalgebra para álgebra de $c$ para qualquer álgebra semântica $a$ (desde que $a$ esteja na imagem da álgebra levantada via anotações ordinais).

• Isso fornece uma explicação coalgebraica para exemplos não bem-fundados (como a sequência descendente) que admitem soluções únicas, mas não são recursivos no sentido padrão.
• Demonstra que a GTC garante que a coalgebra "expandida" (com anotações ordinais) se torne recursiva.

3. Caracterização de GTC e Recursividade

O artigo estabelece uma caracterização bidirecional entre a GTC e a recursividade:

• GTC $\implies$ Recursividade: Uma pré-prova satisfaz a GTC se e somente se sua imagem sob o funtor de anotação ordinal for recursiva (Teorema 4.17).
• Recursividade $\implies$ GTC: Uma pré-prova é recursiva se e somente se satisfizer a GTC para todas as estruturas de rastreamento (Proposição 4.14).
• Isso esclarece que a GTC é essencialmente a condição que garante que, após transporte ao longo de uma adjunção adequada, a coalgebra relevante se torne recursiva.

4. Instanciações Concretas

A estrutura é demonstrada através de três sistemas de prova:

1. Cálculo Modal $\mu$: Um sistema de prova não bem-fundado onde a GTC corresponde à existência de um $\nu$-fio (expansão infinita de um maior ponto fixo). As anotações ordinais correspondem aos aproximantes padrão para maiores pontos fixos.
2. Lógicas de Ponto Fixo de Ordem Superior (HFLN): Um sistema que requer o rastreamento de ambos os rastros $\mu$ e $\nu$, demonstrando a capacidade da estrutura de lidar com estruturas de rastreamento complexas.
3. Categorias $\mu$-Bicompletas: Uma variante não bem-fundada do sistema de prova circular de Santocanale, ilustrando a capacidade da estrutura de lidar com categorias não discretas de julgamentos (onde os julgamentos variam funtorialmente com atribuições de variáveis).

Significado e Alegações

O artigo alega que sua contribuição primária é uma abstração categórica de provas não bem-fundadas que garante com sucesso a correção.

• Insight Conceitual: A GTC não é meramente uma verificação operacional, mas uma propriedade estrutural que garante que a coalgebra se torne recursiva quando vista através da lente de uma adjunção adequada (especificamente, uma guiada por semântica ordinal).
• Unificação: A estrutura unifica o tratamento da correção para vários sistemas de prova não bem-fundados sob um único mecanismo coalgebraico envolvendo funtores familiares e adjunções.
• Preenchimento de Lacuna Teórica: Aborda a lacuna nas teorias existentes de coalgebras recursivas explicando como soluções únicas podem existir para coalgebras não bem-fundadas via "levantamento" de semântica ao longo de adjunções.

Os autores observam que, embora a estrutura estabeleça a correção, trabalhos futuros são necessários para abordar completude, eliminação de corte e outras condições de correção, como condições de reinício ou fios saltitantes, dentro deste cenário coalgebraico.