On Modal Logics of Full Products of Neighborhood Frames

Sintesi Tecnica: Sulle logiche modali dei prodotti pieni di frame di vicinato

Enunciato del problema
Il saggio affronta la caratterizzazione delle logiche modali associate ai "prodotti pieni" di frame di vicinato. Mentre la logica dei prodotti per i frame di Kripke e gli spazi topologici (specificamente per sistemi come $S4$ e $D4$) è ben compresa, il comportamento dei prodotti pieni nel contesto di logiche modali più deboli e non normali rimane meno esplorato.

Nella semantica di Kripke standard, il prodotto pieno di due frame introduce una terza relazione di accessibilità (la relazione sincrona) insieme a quelle orizzontali e verticali. Questa struttura tipicamente valida forti principi di interazione come la commutazione ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) e la convergenza. Al contrario, la semantica di vicinato, che generalizza la semantica di Kripke e include la semantica topologica come un caso speciale, permette la costruzione di prodotti dove tali principi di interazione non necessariamente valgono.

Il problema specifico affrontato è la determinazione dell'esatta assiomatizzazione del prodotto di vicinato pieno per le logiche $T$ (riflessiva) e $D$ (seriale). Gli autori investigano la logica tri-modale generata dalla classe dei prodotti pieni di frame di vicinato che validano $T$ o $D$, dotati di tre funzioni di vicinato: orizzontale ($\square_1$), verticale ($\square_2$) e di prodotto ($\square$).

Metodologia
Gli autori impiegano una combinazione di analisi semantica e dimostrazioni di completezza tramite morfismi limitati.

1. Definizioni e limiti inferiori:
   Il saggio definisce il prodotto di vicinato pieno $X \times^+_n Y$ di due frame di vicinato $X$ e $Y$. Questa struttura include funzioni di vicinato orizzontali e verticali (derivate dai frame componenti) e una funzione di vicinato di prodotto (generata dai prodotti dei vicinati dei componenti).
   Gli autori stabiliscono i limiti inferiori per le logiche $T \times^+_n T$ e $D \times^+_n D$ identificando gli assiomi validi. Introducono l'assioma di interazione $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$. Dimostrano che le logiche $T_3^m = T \otimes T \otimes T + (mix)$ e $D_3^m = D \otimes D \otimes D + (mix)$ sono contenute nelle logiche dei rispettivi prodotti pieni.

2. Completezza tramite alberi infiniti:
   Per provare i limiti superiori (ovvero che le logiche di prodotto sono contenute in $T_3^m$ e $D_3^m$), gli autori costruiscono specifici frame di Kripke infiniti:

   • $T^{r,m}_{\omega,\omega,\omega}$: Un albero riflessivo con ramificazione infinita con relazioni $R, R_1, R_2$ che soddisfano $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$.
   • $T^{i,m}_{\omega,\omega,\omega}$: Un controparte irriflessiva.
     Provano che $T_3^m$ è sano e completo rispetto a $T^{r,m}_{\omega,\omega,\omega}$ e $D_3^m$ rispetto a $T^{i,m}_{\omega,\omega,\omega}$. Ciò si basa sulla Proprietà del Modello Finito (FMP) di queste logiche, stabilita tramite tecniche di filtrazione che preservano la condizione di interazione $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$.

3. Costruzione di frame di vicinato e morfismi limitati:
   Un ostacolo tecnico critico è che i frame di vicinato richiesti per falsificare assiomi di interazione come la commutazione non possono essere derivati direttamente da frame di Kripke (poiché i frame di vicinato indotti da Kripke preservano la commutazione). Per superare ciò, gli autori costruiscono specifici frame di vicinato $N^r_\omega$ e $N^i_\omega$ basati su "sequenze pseudo-infinite" (sequenze di numeri naturali che diventano eventualmente un simbolo speciale $\star$). Questi frame possiedono vicinati che formano catene decrescenti infinite rigorose, garantendo che nessun stato abbia un vicinato minimo, il che è necessario per rompere le proprietà simili a quelle di Kripke.
   Infine, gli autori definiscono un morfismo limitato suriettivo dal prodotto pieno di questi frame di vicinato ($N^r_\omega \times^+_n N^r_\omega$) al frame di vicinato indotto dall'albero $T^{r,m}_{\omega,\omega,\omega}$. Questo morfismo prova che qualsiasi formula valida sull'albero è valida sul prodotto, stabilendo il limite superiore.

Contributi chiave e risultati
Il contributo primario del saggio è l'esatta assiomatizzazione dei prodotti di vicinato pieni per le logiche $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)$

  Qui $\otimes$ denota la fusione delle logiche, e $(mix)$ è l'assioma di interazione $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Distinzione dalla semantica topologica:
  Il saggio evidenzia una divergenza cruciale tra la semantica topologica e la semantica di vicinato generale. Nella semantica topologica (che corrisponde a frame riflessivi), l'assioma $(sub) = \square p \to \square_1 p \land \square_2 p$ è valido sui prodotti pieni. Gli autori mostrano che su $S4 \otimes S4 \otimes S4$, $(sub)$e$(mix)$ sono equivalenti. Tuttavia, per la logica seriale più debole $D$, $(sub)$ non è valido sui prodotti pieni di vicinato. Il saggio fornisce un controesempio (adattando un esempio di frame di Kripke alla semantica di vicinato) mostrando che $(sub) \notin D \times^+_n D$, mentre $(mix)$ rimane valido.

• Decidibilità:
  Stabilendo la Proprietà del Modello Finito per le risultanti logiche $T_3^m$ e $D_3^m$, gli autori concludono che queste logiche sono decidibili.

Significato
Il saggio estende i noti risultati sui prodotti per $S4$ e $D4$ ai sistemi più deboli ($T$ e $D$) all'interno del framework della semantica di vicinato. Chiarisce le differenze strutturali tra i prodotti pieni negli ambienti topologici rispetto ai contesti di vicinato generali, dimostrando specificamente che la riflessività dei frame sottostanti è una condizione necessaria per la validità dell'assioma $(sub)$ nei prodotti pieni. Il lavoro fornisce una caratterizzazione completa delle logiche tri-modali che derivano da questi prodotti, colmando una lacuna nella letteratura riguardante l'interazione delle modalità in strutture di vicinato basate su prodotti non normali. Gli autori notano che estendere questi risultati a logiche non seriali come $K$ o $K4$ rimane una direzione aperta, poiché le tecniche utilizzate (basate sulla serialità) non si applicano direttamente.