Most Properties are Undecidable for Transitive Tense Logics

Resumo Técnico: A maioria das propriedades é indecidível para lógicas de tempo transitivas

Enunciado do Problema
O artigo aborda a decidibilidade algorítmica de propriedades lógicas no reticulado de lógicas de tempo transitivas, denotado por $NExtK4t$. Embora a decidibilidade de propriedades (como completude de Kripke, a propriedade do modelo finito e a própria decidibilidade) seja bem estudada para lógicas unimodais e lógicas de tempo lineares, o status dessas propriedades na classe intermediária de lógicas de tempo transitivas permanece uma questão aberta crítica. Especificamente, os autores investigam se a interação natural entre as modalidades de futuro ($\Box$) e passado ($\blacksquare$) em quadros transitivos torna o problema de decisão para essas propriedades indecidível. Trabalhos anteriores de Chagrov e Shehtman estabeleceram a indecidibilidade da tabularidade e da consistência em $NExtK4t$, mas a decidibilidade da completude de Kripke, da propriedade do modelo finito (FMP) e da decidibilidade geral permanecia não resolvida.

Metodologia
Os autores adaptam uma técnica de redução originalmente desenvolvida por Chagrov para lógicas unimodais, estendendo-a para o cenário bimodal das lógicas de tempo. O método central envolve a construção de uma redução computável de um problema de alcançabilidade de máquinas de Minsky (um problema conhecido como indecidível, equivalente ao problema da parada para máquinas de Turing) para o problema de decisão de propriedades lógicas específicas.

1. Codificação de Máquina de Minsky: Os autores utilizam uma máquina de Minsky $M$ com dois registradores e uma configuração específica $c_0 = \langle s, n, m \rangle$ tal que o conjunto de configurações alcançáveis é indecidível.
2. Construção de Quadro Geral: Um quadro geral específico $\mathcal{F} = (W, R, A)$ é construído. O domínio $W$ codifica as configurações alcançáveis de $M$ juntamente com pontos auxiliares ($a_i, b_i, c_i$) representando os valores dos registradores e uma estrutura de "contador". A relação de acessibilidade $R$ é definida para simular as transições da máquina de Minsky e as operações de incremento/decremento nos registradores.
3. Construção de Fórmulas: Os autores definem um conjunto de fórmulas sem variáveis ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$) que identificam unicamente pontos específicos no quadro $\mathcal{F}$. Eles definem adicionalmente as fórmulas $\psi_A, \psi_B$ e seus sucessores para simular as operações $+1$ e $-1$ nos registradores.
4. Construção de Lógica: Para qualquer configuração $c = \langle t, k, l \rangle$, uma lógica $L(c)$ é definida como uma extensão de $K4t$. Esta lógica inclui:
   • Axiomas ($Ax_M$) codificando as regras de transição de uma máquina de Minsky.
   • Um axioma condicional ligando a configuração inicial à configuração alvo.
   • Uma fórmula específica $\alpha$ (derivada de uma lógica tabular) e uma fórmula "armadilha" $\phi_0$ projetadas para garantir que, se a configuração alvo não for alcançável, a lógica resultante seja incompleta em relação a Kripke e indecidível.

Contribuições e Resultados Principais
O artigo estabelece um critério geral (Teorema 3.5) para a indecidibilidade de propriedades em $NExtK4t$. O teorema afirma que, se uma propriedade $P$ está contida na união da completude de Kripke ($KC$) e da decidibilidade ($DEC$), e existe uma fórmula $\alpha$ tal que $K4t \oplus \alpha \in P$, mas o quadro $\mathcal{F}$ construído não valida $\alpha$, então $P$ é indecidível.

Aplicando este teorema, os autores provam os seguintes resultados (Corolário 3.13):

• Os seguintes conjuntos de fórmulas são indecidíveis em $NExtK4t$:
  1. Completude de Kripke.
  2. Canonicidade.
  3. Definibilidade de primeira ordem.
  4. A propriedade do modelo finito (FMP).
  5. Tabularidade local.
  6. Tabularidade.
  7. Decidibilidade (da própria lógica).
  8. Coincidência com uma lógica tabular fixa.
  9. Consistência (especificamente, o complemento, inconsistência, é indecidível).

Além disso, via Proposição 2.2, os autores observam que, como $K4t$ é uma extensão de $Kt$ (a lógica de tempo mínima), estes resultados de indecidibilidade estendem-se ao reticulado $NExtKt$.

Significância e Alegações
O artigo afirma resolver o status de decidibilidade de importantes propriedades para lógicas de tempo transitivas, demonstrando que "a maioria das propriedades é indecidível" nesta classe. A significância reside em esclarecer como a interação de modalidades afeta a decidibilidade:

• Contraste com o Tempo Linear: Enquanto as propriedades são decidíveis no reticulado de fluxos de tempo lineares ($NExtLint$), a introdução da transitividade sem linearidade ($NExtK4t$) leva à indecidibilidade.
• Contraste com Lógicas Unimodais: Os resultados destacam que o mapa de extensão de tempo mínimo não preserva propriedades como completude de Kripke ou FMP, tornando o caso bimodal fundamentalmente diferente e mais complexo que o caso unimodal ($NExtK4$).
• Esquema Geral: O artigo fornece um esquema de prova geral para estabelecer a indecidibilidade em lógicas de tempo, reduzindo a alcançabilidade de máquinas de Minsky às propriedades lógicas, preenchendo uma lacuna deixada por trabalhos anteriores que não podiam transferir diretamente os resultados de indecidibilidade unimodal para o cenário de tempo devido à não-injetividade do mapa de extensão de tempo.

Os autores concluem que as interações de modalidades em lógicas de tempo transitivas tornam o problema de decisão para propriedades estritamente mais difícil do que em lógicas de tempo lineares e sugerem que, para propriedades como a completude de Kripke, a indecidibilidade em um reticulado unimodal provavelmente implica a indecidibilidade em sua extensão de tempo mínima, embora isso permaneça uma conjectura para trabalhos futuros.