Resumo Técnico: A Lógica Dinâmica Proposicional Possui Interpolação de Craig

1. O Problema

O artigo aborda a questão aberta de longa data sobre se a Lógica Dinâmica Proposicional (PDL) possui a Propriedade de Interpolação de Craig (CIP). A CIP estabelece que para qualquer implicação válida $\phi \to \psi$, existe um interpolante $\theta$ tal que $\phi \to \theta$ e $\theta \to \psi$ são válidas, e $\theta$ contém apenas letras proposicionais e programas atômicos comuns a ambos $\phi$ e $\psi$.

Embora a PDL seja uma lógica modal bem estudada com resultados estabelecidos de decidibilidade e completude, seu status de interpolação permaneceu incerto por décadas. A literatura contém três tentativas anteriores de provar a interpolação:

1. Leivant (1981): Alegou uma prova, posteriormente refutada por Kracht (1999) por razões incorretas, embora uma lacuna genuína na prova de Leivant permaneça.
2. Borzechowski (1988): Uma tese de mestrado (Diplomarbeit) alegando uma prova, que recebeu pouca atenção e foi descartada por alguns como não verificável.
3. Kowalski (2002): Alegou uma prova, que foi refutada e oficialmente retirada em 2004.

A dificuldade surge porque a PDL é uma lógica de ponto fixo modal (devido ao operador de iteração $*$). Embora a interpolação tenha sido estabelecida para o $\mu$-cálculo completo e seu fragmento livre de alternância através de sistemas de prova cíclicos, as restrições específicas da PDL tornam desafiador garantir que as soluções para as equações de ponto fixo que caracterizam os interpolantes possam ser expressas dentro da PDL, em vez de requerer o poder expressivo total do $\mu$-cálculo.

2. Metodologia

Os autores fornecem uma prova construtiva baseada em um sistema de tableau cíclico e uma adaptação do método de Maehara de natureza prova-teórica.

2.1. Um Sistema de Tableau Cíclico para PDL

Os autores definem um novo sistema de tableau para PDL que opera em sequentes divididos (split sequents, pares de conjuntos de fórmulas). Características principais incluem:

• Raciocínio Local vs. Modal: O sistema distingue entre regras locais (raciocínio proposicional e desdobramento de programas dentro de um único estado) e regras modais (movimentação entre estados em um modelo de Kripke).
• Mecanismo de Desdobramento: Em vez de regras de redução padrão para cada construtor de programa, o sistema utiliza um mecanismo de "carregamento" (loading). Fórmulas da forma $[\alpha]\psi$ (onde $\alpha$ não é atômico) são desdobradas em um conjunto finito de sequentes baseados em "perfis de teste". Este conjunto, denotado $\text{unfold}_\square(\alpha, \psi)$, representa a disjunção de todos os caminhos de execução possíveis de $\alpha$ onde testes específicos têm sucesso ou falha.
• Tratamento da Iteração: Para evitar o desdobramento local infinito de fórmulas como $[\alpha^*]\psi$, o sistema elimina ocorrências regeneradas da fórmula durante o processo de desdobramento. Isso se baseia na observação de que $[\alpha^*]\psi$ é um ponto fixo de maior (greatest fixpoint).
• Provas Cíclicas: O sistema permite "repetições" (repeats - nós com rótulos idênticos a um ancestral).
  • Repetições de caminho carregado (loaded-path repeats): Uma repetição onde o caminho do ancestral (companheiro) até o nó atual consiste inteiramente de nós carregados. Estas são tratadas como folhas de sucesso (indicando um loop que satisfaz a fórmula).
  • Repetições livres (free repeats): Uma repetição onde o caminho contém nós não carregados. Estas são tratadas como folhas de insucesso, indicando um potencial contra-modelo.
• Terminação: O sistema garante a finitude ao assegurar que todas as repetições livres e repetições de caminho carregado sejam folhas, e ao utilizar o fechamento de Fischer-Ladner para limitar o conjunto de fórmulas.

2.2. Interpolação via Quasi-Tableaux e Equações de Ponto Fixo

Para construir o interpolante, os autores adaptam o método de Maehara para o contexto cíclico:

• Clusters: O tableau é visto como um grafo com arestas de retorno (back edges) das repetições para os companheiros. Os componentes fortemente conexos (SCCs) deste grafo são chamados de "clusters".
• Quasi-Tableaux: Para um cluster próprio (um SCC de elemento único), os autores definem um "quasi-tableau". Esta estrutura é usada para estabelecer um sistema de equações que caracteriza o interpolante.
• Pré-interpolantes: O método define "pré-interpolantes" para nós no quasi-tableau via indução de folha para raiz.
  • Em nós de saída (folhas que não fazem parte do cluster), o pré-interpolante é o interpolante do nó de saída (assumido existente por indução).
  • Em folhas de repetição, o pré-interpolante é uma variável proposicional interna $q_x$.
  • Em nós companheiros, o pré-interpolante é definido como a solução de uma equação de ponto fixo. Especificamente, se um companheiro $x$ tem um filho $y$ com pré-interpolante $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$, o pré-interpolante para $x$ é definido como $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$.
• Resolução na PDL: A ideia crucial é que esta construção específica garante que as soluções para as equações de ponto fixo permaneçam dentro da linguagem da PDL. O uso do operador de iteração $*$ na definição de $\iota_x$ efetivamente resolve a equação $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ dentro da PDL.
• Interpolante Final: O interpolante para a raiz do cluster é obtido substituindo as variáveis internas no pré-interpolante da raiz pelas correspondentes fórmulas de região (disjunções dos lados esquerdos dos sequentes divididos).

3. Principais Contribuições e Resultados

• Prova de CIP para PDL: O artigo estabelece que a PDL possui a Propriedade de Interpolação de Craig.
• Definibilidade de Beth: Como um corolário, o artigo prova que a PDL possui a Propriedade de Definibilidade de Beth (visto que a CIP implica a definibilidade de Beth na presença de um teorema de dedução).
• Algoritmo Construtivo: A prova é construtiva. Os autores fornecem um algoritmo claro para computar interpolantes a partir de um tableau fechado.
• Verificação Formal: Os autores formalizaram parcialmente a prova no provador de teoremas interativo Lean 4. Até o momento da escrita do artigo, os teoremas de Som e Completude, juntamente com vários lemas de suporte, foram verificados.
• Implementação: Uma implementação em Haskell do sistema de tableau e da construção do interpolante é fornecida, disponível via interface web.

4. Significância e Alegações

O artigo afirma resolver um enigma na literatura sobre o status de interpolação da PDL, fornecendo a primeira prova verificada que supera as lacunas de tentativas anteriores.

• Resolução de Questões Históricas: Os autores abordam explicitamente a história de tentativas falhas, observando que sua abordagem baseia-se nas ideias centrais de Borzechowski (1988), mas formaliza rigorosamente o tratamento de provas cíclicas e a construção de interpolantes dentro da linguagem da PDL.
• Novidade Metodológica: O artigo destaca que, embora o método de Maehara seja padrão para provas não cíclicas, aplicar o mesmo a provas cíclicas (lógicas de ponto fixo) requer a resolução de equações de ponto fixo. Os autores demonstram que, para a PDL, essas soluções podem ser expressas usando o próprio operador de iteração da lógica, um resultado não trivial que distingue a PDL de outros fragmentos onde tais soluções poderiam exigir o $\mu$-cálculo completo.
• Questões em Aberto: Os autores notam modestamente que seu método depende da presença de programas de teste ($\tau?$). Consequentemente, permanece uma questão em aberto se o fragmento livre de testes da PDL possui interpolação, já que sua construção geralmente produz interpolantes contendo testes mesmo quando a entrada é livre de testes. Eles também deixam em aberto a extensão de seu método para outras variantes da PDL (por exemplo, com com ou interseção) e as implicações para a Álgebra de Kleene com Testes (KAT).

Em resumo, o artigo fornece uma prova definitiva e construtiva da Interpolação de Craig para a PDL usando um novo sistema de tableau cíclico e uma técnica especializada de resolução de ponto fixo para interpolantes, apoiada tanto por uma implementação em Haskell quanto por uma verificação formal parcial em Lean.