Four intuitionistic modal connectives

Technische Samenvatting: Vier Intuïtionistische Modale Connectieven

Probleemstelling
Het artikel behandelt de fundamentele semantiek en axiomatisering van Intuïtionistische Modale Logica's (IML's). Traditioneel interpreteren IML's modale connectieven binnen relationele structuren $(W, \leq, R, V)$, waarbij $\leq$ een preordening is en $R$ een binaire relatie. Er bestaat een centrale spanning tussen twee belangrijke stromingen met betrekking tot de mogelijkheidsoperator:

1. De benadering van Fischer Servi: Definieert mogelijkheid ($\diamond_{FS}$) zodanig dat $s \models \diamond_{FS} A$ indien er een $t$ bestaat waarvoor $sRt$ en $t \models A$. Deze benadering vereist doorgaans het beperken van de klasse van modellen tot "voorwaarts en achterwaarts confluente" frames om aan de Erfelijkheidseigenschap (monotoniciteit met betrekking tot $\leq$) te voldoen.
2. De benadering van Wijesekera: Definieert mogelijkheid ($\diamond_{W}$) zodanig dat $s \models \diamond_{W} A$ indien voor alle $t \geq s$, er een $u$ bestaat waarvoor $tRu$ en $u \models A$. Deze benadering vereist niet strikt confluence voor het in stand houden van de Erfelijkheidseigenschap.

De auteurs stellen dat het beperken van de discussie tot confluente modellen (zoals Fischer Servi doet) een willekeurige keuze is die één variant van de Intuïtionistische Eerste-Orde Logica boven andere bevoordeelt. Bovendien merken zij op dat de standaardvertaling van IML's naar eerste-orde logica vaak faalt om de beoogde semantiek te vatten als deze enkel wordt beperkt tot confluente modellen. Daarom streeft het artikel ernaar een verenigd kader te vestigen dat vier verschillende modale connectieven incorporeert zonder de klasse van frames vooraf te beperken, waardoor het volledige landschap van intuïtionistische modaliteiten wordt verkend.

Methodologie
De auteurs maken gebruik van een rigoureuze combinatie van relationele semantiek, correspondentietheorie, algebraïsche bewijssystemen en modeltheoretische technieken:

1. Syntaxis en Semantiek:

   • Ze introduceren een taal die de standaard intuïtionistische connectieven ($\to, \top, \bot, \lor, \land$) en een duale implicatie/co-implicatie ($\leftarrow$) bevat.
   • Vier modale operatoren zijn gedefinieerd:
     • $\Diamond$ (Přenosil-stijl mogelijkheid): $s \models \Diamond A$ indien $\exists t \leq s, \exists u (tRu \land u \models A)$.
     • $\Box$ (Fischer Servi-stijl noodzakelijkheid): $s \models \Box A$ indien $\forall t \geq s, \forall u (tRu \to u \models A)$.
     • $\Diamond$ (Wijesekera-stijl mogelijkheid): $s \models \Diamond A$ indien $\forall t \geq s, \exists u (tRu \land u \models A)$.
     • $\blacksquare$ (Duale noodzakelijkheid): $s \models \blacksquare A$ indien $\exists t \leq s, \forall u (tRu \to u \models A)$.
   • De semantiek is gedefinieerd over de klasse van alle frames (zonder restricties op confluence) en de Erfelijkheidseigenschap wordt bewezen stand te houden voor alle formules onder deze definities.

2. Correspondentietheorie:

   • Het artikel onderzoekt de modale definieerbaarheid van elementaire frameklassen (bijv. serieel, reflexief, symmetrisch, transitief, confluent).
   • Het maakt gebruik van gesigneerde formules en inferentieregels om frame-eigenschappen te karakteriseren.
   • Het hanteert de "Relativatie-eigenschap" uit de modeltheorie om de onbeslisbaarheid van het modale definieerbaarheidsprobleem voor bepaalde klassen van frames te bewijzen.

3. Axiomatisering en Volledigheid:

   • Een Hilbert-stijl systeem wordt gepresenteerd met behulp van verzamelingen gesigneerde formules (positief en negatief), gesloten onder uniforme substitutie en specifieke inferentieregels (inclusief regels voor duale implicatie en de interactie tussen modaliteiten).
   • De auteurs construeren een Canonieke Model met behulp van "gebalanceerde clips" (triples bestaande uit een priem filter, een priem ideaal en hulp-formules). Deze constructie is noodzakelijk om de complexe interacties tussen de vier modaliteiten en de duale implicatie te behanden.
   • Volledigheidstellingen worden bewezen voor de minimale logica en haar uitbreidingen die corresponderen met specifieke frameklassen (reflexief, serieel, voorwaarts/neerwaarts confluent).

4. Beslisbaarheid:

   • Om beslisbaarheid te bewijzen, bedden de auteurs de minimale IML in het Monadische Twee-Variabele Bewaakte Fragment van de Klassieke Eerste-Orde Logica.
   • Ze definiëren vertaalfuncties die intuïtionistische formules mappen naar bewaakte eerste-orde formules, waarbij gebruik wordt gemaakt van de bekende beslisbaarheid van het bewaakte fragment.

Belangrijkste Bijdragen en Resultaten

• Verenigd Kader: Het artikel integreert succesvol vier verschillende modale connectieven ($\Diamond, \Box, \Diamond, \blacksquare$) in één enkel intuïtionistisch kader, en toont aan dat deze niet interdefinieerbaar zijn over de klasse van alle frames.
• Eliminatieanalyse: Er wordt aangetoond dat over de klasse van voorwaarts en neerwaarts confluente frames ($C_{fd}$), alle vier de connectieven elimineerbaar zijn (interdefinieerbaar). Echter, over bredere klassen (zoals $C_{bdu}$), zijn ze verschillend.
• Correspondentieresultaten:
  • De klassen van voorwaarts confluente ($C_f$) en neerwaarts confluente ($C_d$) frames zijn positief definieerbaar.
  • De klassen van reflexieve ($C_{ref}$), symmetrische ($C_{sym}$), transitieve ($C_{tra}$), Euclidische ($C_{Euc}$) en deterministische ($C_{det}$) frames zijn niet modaal definieerbaar met betrekking tot de klasse van alle frames (of specifieke subklassen zoals $C_{fbdu}$).
  • De klassen van achterwaarts confluente ($C_b$) en opwaarts confluente ($C_u$) frames zijn niet modaal definieerbaar met betrekking tot $C_{fd}$.
• Axiomatisering: Het artikel biedt volledige axiomatiseringen voor de minimale logica ($L_{min}$) en haar uitbreidingen die corresponderen met reflexiviteit, serialiteit en confluence-eigenschappen. De minimale logica wordt getoond de logica van alle frames te zijn.
• Beslisbaarheid: Het lidmaatschapsprobleem voor de minimale intuïtionistische modale logica ($L_{min}$) en verschillende van haar uitbreidingen (reflexief, serieel, confluent) wordt bewezen beslisbaar te zijn. Dit wordt bereikt door het probleem te reduceren tot de bevraagbaarheid van het Monadische Twee-Variabele Bewaakte Fragment.
• Onbeslisbaarheid van Definieerbaarheid: Het artikel bewijst dat de beslissingsproblemen voor het bepalen of een elementaire klasse van frames modaal, positief of negatief definieerbaar is, onbeslisbaar zijn.

Betekenis en Claims
De auteurs beweren dat hun werk een meer natuurlijke en minder restrictieve fundering voor IML's biedt door de willekeurige beperking tot confluente modellen te vermijden. Door de duale implicatie en de vier modale connectieven te introduceren, bieden ze een symmetrische en uitgebreide taal die het volledige bereik van verschillende intuïtionistische modale gedragingen vangt.

Het artikel merkt bescheiden op dat hoewel de beslisbaarheid van de minimale logica is vastgesteld, de complexiteitsklasse van dit probleem een open vraag blijft. Daarnaast benadrukken de auteurs dat hoewel bepaalde inferentieregels (specifiek $R8+$ en $R8-$) werden gebruikt in de volledigheidsbewijzen, het momenteel onbekend is of deze regels vervangen kunnen worden door een eindige verzameling axioma's. Ze stellen ook open vragen over de eindige axiomatiseerbaarheid van logica's die corresponderen met symmetrische en transitieve frames, evenals de potentie om filtratietechnieken aan te passen aan deze specifieke setting.

Dit werk dient als een fundamentele stap in het begrijpen van de wisselwerking tussen verschillende intuïtionistische modale semantieken en hun corresponderende frame-eigenschappen, waarbij men verder gaat dan de traditionele Fischer Servi en Wijesekera dichotomieën.