On Modal Logics of Full Products of Neighborhood Frames

Technische Samenvatting: Over Modale Logica's van Volledige Producten van Neighborhood-frames

Probleemstelling
Het artikel behandelt de karakterisering van de modale logica's die geassocieerd zijn met "volledige producten" van neighborhood-frames. Terwijl de logica van producten voor Kripke-frames en topologische ruimtes (specifiek voor systemen zoals $S4$ en $D4$) goed begrepen is, is het gedrag van volledige producten in de context van zwakkere, niet-normale modale logica's minder onderzocht.

In de standaard Kripke-semantiek introduceert het volledige product van twee frames een derde toegankelijkheidsrelatie (de synchrone relatie) naast de horizontale en verticale relaties. Deze structuur valideert doorgaans sterke interactieprincipes zoals commutatie ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) en convergentie. In contrast hiermee staat de neighborhood-semantiek, die de Kripke-semantiek generaliseert en topologische semantiek als een speciaal geval omvat, wat toestaat dat constructies van producten waarbij deze interactieprincipes niet noodzakelijkerwijs gelden, worden gemaakt.

De specifieke probleemstelling die wordt aangepakt, is het bepalen van de precieze axiomatisering van de volledige neighborhood-producten voor de logica's $T$ (reflexief) en $D$ (serieel). De auteurs onderzoeken de tri-modale logica gegenereerd door de klasse van volledige producten van neighborhood-frames die $T$ of $D$ valideren, uitgerust met drie neighborhood-functies: horizontaal ($\square_1$), verticaal ($\square_2$) en een product ($\square$).

Methodologie
De auteurs maken gebruik van een combinatie van semantische analyse en volledigheidsproeven via gebonden morfismen.

1. Definities en Ondergrenzen:
   Het artikel definieert het volledige neighborhood-product $X \times^+_n Y$ van twee neighborhood-frames $X$ en $Y$. Deze structuur bevat horizontale en verticale neighborhood-functies (afgeleid van de component-frames) en een product-neighborhood-functie (gegenereerd door producten van neighborhoods uit de componenten).
   De auteurs stellen de ondergrenzen voor de logica's $T \times^+_n T$ en $D \times^+_n D$ vast door geldende axioma's te identificeren. Ze introduceren het interactie-axioma $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$. Ze demonstreren dat de logica's $T_3^m = T \otimes T \otimes T + (mix)$ en $D_3^m = D \otimes D \otimes D + (mix)$ bevatten in de logica's van de respectieve volledige producten.

2. Volledigheid via Oneindige Bomen:
   Om de bovengrenzen te bewijzen (dat wil zeggen, dat de product-logica's bevat zijn in $T_3^m$ en $D_3^m$), construeren de auteurs specifieke oneindige Kripke-frames:

   • $T^{r,m}_{\omega,\omega,\omega}$: Een reflexieve, oneindig vertakkende boom met relaties $R, R_1, R_2$ die voldoen aan $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$.
   • $T^{i,m}_{\omega,\omega,\omega}$: Een irreflexief tegenhanger.
     Ze bewijzen dat $T_3^m$ geldig en volledig is met betrekking tot $T^{r,m}_{\omega,\omega,\omega}$ en $D_3^m$ met betrekking tot $T^{i,m}_{\omega,\omega,\omega}$. Dit berust op de Eindige Model Eigenschap (FMP) van deze logica's, die wordt vastgesteld via filtratietechnieken die de interactieconditie $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$ behouden.

3. Constructie van Neighborhood-frames en Gebonden Morfismen:
   Een cruciale technische hindernis is dat de neighborhood-frames die nodig zijn om interactie-axioma's zoals commutatie te weerleggen, niet direct afgeleid kunnen worden van Kripke-frames (aangezien Kripke-geïnduceerde neighborhood-frames commutatie behouden). Om dit te overwinnen, construeren de auteurs specifieke neighborhood-frames $N^r_\omega$ en $N^i_\omega$ gebaseerd op "pseudo-oneindige sequenties" (sequenties van natuurlijke getallen die uiteindelijk een speciaal symbool $\star$ worden). Deze frames bezitten neighborhoods die oneindige strikt dalende ketens vormen, wat ervoor zorgt dat geen enkele toestand een kleinste neighborhood heeft, wat noodzakelijk is om Kripke-achtige eigenschappen te breken.
   Ten slotte definiëren de auteurs een surjectieve gebonden morfisme van het volledige product van deze neighborhood-frames ($N^r_\omega \times^+_n N^r_\omega$) naar het neighborhood-frame geïnduceerd door de boom $T^{r,m}_{\omega,\omega,\omega}$. Dit morfisme bewijst dat elke formule die geldig is op de boom, ook geldig is op het product, waarmee de bovengrens wordt vastgesteld.

Belangrijkste Bijdragen en Resultaten
De primaire bijdrage van het artikel is de exacte axiomatisering van de volledige neighborhood-producten voor de logica's $T$ en $D$:

• Theorema 1.4:

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

  Hierbij staat $\otimes$ voor de fusie van logica's, en $(mix)$ is het interactie-axioma $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Onderscheid van Topologische Semantiek:
  Het artikel benadrukt een cruciaal verschil tussen topologische semantiek en algemene neighborhood-semantiek. In topologische semantiek (die overeenkomt met reflexieve frames) is het axioma $(sub) = \square p \to \square_1 p \land \square_2 p$ geldig op volledige producten. De auteurs tonen aan dat over $S4 \otimes S4 \otimes S4$, $(sub)$ en $(mix)$ equivalent zijn. Echter, voor de zwakkere seriele logica $D$, is $(sub)$ niet geldig op volledige neighborhood-producten. Het artikel biedt een tegenvoorbeeld (door een Kripke-frame voorbeeld aan te passen aan de neighborhood-semantiek) waaruit blijkt dat $(sub) \notin D \times^+_n D$, terwijl $(mix)$ wel geldig blijft.

• Beslisbaarheid:
  Door de Eindige Model Eigenschap voor de resulterende logica's $T_3^m$ en $D_3^m$ vast te stellen, concluderen de auteurs dat deze logica's beslisbaar zijn.

Betekenis
Het artikel breidt bekende productresultaten voor $S4$ en $D4$ uit naar zwakkere systemen ($T$ en $D$) binnen het framework van de neighborhood-semantiek. Het verheldert de structurele verschillen tussen volledige producten in topologische settings versus algemene neighborhood-settings, waarbij specifiek wordt aangetoond dat de reflexiviteit van de onderliggende frames een noodzakelijke voorwaarde is voor de geldigheid van het $(sub)$ axioma in volledige producten. Het werk biedt een volledige karakterisering van de tri-modale logica's die voortvloeien uit deze producten, en vult een gat in de literatuur met betrekking tot de interactie van modaliteiten in niet-normale, op producten gebaseerde neighborhood-structuren. De auteurs merken op dat het uitbreiden van deze resultaten naar niet-seriele logica's zoals $K$ of $K4$ een openstaande richting is, aangezien de gebruikte technieken (die steunen op serialiteit) hier niet direct van toepassing zijn.