On Modal Logics of Full Products of Neighborhood Frames

Resumen Técnico: Sobre las lógicas modales de los productos totales de marcos de vecindad

Planteamiento del problema
El artículo aborda la caracterización de las lógicas modales asociadas a los "productos totales" de marcos de vecindad. Mientras que la lógica de productos para marcos de Kripke y espacios topológicos (específicamente para sistemas como $S4$ y $D4$) está bien comprendida, el comportamiento de los productos totales en el contexto de lógicas modales más débiles y no normales ha sido menos explorado.

En la semántica de Kripke estándar, el producto total de dos marcos introduce una tercera relación de accesibilidad (la relación sincrónica) junto con las relaciones horizontales y verticales. Esta estructura típicamente valida principios de interacción fuertes como la conmutación ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) y la convergencia. En contraste, la semántica de vecindad, que generaliza la semántica de Kripke e incluye la semántica topológica como un caso especial, permite la construcción de productos donde tales principios de interacción no necesariamente se cumplen.

El problema específico abordado es determinar la axiomatización precisa del producto de vecindad total para las lógicas $T$ (reflexiva) y $D$ (serial). Los autores investigan la lógica trimodal generada por la clase de productos totales de marcos de vecindad que validan $T$ o $D$, equipados con tres funciones de vecindad: horizontal ($\square_1$), vertical ($\square_2$) y de producto ($\square$).

Metodología
Los autores emplean una combinación de análisis semántico y demostraciones de completitud mediante morfismos acotados.

1. Definiciones y cotas inferiores:
   El artículo define el producto de vecindad total $X \times^+_n Y$ de dos marcos de vecindad $X$ e $Y$. Esta estructura incluye funciones de vecindad horizontales y verticales (derivadas de los marcos componentes) y una función de vecindad de producto (generada por productos de vecindades de los componentes).
   Los autores establecen cotas inferiores para las lógicas $T \times^+_n T$ y $D \times^+_n D$ identificando axiomas válidos. Introducen el axioma de interacción $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$. Demuestran que las lógicas $T_3^m = T \otimes T \otimes T + (mix)$ y $D_3^m = D \otimes D \otimes D + (mix)$ están contenidas dentro de las lógicas de los respectivos productos totales.

2. Completitud mediante árboles infinitos:
   Para probar las cotas superiores (es decir, que las lógicas de producto están contenidas en $T_3^m$ y $D_3^m$), los autores construyen marcos de Kripke infinitos específicos:

   • $T^{r,m}_{\omega,\omega,\omega}$: Un árbol reflexivo de ramificación infinita con relaciones $R, R_1, R_2$ que satisfacen $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$.
   • $T^{i,m}_{\omega,\omega,\omega}$: Un contraparte irreflexiva.
     Prueban que $T_3^m$ es sólido y completo con respecto a $T^{r,m}_{\omega,\omega,\omega}$ y $D_3^m$ con respecto a $T^{i,m}_{\omega,\omega,\omega}$. Esto se basa en la Propiedad del Modelo Finito (FMP) de estas lógicas, establecida mediante técnicas de filtración que preservan la condición de interacción $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$.

3. Construcción de marcos de vecindad y morfismos acotados:
   Un obstáculo técnico crítico es que los marcos de vecindad requeridos para falsar axiomas de interacción como la conmutación no pueden derivarse directamente de marcos de Kripke (ya que los marcos de vecindad inducidos por Kripke preservan la conmutación). Para superar esto, los autores construyen marcos de vecindad específicos $N^r_\omega$ y $N^i_\omega$ basados en "secuencias pseudo-infinitas" (secuencias de números naturales que eventualmente se convierten en un símbolo especial $\star$). Estos marcos poseen vecindades que forman cadenas estrictamente decrecientes infinitas, asegurando que ningún estado tenga una vecindad mínima, lo cual es necesario para romper las propiedades tipo Kripke.
   Finalmente, los autores definen un morfismo acotado suprayectivo desde el producto total de estos marcos de vecindad ($N^r_\omega \times^+_n N^r_\omega$) hacia el marco de vecindad inducido por el árbol $T^{r,m}_{\omega,\omega,\omega}$. Este morfismo prueba que cualquier fórmula válida en el árbol es válida en el producto, estableciendo la cota superior.

Contribuciones principales y resultados
La principal contribución del artículo es la axiomatización exacta de los productos de vecindad totales para las lógicas $T$ y $D$:

• Teorema 1.4:

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

  Aquí, $\otimes$ denota la fusión de lógicas, y $(mix)$ es el axioma de interacción $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Distinción de la semántica topológica:
  El artículo destaca una divergencia crucial entre la semántica topológica y la semántica de vecindad general. En la semántica topológica (que corresponde a marcos reflexivos), el axioma $(sub) = \square p \to \square_1 p \land \square_2 p$ es válido en productos totales. Los autores muestran que sobre $S4 \otimes S4 \otimes S4$, $(sub)$y$(mix)$ son equivalentes. Sin embargo, para la lógica serial más débil $D$, $(sub)$ no es válida en productos totales de vecindad. El artículo proporciona un contraejemplo (adaptando un ejemplo de marco de Kripke a la semántica de vecindad) mostrando que $(sub) \notin D \times^+_n D$, mientras que $(mix)$ permanece válida.

• Decidibilidad:
  Al establecer la Propiedad del Modelo Finito para las lógicas resultantes $T_3^m$ y $D_3^m$, los autores concluyen que estas lógicas son decidibles.

Significado
El artículo extiende los resultados de productos conocidos para $S4$ y $D4$ a sistemas más débiles ($T$ y $D$) dentro del marco de la semántica de vecindad. Clarifica las diferencias estructurales entre productos totales en entornos topológicos frente a entornos de vecindad generales, demostrando específicamente que la reflexividad de los marcos subyacentes es una condición necesaria para la validez del axioma $(sub)$ en productos totales. El trabajo proporciona una caracterización completa de las lógicas trimodales que surgen de estos productos, llenando un vacío en la literatura respecto a la interacción de las modalidades en estructuras de vecindad basadas en productos y no normales. Los autores señalan que extender estos resultados a lógicas no seriales como $K$ o $K4$ sigue siendo una dirección abierta, ya que las técnicas utilizadas (que dependen de la serialidad) no se aplican directamente.