Fusions of One-Variable First-Order Modal Logics

Dit artikel onderzoekt behoudsresultaten voor de onafhankelijke fusie van één-variabele eerste-orde modale logieken en toont aan dat Kripke-compleetheid en beslisbaarheid behouden blijven zonder gelijkheid, maar verloren gaan bij fusies met gelijkheid en niet-rigide constanten door middel van het coderen van Diophantische vergelijkingen.

De kern

Stel je voor dat logica een soort receptenboek is voor het bouwen van slimme computers of het begrijpen van complexe regels in de wereld. In dit receptenboek staan twee soorten ingrediënten:

1. Propositionele logica: Dit zijn simpele zinnen zoals "Het regent" of "De deur is open".
2. Eerste-orde logica: Dit is iets geavanceerder, waar je kunt zeggen "Er is iemand die regent" of "Voor elke deur geldt...".

De auteurs van dit artikel (Roman, Dmitry en Frank) zijn op onderzoek uit naar wat er gebeurt als je twee verschillende receptenboeken samenvoegt (een zogenaamde "fusie"). Ze kijken specifiek naar logische systemen die slechts één variabele gebruiken (bijvoorbeeld alleen de variabele 'x' voor "iemand").

Hier is de kern van hun ontdekking, vertaald naar alledaagse taal:

1. De "Vriendelijke" Fusie (Zonder "Gelijkheid")

Stel je voor dat je twee verschillende spellen combineert. In het ene spel mag je alleen bewegen als het dag is, in het andere alleen als het nacht is. Als je deze spellen samenvoegt, maar niet zegt dat "ik" in het ene spel precies dezelfde persoon ben als "ik" in het andere spel (geen "gelijkheid"), dan werkt het wonderbaarlijk goed.

• Wat ze ontdekten: Als je twee logische systemen samenvoegt zonder de regel "x is hetzelfde als y", dan blijven de belangrijkste eigenschappen behouden.
  • Beslisbaarheid: Je kunt nog steeds altijd een computerprogramma schrijven dat zegt: "Ja, deze zin is waar" of "Nee, deze zin is onwaar".
  • Volledigheid: De regels zijn compleet; er zijn geen gaten in het systeem.
• De Metafoor: Het is alsof je twee verschillende soorten Lego-blokken in één doos doet. Zolang je niet probeert twee blokken aan elkaar te "lijmen" (gelijkheid), kun je er nog steeds prachtige, voorspelbare kasten mee bouwen. Je weet precies wat er gebeurt.

Een kleine nuance: Als je kijkt naar de lokale regels (wat gebeurt er op dit specifieke moment?), werkt het perfect. Maar als je kijkt naar de globale regels (wat geldt er voor het hele universum?), kan het soms een beetje "ontsnappen" aan de eindigheid. Je kunt een oneindig groot model nodig hebben om een fout te vinden, zelfs als de regels zelf simpel zijn.

2. De "Gevaarlijke" Fusie (Met "Gelijkheid" en Tellen)

Nu wordt het spannend. Wat gebeurt er als we de regel toevoegen: "x is precies hetzelfde object als y"? En wat als we ook kunnen tellen, bijvoorbeeld: "Er is precies één persoon die dit doet"?

• Wat ze ontdekten: Dit is de valkuil. Zodra je "gelijkheid" en het vermogen om te tellen (tot één) toevoegt, crasht het systeem.
  • Onbeslisbaarheid: Plotseling is het onmogelijk om een computerprogramma te schrijven dat voor elke zin kan zeggen of deze waar is of niet. Het wordt een raadsel dat nooit opgelost kan worden.
  • De Oorzaak: De auteurs tonen aan dat je met deze regels Diophantische vergelijkingen kunt coderen. Dat zijn wiskundige vergelijkingen met gehele getallen (zoals $x^2 + y^2 = z^2$). Het bewijzen dat je deze vergelijkingen kunt simuleren in je logica betekent dat je het probleem van de "onoplosbare vergelijkingen" in je systeem hebt ingebouwd.
• De Metafoor: Stel je voor dat je twee spellen samenvoegt, maar je voegt een regel toe: "Als ik in spel A een rode bal heb, is dat exact dezelfde rode bal als in spel B, en we moeten precies tellen hoeveel er zijn." Plotseling wordt het spel zo complex dat het een Minsky-machine (een soort simpele computer) wordt die oneindig door kan rekenen zonder ooit te stoppen. Je kunt niet meer voorspellen of het spel ooit klaar is.

3. De "S5" Oplossing (De Veilige Haven)

De auteurs kijken ook naar een specifieke manier om deze systemen te combineren, waarbij ze een speciale "S5-modus" gebruiken. Denk aan S5 als een universale camera die alles tegelijk ziet en weet dat alles wat waar is, overal waar is.

• De Oplossing: Als je twee systemen samenvoegt die deze "universale camera" (S5) delen, en je zorgt ervoor dat je modellen "homogeen" zijn (dat wil zeggen: als iets ergens waar is, is het overal in die groep waar), dan kun je de veiligheid terugwinnen.
• De Metafoor: Het is alsof je twee verschillende landen laat samensmelten, maar je zorgt ervoor dat ze allemaal onder één grote, onfeilbare wet vallen (de S5). Zolang ze zich aan die ene grote wet houden, blijven de regels voorspelbaar en beslisbaar, zelfs als je "gelijkheid" gebruikt.

Samenvatting in het Kort

• Geen "Gelijkheid": Alles is veilig, voorspelbaar en oplosbaar. Je kunt twee logische systemen moeiteloos samenvoegen.
• Met "Gelijkheid" en Tellen: Pas op! Je systeem wordt onvoorspelbaar. Je kunt problemen creëren die wiskundig onoplosbaar zijn (zoals het oplossen van bepaalde vergelijkingen).
• De S5-Strategie: Als je een specifieke, sterke regel (S5) deelt tussen de systemen, kun je de veiligheid behouden, zelfs met gelijkheid.

Waarom is dit belangrijk?
Dit onderzoek helpt wetenschappers en programmeurs te begrijpen waar de grenzen liggen van slimme systemen. Het vertelt ons: "Je kunt veel dingen combineren, maar pas op als je begint te tellen en te zeggen 'dit is hetzelfde als dat', want dan verdwalen we in een wiskundige doolhof waar geen uitweg meer is."

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Fusions of One-Variable First-Order Modal Logics" van Kontchakov, Shkatov en Wolter, in het Nederlands.

Titel: Fusies van Eén-variabele Eerste-orde Modale Logica's

1. Probleemstelling

Het onderzoek richt zich op de vraag in welke mate eigenschappen van fusies (independent fusions) van modale logica's behouden blijven wanneer men overgaat van propositional (propositionele) logica naar één-variabele eerste-orde modale logica's.

• Context: In de propositional modale logica is de fusie van twee logica's (waarbij de modale operatoren niet gemengd worden) een "robuuste" combinatie: eigenschappen zoals Kripke-compleetheid, decidabiliteit, de eindige model-eigenschap (FMP) en Craig-interpolatie worden over het algemeen behouden.
• De Uitdaging: Het is onduidelijk of deze behoudsresultaten (preservation results) kunnen worden "opgetild" (lifted) naar eerste-orde logica's, zelfs in de beperkte fragmenten met slechts één variabele.
• Specifieke Variabelen: Het artikel onderzoekt twee scenario's:
  1. Eén-variabele logica's zonder gelijkheid (equality-free).
  2. Eén-variabele logica's met gelijkheid en niet-rigide constanten (of equivalent: tellende kwantificatoren zoals $\exists=1$).
• Semantiek: De analyse omvat zowel expanderende domeinen (expanding domains) als constante domeinen (constant domains).

2. Methodologie

De auteurs gebruiken een combinatie van semantische constructies en rekenkundige reducties:

• Quasimodellen en Cactus-constructies: Voor de logica's zonder gelijkheid bouwen de auteurs voort op de bestaande "cactus model" constructie (uit [18]) en passen deze toe via de quasimodel-techniek (uit [26]). Dit stelt hen in staat om een oneindig aantal domeinelementen te representeren met een eindige set van "types" en "quasistaten".
• Surrogaat-methode: Om de interactie tussen de twee verschillende modale operatoren ($\Box_1$ en $\Box_2$) te analyseren, worden "surrogaat"-predicaten geïntroduceerd. Dit splitst het probleem op in componenten die los van elkaar kunnen worden geanalyseerd binnen de oorspronkelijke logica's.
• Alternatiediepte (Alternation Depth): Voor lokale consequentie wordt een recursieve methode ontwikkeld die de diepte van de afwisseling tussen de modale operatoren meet. Dit maakt een decisiemogelijkheid mogelijk door het probleem te reduceren tot eenvoudigere formules.
• Rekenkundige Reducties (Onbeslisbaarheid): Voor de logica's met gelijkheid worden Diophantische vergelijkingen en Minsky-machines (twee-teller automaten) gecodeerd in de logica. Dit dient om onbeslisbaarheid aan te tonen.
• Homogene Modellen: Voor de propositional logica's die een gedeelde S5-modus delen, introduceren de auteurs het concept van E-homogene modellen. Hierin is de waarheid van een formule binnen een equivalentieklasse van de S5-relatie ofwel nergens waar ofwel waar in een oneindig groot aantal werelden (grootte $\kappa$).

3. Belangrijkste Resultaten

De paper presenteert drie hoofdstellingen (Theorema A, B en C):

A. Fusies zonder Gelijkheid (Theorema A)
Voor één-variabele logica's zonder gelijkheid worden de volgende behoudsresultaten bewezen:

• Kripke-compleetheid: Wordt behouden voor zowel lokale als globale consequentie, onder zowel expanderende als constante domein-semantiek.
• Decidabiliteit: Wordt behouden voor zowel lokale als globale consequentie.
• Eindige Model-eigenschap (FMP):
  • Wordt behouden voor de lokale consequentie.
  • Wordt niet behouden voor de globale consequentie. De auteurs tonen aan dat voor alle niet-triviale fusies de globale consequentie faalt om de FMP te hebben (er zijn geen eindige tegenvoorbeelden voor niet-geldigheid).

B. Fusies met Gelijkheid (Theorema B)
Zodra gelijkheid en niet-rigide constanten worden toegestaan, breken de behoudsresultaten volledig:

• Decidabiliteit en Recursieve Axiomatisatie: Worden niet behouden. Zelfs als de componenten decibel zijn, kan de fusie onbeslisbaar worden.
• Bewijs: Dit wordt aangetoond door Diophantische vergelijkingen te coderen in de fusie van specifieke logica's (gebaseerd op de 'elsewhere' logica en eindige domeinen).
• Globale Consequentie: Voor constante domeinen is de globale consequentie van alle niet-triviale fusies met gelijkheid onbeslisbaar.

C. Propositional Fusies met Gedeelde S5 (Theorema C)
De auteurs bieden een algemene voldoende voorwaarde voor de overdracht van eigenschappen in propositional logica's die een gedeelde S5-modus delen:

• Als de component-logica's E-homogene modellen toelaten, dan worden Kripke-compleetheid en decidabiliteit behouden bij de fusie.
• Dit resulteert in transfer-resultaten voor de corresponderende één-variabele logica's (via een vertaling waarbij $\forall x$ wordt gemappt naar de S5-modus).
• Beperking: Net als bij de eerste-orde resultaten, wordt de eindige model-eigenschap niet noodzakelijk behouden in deze context.

4. Significatie en Implicaties

• Fundamenteel Inzicht: Het artikel maakt een scherpe scheiding tussen de "goede" wereld van één-variabele logica's zonder gelijkheid (waar fusies goed gedragen) en de "slechte" wereld met gelijkheid (waar fusies onbeslisbaar kunnen worden).
• Grenzen van Decidabiliteit: Het resultaat dat de monodische fragmenten van eerste-orde logica met gelijkheid onbeslisbaar kunnen zijn (zelfs als de onderliggende twee-variabele fragmenten met tellen decibel zijn), is een belangrijk negatief resultaat voor de theorie van monodische logica's.
• Methodologische Vooruitgang: De uitbreiding van de cactus-constructie en de introductie van homogene modellen bieden nieuwe gereedschappen voor het analyseren van complexe modale systemen en hun fusies.
• Toekomstige Richtingen: De auteurs wijzen op open vragen, zoals het gedrag van fusies van volledige eerste-orde logica's en het vinden van voldoende voorwaarden voor behoud van eigenschappen bij fusies met gelijkheid (waarbij standaard systemen zoals polymodale K en S5 toch decibel blijven, ondanks het algemene onbeslisbaarheidsresultaat).

Conclusie:
De paper concludeert dat de robuustheid van fusies in propositional logica niet automatisch naar eerste-orde logica's overgaat. De aanwezigheid van gelijkheid is een kritieke factor die de decidabiliteit en de eindige model-eigenschap kan vernietigen, terwijl de afwezigheid van gelijkheid (in combinatie met de één-variabele beperking) de behoudsresultaten voor compleetheid en decidabiliteit in stand houdt.