Wider systems for linear logic with fixed points: proof theory and complexity

Resumo Técnico: Sistemas Infinitários para Lógica Linear com Pontos Fixos

1. Problema e Contexto

O artigo investiga a teoria da prova e a complexidade computacional de sistemas de lógica linear com pontos fixos (mínimos e máximos), especificamente extensões da lógica linear multiplicativa-aditiva (MALL) denominadas $\mu$MALL$_{\alpha,\alpha}$.

• O Desafio: Sistemas anteriores de lógica com pontos fixos (como $\mu$MALL padrão ou sistemas com ramificação $\omega$) são adequados apenas para modelos contínuos, onde os operadores atingem seus pontos fixos em no máximo $\omega$ passos. No entanto, modelos gerais (como o cálculo modal $\mu$ ou aritmética de primeira ordem) podem exigir ordinais de fechamento arbitrários (transfinitos) para atingir a estabilidade dos pontos fixos.
• A Questão Central: Qual é a complexidade algorítmica do problema de provabilidade (decidibilidade) nestes sistemas quando a ramificação das regras de inferência é indexada por um ordinal computável $\alpha$ arbitrário? O artigo busca classificar essa complexidade dentro da hierarquia hiperaritmética.

2. Metodologia

Os autores utilizam uma abordagem fundamentada na teoria da prova estrutural, combinando técnicas de eliminação de cortes, focagem (focussing) e uma análise refinada de ordinais.

• Sistemas $\mu$MALL$_{\alpha,\alpha}$: O sistema é definido com regras de pontos fixos ($\mu$ e $\nu$) que permitem ramificação indexada por ordinais $\beta \leq \alpha$. As regras $\nu_\beta$ possuem premissas infinitas indexadas por todos $\gamma < \beta$.
• Rank de Fórmulas (Medida de Complexidade): Uma contribuição metodológica crucial é a definição de uma função de rank (ranqueamento) para fórmulas baseada em operações naturais de ordinais (soma natural $\oplus$ e produto natural $\otimes$). Diferente de abordagens anteriores que usavam o tamanho da fórmula ou o máximo, o uso da soma natural permite um limite superior "apertado" (tight bound) para a altura da árvore de busca de provas sem cortes.
• Fundamentos de Prova:
  1. Eliminação de Corte: Demonstram que qualquer prova em $\mu$MALL$_{\alpha,\alpha}$ pode ser transformada em uma prova sem cortes, preservando a terminação da busca.
  2. Focagem (Focussing): Estabelecem um teorema de focagem que organiza a busca de provas em fases síncronas (não invertíveis) e assíncronas (invertíveis), restringindo drasticamente o espaço de busca necessário para a análise de complexidade.
• Reduções Computacionais:
  • Limite Superior: Codificam a busca de provas sem cortes como uma definição indutiva positiva sobre ordinais, mostrando que o conjunto de teoremas é enumerável computavelmente em relação a um "salto de Turing" iterado $\omega^{\alpha\omega}$ vezes.
  • Limite Inferior: Codificam fórmulas infinitárias computáveis (sentenças verdadeiras da hierarquia hiperaritmética) dentro do sistema $\mu$MALL$_{\alpha,\alpha}$, simulando máquinas de Minsky e a semântica de verdade de sentenças infinitárias.

3. Principais Contribuições

1. Generalização de Ordinais: Estendem a teoria de pontos fixos em lógica linear de ramificação $\omega$ para ordinais computáveis arbitrários $\alpha$, permitindo modelar comportamentos de fechamento transfinitos.
2. Novo Conceito de Rank: Introduzem um rank de fórmulas baseado em operações naturais de ordinais que fornece um limite superior exato para a altura das provas sem cortes, superando limitações de definições anteriores (como as de [2, 12]).
3. Teorema de Focagem para Sistemas Infinitários: Adaptam a disciplina de focagem para sistemas com ramificação ordinal infinita, provando que a busca de provas pode ser normalizada em uma forma focada.
4. Classificação de Complexidade Completa: Estabelecem uma correspondência exata entre o ordinal de fechamento $\alpha$ e o nível da hierarquia hiperaritmética.

4. Resultados Principais

O resultado central é o Teorema 2.8:

Para ordinais computáveis $\alpha \geq \omega$, o problema de provabilidade no sistema $\mu$MALL$_{\alpha,\alpha}$ é $\Sigma^0_{\omega^{\alpha\omega}}$-completo (sob reduções de Turing).

• Interpretação:
  • O nível de complexidade não é apenas $\omega^\alpha$, mas sim $\omega^{\alpha\omega}$.
  • Para $\alpha = \omega$, o sistema é $\Sigma^0_{\omega^\omega}$-completo.
  • Para $\omega \leq \alpha < \omega^\omega$, o sistema permanece $\Sigma^0_{\omega^\omega}$-completo (Corolário 8.1), indicando que a complexidade salta apenas quando o grau do ordinal ($\text{deg } \alpha$) aumenta.
• Mecanismo:
  • Limite Superior: A completude é provada mostrando que o conjunto de teoremas é enumerável a partir de $H(b)$ (o conjunto hiperaritmético associado a uma notação de $\omega^{\alpha\omega}$).
  • Limite Inferior: A dureza (hardness) é provada reduzindo o conjunto de sentenças infinitárias verdadeiras (completas para cada nível da hierarquia) para a provabilidade em $\mu$MALL$_{\alpha,\alpha}$, utilizando a codificação de máquinas de Minsky e a estrutura de pontos fixos para simular a iteração transfinita da verdade.

5. Significado e Impacto

• Precisão na Classificação de Complexidade: O trabalho fornece uma classificação precisa de como a "profundidade" da indução/coindução (medida pelo ordinal $\alpha$) se traduz em complexidade computacional. Mostra que a lógica linear com pontos fixos transfinitos é um sistema extremamente expressivo, capaz de capturar níveis profundos da hierarquia hiperaritmética.
• Ferramentas de Teoria da Prova: A demonstração de que a eliminação de corte e a focagem funcionam em sistemas com raminação ordinal infinita valida a robustez das ferramentas da teoria da prova estrutural para lidar com lógica infinitária.
• Comparação com Outros Sistemas: O resultado contrasta com outras lógicas de ação infinitária (como a lógica de ação com multiplexação), que possuem complexidade significativamente menor ($\Sigma^0_{\omega^\omega}$), destacando como a combinação de conectivos multiplicativos, aditivos e pontos fixos transfinitos eleva a complexidade.
• Aplicações Teóricas: Oferece uma base formal para entender a complexidade de sistemas que modelam recursão profunda, verificação de programas com loops infinitos e semântica de linguagens de programação com tipos recursivos complexos.

Em suma, o artigo estabelece que a provabilidade em lógica linear com pontos fixos parametrizados por um ordinal $\alpha$ é exatamente tão complexa quanto o nível $\omega^{\alpha\omega}$ da hierarquia hiperaritmética, unindo profundamente a teoria dos ordinais, a teoria da prova e a teoria da computabilidade.