On Modal Logics of Full Products of Neighborhood Frames

Resumo Técnico: Sobre Lógicas Modais de Produtos Totais de Estruturas de Vizinhança

Enunciado do Problema
O artigo aborda a caracterização das lógicas modais associadas a "produtos totais" de estruturas de vizinhança. Enquanto a lógica de produtos para estruturas de Kripke e espaços topológicos (especificamente para sistemas como $S4$ e $D4$) é bem compreendida, o comportamento dos produtos totais no contexto de lógicas modais mais fracas e não normais permanece menos explorado.

Na semântica de Kripke padrão, o produto total de duas estruturas introduz uma terceira relação de acessibilidade (a relação sincrônica) ao lado das relações horizontal e vertical. Essa estrutura tipicamente valida princípios de interação fortes, como a comutação ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) e a convergência. Em contraste, a semântica de vizinhança, que generaliza a semântica de Kripke e inclui a semântica topológica como um caso especial, permite a construção de produtos onde esses princípios de interação não necessariamente se sustentam.

O problema específico tratado é a determinação da axiomatização precisa do produto de vizinhança total para as lógicas $T$ (reflexiva) e $D$ (serial). Os autores investigam a lógica trimodal gerada pela classe de produtos totais de estruturas de vizinhança que validam $T$ ou $D$, equipadas com três funções de vizinhança: horizontal ($\square_1$), vertical ($\square_2$) e de produto ($\square$).

Metodologia
Os autores empregam uma combinação de análise semântica e provas de completude via morfismos limitados.

1. Definições e Limites Inferiores:
   O artigo define o produto de vizinhança total $X \times^+_n Y$ de duas estruturas de vizinhança $X$ e $Y$. Esta estrutura inclui funções de vizinhança horizontal e vertical (derivadas das estruturas componentes) e uma função de vizinhança de produto (gerada por produtos de vizinhanças das componentes).
   Os autores estabelecem limites inferiores para as lógicas $T \times^+_n T$ e $D \times^+_n D$ identificando axiomas válidos. Eles introduzem o axioma de interação $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$. Eles demonstram que as lógicas $T_3^m = T \otimes T \otimes T + (mix)$ e $D_3^m = D \otimes D \otimes D + (mix)$ estão contidas nas lógicas dos respectivos produtos totais.

2. Completude via Árvores Infinitas:
   Para provar os limites superiores (isto é, que as lógicas de produto estão contidas em $T_3^m$ e $D_3^m$), os autores constroem estruturas de Kripke infinitas específicas:

   • $T^{r,m}_{\omega,\omega,\omega}$: Uma árvore reflexiva, de ramificação infinita, com relações $R, R_1, R_2$ satisfazendo $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$.
   • $T^{i,m}_{\omega,\omega,\omega}$: Uma contraparte irreflexiva.
     Eles provam que $T_3^m$ é sã e completa em relação a $T^{r,m}_{\omega,\omega,\omega}$ e $D_3^m$ em relação a $T^{i,m}_{\omega,\omega,\omega}$. Isso baseia-se na Propriedade do Modelo Finito (PMF) dessas lógicas, estabelecida via técnicas de filtração que preservam a condição de interação $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$.

3. Construção de Estrutura de Vizinhança e Morfismos Limitados:
   Um obstáculo técnico crítico é que as estruturas de vizinhança necessárias para falsificar axiomas de interação como a comutação não podem ser derivadas diretamente de estruturas de Kripke (pois estruturas de vizinhança induzidas por Kripke preservam a comutação). Para superar isso, os autores constroem estruturas de vizinhança específicas $N^r_\omega$ e $N^i_\omega$ baseadas em "sequências pseudo-infinitas" (sequências de números naturais que eventualmente tornam-se um símbolo especial $\star$). Essas estruturas possuem vizinhanças que formam cadeias estritamente decrescentes infinitas, garantindo que nenhum estado possua uma vizinhança mínima, o que é necessário para quebrar propriedades do tipo Kripke.
   Finalmente, os autores definem um morfismo limitado sobrejetor do produto total dessas estruturas de vizinhança ($N^r_\omega \times^+_n N^r_\omega$) para a estrutura de vizinhança induzida pela árvore $T^{r,m}_{\omega,\omega,\omega}$. Este morfismo prova que qualquer fórmula válida na árvore é válida no produto, estabelecendo o limite superior.

Principais Contribuições e Resultados
A principal contribuição do artigo é a axiomatização exata dos produtos de vizinhança totais para as lógicas $T$ e $D$:

• Teorema 1.4:

  • $T \times^+_n T = T \otimes T \otimes T + (mix)$
  • $D \times^+_n D = D \otimes D \otimes D + (mix)$

  Aqui, $\otimes$ denota a fusão de lógicas, e $(mix)$ é o axioma de interação $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Distinção da Semântica Topológica:
  O artigo destaca uma divergência crucial entre a semântica topológica e a semântica de vizinhança geral. Na semântica topológica (que corresponde a estruturas reflexivas), o axioma $(sub) = \square p \to \square_1 p \land \square_2 p$ é válido em produtos totais. Os autores mostram que sobre $S4 \otimes S4 \otimes S4$, $(sub)$e$(mix)$ são equivalentes. No entanto, para a lógica serial mais fraca $D$, $(sub)$ não é válido em produtos de vizinhança totais. O artigo fornece um contraexemplo (adaptando um exemplo de estrutura de Kripke para a semântica de vizinhança) mostrando que $(sub) \notin D \times^+_n D$, enquanto $(mix)$ permanece válido.

• Decidibilidade:
  Ao estabelecer a Propriedade do Modelo Finito para as lógicas resultantes $T_3^m$ e $D_3^m$, os autores concluem que essas lógicas são decidíveis.

Significância
O artigo estende os resultados de produtos conhecidos para $S4$ e $D4$ para sistemas mais fracos ($T$ e $D$) dentro do framework da semântica de vizinhança. Ele esclarece as diferenças estruturais entre produtos totais em contextos topológicos versus contextos gerais de vizinhança, demonstrando especificamente que a reflexividade das estruturas subjacentes é uma condição necessária para a validade do axioma $(sub)$ em produtos totais. O trabalho fornece uma caracterização completa das lógicas trimodais decorrentes desses produtos, preenchendo uma lacuna na literatura sobre a interação de modalidades em estruturas de vizinhança baseadas em produtos não normais. Os autores observam que estender esses resultados para lógicas não seriais como $K$ ou $K4$ permanece uma direção aberta, pois as técnicas utilizadas (que dependem da serialidade) não se aplicam diretamente.