Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents

1. O Problema

O artigo aborda a dificuldade de desenvolver procedimentos de busca de prova (proof-search) para Lógicas de Tempo Intuicionistas (ITLs), especificamente a lógica básica $IKt$ de Ewald e suas extensões com axiomas de reflexividade (T), simetria (B) e serialidade (D).

Existem dois obstáculos principais que tornam a automação e a extração de modelos nestas lógicas notoriamente difíceis:

1. Não-Terminação devido à Transitividade: As lógicas intuicionistas são caracterizadas semanticamente por modelos de Kripke bi-relacionais onde a relação de acessibilidade intuicionista ($\leq$) é transitiva. Em cálculos de sequentes, essa transitividade pode levar a buscas de prova que nunca terminam, exigindo mecanismos sofisticados de verificação de loops (loop-checking).
2. Não-Invertibilidade das Regras: Diferente da lógica clássica, as regras de inferência em lógicas de modais intuicionistas (especialmente $\to R$ e regras de propagação modal) não são invertíveis. Isso significa que a validade da conclusão não implica necessariamente a validade das premissas. Consequentemente, a busca de prova gera uma estrutura ramificada (branching) intrínseca, impedindo a construção de uma única derivação linear. Isso torna difícil extrair tanto uma prova (em caso de sucesso) quanto um contra-modelo (em caso de falha) usando métodos tradicionais.

O objetivo do artigo é preencher essa lacuna, fornecendo um algoritmo de busca de prova que garanta a terminação e permita a extração de contra-modelos finitos quando a prova falha, estabelecendo assim a Propriedade do Modelo Finito (FMP).

2. Metodologia

A abordagem proposta baseia-se no formalismo de Sequentes Aninhados (Nested Sequents), que generaliza o formalismo de Gentzen ao permitir sequentes dentro de outros sequentes, representando estruturas de árvores.

A. Estrutura de Dados: Sequentes Aninhados e Árvores Seq

O autor utiliza sequentes aninhados onde as fórmulas modais introduzem novos componentes (nós) na estrutura. Cada componente é rotulado com um nome único, permitindo a representação de modelos bi-relacionais como árvores rotuladas (seq-trees).

B. O Algoritmo de Busca: ProveC

O algoritmo central, ProveC, opera de baixo para cima (bottom-up) e gera uma estrutura chamada Árvore de Computação (Computation Tree), em vez de uma única derivação.

• Ramificação Conjunção vs. Disjunção:
  • Regras invertíveis (como $\lor L$, $\land R$) geram ramificação conjuntiva (ambos os ramos devem ser provados).
  • Regras não-invertíveis ($\to R$, $[x]R$) geram ramificação disjuntiva. O algoritmo aplica uma regra de ramificação disjuntiva (db) que tenta todas as combinações possíveis de aplicação dessas regras simultaneamente.
• Árvore de Computação: É uma estrutura que codifica todas as derivações possíveis do input. Se a busca falha em todos os ramos, a árvore inteira representa o fracasso.

C. Verificação de Loops via Homomorfismos

Para garantir a terminação e detectar repetições (loops) que levariam a uma busca infinita, o autor introduz uma técnica inovadora de verificação de loops baseada em homomorfismos:

• Uma repetição (repeat) ocorre quando um sequente aninhado em um ramo da árvore de computação é morficamente equivalente a um de seus ancestrais.
• São definidos morfismos fracos e fortes entre as árvores de sequentes. Um repeat é detectado se existir um morfismo forte de um nó atual para um nó ancestral.
• O autor prova que o número de classes de equivalência de sequentes aninhados de profundidade limitada é finito. Pelo princípio do pombal, qualquer ramo infinito deve conter uma repetição, permitindo que o algoritmo pare.

D. Extração de Contra-Modelos

Quando a busca falha (a árvore de computação é totalmente marcada como "Falso" e contém repetições), o algoritmo extrai um contra-modelo finito:

1. Blueprint: A árvore de computação é processada para criar um "blueprint" contendo apenas os sequentes saturados e rotulados como falha.
2. Renomeação: Para evitar identificar erroneamente mundos de diferentes sequentes, aplica-se um mecanismo de renomeação sistemática.
3. Construção do Modelo:
   • Mundos: São os nós (nomes) dos componentes dos sequentes no blueprint.
   • Relação Intuicionista ($\leq$): Definida por sequências de morfismos (naturais e fortes) ao longo do blueprint.
   • Relação Modal ($R$): Definida pelas conexões explícitas nos sequentes e pelas condições de fechamento (closure) dos axiomas (T, B, D).
4. Correção: O modelo extraído é provado satisfazer as condições de um modelo bi-relacional e falsificar a fórmula de entrada.

3. Principais Contribuições

1. Algoritmo de Busca de Prova Terminante: Apresentação do primeiro algoritmo de busca de prova especificamente desenvolvido para sistemas de sequentes aninhados não-invertíveis, garantindo terminação através de verificação de loops baseada em homomorfismos.
2. Estrutura de Árvore de Computação: Introdução de uma nova estrutura de dados que generaliza a derivação única, permitindo lidar com a ramificação disjuntiva inerente às regras não-invertíveis da lógica intuicionista.
3. Extração de Contra-Modelos Finitos: Demonstração de como extrair modelos bi-relacionais finitos diretamente das árvores de computação falhas, definindo a relação intuicionista através de sequências de morfismos entre sequentes.
4. Prova da Propriedade do Modelo Finito (FMP): Estabelecimento rigoroso da FMP para as lógicas $IKt \cup A$ (onde $A \subseteq \{T, B, D\}$). O artigo corrige implicitamente uma tentativa anterior falha de Ewald (1986) de provar essa propriedade, fornecendo uma prova correta via métodos sintáticos.
5. Decidabilidade: Consequência direta da terminação do algoritmo e da FMP, provando que essas lógicas são decidíveis.

4. Resultados

• Correção e Completude: O sistema de sequentes aninhados proposto é demonstrado ser correto (sound) e completo (complete) para as lógicas alvo.
• Terminação: O algoritmo ProveC é provado terminar para qualquer fórmula de entrada, devido aos limites na profundidade dos sequentes e à detecção de repetições via morfismos.
• FMP e Decidabilidade: O Teorema 4.20 conclui que para $C \subseteq \{T, B, D\}$, a lógica $IKtC$ possui a Propriedade do Modelo Finito e é decidível.
• Exemplos: O artigo fornece exemplos detalhados de como a árvore de computação é construída, como os loops são detectados (Exemplo 4.14) e como o contra-modelo é extraído visualmente (Exemplo 4.17 e Figura 5).

5. Significado e Impacto

Este trabalho é significativo por resolver um problema aberto na área de lógica modal intuicionista e lógica temporal: a automação da busca de prova com extração de contra-modelos para lógicas não-invertíveis.

• Fundamentos Teóricos: Fornece uma base sólida para a decidabilidade de extensões de $IKt$, corrigindo lacunas históricas na literatura sobre a FMP dessas lógicas.
• Aplicações Computacionais: A capacidade de extrair contra-modelos finitos é crucial para ferramentas de verificação de modelos e depuração de especificações em sistemas computacionais que utilizam lógica temporal intuicionista (ex: verificação de programas concorrentes ou sistemas reativos).
• Metodologia Geral: A técnica de usar morfismos para verificação de loops em sequentes aninhados pode ser generalizada para outras classes de lógicas modais e gramáticas, sugerindo caminhos para resolver problemas de decidabilidade em lógicas modais transitivas (como $IS4$), que permanecem como problemas em aberto.

Em resumo, o artigo oferece uma solução completa e mecanizável para a análise sintática e semântica de lógicas de tempo intuicionistas, superando as barreiras impostas pela não-invertibilidade e pela transitividade da relação de acessibilidade.