Modeling Deontic Modal Logic in ASP

Stel je voor dat je de scheidsrechter bent van een gigantisch, onzichtbaar spel van "Wat als?" dat zich afspeelt in de hersenen van een computer. In de wereld van de logica zijn er twee belangrijke manieren om over regels te praten. De eerste is als een strikte wiskundige vergelijking: "Als A waar is, dan moet B waar zijn." Dit is klassieke logica, en het is geweldig voor feiten. Maar de tweede manier is veel menselijker: "Je behoort B te doen," of "Het is verboden om A te doen," of "Je bent toegestaan om B te doen." Dit is deontische logica (afgeleid van het Griekse woord voor plicht). Het is de logica van regels, wetten en morele verplichtingen. Het lastige is dat het echte leven rommelig is. Soms ben je verplicht iets te doen, maar kun je dat niet. Soms is het verboden om iets te doen, maar doe je het toch. Decennialang hebben informaticus en filosofen geprobeerd om computers te leren hoe ze met deze "behoort" en "verboden" om moeten gaan zonder in de war te raken of vast te lopen in logische tegenstrijdigheden die bekend staan als "paradoxen."

Dit artikel, getitst "Modeling Deontic Modal Logic in ASP," pakt precies dat probleem aan. De auteurs, een team van onderzoekers uit de VS en Spanje, stellen een slimme nieuwe manier voor om computers te leren hoe ze regels en verplichtingen begrijpen. Ze gebruiken een programmeertaal genaamd Answer Set Programming (ASP), die al beroemd is om zijn vermogen om "wat als"-scenario's en onvolledige informatie te verwerken. Het artikel betoogt dat door regels niet te behandelen als rigide commando's die feiten dwingen te gebeuren, maar als globale restricties (zoals de fluit van een scheidsrechter die blaast als een regel wordt overtreden), computers eindelijk oude, decennia-oude puzzels kunnen oplossen die logici al zo lang in de ban houden. Ze laten zien dat deze methode beroemde logische vallen, zoals de "Contrary-to-Duty"-paradox, waarbij een regel op zichzelf lijkt te spreken wanneer iemand een eerdere regel niet heeft nageleefd, elegant oplost.

De magie van "Behoort" en "Moet"

Om te begrijpen wat de auteurs hebben gedaan, moeten we eerst kennis maken met de twee hoofdrolspelers in hun verhaal: Verplichting en Toestemming. In het dagelijks leven weten we het verschil tussen "Het is noodzakelijk dat de zon opkomt" (een natuurfeit) en "Je behoort je bibliotheekboek in te leveren" (een regel die je kunt breken). In de wereld van de logica wordt het eerste alethisch genoemd (over waarheid en noodzakelijkheid), en het tweede deontisch (over plicht en normen).

De auteurs merkten op dat computers al twee speciale hulpmiddelen hebben om deze verschillende soorten denken aan te pakken, maar dat deze op de verkeerde manier werden gebruikt.

1. Sterke Negatie: Dit is als een harde "Nee." Als een computer zegt "Het regent niet" (sterke negatie), betekent dit dat de computer bewijs heeft dat het absoluut niet regent. Het is een feit.
2. Default Negatie (Negation-as-Failure): Dit is als een "Misschien niet." Als een computer zegt "Het regent niet" (default negatie), betekent dit simpelweg dat de computer geen bewijs heeft gevonden dat het wel regent. Het is een gok gebaseerd op ontbrekende informatie.

Het grote idee van het artikel is om deze twee computertools direct te koppelen aan de twee soorten logica. Ze suggereren dat wanneer we praten over "Het is noodzakelijk dat P" (een feit), we Sterke Negatie gebruiken. Maar wanneer we praten over "Het is niet noodzakelijk dat P" (wat betekent dat P misschien onwaar is, of dat we het gewoon niet weten), gebruiken we Default Negatie. Deze eenvoudige omschakeling stelt de computer in staat om onderscheid te maken tussen een hard feit en een regel die gebroken kan worden.

De "Scheidsrechter"-benadering

Het meest creatieve deel van het artikel is hoe ze omgaan met verplichtingen. In veel oude systemen werd een verplichting zoals "Je moet de auto teruggeven" behandeld als een commando dat de computer dwingt om de auto terug te laten keren. Maar wat als de auto gestolen is? De computer zou crashen omdat hij de auto niet kan dwingen terug te keren.

De auteurs stellen een andere aanpak voor: behandel verplichtingen als Globale Restricties (of "Ontzeggingen"). Stel je een scheidsrechter voor in een voetbalwedstrijd. De scheidsrechter dwingt de spelers niet om te scoren; de scheidsrechter blaast alleen op de fluit als er een overtreding plaatsvindt. In het systeem van de auteurs is een verplichting geen commando om iets waar te maken; het is een regel die zegt: "Als je in een wereld bent waarin deze regel wordt overtreden, dan is die wereld ongeldig."

Bijvoorbeeld, als de regel is "Je moet een autogordel dragen," dan dwingt de computer je niet om hem te dragen. In plaats daarvan stelt het een restrictie op: "Elke wereld waarin je rijdt zonder autogordel, wordt uitgesloten." Als je rijdt en geen autogordel draagt, zegt de computer simpelweg: "Dat scenario is onmogelijk onder deze regels," en zoekt naar een ander scenario waarin je wel een autogordel draagt. Maar cruciaal is dat als je een geldige reden hebt om hem niet te dragen (zoals een medisch noodgeval), de computer deze regel kan "preëmteren" (voorgaan). Het laat de restrictie voor die specifieke situatie vallen, waardoor het scenario toch kan bestaan zonder dat de computer crasht.

Het oplossen van de "Chisholm"-puzzel

Het artikel blinkt het meest uit wanneer het de Contrary-to-Duty Paradox oplost (ook wel bekend als de Chisholm-paradox). Dit is een beroemd logisch hoofdpijndossier dat als volgt gaat:

1. Je behoort naar het feestje te gaan.
2. Als je gaat, behoort je je moeder te vertellen.
3. Als je niet gaat, behoort je je moeder niet te vertellen.
4. Je gaat niet.

In oude logische systemen creëert dit een puinhoop. De computer probeert te bepalen of je je moeder wel of niet moet vertellen, en komt tot een tegenstrijdigheid: je moet haar zowel wel als niet vertellen. Het is alsof een robot hoofdpijn krijgt.

De auteurs laten zien dat hun "Scheidsrechter"-methode dit direct oplost. Ze stellen de regels op als restricties:

• Restrictie 1: Als je niet gaat, mag je je moeder niet vertellen.
• Restrictie 2: Als je gaat, moet je je moeder vertellen.

Wanneer de computer ziet dat je niet bent gegaan (Feit 4), controleert hij de restricties. Hij ziet dat Restrictie 2 (de "Als je gaat"-regel) niet van toepassing is omdat de voorwaarde niet is vervuld. Vervolgens kijelt hij naar Restrictie 1. Omdat je niet bent gegaan, zegt de regel: "Vertel het niet." De computer vindt gemakkelijk een geldige wereld waarin je niet bent gegaan en je moeder niet hebt verteld. Geen tegenstrijdigheid, geen hoofdpijn. De "paradox" verdwijnt omdat de regels worden behandeld als flexibele restricties die alleen van toepassing zijn wanneer hun voorwaarden worden vervuld, in plaats van rigide commando's die met elkaar in strijd zijn.

Waarom dit ertoe doet

De auteurs lossen niet slechts één puzzel op; ze tonen aan dat deze methode werkt voor een hele familie van logische problemen, inclus[ief] "Forrester's paradox" en "Sartre's dilemma." Ze demonstreren dat door Answer Set Programming te gebruiken met zijn ingebouwde vermogen om met "wat als"-scenario's en "uitzonderingen" om te gaan, we complexe ethische en juridische systemen veel natuurlijker kunnen modelleren dan voorheen.

Ze laten ook zien hoe dit omgaat met "secundaire verplichtingen." Stel je voor dat je de auto van een vriend leent. Je hebt een hoofdregel: "Geef de auto terug." Maar er zijn secundaire regels: "Lever hem vóór twaalf uur in" en "Lever hem in met een volle batterij." Als je de auto total loss rijdt (een schending van de hoofdregel), kunnen de secundaire regels veranderen of verdwijnen. De auteurs laten zien hoe hun systeem deze regels automatisch kan "preëmteren". Als de auto verwoest is, wordt de restrictie "Lever voor twaalf uur in" geschrapt omdat de voorwaarde (het hebben van een auto om terug te geven) is vervallen. De computer raakt niet in de war; hij actualiseert simpelweg de lijst met geldige werelden.

De kern van de zaak

Dit artikel beweert niet dat het alle problemen in de ethiek of het recht heeft opgelost. In plaats daarvan biedt het een heldere, elegante toolkit voor het bouwen van systemen die regels begrijpen. Het bewijst dat door "behoortes" te behandelen als restricties op mogelijke werelden in plaats van commando's om de realiteit te veranderen, we computers kunnen bouwen die over regels redeneren zoals mensen dat doen: flexibel, met uitzonderingen en zonder vast te lopen in logische lussen. De auteurs suggereren dat deze aanpak eenvoudiger en directer is dan eerdere methoden, die vaak complexe nieuwe wiskunde of "sancties" (straffen) vereisten om de logica te laten werken. Door gebruik te maken van de instrumenten die al beschikbaar zijn in Answer Set Programming, hebben ze aangetoond dat de weg naar het begrijpen van menselijke regels korter en rechter is dan we gedacht hadden.