Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability

Resumo Técnico: Sequentes Aninhados para Lógicas Multimodais Intuicionistas

Enunciado do Problema
O artigo aborda a ausência de sistemas de prova analíticos para as Lógicas de Gramática Intuicionistas (IGLs), uma ampla classe de lógicas multimodais intuicionistas introduzida em [35]. Embora as IGLs sirvam como contrapartes intuicionistas das lógicas de gramática clássicas (CGLs) e subsumam as lógicas modais e temporais intuicionistas padrão (incluindo extensões de IK e IKt com os axiomas T, B, 4, 5 e D), anteriormente elas eram equipadas apenas com axiomatizações no estilo de Hilbert. Esses sistemas de Hilbert são subótimos para análise metalógica porque invalidam a propriedade do subfórmula, dificultando o estudo de propriedades como decidibilidade, interpolação e raciocínio automatizado. Além disso, abordagens baseadas em sequentes existentes para lógicas modais intuicionistas (por exemplo, sequentes rotulados ou sequentes aninhados) frequentemente lutam para lidar naturalmente com modalidades inversas e condições de quadro complexas (como axiomas de caminho), mantendo a modularidade e a eliminação de corte.

Metodologia
O autor introduz cálculos de sequentes aninhados de conclusão única para IGLs, formulados dentro da estrutura de sequentes aninhados. Essa estrutura generaliza os sequentes de Gentzen para árvores de sequentes, permitindo uma representação mais natural das dependências modais e das modalidades inversas do que os sequentes tradicionais.

A metodologia baseia-se em três componentes técnicos centrais:

1. Parametrização Teórica de Gramática: Os cálculos são parametrizados por um conjunto de axiomas $\mathcal{A}$ (especificamente axiomas de serialidade e Axiomas de Caminho Intuicionistas, ou IPAs). Esses axiomas são codificados como gramáticas $\mathcal{A}$ (sistemas de Semi-Thue) que definem regras de reescrita de strings sobre o alfabeto das modalidades.
2. Regras de Propagação: O sistema emprega regras de propagação especializadas ($\langle x \rangle R$ e $[x]L$) que tratam sequentes aninhados como autômatos. Essas regras permitem que fórmulas sejam propagadas ao longo de caminhos dentro da estrutura de árvore de um sequente, desde que o caminho corresponda a uma string gerada pela gramática $\mathcal{A}$.
3. A Regra de Deslocamento: Uma nova regra estrutural, denotada $sft(\mathcal{A})$, é introduzida. Essa regra unifica o tratamento de todas as condições de quadro induzidas por IPAs em um único mecanismo estrutural, em vez de exigir regras estruturais distintas para cada axioma específico.

Principais Contribuições

1. Primeiros Cálculos de Sequentes Aninhados para IGLs: O artigo inicia a teoria da prova estrutural das IGLs definindo o cálculo $NIK_m(\mathcal{A})$. Estabelece a correção e completude desses sistemas em relação à semântica bi-relacional das IGLs.
2. Modularidade e a Regra de Deslocamento: O autor demonstra que os cálculos são modulares; transformar um sistema de uma IGL para outra envolve apenas mudanças sistemáticas nas condições laterais das regras de propagação. A introdução da regra de deslocamento é uma novidade central, unificando o tratamento dos axiomas de caminho.
3. Eliminação de Corte Sintática Uniforme: O artigo fornece uma prova sintática uniforme de admissibilidade de corte para todas as IGLs. Diferentemente de abordagens anteriores que frequentemente dependem de regras estruturais ad hoc ou traduções indiretas (por exemplo, para cálculos de exibição), essa prova aproveita a admissibilidade que preserva a altura da regra de deslocamento para eliminar cortes diretamente dentro da estrutura de sequentes aninhados.
4. Embutimento Fiel e Indecidibilidade: O autor define uma tradução negativa (adaptada de Gödel, Gentzen e Kolmogorov) que embute as Lógicas de Gramática Clássicas (CGLs) nas IGLs. Esse embutimento é atestado por transformações de prova entre provas de sequentes aninhados de múltiplas conclusões (para CGLs) e provas de sequentes aninhados de conclusão única (para IGLs).

Resultados

• Propriedades Metalógicas: Os cálculos satisfazem propriedades fundamentais, incluindo a admissibilidade de regras estruturais (enfraquecimento, contração, corte) e a invertibilidade da maioria das regras à esquerda (embora $\to L$ seja notada como não invertível).
• Completude: A completude é estabelecida sintaticamente como um corolário da prova de admissibilidade de corte.
• Indecidibilidade: Ao reduzir o problema geral de validade das CGLs (conhecido por ser indecidível [2]) ao das IGLs via tradução negativa, o artigo prova que o problema geral de validade para IGLs é indecidível.
• Propriedade de Separação: Os sistemas satisfazem a propriedade de separação, garantindo que as IGLs sejam extensões conservadoras de seus contrapartes de modalidade única (lógicas modais intuicionistas padrão).

Significado
O artigo reivindica significado em três áreas primárias:

1. Fundacional: Preenche uma lacuna na teoria da prova das lógicas modais intuicionistas ao fornecer os primeiros sistemas de sequentes analíticos e livres de corte para a ampla classe das IGLs, indo além dos sistemas de Hilbert.
2. Metodológico: A introdução da regra de deslocamento oferece uma abordagem unificada e modular para lidar com condições de quadro em sequentes aninhados, simplificando argumentos de eliminação de corte e evitando a proliferação de regras estruturais ad hoc encontradas em trabalhos anteriores [5, 38, 48].
3. Teórico da Complexidade: Ao estabelecer um embutimento fiel das lógicas de gramática clássicas no cenário intuicionista, o trabalho esclarece o panorama computacional das IGLs, provando que o problema geral de validade é indecidível para essa classe. Esse resultado é derivado diretamente da indecidibilidade das CGLs, em vez de ser uma análise de complexidade independente.

O autor observa que, embora os sistemas atuais não sejam totalmente invertíveis (especificamente no que diz respeito à regra $\to L$), eles fornecem uma base robusta para pesquisas futuras sobre sistemas totalmente invertíveis (potencialmente via generalizações rotuladas) e a identificação de fragmentos decidíveis dentro da classe indecidível das IGLs.