A non-uniform view of Craig interpolation in modal logics with linear frames

Resumo Técnico: Uma Visão Não Uniforme da Interpolação de Craig em Lógicas Modais com Quadros Lineares

Enunciado do Problema
A Propriedade de Interpolação de Craig (PIC) é uma propriedade fundamental na lógica que estabelece que, para qualquer implicação válida $\phi \to \psi$, existe um interpolante $\iota$ utilizando apenas o vocabulário compartilhado de $\phi$ e $\psi$ tal que $\phi \to \iota$ e $\iota \to \psi$ também sejam válidas. É um fato "negativo" bem estabelecido que muitas lógicas modais normais que estendem K4.3 (a lógica de quadros transitivos lineares) carecem da PIC, particularmente aquelas com quadros de profundidade ilimitada. Tradicionalmente, a ausência da PIC encerrou a pesquisa sobre interpolantes para uma determinada lógica.

Este artigo reformula a ausência da PIC como uma questão de pesquisa, investigando o Problema da Existência de Interpolante (PEI): dado dois fórmulas $\phi$ e $\psi$ tais que $\phi \to \psi$ é válida em uma lógica $L$, existe um interpolante de Craig em $L$? Diferente da PIC uniforme, o PEI não se reduz à simples verificação de validade porque a validade da implicação não garante a existência de um interpolante. A questão central abordada é se o PEI é computacionalmente mais difícil do que o problema da validade (entailment) para essas lógicas. Resultados anteriores em outras lógicas (por exemplo, lógicas modais com nominais, fragmentos da lógica de primeira ordem) sugeriram que o PEI poderia ser significativamente mais difícil (por exemplo, 3ExpTime). Este artigo investiga se isso ocorre para lógicas modais proposicionais contendo K4.3.

Metodologia
Os autores empregam uma abordagem não uniforme, modelotética, baseada em bisimulações e quadros descritivos.

1. Caracterização por Bisimulação: O artigo utiliza um critério conhecido (Teorema 3.2) afirmando que $\phi \to \psi$ carece de um interpolante em $L$ se, e somente se, existem dois modelos, $M_1$ e $M_2$, baseados em quadros descritivos para $L$, tais que $M_1$ satisfaz $\phi$, $M_2$ satisfaz $\neg\psi$, e os pontos raiz desses modelos são $\sigma$-bisimilares (onde $\sigma$ é a assinatura compartilhada).
2. Quadros Descritivos: A análise depende fortemente da estrutura de quadros descritivos (quadros equipados com uma álgebra específica de conjuntos internos satisfazendo condições de diferenciação, densidade e compacidade). Isso é crucial porque, para lógicas como GL.3 e Log{(N, <)}, contraexemplos à PIC não podem ser testemunhados por quadros de Kripke padrão, mas exigem quadros descritivos infinitos.
3. Decomposição Estrutural: A inovação técnica central envolve a análise da estrutura desses modelos bisimilares. Os autores particionam os modelos em $\sigma$-blocos (intervalos de pontos com propriedades de bisimulação específicas) e mostram que qualquer par de modelos bisimilares que testemunha a falta de um interpolante pode ser transformado em um par de modelos "quasi-finitos". Esses modelos são construídos como somas ordenadas de modelos simples baseados em quadros atômicos específicos (cadeias finitas, clusters finitos ou estruturas de "tadpole" como $C(\bigcirc_k, \bullet)$).
4. Propriedade Quasi-Polinomial: Para lógicas finitamente axiomatisáveis, os autores provam que esses modelos testemunhas podem ser limitados em tamanho por um polinômio no tamanho das fórmulas de entrada e nos axiomas da lógica. Isso é denominado propriedade de modelo bisimilar quasi-polinomial.

Principais Contribuições e Resultados

• Decidibilidade e Complexidade: O artigo prova que, para todas as lógicas modais normais finitamente axiomatisáveis contendo K4.3, o PEI é decidível e coNP-completo.

  • Este resultado é significativo porque mostra que o PEI não é mais difícil que o problema da validade (que também é coNP para essas lógicas). Isso contrasta fortemente com resultados recentes de interpolação não uniforme em outros frameworks lógicos onde o PEI é estritamente mais difícil.
  • A prova envolve um algoritmo não determinístico que adivinha modelos de tamanho polinomial satisfazendo o critério de bisimulação e verifica os axiomas da lógica.

• Propriedade de Modelo Bisimilar Quasi-Polinomial: Os autores estabelecem que todas as extensões de K4.3 finitamente axiomatisáveis possuem a "propriedade de modelo bisimilar quasi-polinomial". Isso significa que, se um interpolante não existe, existe um par de modelos bisimilares testemunhando este fato onde os modelos são somas ordenadas de um número polinomial de modelos simples baseados em quadros atômicos de tamanho polinomial.

  • Para lógicas de subquadro cofinales d-persistentes (uma subclasse), a propriedade é ainda mais forte: elas possuem a propriedade de modelo bisimilar polinomial, onde os modelos são quadros de Kripke padrão de tamanho polinomial.

• Extensão para Lógicas Temporais Prioreanas: A metodologia é estendida para lógicas temporais prioreanas (contendo tanto modalidades de futuro quanto de passado) sobre fluxos de tempo padrão:

  • Lin (todos os quadros lineares), LinQ (racionais) e LinR (reais): Mostra-se que essas lógicas possuem a propriedade de modelo bisimilar polinomial, e seu PEI é coNP-completo.
  • Lin<ω (ordens lineares estritas finitas) e LinZ (inteiros): Estas lógicas não possuem a propriedade polinomial, mas possuem a propriedade de modelo bisimilar quasi-polinomial. Seu PEI também é provado como sendo coNP-completo.
  • A prova para lógicas temporais requer o tratamento de cadeias bidirecionais e clusters de limite em ambas as direções, necessitando de novas construções de quadros (por exemplo, quadros "tadpole" simétricos $C(\bullet, \bigcirc_k, \bullet)$).

Significância e Alegações
O artigo afirma fornecer o primeiro resultado geral sobre a existência de interpolantes de Craig cobrindo uma grande família de lógicas modais (extensões de K4.3) que carecem da PIC. Ao demonstrar que o PEI é coNP-completo para essas lógicas, os autores desafiam a intuição de que a ausência da PIC necessariamente leva a uma classe de complexidade superior para o problema de existência.

O trabalho sugere que a complexidade do PEI não está inerentemente ligada à falha da PIC, mas sim depende das propriedades estruturais dos modelos necessários para testemunhar essa falha. Os autores posicionam isso como um passo em direção a uma classificação de lógicas modais baseada na complexidade de seu PEI.

O artigo observa explicitamente que sua prova não é construtiva em relação ao cálculo dos interpolantes; ela fornece um procedimento de decisão para a existência, mas não produz um algoritmo eficiente para calcular o próprio interpolante ou limites superiores sobre seu tamanho. Os autores também destacam que os quadros descritivos são essenciais para suas provas, levantando a questão aberta de se os quadros de Kripke são suficientes para o PEI em lógicas que não são d-persistentes, mas que são fortemente completas em Kripke (como LinR).