On Modal Logics of Full Products of Neighborhood Frames

Résumé technique : Sur les logiques modales des produits complets de cadres de voisinage

Énoncé du problème
L'article traite de la caractérisation des logiques modales associées aux « produits complets » de cadres de voisinage. Si la logique des produits pour les cadres de Kripke et les espaces topologiques (spécifiquement pour des systèmes comme $S4$ et $D4$) est bien comprise, le comportement des produits complets dans le contexte des logiques modales plus faibles et non normales est moins exploré.

Dans la sémantique de Kripke standard, le produit complet de deux cadres introduit une troisième relation d'accessibilité (la relation synchrone) aux côtés des relations horizontale et verticale. Cette structure valide typiquement des principes d'interaction forts tels que la commutation ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) et la convergence. En revanche, la sémantique de voisinage, qui généralise la sémantique de Kripke et inclut la sémantique topologique comme un cas particulier, permet la construction de produits où ces principes d'interaction ne se tiennent pas nécessairement.

Le problème spécifique abordé est la détermination de l'axiomatisation précise du produit de voisinage complet pour les logiques $T$ (réflexive) et $D$ (sérielle). Les auteurs étudient la logique tri-modale générée par la classe des produits complets de cadres de voisinage validant $T$ ou $D$, équipés de trois fonctions de voisinage : horizontale ($\square_1$), verticale ($\square_2$) et de produit ($\square$).

Méthodologie
Les auteurs emploient une combinaison d'analyse sémantique et de preuves de complétude via des morphismes bornés.

1. Définitions et bornes inférieures :
   L'article définit le produit de voisinage complet $X \times^+_n Y$ de deux cadres de voisinage $X$ et $Y$. Cette structure inclut des fonctions de voisinage horizontale et verticale (dérivées des cadres composants) ainsi qu'une fonction de voisinage de produit (générée par les produits des voisinages des composants).
   Les auteurs établissent les bornes inférieures pour les logiques $T \times^+_n T$ et $D \times^+_n D$ en identifiant des axiomes valides. Ils introduisent l'axiome d'interaction $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$. Ils démontrent que les logiques $T_3^m = T \otimes T \otimes T + (mix)$ et $D_3^m = D \otimes D \otimes D + (mix)$ sont contenues dans les logiques des produits complets respectifs.

2. Complétude via des arbres infinis :
   Pour prouver les bornes supérieures (c'est-à-dire que les logiques de produit sont contenues dans $T_3^m$ et $D_3^m$), les auteurs construisent des cadres de Kripke infinis spécifiques :

   • $T^{r,m}_{\omega,\omega,\omega}$ : Un arbre réflexif à branchement infini avec des relations $R, R_1, R_2$ satisfaisant $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$.
   • $T^{i,m}_{\omega,\omega,\omega}$ : Un contrepartie irréflexive.
     Ils prouvent que $T_3^m$ est sain et complet par rapport à $T^{r,m}_{\omega,\omega,\omega}$ et $D_3^m$ par rapport à $T^{i,m}_{\omega,\omega,\omega}$. Cela repose sur la propriété du modèle fini (FMP) de ces logiques, établie via des techniques de filtration qui préservent la condition d'interaction $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$.

3. Construction de cadres de voisinage et morphismes bornés :
   Un obstacle technique critique est que les cadres de voisinage requis pour falsifier les axiomes d'interaction comme la commutation ne peuvent pas être dérivés directement des cadres de Kripke (car les cadres de voisinage induits par Kripke préservent la commutation). Pour surmonter cela, les auteurs construisent des cadres de voisinage spécifiques $N^r_\omega$ et $N^i_\omega$ basés sur des « pseudo-séquences infinies » (des séquences de nombres naturels devenant finalement un symbole spécial $\star$). Ces cadres possèdent des voisinages qui forment des chaînes décroissantes strictes infinies, garantissant qu'aucun état n'a de plus petit voisinage, ce qui est nécessaire pour briser les propriétés de type Kripke.
   Enfin, les auteurs définissent un morphisme borné surjectif du produit complet de ces cadres de voisinage ($N^r_\omega \times^+_n N^r_\omega$) vers le cadre de voisinage induit par l'arbre $T^{r,m}_{\omega,\omega,\omega}$. Ce morphisme prouve que toute formule valide sur l'arbre est valide sur le produit, établissant ainsi la borne supérieure.

Contributions principales et résultats
La contribution principale de l'article est l'axiomatisation exacte des produits de voisinage complets pour les logiques $T$ et $D$ :

• Théorème 1.4 :

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

  Ici, $\otimes$ désigne la fusion de logiques, et $(mix)$ est l'axiome d'interaction $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Distinction par rapport à la sémantique topologique :
  L'article souligne une divergence cruciale entre la sémantique topologique et la sémantique de voisinage générale. Dans la sémantique topologique (qui correspond aux cadres réflexifs), l'axiome $(sub) = \square p \to \square_1 p \land \square_2 p$ est valide sur les produits complets. Les auteurs montrent que sur $S4 \otimes S4 \otimes S4$, $(sub)$ et $(mix)$ sont équivalents. Cependant, pour la logique sérielle plus faible $D$, $(sub)$ n'est pas valide sur les produits de voisinage complets. L'article fournit un contre-exemple (adaptant un exemple de cadre de Kripke à la sémantique de voisinage) montrant que $(sub) \notin D \times^+_n D$, alors que $(mix)$ reste valide.

• Décidabilité :
  En établissant la propriété du modèle fini pour les logiques résultantes $T_3^m$ et $D_3^m$, les auteurs concluent que ces logiques sont décidables.

Signification
L'article étend les résultats de produits connus pour $S4$ et $D4$ aux systèmes plus faibles ($T$ et $D$) dans le cadre de la sémantique de voisinage. Il clarifie les différences structurelles entre les produits complets dans les contextes topologiques versus les contextes de voisinage généraux, démontrant spécifiquement que la réflexivité des cadres sous-jacents est une condition nécessaire pour la validité de l'axiome $(sub)$ dans les produits complets. Le travail fournit une caractérisation complète des logiques tri-modales issues de ces produits, comblant une lacune dans la littérature concernant l'interaction des modalités dans les structures de voisinage basées sur des produits non normales. Les auteurs notent que l'extension de ces résultats à des logiques non sérielles comme $K$ ou $K4$ reste une direction ouverte, car les techniques utilisées (reposant sur la sérialité) ne s'appliquent pas directement.