A Existência de Interpolantes é Indecidível para Lógica de Primeira Ordem com Duas Variáveis com Duas Relações de Equivalência

O problema da existência de interpolantes (IEP) para uma lógica L é decidir, dadas as fórmulas P e Q, se existe uma fórmula I, construída a partir dos símbolos compartilhados de P e Q, tal que P implica I e I implica Q em L. Se L possui a propriedade de interpolação de Craig (CIP), então o IEP se reduz à validade em L. Recentemente, o IEP foi estudado para lógicas sem CIP. Os resultados obtidos até agora indicam que, embora o IEP possa ser computacionalmente mais difícil do que a validade, ele é decidível quando L é decidível. Aqui, apresentamos os primeiros exemplos de fragmentos decidíveis da lógica de primeira ordem para os quais o IEP é indecidível. Ou seja, mostramos que o IEP é indecidível para o fragmento de duas variáveis com duas relações de equivalência e para o fragmento de duas variáveis com guarda e constantes individuais e duas relações de equivalência. Também determinamos as lógicas de descrição booleanas correspondentes decidíveis, para as quais o IEP é indecidível.