Axiomatisierung des Schließens mit normativen Konditionalen

Klassische Logik, die mit Wahrheitswerten (wahr und falsch) manipuliert, bietet eine solide Grundlage für die Mathematik und hat wichtige Anwendungen in der Informatik. Sie hat jedoch ihre Grenzen in Bereichen gezeigt, in denen es notwendig ist, den Unterscheid zwischen dem was der Fall sein sollte und dem, was der Fall ist (zwischen dem Idealen und dem Wirklichen) offenzulegen und formal zu argumentieren. Normen sagen uns, was der Fall sein sollte und haben normalerweise eine bedingte Form: wenn-dann. Beispiel: Wenn die Ampel rot ist, sollte das Auto anhalten. In der künstlicher Intelligenz (KI) und Multi-Agenten-Systemen spielen Normen eine Schlüsselrolle bei der Regulierung des Verhaltens von Agenten. Sie erleichtern die Koordination zwischen den Agenten und ermöglichen deren Interaktion. Ein selbstfahrendes Auto muss beispielsweise in der Lage sein, aus Verkehrsregeln die notwendigen Schlüsse zu ziehen. Wichtig ist, dass die Normen Verhalten zulassen, das manchmal vom Ideal abweicht, d. h. dass es zu Normverletzungen kommen kann. Dahingehend wurde die deontische Logik (aus dem Griechischen déon, das, was verbindlich oder richtig ist) als mathematisches Modell für bedingtes normatives Schließen entwickelt. Es bietet die Grundlage für KI-Systeme, über die Rechtmäßigkeit ihres eigenen Verhaltens nachzudenken. Seit ihrer Einführung gab es große Fortschritte in der deontischen Logik, aber ihr fehlt noch immer eine axiomatische Grundlage. Das Projekt wird sich auf das vorherrschende Framework für normatives Denken konzentrieren. Die Semantik dieses Frameworks ermöglicht verschiedene Grade oder Stufen der Idealität. Eine binäre Einteilung der Zustände in gut/schlecht ist für realistische Anwendungen zu grob. Axiomatisierung ist der Prozess, die Theorie auf ein System von Grundwahrheiten oder Axiomen zu reduzieren. Sie ist zwingende Voraussetzung für automatisiertes Schlussfolgern und Entscheidungsfindung. Darüber hinaus hilft sie, die Verpflichtungen der Systeme zu verstehen, indem es ihre Grundprinzipien identifiziert. In der deontischen Logik ist Axiomatisierung jedoch eine Herausforderung geblieben: Die traditionellen Methoden sind aufgrund der höheren Ausdruckskraft des verwendeten Rahmens nicht so einfach anzuwenden. Ziel des Projekts ist es, diese Lücke zu schließen. Es werden Axiomatisierungstechniken für das normative Denken entwickelt. Damit wird die deontische Logik den Anwendungen näher gebracht und unser Verständnis von normativem Denken verbessert.

Ziel des Projekts war es, die erste umfassende metatheoretische Studie über bedingtes normatives Schließen zu erstellen, mit besonderem Schwerpunkt auf Axiomatisierung und Automatisierung. Das bedingte normative Schließen, das sich auf das Schließen über bedingte Normen bezieht, ist ein zentraler Schwerpunkt der dyadischen deontischen Logik, der auf die Arbeiten von Hansson, Lewis, Aqvist und anderen zurückgeht. (1) Das überraschendste Ergebnis in Hinblick auf die Axiomatisierung ist die Eigenschaft der Transitivität der Besserheitsrelation in den Modellen sowie die verschiedenen, in den Wirtschaftswissenschaften diskutierten, Abschwächungen: Quasi-Transitivität, Azyklizität, Suzumura-Konsistenz und die Intervallordnungsbedingung. Das Projekt zeigte, dass die Intervallordnungsbedingung der Logik ein neues Axiom hinzufügt, das als Prinzip der disjunktiven Rationalität bezeichnet wird. Im Gegensatz dazu habe ich gezeigt, dass einfache Transitivität, Quasi-Transitivität, Azyklizität und Suzumura-Konsistenz die Axiomatisierung nicht verändern. Darüber hinaus wurden alternative Wahrheitsbedingungen für das deontische Konditional erforscht. Insbesondere wurde eine nicht standardisierte Interpretationsregel namens "starke Maximalität" untersucht, die zu neuen Axiomatisierungs- und Entscheidbarkeitsergebnissen führte. Diese Ergebnisse lieferten neue Einsichten in die Rolle der Transitivität in Parfits "abscheulichen Schlussfolgerung" , einem bekannten Paradoxon in der Bevölkerungsethik. (2) Für das schwächste in diesem Projekt betrachtete System, Aqvists System E, wurde eine Komplexitätsgrenze gefunden. Es hat sich herausgestellt, dass die Komplexität des Gültigkeitsproblems in E dieselbe ist wie in der klassischen Aussagenlogik: Co-NP vollständig. Das Ergebnis ist von größter philosophischer und praktischer Bedeutung. Es deutet darauf hin, dass das logische Schließen über Normen nicht komplexer ist als die propositionale Aussagenlogik, trotz der höheren Ausdruckskraft der verwendeten Sprache. Um zu diesem Ergebnis zu gelangen, wurde ein Umweg über sogenannte analytische Gentzen-Systeme gemacht. (3) Für die Automatisierung wurde ein indirekter Ansatz gewählt. Im Rahmen des Projekts wurde die betrachtete Logik vollständig in die Logik höherer Ordnung (HOL) integriert, so dass Isabelle/HOL, ein etablierter automatisierter Beweiser für HOL, für die Automatisierung verwendet werden konnte. Dies war die erste Mechanisierung dieser Art. Es wurden zwei potenzielle Verwendungsmöglichkeiten des Frameworks untersucht. Der erste ist ein Werkzeug für Metaüberlegungen über die betrachtete Logik, das für die automatisierte Verifikation von deontischen Korrespondenzen (im weitesten Sinne) und damit zusammenhängenden Angelegenheiten verwendet wurde, ähnlich den früheren Errungenschaften mit dem modalen Logikwürfel. Der zweite Verwendungszweck ist ein Werkzeug zur Bewertung ethischer Argumente. Wie bereits erwähnt, wurde eine Computerkodierung von Parfit's abscheulichen Schlussfolgerung erstellt, die ein besseres Verständnis dieser Schlussfolgerung ermöglicht. (4) Ergebnisse wurden auch in Prädikatenlogik erster Stufe erzielt, was auf den Wunsch zurückzuführen ist, einen differenzierteren Ansatz für deontische Prinzipien erster Ordnung und die Quantifizierung über Personen innerhalb des deontischen Bereichs zu erforschen. Alles in allem hat das Projekt unser Verständnis von bedingtem normativem Denken erweitert und die deontische Logik näher an praktische Anwendungen herangeführt.