On obligations and normative ability: Towards a logical analysis of the social contract (Q2568339)

The Alternating-time Temporal Logic (ATL) of Alur, Henzinger and Kupferman contains cooperation modalities \(\langle\langle C\rangle\rangle\varphi\) to express that a multi-agent coalition (set of individuals) \(C\) has the ability to bring about \(\varphi\). The logic Normative ATL (NATL\(^*\)) replaces those with constructions \(\langle\langle\eta: C\rangle\rangle\varphi\) to express that \(C\) has the ability to bring about \(\varphi\) within the context of a normative system \(\eta\), where a normative system is a set of constraints on the actions that may be performed in any given state. These constructions of normative ability are then used to define deontic operations of (relative) obligation and permission. After introducing the basic concepts in detail, many properties of the system NATL\(^*\) are examined. In particular, to illustrate its value as a logic for reasoning about multi-agent systems, the authors show how these concepts can be used to formalize a useful notion of the social contract. This is very much deontic logic for computer science; the multi-agent systems being considered are artificial systems and the problems addressed are problems that arise in the theory of computation. This work should, however, also be of interest and value to anyone working in deontic logic generally, including philosophers, as the concepts employed can have broad application to notions of normativity and agency.