Computation by infinite descent made explicit

Problema e Motivação
A teoria da prova não-bem-fundada, que se originou no contexto do $\mu$-cálculo modal, permite que árvores de prova infinitas representem raciocínios indutivos e coindutivos. Um desafio central neste campo é definir um critério de correção que distinga provas válidas de árvores de derivação inválidas. Os critérios tradicionais, como a condição de "traço" (trace) ou de "fio progressivo" (progressing thread), exigem que cada ramo infinito de uma árvore de prova contenha uma sequência específica de fórmulas onde um ponto fixo mínimo é desenrolado infinitamente à esquerda ou um ponto fixo máximo à direita.

No entanto, trabalhos recentes por Baelde et al. [BDKS22] identificaram limitações nas condições baseadas em traços, particularmente no que diz respeito à composicionalidade. Eles introduziram os "fios saltitantes" (bouncing threads) para lidar com casos em que cortes desconectam os traços, mas observaram que esta condição é indecidível e interage mal com as regras estruturais dos sistemas de prova. Além disso, embora a correspondência Curry-Howard veja as provas como programas, estabelecer que provas não-bem-fundadas representam funções computáveis (normalização) é não trivial sob estas condições de validade complexas.

Este artigo aborda o problema da composicionalidade e do conteúdo computacional das provas não-bem-fundadas explorando um quadro alternativo: sistemas de prova com variáveis ordinais explícitas. Esta abordagem, pioneirada por Dam, Gurov e Sprenger [DG02, SD03a], anota fórmulas de ponto fixo com variáveis representando aproximantes ordinais. O artigo investiga se este quadro pode fornecer um critério de correção mais transparente que suporte uma interpretação Curry-Howard robusta, potencialmente capturando provas que as condições de traço padrão perdem, mantendo-se, contudo, decidível.

Metodologia
O autor, Sebastian Enqvist, desenvolve um sistema de prova não-bem-fundado para a lógica proposicional intuicionista estendida com definições indutivas ($\mu$) e coindutivas ($\nu$). A metodologia central envolve:

1. Extensão da Sintaxe: A linguagem é estendida com variáveis ordinais explícitas e restrições. Fórmulas como $\mu X. A$ são anotadas como $\mu_\alpha X. A$, onde $\alpha$ é um termo ordinal (variáveis $a, b, \dots$ ou uma constante $\infty$). Os sequentes incluem uma árvore de restrições $O$ representando desigualdades entre estes termos ordinais.
2. Critério de Validade: Uma derivação é definida como válida se, para cada ramo infinito, existir uma cadeia descendente infinita de variáveis ordinais ($a_0 > a_1 > a_2 > \dots$) que eventualmente se verifica naquele ramo. Isto torna o argumento de "descida infinita", central para a correção do raciocínio indutivo, explícito na sintaxe.
3. Semântica de Computabilidade: O artigo define uma noção de computabilidade para derivações fechadas. Uma prova é computável se ela reduz a uma forma normal que satisfaz cláusulas indutivas específicas correspondentes aos conectivos lógicos e pontos fixos. Por exemplo, uma prova de um ponto fixo mínimo $\mu_\infty X. A$ é computável se ela reduz a uma prova de um aproximante $\mu_\xi X. A$ para algum $\xi$ ordinal.
4. Reduções de Corte: Um conjunto de regras de reescrita (reduções de corte e regras de permutação) é introduzido para definir o comportamento computacional das provas. O sistema é projetado para ser conforme sob estas regras específicas, permitindo uma noção bem definida de normalização.
5. Modelagem Categórica: Uma categoria de provas é construída onde os objetos são fórmulas fechadas e as setas são classes de equivalência de provas. O autor demonstra que esta categoria suporta a estrutura de álgebras iniciais e coálgebras finais para os respetivos pontos fixos.

Principais Contribções e Resultados

• Computabilidade de Provas Válidas: O resultado principal (Teorema 4.9) estabelece que toda prova válida (aquela que satisfaz a condição de cadeia descendente infinita) é computável. Isto é provado mostrando que, se uma prova fosse não-computável, seria possível construir um ramo infinito sem uma cadeia descendente de ordinais, contradizendo a condição de validade.
• Normalização para Fórmulas Finitárias: Como consequência do resultado de computabilidade, o artigo prova que provas de "fórmulas finitárias" (fórmulas construídas a partir de $\top, \land, \lor, \mu$ sem $\nu$) sempre normalizam para uma forma normal única (Teorema 4.11).
• Representação de Funções: O sistema produz um resultado de normalização para provas de sequentes da forma $N, \dots, N \vdash N$ (onde $N$ representa números naturais). Tais provas representam funções totais únicas sobre números naturais (Teorema 4.12).
• Lidando com Casos de "Salto" (Bouncing): O artigo demonstra que o quadro de variáveis ordinais pode capturar provas que falham na condição de fio progressivo padrão, mas que são válidas sob a condição de fio saltitante. É fornecido um exemplo onde um corte interrompe um traço padrão, mas as variáveis ordinais explícitas na fórmula do corte preservam o argumento de descida, tornando a prova válida neste sistema.
• Semântica Categórica: O artigo constrói um modelo categórico onde os pontos fixos mínimos correspondem a álgebras iniciais e os pontos fixos máximos a coálgebras finais (Secções 5.2 e 5.3). Isto confirma que a semântica de computabilidade se alinha com as interpretações categóricas padrão de tipos indutivos e coindutivos.
• Decidibilidade: Ao contrário da condição de fio saltitante, o critério de validade baseado em variáveis ordinais é conhecido por ser decidível [SD03a].

Significância e Alegações
O artigo posiciona-se como um estudo piloto que contribui para o projeto iniciado por Baelde et al. [BDKS22] de encontrar critérios de validade naturais para provas não-bem-fundadas que se estendam além dos padrões de traço. O autor afirma que o quadro de variáveis ordinais explícitas de Dam-Gurov-Sprenger é um candidato adequado para este propósito.

A significância reside em duas observações principais:

1. Expressividade: A condição de validade captura provas (especificamente aquelas com comportamento de "salto") que não são reconhecidas como válidas pela condição de fio progressivo padrão.
2. Significado Computacional: Ao fornecer uma semântica de computabilidade, o artigo demonstra que todas as provas válidas neste sistema representam programas computáveis bem definidos. Isto preenche a lacuna entre a condição de validade sintática e o requisito semântico de terminação/computabilidade.

O autor nota modestamente que o artigo não fornece um teorema completo de eliminação de corte para a lógica (o que exigiria regras de permutação adicionais), nem uma prova definitiva de que o sistema de variáveis ordinais é equivalente em poder à condição de fio saltitante. Em vez disso, deixa a questão de se toda prova válida sob a condição de fio saltitante pode ser representada usando variáveis ordinais como um problema aberto para investigação futura. O trabalho serve para motivar a exploração adicional das variáveis ordinais sob uma perspectiva Curry-Howard.