Uniform Interpolation of Basic Tense Logic

Resumo Técnico: Interpolação Uniforme da Lógica de Tempo Básica

Problema
O artigo aborda o problema em aberto de estabelecer a propriedade de interpolação uniforme para a lógica de tempo básica (também conhecida como lógica modal de duas vias ou lógica modal com conversa), denotada por $K_t$. Embora a propriedade de interpolação de Craig para $K_t$ esteja bem estabelecida através de métodos tanto prova-teóricos quanto semânticos, a propriedade de interpolação uniforme — que exige a existência de um "interpolante uniforme" $\exists p.\phi$ para qualquer fórmula $\phi$ e variável $p$, tal que $\exists p.\phi$ seja independente de $p$ e preserve relações de provabilidade com todas as fórmulas livres de $p$ — não havia sido totalmente demonstrada para esta lógica. O autor observa que, embora Visser (1996) tenha fornecido um argumento semântico para a interpolação uniforme da lógica modal básica $K$ usando bisimulações em camadas, este resultado não havia sido estendido à expansão de tempo envolvendo modalidades de conversa.

Metodologia
O artigo emprega uma abordagem semântica, estendendo o argumento modelo-teórico de Visser baseado em bisimulações em camadas (ou limitadas) para o contexto da lógica de tempo. A metodologia procede através das seguintes etapas:

1. Definições e Estrutura: O autor define a sintaxe e a semântica da lógica de tempo básica, introduzindo o sistema de Hilbert padrão $H(K_t)$ e a semântica de Kripke com modalidades de avanço ($\square$) e retrocesso ($\blacksquare$). O conceito de bisimulação em camadas é adaptado para a lógica de tempo, incorporando condições para ambas as transições de avanço (Forth, Back) e retrocesso (Forth$^{-1}$, Back$^{-1}$), indexadas pela profundidade modal $n$.
2. Propriedade de Expansão de Bisimulação: Uma condição suficiente para que uma lógica de tempo normal $\Lambda_{\mathcal{F}}$ (associada a uma classe de quadros $\mathcal{F}$) possua a propriedade de interpolação uniforme é formulada. Esta condição, denominada propriedade de expansão de bisimulação, exige que, para quaisquer dois modelos pontuados $(M_1, w_1)$ e $(M_2, w_2)$ em $\mathcal{F}$ que sejam bisimilares até a profundidade $n$ sobre um conjunto compartilhado de variáveis, exista um modelo intermediário $(N, x)$ em $\mathcal{F}$ que os conecte via bisimulações sobre os respectivos conjuntos de variáveis.
3. Construção do Modelo Intermediário: A principal contribuição técnica envolve provar que a classe de todos os quadros ($\mathcal{F}_{all}$) possui a propriedade de expansão de bisimulação. O autor constrói um modelo intermediário $N$ tomando a união disjunta dos dois modelos de entrada e adicionando um novo estado "universal" $T$ conectado a todos os estados. A relação em $N$ é definida sobre um espaço de produto envolvendo os estados dos modelos originais e um índice de "camada", efetivamente simulando as etapas de bisimulação necessárias para satisfazer a propriedade de expansão.
4. Resultados de Transferência: O artigo investiga a preservação da propriedade de interpolação uniforme sob várias extensões:
   • Imagens Espelhadas: Se uma lógica $\Lambda$ é invariante sob a operação de imagem espelhada (troca de $\square$ por $\blacksquare$), a propriedade se transfere para extensões por axiomas de imagem espelhada.
   • Axiomas Constantes: A propriedade é preservada ao adicionar fórmulas constantes (fórmulas sem variáveis proposicionais).
   • Tradução Boxdot: A propriedade é mostrada como se transferindo para a contraparte reflexiva de uma lógica via tradução boxdot.
5. Construção de Contraexemplo: Para demonstrar os limites da propriedade, o artigo analisa a expansão de tempo da lógica modal $S4$ (denotada como $S4_t$). Usando uma construção de modelo específica (um caminho infinito com valores de verdade alternados para uma proposição $r$) e um argumento de bisimulação em camadas, o autor prova que $S4_t$ carece da propriedade de interpolação uniforme.

Principais Contribuições e Resultados

• Teorema Principal: O artigo estabelece que a lógica de tempo básica mínima $K_t$ possui a propriedade de interpolação uniforme. Isso é alcançado ao provar que a classe de todos os quadros satisfaz a propriedade de expansão de bisimulação.
• Caracterização Semântica: Demonstra-se que o interpolante uniforme em $K_t$ coincide com um quantificador de bisimulação. Especificamente, uma fórmula $\exists p.\phi$ é verdadeira em um estado se, e somente se, existe um modelo bisimilar (onde $p$ é interpretado de forma diferente) no qual $\phi$ é verdadeiro.
• Extensão para Sublógicas: A propriedade de interpolação uniforme é mostrada como válida para várias extensões de $K_t$, incluindo aquelas definidas por axiomas constantes (ex: existência de momentos iniciais/finais) e extensões invariantes de imagem espelhada.
• Falha em $S4_t$: O artigo prova que a expansão de tempo de $S4$ ($S4_t$) não possui a propriedade de interpolação uniforme. Este resultado estende as descobertas anteriores de Ghilardi e Zawadowski sobre $S4$ para o cenário de tempo, mostrando que a adição de axiomas de reflexividade e transitividade quebra a propriedade de interpolação uniforme.
• Mecanismos de Transferência: O artigo fornece provas formais para a transferência da propriedade de interpolação uniforme via imagens espelhadas, extensões constantes e a tradução boxdot, permitindo a derivação de resultados para lógicas como $K_t \oplus T_\square$ e $K_t \oplus 4_\square$ (sob condições específicas).

Significância
O artigo afirma resolver uma lacuna significativa na literatura em relação às propriedades metalógicas da lógica de tempo básica. Ao estender o argumento semântico de Visser para o cenário de duas vias, o autor confirma que $K_t$ desfruta da propriedade de interpolação uniforme, um resultado que era anteriormente desconhecido, apesar do uso generalizado desta lógica na filosofia, ciência da computação e semântica formal. O trabalho esclarece a fronteira entre as lógicas que possuem esta forte propriedade de interpolação (como $K_t$) e aquelas que não possuem (como $S4_t$), fornecendo um arcabouço semântico robusto (bisimulações em camadas) para analisar a interpolação em lógicas de tempo. Além disso, o artigo sugere que o interpolante uniforme em $K_t$ pode ser entendido semanticamente como uma versão temporal de um quantificador de bisimulação, oferecendo uma compreensão conceitual mais profunda do poder expressivo da lógica. Os resultados também lançam as bases para investigações futuras sobre a interpolação de Lyndon uniforme e a aplicação destas técnicas a lógicas de tempo multimodais e híbridas.