Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Resumo Técnico: Unificando Sistemas de Sequentes para a Lógica de Provabilidade de Gödel-Löb

Definição do Problema
O artigo aborda uma lacuna significativa na teoria da prova da lógica de provabilidade de Gödel-Löb (GL). Embora a GL possua uma rica variedade de formalismos de estilo de sequente sem corte, as relações entre eles não foram totalmente estabelecidas. Especificamente, trabalhos anteriores haviam estabelecido correspondências teoriais de prova entre:

1. Sistemas estruturais: O sistema de sequente rotulado de Negri ($G3KGL$) e o sistema de hipersequente de árvore de Poggiolesi ($CSGL^*$), via Goré e Ramanayake.
2. Generalizações de estrutura de prova: O sistema de Gentzen de Sambin e Valentini ($GL_{seq}$), o sistema não-bem-fundado de Shamkanov ($GL_\infty$) e o sistema cíclico de Shamkanov ($GL_{circ}$), via Shamkanov.

A inter-translatabilidade de provas entre os sistemas estruturais ($G3KGL$, $CSGL^*$) e as generalizações de estrutura de prova ($GL_{seq}$, $GL_\infty$, $GL_{circ}$) permaneceu um problema em aberto. A dificuldade inerente reside em transformar provas que utilizam sequentes estruturais complexos (grafos ou árvores de sequentes de Gentzen) em provas que utilizam sequentes de Gentzen padrão, um processo que requer o "descarte" desses dados estruturais extras.

Metodologia
O autor, Tim S. Lyon, resolve este problema em aberto construindo uma cadeia de transformações sintáticas de prova que unem estas distintas formalidades. A metodologia procede em três fases primárias:

1. Reestruturação para a Forma Fim-Ativa: O artigo demonstra primeiro como reestruturar provas no sistema de hipersequente de árvore $CSGL^*$ em uma forma "fim-ativa". Em uma prova fim-ativa, as fórmulas principais e auxiliares das regras de inferência ocorrem apenas nas (pré-)folhas da estrutura de sequente de árvore. Isso é alcançado permutando regras não fim-ativas para baixo através da árvore de prova, aproveitando a invertibilidade preservadora de altura das regras em $CSGL^*$.

2. Linearização: Uma nova "técnica de linearização" é introduzida para transformar estas provas de sequente de árvore fim-ativas em provas usando sequentes aninhados lineares. Esta técnica envolve identificar caminhos específicos da raiz até uma folha no sequente de árvore e "podar" as subárvores, efetivamente colapsando a estrutura de árvore em uma sequência linear de sequentes de Gentzen. Este processo resulta em um novo cálculo, LNGL (Cálculo de Sequente Aninhado Linear para GL).

3. Forma Normal e Tradução para Gentzen: O artigo mostra que provas em LNGL podem ser transformadas em uma forma normal específica. Nesta forma, as provas procedem em estágios repetitivos: regras locais, seguidas por regras de propagação ($4L$ e $\Box L$), e finalmente a regra modal ($\Box R$). Esta prova estruturada é então traduzida para o sistema de Gentzen de Sambin e Valentini ($GL_{seq}$). Finalmente, transformações padrão mapeiam provas de $GL_{seq}$ de volta para o sistema rotulado $G3KGL$ e para os sistemas cíclicos/não-bem-fundados ($GL_{circ}$, $GL_\infty$).

Principais Contribuições

• Novo Cálculo (LNGL): O artigo introduz o LNGL, o primeiro cálculo de sequente aninhado linear sem corte para a lógica de Gödel-Löb. Este sistema opera sobre linhas de sequentes de Gentzen e retém propriedades fundamentais como invertibilidade e admissibilidade de corte.
• Nova Técnica de Linearização: O autor apresenta um método geral para extrair sistemas de sequentes aninhados lineares a partir de sistemas de hipersequentes de árvore. Esta técnica é conjecturada como aplicável a outras lógicas modais e relacionadas para gerar novos sistemas aninhados lineares.
• Correspondência Teórica de Prova Completa: O artigo estabelece uma correspondência sintática completa de seis vias entre os seguintes sistemas: $G3KGL$, $CSGL^*$, $LNGL$, $GL_{seq}$, $GL_\infty$ e $GL_{circ}$.
• Mapeamentos Construtivos: O trabalho fornece os primeiros mapeamentos construtivos de prova entre sistemas estruturais (rotulados, hipersequentes de árvore, aninhados lineares) e o sistema de sequente cíclico ($GL_{circ}$).

Resultos
O resultado primário é a demonstração de que provas em qualquer um dos seis principais sistemas de sequente para GL podem ser sintaticamente transformadas em provas em qualquer outro. Especificamente:

• Provas em $CSGL^*$ podem ser transformadas em provas fim-ativas, depois linearizadas em LNGL.
• Provas em LNGL podem ser normalizadas e transformadas em $GL_{seq}$.
• Provas em $GL_{seq}$ podem ser transformadas em $G3KGL$ e nos sistemas cíclicos ($GL_{circ}$, $GL_\infty$).
• O artigo confirma que $LNGL$ é som e completo para GL, e que provas em $LNGL$ podem ser colocadas em uma forma normal onde as aplicações de regras modais e locais se repetem em estágios.

Significância
O artigo afirma "completar o quadro" das correspondências de teoria da prova para a lógica de Gödel-Löb. Ao estabelecer estas transformações sintáticas, o trabalho permite a transferência de resultados (como propriedades de interpolação ou limites de complexidade) entre sistemas sem a necessidade de provas independentes em cada formalismo. Além disso, a introdução do LNGL fornece uma nova ferramenta para busca de prova com propriedades de complexidade ótima, enquanto a técnica de linearização oferece um caminho potencial para gerar sistemas aninhados lineares para outras lógicas. O trabalho também fornece o primeiro mapeamento constutivo entre sistemas estruturais e provas cíclicas, unindo uma lacuna entre diferentes abordagens para lidar com o raciocínio indutivo/coindutivo em lógica modal.