A General Theory of Propositional Modal Bundled Modalities

Probleemstelling

De studie van "gebundelde modaliteiten" (bundled modalities) houdt zich bezig met het coderen van complexe conceptuele noties in de semantiek van een enkele modale operator, waarna de logica van deze operator wordt bestudeerd. Hoewel er reeds een aanzienlijke hoeveelheid werk bestaat over specifieke gevallen (zoals de niet-contingentie-operator $\Delta\phi := \Box\phi \lor \Box\neg\phi$, valse overtuiging, of "iemand weet"), ontbreekt er een algemeen theoretisch raamwerk.
Bestaande pogingen tot generalisatie zijn onvolledig:

1. Methodes om bisimulaties te definiëren (zoals in [1]) zijn beperkt tot een specifieke klasse van "uniforme connectieven".
2. Axiomatisatiemethodes (zoals in [12]) bieden geen uniforme manier om schema's te vinden voor willekeurige gebundelde modaliteiten.
   Dit leidt ertoe dat in studies van concrete gevallen bisimulaties vaak als open problemen worden gelaten en dat fundamenteel verschillende concepten van canonieke modellen worden geïntroduceerd, ondanks dat de logica's vaak veel gemeen hebben.

Methodologie

De auteurs ontwikkelen een uniforme theorie voor zowel de expressiviteit als de axiomatisering van gebundelde modaliteiten door de volgende stappen te doorlopen:

1. Semantiek als Neighbourhood Semantics:
   De auteurs interpreteren de semantiek van gebundelde modaliteiten als een speciale vorm van neighbourhood semantics (buursemantiek). Ze definiëren een "gebundelde term" ($\tau$) die de structuur van de bundel beschrijft. Voor een Kripke-model $M$ en een term $\tau$ genereren ze een verzameling van "buurparen" $(X, Y)$, waarbij $X$ de wereldjes aangeeft waar een formule waar moet zijn en $Y$ waar ze onwaar moet zijn, om de gebundelde operator waar te maken.

2. Uniforme Bisimulaties:
   Gebaseerd op deze gegenereerde buurstructuren definiëren ze een uniforme definitie van $\tau$-bisimulatie. Twee wereldjes zijn $\tau$-bisimilar als ze dezelfde waarheidswaarden hebben voor proposities en als hun respectievelijke buurparen (die de waarheid/falsheid van de formule ondersteunen) onderling coherent zijn via de relatie. Ze bewijzen een Hennessy-Milner-stelling: voor beeld-endelijke modellen (image-finite) karakteriseert $\tau$-bisimilariteit precies de expressiviteit van de taal (twee modellen zijn bisimilar dan en slechts dan als ze logisch equivalent zijn).

3. Convexe Bundles:
   Ze introduceren een speciale klasse van bundels genaamd convexe bundels. Een bundel is convex als de verzameling van geldige buurparen een zekere "tussenliggende" eigenschap bezit (als $(X_1, Y_1)$ en $(X_2, Y_2)$ geldig zijn en $X_1 \cap Y_2 = \emptyset$, dan is $(X_1, Y_2)$ ook geldig).

   • Ze tonen aan dat de meeste bestaande bundels in de literatuur (zoals onzekerheid, valse overtuiging, geheimkennis) convex zijn of het duaal daarvan.
   • Voor deze klasse definiëren ze een sterkere, efficiëntere vorm van bisimulatie (convexe $\tau$-bisimulatie) die kwantificeert over de gegenereerde buurparen in plaats van alle mogelijke deelverzamelingen.

4. Axiomatisering via Representatie:
   Voor de axiomatisering gebruiken ze een tweestapsstrategie:

   • Stap 1: Construeer een canoniek model voor een abstracte convexe buurlogica (met axioma's zoals CONV). Ze bewijzen sterkheid en volledigheid voor deze abstracte logica.
   • Stap 2: Gebruik representatietheorema's om te tonen dat deze abstracte convexe buurmodellen kunnen worden vertaald (gerepresenteerd) door concrete Kripke-modellen met specifieke eigenschappen (zoals S5, KD45, S4.2). Hierdoor wordt de volledigheid voor de concrete gebundelde logica's bewezen.

Belangrijkste Bijdragen en Resultaten

• Unificatie van Semantiek en Bisimulatie: De paper biedt de eerste uniforme definitie van bisimulaties voor willekeurige gebundelde modaliteiten, gebaseerd op een veralgemeende buursemantiek. Dit lost het probleem op dat bisimulaties voor elke nieuwe bundel opnieuw moesten worden ontworpen.
• Definitie van Convexe Bundels: De introductie van de klasse van "convexe bundels" en de bijbehorende "convexe buursemantiek" (die ligt tussen minimale en monotone buursemantiek). Dit biedt een robuust raamwerk voor de meeste bestaande voorbeelden.
• Nieuwe Axiomatisaties (Case Studies): De auteurs passen hun methode toe om volledige axiomatisaties te geven voor drie specifieke bundels over specifieke klassen van modellen. Deze resultaten waren tot nu toe niet in de literatuur beschikbaar:
  1. "Iemand weet" ($\bigvee_{a \in A} \Box_a \phi$): Axiomatisatie over S5-modellen.
  2. "Onenigheid in een groep" ($\bigvee_{a,b \in A} \Box_a \phi \land \Box_b \neg \phi$): Axiomatisatie over KD45-modellen.
  3. "Overtuiging zonder kennis" ($B\phi \land \neg K\phi$): Axiomatisatie over S4.2-modellen (en S4F-modellen). Dit wordt geïnterpreteerd als "Dunning-Kruger onwetendheid".
• Technische Innovatie: Ze tonen aan dat de standaard strategie voor volledigheid (canoniek model bouwen + transformatie naar een semantisch equivalent model) met hoge mate van uniformiteit werkt voor deze klasse, mits de juiste representatie-eigenschappen worden aangetoond.

Significantie

Deze paper is significant omdat het een fundamentele theoretische basis legt voor het gebied van gebundelde modaliteiten.

• Het verlegt de focus van het bestuderen van geïsoleerde voorbeelden naar het ontwikkelen van een algemene theorie.
• Het biedt een systematische methode voor het afleiden van bisimulaties en axiomatisaties, wat de ontwikkeling van nieuwe gebundelde logica's aanzienlijk vergemakkelijkt.
• Het introduceert convexe buurlogica als een waardevol nieuw onderzoeksgebied dat strikter is dan algemene buurlogica's maar flexibeler dan normale modale logica's, met rijke semantische eigenschappen.
• De resultaten sluiten de gaten in de literatuur voor specifieke, maar conceptueel belangrijke, logica's zoals die van "valse overtuiging" en "groepsoneenheid", en bieden een blauwdruk voor toekomstig werk in epistemische logica en multi-agent systemen.

Kortom, de auteurs transformeren een fragmentarisch onderzoeksgebied in een gestructureerd theoretisch domein met uniforme tools voor expressiviteit en volledigheid.