Four intuitionistic modal connectives

Resumo Técnico: Quatro Conectivos Modais Intuicionistas

Enunciado do Problema
O artigo aborda a semântica fundamental e a axiomatização das Lógicas Modais Intuicionistas (LMI). Tradicionalmente, as LMIs interpretam os conectivos modais dentro de estruturas relacionais $(W, \leq, R, V)$, onde $\leq$ é uma pré-ordem e $R$ é uma relação binária. Existe uma tensão central entre duas grandes escolas de pensamento em relação ao operador de possibilidade:

1. A abordagem de Fischer Servi: Define a possibilidade ($\diamond_{FS}$) tal que $s \models \diamond_{FS} A$ se, e somente se, existe um $t$ tal que $sRt$e$t \models A$. Esta abordagem tipicamente exige a restrição da classe de modelos aos quadros (frames) "confluentes para frente e para trás" para satisfazer a Propriedade da Hereditariedade (monotonicidade em relação a $\leq$).
2. A abordagem de Wijesekera: Define a possibilidade ($\diamond_{W}$) tal que $s \models \diamond_{W} A$ se, e somente se, para todo $t \geq s$, existe um $u$ tal que $tRu$e$u \models A$. Esta abordagem não exige estritamente a confluência para que a Propriedade da Hereditariedade seja mantida.

Os autores argumentam que limitar a discussão a modelos confluentes (como faz Fischer Servi) é uma escolha arbitrária que privilegia uma variante do Cálculo de Primeira Ordem Intuicionista sobre outras. Além disso, observam que a tradução padrão das LMIs para a lógica de primeira ordem frequentemente falha em capturar a semântica pretendida se restringida apenas a modelos confluentes. Consequentemente, o artigo busca estabelecer um arcabouço unificado que incorpore quatro conectivos modais distintos sem restringir a classe de quadros a priori, explorando assim todo o panorama das modalidades intuicionistas.

Metodologia
Os autores empregam uma combinação rigorosa de semântica relacional, teoria da correspondência, sistemas algébricos de prova e técnicas de modelagem:

1. Sintaxe e Semântica:

   • Eles introduzem uma linguagem contendo os conectivos intuicionistas padrão ($\to, \top, \bot, \lor, \land$) e uma dupla implicação/co-implicação ($\leftarrow$).
   • Quatro operadores modais são definidos:
     • $\Diamond$ (Possibilidade estilo Přenosil): $s \models \Diamond A$ se, e somente se, $\exists t \leq s, \exists u (tRu \land u \models A)$.
     • $\Box$ (Necessidade estilo Fischer Servi): $s \models \Box A$ se, e somente se, $\forall t \geq s, \forall u (tRu \to u \models A)$.
     • $\Diamond$ (Possibilidade estilo Wijesekera): $s \models \Diamond A$ se, e somente se, $\forall t \geq s, \exists u (tRu \land u \models A)$.
     • $\blacksquare$ (Necessidade dual): $s \models \blacksquare A$ se, e somente se, $\exists t \leq s, \forall u (tRu \to u \models A)$.
   • As semáticas são definidas sobre a classe de todos os quadros (sem restrições de confluência), e a Propriedade da Hereditariedade é provada como válida para todas as fórmulas sob estas definições.

2. Teoria da Correspondência:

   • O artigo investiga a definibilidade modal de classes elementares de quadros (ex: serial, reflexiva, simétrica, transitiva, confluente).
   • Utiliza fórmulas assinadas e regras de inferência para caracterizar propriedades de quadros.
   • Emprega a "Propriedade de Relativização" da teoria dos modelos para provar a indecidibilidade do problema de definibilidade modal para certas classes de quadros.

3. Axiomatização e Completude:

   • Um sistema de estilo Hilbert é apresentado utilizando conjuntos de fórmulas assinadas (positivas e negativas), fechados sob substituição uniforme e regras de inferência específicas (incluindo regras para dupla implicação e a interação entre modalidades).
   • Os autores constroem um Modelo Canônico utilizando "clips balanceados" (trios consistindo de um filtro primo, um ideal primo e fórmulas auxiliares). Esta construção é necessária para lidar com as complexas interações entre os quatro conectivos modais e a dupla implicação.
   • Teoremas de completude são provados para a lógica mínima e suas extensões correspondentes a classes específicas de quadros (reflexiva, serial, confluência para frente/baixo).

4. Decidibilidade:

   • Para provar a decidibilidade, os autores inserem a LMI mínima no Fragment Guardado Monádico de Duas Variáveis da Lógica de Primeira Ordem Clássica.
   • Eles definem funções de tradução que mapeiam fórmulas intuicionistas para fórmulas guardadas de primeira ordem, aproveitando a decidibilidade conhecida do fragmento guardado.

Principais Contribuições e Resultados

• Arcabouço Unificado: O artigo integra com sucesso quatro conectivos modais distintos ($\Diamond, \Box, \Diamond, \blacksquare$) em um único arcabouço intuicionista, demonstrando que eles não são interdefiníveis sobre a classe de todos os quadros.
• Análise de Eliminabilidade: Demonstra-se que, sobre a classe de quadros confluentes para frente e para baixo ($C_{fd}$), todos os quatro conectivos são elimináveis (interdefiníveis). No entanto, sobre classes mais amplas (como $C_{bdu}$), eles são distintos.
• Resultos de Correspondência:
  • As classes de quadros confluentes para frente ($C_f$) e para baixo ($C_d$) são positivamente definíveis.
  • As classes de quadros reflexivos ($C_{ref}$), simétricos ($C_{sym}$), transitivos ($C_{tra}$), euclidianos ($C_{Euc}$) e determinísticos ($C_{det}$) não são modalmente definíveis em relação à classe de todos os quadros (ou subclasses específicas como $C_{fbdu}$).
  • As classes de quadros confluentes para trás ($C_b$) e para cima ($C_u$) não são modalmente definíveis em relação a $C_{fd}$.
• Axiomatização: O artigo fornece axiomatizações completas para a lógica mínima ($L_{min}$) e suas extensões correspondentes às propriedades de reflexividade, serialidade e confluência. A lógica mínima é mostrada como sendo a lógica de todos os quadros.
• Decidibilidade: O problema de pertinência para a lógica modal intuicionista mínima ($L_{min}$) e diversas de suas extensões (reflexiva, serial, confluente) é provado como decidível. Isto é alcançado reduzindo o problema à satisfatibilidade do Fragmento Guardado Monádico de Duas Variáveis.
• Indecidibilidade da Definibilidade: O artigo prova que os problemas de decisão para determinar se uma classe elementar de quadros é modal, positiva ou negativamente definível são indecidíveis.

Significância e Alegações
Os autores alegam que seu trabalho fornece uma fundação mais natural e menos restritiva para as LMIs ao evitar a limitação arbitrária aos modelos confluentes. Ao introduzir a dupla implicação e os quatro conectivos modais, eles oferecem uma linguagem simétrica e abrangente que captura toda a gama de comportamentos modais intuicionistas.

O artigo nota modestamente que, embora a decidibilidade da lógica mínima tenha sido estabelecida, a classe de complexidade deste problema permanece uma questão aberta. Adicionalmente, os autores destacam que, embora certas regras de inferência (especificamente $R8+$ e $R8-$) tenham sido usadas nas provas de completude, ainda não se sabe se essas regras podem ser substituídas por um conjunto finito de axiomas. Eles também colocam questões abertas sobre a axiomatização finita de lógicas correspondentes a quadros simétricos e transitivos, bem como o potencial de adaptar técnicas de filtração para este cenário específico.

Este trabalho serve como um passo fundamental para compreender a interação entre diferentes semânticas modais intuicionistas e suas propriedades de quadros correspondentes, indo além da tradicional dicotomia de Fischer Servi e Wijesekera.