Axiomatizing conditional normative reasoning

Classical logic, which manipulates truth values ("true" and "false"), provides a firm foundation for mathematics, and has had important applications in computer science. It has shown its limits in domains where it is necessary to make explicit, and then reason about, the distinction between what ought to be the case and what is the case, or between the ideal and the actual. Norms tell us what ought to be the case, and usually have a conditional form, if-then. Example: if the light is red, then the car ought to stop. In artificial intelligence (AI) and multi-agent systems, norms play a key role in regulating agents behaviors. They are a means of facilitating the coordination among agents, and they make their interaction possible. For instance, a self-driving car must be able to reason about traffic rules. Importantly the norms allow for the possibility that actual behavior may at times deviates from the ideal, i.e. that norm violations may occur. Deontic logic (from the Greek déon, meaning "that which is binding or proper") was created to provide a mathematical model for conditional normative reasoning thus conceived. It holds the promise of giving an AI system the ability to reason about the lawfulness of its own behavior. Since its inception, deontic logic has made major advances, but it still lacks an axiomatic foundation. The project will focus on a prevailing framework for normative reasoning. Its semantics allows for various grades or levels of ideality; a binary classification of states into good/bad is too crude for realistic applications. Axiomatisation is the process of reducing down the theory to a system of basic truths or axioms. It is a mandatory prerequisite for automated reasoning and decision-making. It also helps to understand the commitments of the systems, by identifying their fundamental principles. In deontic logic, axiomatization has remained a challenge: the traditional methods do not so easily apply, due to the higher level of expressiveness of the framework. The projects aim is to fill in this gap. It will develop axiomatisation techniques for normative reasoning, hence bringing deontic logic closer to applications, and enhancing its understanding.

The project aimed to deliver the first comprehensive meta-theoretical study of conditional normative reasoning, with a particular emphasis on axiomatization and automation. Conditional normative reasoning, which pertains to reasoning about conditional norms, is a key focus of dyadic deontic logic, originating from the works of Hansson, Lewis, Aqvist and others. (1) For axiomatization, the most surprising result concerns the role of the property of transitivity of the betterness relation in the models, and the role of various candidate weakenings discussed in economics: quasi-transitivity, acyclicity, Suzumura consistency, and the interval order condition. The project demonstrated that the addition of the interval order condition adds a new axiom to the logic, called the principle of disjunctive rationality. I showed that in contrast, plain transitivity, quasi-transitivity, acyclicity, and Suzumura consistency do not modify the axiomatic characterization. Additionally, alternative truth conditions for the deontic conditional were explored. Notably, a non-standard rule of interpretation called "strong maximality" was studied, leading to new axiomatization and decidability results. These findings provided fresh insights into the role of transitivity in Parfit's repugnant conclusion, a well-known paradox in population ethics. (2) A complexity bound was found for the weakest system considered in this project, Aqvist's system E. It has been shown that the complexity of the validity problem in E is the same as in classical propositional logic: co-NP complete. The result is of prime philosophical and practical importance. It suggests that reasoning about norms is no more complex than propositional reasoning, although the language used for normative reasoning is considerably more expressive. To obtain this result, a detour was made through so-called analytic Gentzen systems. (3) For automation, an indirect approach was taken. The project thoroughly integrated the logic considered in the project into Higher-Order Logic (HOL), enabling the use of Isabelle/HOL, a well-established prover for HOL, for automation. This marked the first mechanization of its kind. Two potential uses of the framework were explored. The first is as a tool for meta-reasoning about the considered logic: the framework was employed for the automated verification of deontic correspondences (broadly conceived) and related matters, similar to previous achievements with the modal logic cube. The second use is as a tool for assessing ethical arguments. As mentioned, a computer encoding of Parfit's repugnant conclusion was provided, enabling a better understanding of this paradox. (4) Results were also achieved in the first-order case, driven by the desire to explore a more nuanced approach to first-order deontic principles and the quantification over individuals within the deontic domain. All in all, the project advanced our understanding of conditional normative reasoning and brought deontic logic closer to applications.