Uniform Lyndon Interpolation via Non-wellfounded Proofs

Resumo Técnico: Interpolação de Lyndon Uniforme via Provas Não-bem-fundadas

Enunciado do Problema
A teoria de provas não-bem-fundada tem sido empregada com sucesso para estabelecer interpolação de Craig, interpolação de Lyndon e interpolação uniforme para várias lógicas, incluindo lógicas de provabilidade. No entanto, a combinação dessas propriedades — especificamente a Propriedade de Interpolação de Lyndon Uniforme (ULIP) — não havia sido abordada utilizando métodos não-bem-fundados antes deste trabalho. O artigo foca na lógica de provabilidade GLS (também conhecida como S), que corresponde ao predicado de provabilidade da Aritmética de Peano sob aritmética verdadeira. Embora fosse conhecido que a GLS possuía interpolação uniforme e interpolação de Craig, permanecia uma questão em aberto se a GLS admite interpolação de Lyndon uniforme (ou mesmo interpolação de Lyndon não-uniforme). Um obstáculo primário em sistemas de prova bem-fundados para tais lógicas é a "fórmula diagonal" em regras modais, que falha em preservar a polaridade das variáveis, um requisito para a interpolação de Lyndon.

Metodologia
Os autores utilizam cálculos sequentes não-bem-fundados e teoria de prova de progresso local para superar as limitações das provas bem-fundadas. A metodologia baseia-se em três componentes técnicos principais:

1. Cálculos Sequentes de Progresso Local: Os autores empregam um cálculo, $G_{\infty}^{GLS}$, que é um sistema de progresso local. Diferente dos cálculos bem-fundados padrão, as provas neste sistema são árvores que podem conter ramos infinitos, desde que cada ramo infinito contenha infinitamente muitos "nós de progresso" (especificamente, aplicações da regra modal $\square K4_{sat}$). Este sistema evita a fórmula diagonal encontrada no cálculo bem-fundado $G_{GLS}$, preservando assim a polaridade das variáveis ao longo da busca de prova.
2. Templates de Interpolação: Para construir interpolantes, os autores definem "templates de interpolação", que são pré-provas cíclicas (provas com arestas de retorno) geradas por um conjunto específico de regras de saturação. Esses templates são construídos aplicando regras que decompõem fórmulas até que alcancem um estado saturado. Os templates são anotados com "pré-interpolantes", que são pseudo-fórmulas envolvendo variáveis ligadas correspondentes aos nós de repetição no cálculo cíclico.
3. Sistemas Equacionais de Lyndon: Para resolver os pré-interpolantes em fórmulas válidas, os autores introduzem os conceitos de pontos fixos de Lyndon e sistemas equacionais de Lyndon. Um sistema equacional consiste em equações que ligam variáveis desconhecidas a fórmulas, restritas por vocabulários positivos e negativos (conjuntos de variáveis que aparecem com polaridades específicas). Os autores provam que sistemas equacionais de Lyndon "simples" e "modais positivos" são solucionáveis em GLS. Essa solucionabilidade permite a substituição das variáveis ligadas nos pré-interpolantes por fórmulas reais que respeitam as polaridades exigidas.

Principais Contribuições
O artigo apresenta três contribuições distintas:

1. Eliminação de Corte Alternativa: Fornece uma nova prova de eliminação de corte para $G_{GLS}$ através da tradução de provas do cálculo bem-fundado para o cálculo não-bem-fundado $G_{\infty}^{GLS}$ e estabelecendo a admissibilidade local da regra de corte nesta última.
2. Novos Conceitos Teóricos: Introduz pontos fixos de Lyndon e sistemas equacionais de Lyndon. Esses conceitos são essenciais para demonstrar que os interpolantes uniformes construídos via provas não-bem-fundadas respeitam as restrições de polaridade exigidas pela interpolação de Lyndon.
3. Prova de ULIP para GLS: Apresenta a primeira prova de que a GLS possui a Propriedade de Interpolação de Lyndon Uniforme.

O resultado central é o Teorema 4.16, que afirma que a GLS possui a Propriedade de Interpolação de Lyndon Uniforme. A prova procede por:

• Construir um template de interpolação para um dado sequente.
• Associar um sistema equacional de Lyndon modal positivo ao nó de repetição do template.
• Resolver este sistema em GLS (garantido pelo Teorema 4.7) para obter uma sequência de solução.
• Substituir esta solução no pré-interpolante do nó raiz para gerar o interpolante de Lyndon uniforme $\iota_T$.
• Verificar via Lema 4.14 e 4.15 que $\iota_T$ satisfaz as condições de ULIP: contém apenas os vocabulários positivos e negativos especificados, e atua como um interpolante para qualquer fórmula $\psi$ com vocabulários compatíveis.

Adicionalmente, o artigo estabelece que a regra de corte é eliminável em $G_{GLS}$ via tradução para $G_{\infty}^{GLS}$, e que a regra de corte é localmente admissível em $G_{\infty}^{GLS}$.

Significância e Escopo
O artigo afirma fechar a lacuna na literatura sobre interpolação de Lyndon uniforme para lógicas de provabilidade usando métodos não-bem-fundados. Os autores observam que sua metodologia é adaptável a outras lógicas de provabilidade, desde que um cálculo sequente não-bem-fundado esteja disponível para elas. Eles identificam explicitamente direções futuras, incluindo a aplicação do método a lógicas de interpretabilidade unárias, lógicas de provabilidade bimodais e lógicas de provabilidade intuicionistas. Eles também sugerem investigar lógicas onde pontos fixos simples de Lyndon não existem (como a lógica de interpretabilidade IL) e se sistemas equacionais de Lyndon modais positivos ainda podem ser resolvidos nesses contextos. O trabalho não pretende resolver a ULIP para todas as lógicas modais, mas sim demonstrar a viabilidade da abordagem não-bem-fundada para a GLS e delinear um framework para extensão.