Agentive Permissions in Multiagent Systems

1 Introduction

Imagine a large factory being built in a city on a river. The factory will dump a pollutant into the river. It is known that a small factory located in another city higher up the river already exists and can dump up to 60g/day of the same pollutant. Also, more than 100g/day of the pollutant dumped into the river combined by the two factories will kill the fish.

Suppose that the large factory will dump 20g/day of the pollutant. Then, the total dumped amount by both factories will not exceed 80g/day no matter how much the other factory dumps and thus the fish in the river will survive for sure. In other words, the action that dumping 20g/day ensures the survival of the fish. On the contrary, if the large factory will dump 60g/day of the pollutant, then the fish will be killed once the other factory dumps more than 40g/day. That is to say, the action that dumping 60g/day does not ensure the survival of the fish. However, it still leaves the possibility for the fish to survive, e.g. when the other factory dumps no more than 40g/day. In this situation, we say that the action that dumping 60g/day admits of the survival of the fish.

To ensure and to admit show two different types of agency of an action. The difference comes from that, in multiagent or nondeterministic settings, the effect of an action of one agent might be affected by the actions of other agents or the nondeterminacy. It is worth noting that, admitting is the dual of ensuring. To be specific, if an action of an agent ensures an outcome, then the action does not admit of the opposite outcome, and vice versa. It is easy to see that their meanings coincide in single-agent deterministic settings.

In this paper, we consider the two types of agency together with permissions. Let us come back to the large factory. Sup- The factory is permitted to dump any amount of the pollutant as long as the fish is not killed.

The full version of this paper includes an appendix, which can be found at arXiv: 2404.17053.

This regulation can be interpreted in two ways corresponding to two types of agency. The first could be

any dumping amount that admits of the survival of the fish is permitted. (SA)

In this interpretation, the permitted dumping amount of the factory is any amount no more than 100g/day. As long as the factory follows this regulation, there is a chance for the fish to survive if the other factory dumps so little that the total dumped amount does not exceed 100g/day. The second interpretation of the regulation could be

any dumping amount that ensures the survival of the fish is permitted. (SE)

In this interpretation, the factory should not dump any amount over 40g/day and the fish cannot be killed as long as the factory follows the regulation, no matter how much of the pollutant is dumped by the other factory.

The above two interpretations give the factory two different permissions. It is worth noting that, either of the permissions enables the factory to take any of the actions satisfying some criteria. In this paper, we call such permissions "strong". Specifically, we refer to (SA) and (SE) as strong permission to admit and strong permission to ensure, respectively.

Not all permissions are in the same form as strong permissions. Suppose that, instead of the city's regulation, the factory is under some contractual obligation. To satisfy this obligation, the factory has to dump at least 30g/day of the pollutant. In this case, not every amount that ensures/admits of the survival of the fish (e.g. 20g/day) is contractually permitted to be dumped. Nevertheless,

there is a permitted dumping amount that ensures the survival of the fish. (WE)

For example, 35g/day is a contractually permitted dumping amount that ensures the survival of the fish. Similarly, if the contractual obligation forces the factory to dump at least 50g/day of the pollutant, then no contractually permitted dumping amount ensures the survival of the fish. However,

there is a permitted dumping amount that admits of the survival of the fish. (WA)

In contrast to strong permissions, the above two permissions express the capability of the factory to achieve some statements with a permitted action. We call such permissions "weak". Specifically, we refer to (WE) and (WA) as weak per-

mission to ensure and weak permission to admit, respectively.

As shown in Section 2, the terms "strong permission" and "weak permission" have already existed in the literature for decades [Raz, 1975; Royakkers, 1997; Governatori et al., 2013]. In Section 5, we show the consistency between how these terms are used in our paper and in the literature. However, as far as we see, we are the first to make a clear distinction between "permission to ensure" and "permission to admit", which are agentive permissions specific to multiagent settings. We are also the first to cross-discuss both strong and weak agentive permissions in multiagent settings.

In this paper, we discuss four forms of permissions in multiagent settings that generalise those expressed in statements (SA), (SE), (WE), and (WA). Our contribution is three-fold. First, we propose a formal semantics for the four corresponding modalities in multiagent transition systems (Section 3). We also consider the model-checking problem (Section 3.1) and the reduction to STIT logic and ATL (Section 3.2). Second, we prove these modalities are semantically undefinable through each other (Section 4). This contrasts to the fact that, when separated from permissions, ensuring and admitting are dual to each other. Third, we give a sound and complete logical system for the four modalities (Section 5 and Section 6). This reveals the interplay between the four forms of permissions and offers an efficient way for permission reasoning.

2 Literature Review and Notion Discussion

Deontic logic [McNamara and van de Putte, 2022] is an appealing approach to solving AI ethics problems by enabling autonomous agents to comprehend and reason about their obligation, permission, and prohibition. It aims at "translating" the deontic statements in natural languages into logical propositions and building up a system for plausible deduction. Von Wright [1951] launched the active development of symbolic deontic logic from the analogies between normative and alethic modalities. Several follow-up works [Anderson, 1956; Prior, 1963] built up the Standard Deontic Logic (SDL), taking obligation as the basic modality and defining permission as the dual of obligation and prohibition as the obligation of the negation. Anderson [1967] and Kanger [1971] reduced this system by defining a propositional constant d for "all (relative) normative demands are met". By this means, obligation (modality O) can be defined as O' := ⇤(d ! ')↪ which is read as "it is necessary that ' is true when all normative demands are met". As the dual of obligation, permission (modality P) is defined as

which is read as "it is possible that all normative demands are met and ' is true". In this way, the inference rule

is valid. The notion of permission that satisfies statement (2) is called weak permission. There are two well-known related paradoxes about weak permission:

(i) Ross's paradox [Ross, 1944]. The formula

is valid by statement (2). However, in common sense, for a kid "it is permitted to eat an apple" is true but "it is permitted to eat an apple or drink alcohol" should be false, which contradicts statement (3).

(ii) The free choice permission paradox [von Wright, 1968; Kamp, 1973]. According to linguistic intuition, if "it is permitted to eat an apple or a banana", then both "eating an apple" and "eating a banana" should be permitted. This shows that disjunctive permission is treated as free choice permission, which means the formula

should be valid. However, statement (4) is not derivable in SDL. Free choice permission is a form of strong permission [Asher and Bonevac, 2005], satisfying the inference rule

Following Anderson and Kanger's way, van Benthem [1979] captured the notion of strong permission as

which is read as "it is necessary that if ' is true then all normative demands are met". He then gave a complete axiom system for obligation (O) and strong permission (Ps ).

Most researchers agree that both weak and strong permission makes sense. As discussed by Lewis [1979], no universal comprehension of permission seems to exist. In general, weak permission is treated as the dual of obligation. Strong permission, as well as free choice permission, is more intractable and arouses more interesting discussions due to its anti-monotonic inference property in statement (5). For instance, Anglberger et al. [2015] adopted the notion of strong permission and defined a notion of obligation as the weakest form of (strong) permission. Wang and Wang [2023] axiomatised a logic of strong permission that satisfies some commonly desirable logical properties. Strong permission is also studied in defeasible logic [Asher and Bonevac, 2005; Governatori et al., 2013], which is believed to be able to capture the logical intuition about permission.

The above discussion of permission applies possible-world semantics without specifically considering agents and their agency. However, it is noticed that two kinds of normative statements exist: the agentless norms that talk about states (e.g. it is permitted to eat an apple) and the agentive norms that talk about actions (e.g. John is permitted to eat an apple). The possible-world semantics cannot distinguish them. To fill the gap, Chisholm [1964] proposed a transfer from any agentive norm to an agentless norm. For instance, the statement "agent a is permitted to do '" is transformed into "it is permitted that agent a does '". Some recent work [Kulicki and Trypuz, 2017; Kulicki et al., 2023] aimed at integrating the agentless and agentive norms in a unified logical frame.

Things become more complicated when agents and their agency are incorporated. In the literature, STIT logic [Chellas, 1969; Belnap and Perloff, 1988; Belnap and Perloff,

1992] is used to express the agency. Horty and Belnap [1995] and Horty [2001, chapter 4] introduced a deontic STIT logic for ought-to-be and ought-to-do semantics, respectively. The former corresponds to the agentless obligations while the latter corresponds to the agentive obligations in STIT models. Horty [2001, chapter 3] further showed that the transfer proposed by Chisholm does not always work properly. Following Horty, van de Putte [2017] briefly discussed the dual of the ought-to-do obligation, which is the weak permission in deontic STIT logic, and then defined a form of free choice permission following statement (4). Although the agency is considered in deontic STIT logic, the distinction between to ensure and to admit is never discussed there.

In the field of AI, there is a rising interest in applying deontic logic into agents' planning: how to achieve a goal while complying with the deontic constraints [Pandˇzi´c et al., 2022; Areces et al., 2023]. There is also some discussion of agents' comprehending and reasoning norms [Arkoudas et al., 2005; Broersen and Ram´ırez Abarca, 2018]. However, to the best of our knowledge, the agentive weak and strong permissions have never been cross-discussed before.

In this paper, we consider both permission to ensure and permission to admit in both weak and strong forms that follow statements (1) and (6). In a word, we consider four forms of permissions as illustrated in statements (SA), (SE), (WE), and (WA). It is worth mentioning that, our formalisation has a connection with Horty's ought-to-do deontic STIT logic [Horty, 2001]. On the one hand, the notion "ensure" captures the same idea as "see to it that" in STIT logic. On the other hand, our formalisation can be seen as a reasonable reduction of Horty's formalisation. Specifically, Horty's approach is to, first, define a preference over the outcomes (i.e. "histories" in STIT models) of actions in the model, then, apply the dominance act utiliarianism to decide which actions are permitted (i.e. "optimal" in his work) in semantics, and, finally, define the ought-to-do obligation based on the permitted actions in semantics. In particular, an action in the STIT frame is the set of outcomes that may follow from the action. An action "sees to it that" ' if and only if ' is true in all the potential outcomes. Then, "do '" is interpreted as "seeing to it that '". In this paper, we combine the first two steps of Horty's approach, directly defining the deontic constraints on actions in the model and then defining four forms of permissions in semantics. Note that, the definition of deontic notions is independent of the process that combines the first two steps in Horty's approach. In other words, our work in this paper can easily be transformed from action-based models into outcome-based models by recovering the step of deciding permitted actions based on preference over outcomes using dominance act utilitarianism. Moreover, we give a reduction of our semantics into STIT logic in Section 3.2.

3 Syntax and Semantics

In this section, we introduce the syntax and semantics of our logical system. Throughout the paper, unless stated otherwise, we assume a fixed set A of agents and a fixed nonempty set of propositional variables.

Definition 1. A transition system is a tuple (S↪ ∆↪ D↪ M↪ ⇡):

1. S is a (possibly empty) set of states;
2. ∆ = ¶∆sa ♦s2S↪a2A is the action space, where ∆sa is a nonempty set of actions available to agent a in state s;
3. D = ¶Dsa ♦s2S↪a2A is the deontic constraints, where Dsa is a set of permitted actions and ? ( Dsa ✓ ∆sa ;
4. M = ¶Ms♦s2S is the mechanism, where a relation Ms ✓ Qa2A ∆sa ⇥ S satisfies the continuity condition: for each action profile δ 2 Qa2A ∆sa there is a state t 2 S such that (δ↪ t) 2 Ms;
5. ⇡(p) ✓ S for each propositional variable p.

The continuity condition in item 4 above requires the existence of a "next" state t. We say that a transition system is deterministic if such state t is always unique.

The language Φ of our logical system is defined by the following grammar:

where p is a propositional variable and a 2 A is an agent. Intuitively, we interpret WAa' as "there is a permitted action of agent a that admits of '", WEa' as "there is a permitted action of agent a that ensures '", SEa' as "each action of agent a that ensures ' is permitted", and SAa' as "each action of agent a that admits of ' is permitted". We assume that conjunction ^, implication !, and Boolean constants true > and false ? are defined in the usual way. Also, by Vin 'i and Win 'i we denote, respectively, the conjunction and the disjunction of the formulae '1↪ ▷ ▷ ▷ 'n. As usual, we assume that the conjunction and the disjunction of an empty list are > and ?, respectively.

Definition 2. For each transition system (S↪∆↪D↪M↪ ⇡), each state s 2 S, and each formula ' 2 Φ, the satisfaction relation s ⊩ ' is defined recursively as follows:

1. s ⊩ p, if s 2 ⇡(p);
2. s ⊩ '_ , if s ⊩ ' or s ⊩ ;
3. s ⊩ ≻', if s 1 ';
4. s ⊩ WAa', if (s↪ i) 6 a ≻' for some i 2 Dsa ;
5. s ⊩ SEa', if i 2 Dsa for each i such that (s↪ i) a ';
6. s ⊩ WEa', if (s↪ i) a ' for some i 2 Dsa ;
7. s ⊩ SAa', if i 2 Dsa for each i such that (s↪ i) 6 a ≻',

where the notation (s↪ i) a ' means that, for each tuple (δ↪ t) 2 Ms, if δa = i, then t ⊩ '.

Items 4 - 7 above capture the generalised notions of permissions in statements (WA), (WE), (SE), and (SA) in Section 1. Informally, (s↪ i) a ' means that that action i of agent a in state s ensures that ' is true in the next state. Accordingly, (s↪ i) 6 a ≻' means that action i of agent a in state s admits of the situation that ' is true in the next state. Observe that, if a transition system is deterministic and has only one agent a, then (s↪ i) 6 a ≻' if and only if (s↪ i) a '. Then, the next lemma follows from items 4 - 7 of Definition 2.

Lemma 1. If set A contains only agent a, then for any for-

mula ' 2 Φ and state s of a deterministic transition system, 1. s ⊩ WAa' if and only if s ⊩ WEa';

Note that, in other cases (i.e. multiagent or nondeterministic systems), these modalities are not only semantically inequivalent but also undefinable through each other. We show this in Section 4.

3.1 Model Checking

Following Definition 2, we consider the global modelchecking problem [M¨uller-Olm et al., 1999] of language Φ. For a finite transition system and a formula ' 2 Φ, the global model checking determines the truth set J'K that consists of all states satisfying ' in the transition system. Formally, we define the truth set of a formula as follows.

Definition 3. For any given transition system and any for-

mula ' 2 Φ, the truth set J'K is the set ¶s ♣ s ⊩ '♦. The global model checking of formula ' applies a trivial recursive process on its structural complexity. The next theorem shows its time complexity. See Appendix A of the full version [Shi, 2024] for a detailed analysis of the algorithm.

Theorem 1 (time complexity). For a finite transition system (S↪∆↪D↪M↪ ⇡) and a formula ' 2 Φ, the time complexity of global model checking is O(♣'♣ · (♣S♣+♣M♣+♣∆♣)), where ♣'♣ is the size of the formula, ♣S♣ is the number of states, ♣M♣ = Ps2S ♣Ms♣ is the size of the mechanism, and ♣∆♣ = Pa2A Ps2S ♣∆sa ♣ is the size of the action space.

3.2 Reduction to Other Logics

Recall statements (1) and (6) in Section 2, which show the way how Anderson and Kanger reduces SDL. Using a similar technique, we can translate our modalities into modalities in STIT logic and ATL [Alur et al., 2002] after properly interpreting the transition system in Definition 1.

Reduction to STIT Instead of being about the states, the statements in STIT logic are about moment-history (m◁h) pairs. Due to this fact, there is no exact reduction of our logic to STIT logic. However, we can interpret our modalities in STIT models in the appearance of the necessity and possibility modalities ⇤ and ⌃1 . In order to do this, we first incorporate the deontic constraints into the models as atomic propositions. To be specific, m◁h ⊩ da represents that the action of agent a at moment m that includes history h is permitted. We use the modality XSTIT [Broersen, 2008; Broersen, 2011]. Informally, m◁h ⊩ XSTITa' could be interpreted as "the action of agent a at moment m that includes history h sees to it that ' is true at the next moment". Then, our four modalities can be translated as:

Reduction to ATL Unlike in STIT logic, in ATL, the statements are about states but there is no way to express the properties of actions. For this reason, we encode deontic constraints into the states. To do this, we expand each state in our original transition system into a set of states in the ATL model. Specifically, each state s in our original transition system corresponds to a set ¶hs↪Di ♣D ✓ A♦ of states in the ATL model. Informally, the tuple hs↪Di encodes the information that "state s is reached after the agents in set D taking permitted actions and the others taking non-permitted actions". Then, hs↪Di ⊩ da if and only if a 2 D. Also, hs↪Di ⊩ p if and only if s ⊩ p in our original transition system. Correspondingly, the transition (hs↪ ⇤i↪ ht↪Di) exists in the ATL model if there is a tuple (δ↪ t) 2 Ms in our original transition system such that D = ¶a 2 A ♣ δa 2 Dsa ♦ and ⇤ is a wildcard. Note that, ATL requires the transitions to be deterministic. Thus, if needed, we incorporate a dummy agent Nature into the agent set A to achieve determinacy. Then, we can translate our modalities into standard ATL syntax as:

1m◁h ⊩ ⇤' iff m◁h0 ⊩ ' for each history h0 such that m 2 h0 .

where hhCiiX' is informally interpreted as "the agents in set C can cooperate to enforce ' in the next state" and hhaii is the abbreviation for hh¶a♦ii.

4 Mutual Undefinability

As we define four modalities in the language, we would like to figure out if all of them are necessary to express the corresponding notions of permission. Specifically, if some of these modalities are semantically definable through the others, then the definable ones are not necessary for the language. As an example, a well-known result in Boolean logic is De Morgan's laws, which say conjunction and disjunction are interdefinable in the presence of negation. Therefore, to consider a "minimal" system for propositional logic, it is not necessary to include both conjunction and disjunction.

In this section, we consider the definability of modalities in the same way as De Morgan's laws (i.e. semantical equivalence). For example, modality WA is definable through modalities WE, SE, and SA if every formula in language Φ is semantically equivalent to a formula using only modalities WE, SE, and SA. Formally, in the transition systems, we define semantical equivalence as follows.

Definition 4. Formulae ' and are semantically equivalent

if J'K = J K for each transition system. We prove that none of the modalities WA, WE, SE, and SA is definable through the other three. To do this, it suffices to show that, for each modality ⊙ of the four modalities, there exists a formula ⊙' 2 Φ and a transition system where J⊙'K 6= J K for each formula not usingmodality⊙. In particular, we use the truth set algebra technique [Knight et al., 2022]. This technique uses one model (i.e. transition system) and shows that, in this model, the truth sets of all formulae not using modality ⊙ form a proper subset of the family of all truth sets in language Φ, while the truth set of the formula ⊙' does not belong to this subset. We formally state the undefinability results in the next theorem. A detailed explanation of the technique and proof can be found in Appendix B of the full version.

Theorem 2 (undefinability of WA). The formula WAap is not semantically equivalent to any formula in language Φ that does not use modality WA.

The formal statements of the undefinability results for modalities WE, SE, and SA are the same as Theorem 2 except for using the corresponding modalities instead of WA, see Theorem 5, Theorem 6, and Theorem 7 in Appendix B of the full version.

Note that, all four undefinability results, as presented in Appendix B of the full version, require that our language contains at least two agents. In single-agent settings, if a transition system is nondeterministic, these undefinability results still hold. This can be observed by modifying the two-agent transition systems in the proofs into single-agent nondeterministic transition systems by treating one of the agents as the nondeterministic factor. If a single-agent transition system is deterministic, then, as observed in Lemma 1, modalities WA and WE are semantically equivalent, so as modalities SE and SA. However, modalities WA (WE) and SA (SE) are not definable through each other, see Appendix B.5 of the full version.

5 Axioms

In addition to the tautologies in language Φ, our logical system contains the following schemes of axioms for all agents a↪ b 2 A and all formulae '↪ 2 Φ:

Axiom A1 says agent a does not have a permitted action that has no next state. This is true because of the continuity property of the mechanism (item 4 of Definition 1). Axiom A2 says agent a always has a permitted action that ensures a next state. This is true because of the continuity property and the nonempty set of permitted actions (item 3 of Definition 1). Axiom A3 says every action that may have no next state is permitted. This is true because no such actions exist again due to the continuity property. Axiom A4 is true because both SEa> and SAa> mean that every action of agent a is permitted.

Axiom A5 says, if agent a has a permitted action that admits of '_ , then agent a either has a permitted action that admits of ' or has a permitted action that admits of . This is true because the permitted action that admits of '_ indeed either admits of ' or admits of (item 3 of Definition 2). Axiom A6 says, if every action of agent a that admits of ' is permitted and every action of agent a that admits of is permitted, then every action of agent a that admits of '_ is permitted. This is true because any action that admits of '_ either admits of ' or admits of (item 3 of Definition 2).

Axiom A7 says, if agent a has a permitted action that ensures ' and has no permitted action that ensures , then agent a has a permitted action that admits of ' ^ ≻ . This is true because the permitted action i that ensures ' does not ensure . Hence, action i admits of ≻ while ' is ensured to happen. Axiom A8 says, if agent a has a non-permitted action that ensures ' and every action that ensures is permitted, then agent a has a non-permitted action that admits of '^≻ . This is true because the non-permitted action j that ensures ' does not ensure . Hence, action j admits of ≻ while ' is ensured to happen.

Axiom A9 says, if agent a has no permitted action that admits of ' and every action that admits of is permitted, then agent b has no permitted action that admits of '^ and every action of agent b that admits of ' ^ is permitted. This is true because the antecedent means agent a's permitted actions ensure ≻' and non-permitted actions (if existing) ensure ≻ . Thus, every action of agent a ensures ≻' _ ≻ (item 3 of Definition 2). Hence, ≻(' ^ ) is unavoidable in the next state. This implies that agent b has no permitted action that admits of '^ , and any action of agent b that admits of '^ is permitted because no such action of agent b exists.

We write ` ' and say that formula ' is a theorem of our logical system if it can be derived from the axioms using the following four inference rules:

Rule IR2 is the monotonicity rule for modality WA. It is valid because, in each state of each transition system, the permitted action of agent a that admits of ' also admits of , as ' ! is universally true. By this rule, modality WA represents a form of weak permission following statement (2). Rule IR3 is the anti-monotonicity rule for modality SA. It is valid because, in each state of each transition system, the set of actions that admits of is a superset of the set of actions that admits of ', as '! is universally true. Hence, as long as the actions in the former set are all permitted, those in the latter set are also permitted. This rule shows that modality SA represents a form of strong permission following statement (5). It can be derived that modality WE represents a form of weak permission and modality SE represents a form of strong permission, see Appendix C.1 of the full version.

Rule IR4 is a conflict-preventing rule following the notion of "ensure" in semantics. The premise says, if every one of '1↪ ▷ ▷ ▷ ↪ 'm is true, then at least one of 1↪ ▷ ▷ ▷ ↪ n is false. The conclusion says, for a set of distinct agents ¶a1↪ ▷ ▷ ▷ ↪ am↪ b1↪ ▷ ▷ ▷ ↪ bn♦ ✓ A, if every agent ai has a permitted action to ensure 'i, then for at least one agent bj, every action that ensures j is permitted. This is valid because there would be a conflict otherwise. To be specific, if there is a state s where the conclusion of the rule is false, then, each agent ai has a permitted action ki that ensures 'i and each agent bj has a non-permitted action `j that ensures j. Consider an action profile δ such that δai = ki for each i  m and δbj = `j for each j  n. By the continuity condition in item 4 of Definition 1, there is a state t such that (δ↪ t) 2 Ms. In such state t, each of the formulae '1↪ ▷ ▷ ▷ ↪ 'm↪ 1↪ ▷ ▷ ▷ ↪ n is true. However, this conflicts with the premise of the rule.

We write X ` ' if a formula ' can be derived from the theorems of our logical system and an additional set of assumptions X using only the Modus Ponens rule. Note that statements ? ` ' and ` ' are equivalent. We say that a set of formulae X is consistent if X 0 ?.

See the proof of Lemma 2 in Appendix C.2 of the full version.

Lemma 3 (Lindenbaum). Any consistent set of formulae can be extended to a maximal consistent set of formulae.

The standard proof of this lemma can be found in [Mendelson, 2009, Proposition 2.14].

See the proofs of the above two lemmas in Appendix C.3 of the full version. The next theorem follows from the above discussion of the axioms and the inference rules.

Theorem 3 (soundness). If ` ', then s ⊩ ' for each state s of each transition system.

6 Completeness

In this section, we prove the strong completeness of our logical system. As usual, at the core of the completeness theorem is the canonical model construction. In our case, it is a canonical transition system.

6.1 Canonical Transition System

In this subsection, we define the canonical transition system (S↪ ∆↪ D↪ M↪ ⇡).

Definition 5. Set S of states is the family of all maximal consistent subsets of our language Φ.

For each formula ' 2 Φ, we introduce two actions: a permitted action '+ and a non-permitted action '-. Formally, by '+ and '- we mean the pairs ('↪ +) and ('↪ -), respectively. By item 7 of Definition 2, the formula SAa> expresses that agent a is permitted to use every action. In other words, if SAa> is true, then there are no non-permitted actions available to agent a in the current state. This explains the intuition behind the following definition.

Definition 6. For each state s 2 S and each agent a 2 A,

The next definition is the key part of the canonical transition system construction. It specifies the mechanism of the transition system. Recall that ≻WAa' means that agent a is not permitted to use any action that admits of '. Hence, each permitted action of a must ensure ≻'. We capture this rule in item 1 of the definition below. Recall that WEa' means that agent a has at least one permitted action that ensures '. In the canonical transition system, this action is defined to be '+. The rule captured in item 2 below guarantees ' in the next state whenever agent a uses action '+. Next, ≻SEa' means that agent a is not permitted to use at least one action that ensures '. We denote such action by '-. The rule captured by item 3 stipulates that action '- ensures '. Finally, SAa' means that agent a is permitted to use all actions that admit of '. In other words, SAa' means that all non-permitted actions ensure ≻'. This is captured by item 4 below.

Definition 7. (δ↪ t) 2 Ms when for each agent a 2 A and each formula ' 2 Φ,

1. if δa 2 Dsa and WAa' ◁2 s, then ≻' 2 t;
2. if δa = '- and SEa' ◁2 s, then ' 2 t;

Note that, each state s is a maximal consistent set by Defintion 5. Hence, for item 1 above, the statement WAa' ◁2 s is equivalent to ≻WAa' 2 s. The same goes for item 3.

This concludes the definition of the canonical transition system (S↪∆↪D↪M↪ ⇡). Next, we show that it satisfies the continuity condition in item 4 of Definition 1.

Lemma 6 (continuity). For each state s 2 S and each action profile δ 2 Qa2A ∆sa , there is a state t such that (δ↪ t) 2 Ms.

Proof. Consider a partition ¶A↪ B♦ of the set A of agents:

Then, SAb> ◁2 s for each agent b 2 B by Definitions 6. Hence, ≻SAb> 2 s for each agent b 2 B because s is a maximal consistent set. Then, by the contrapositive of axiom A4,

Consider the set of formulae

Claim 1. Set X is consistent.

Proof of Claim. Suppose the opposite. Then, by axiom A2, statements (9) and (10), there are formulae

where

for each i  m, and

for each i  n, such that

By multiple application of the countrapositive of axiom A5 and propositional reasoning, statement (11) implies that

Note that, in the specific case where ki = 0, statement (15) follows directly from axiom A1. By Lemma 4, statement (15) and the part WEai b σi 2 s of statement (11) imply

Meanwhile, by multiple application of Lemma 2 and propositional reasoning, statement (14) can be reformulated to

By statement (13) and rule IR4, statement (17) implies

Then, by statement (16) and the Modus Ponens rule,

At the same time, by multiple application of axiom A6 and propositional reasoning, statement (12) implies

Note that, in the specific case where `i = 0, statement (19) follows directly from axiom A3. By Lemma 5, statement (19) and the part ≻SEbi b ⌧i 2 s of statement (12) imply

which contradicts statement (18). ⇥

Let t be any maximal consistent extension of set X. By Lemma 3, such t must exist. Hence, t 2 S by Definition 5.

Claim 2. (δ↪ t) 2Ms.

Proof of Claim. It suffices to verify that conditions 1 - 4 of Definition 7 are satisfied for the tuple (δ↪ t) for each agent x 2 A. Recall that sets A and B form a partition of the agent set A. Hence, it suffices to consider the following two cases.

Case 2: x 2 B. Conditions 1 and 2 of Definition 7 trivially follow from δx ◁2 Dsx by statement (8). Condition 3 follows from line 4 of statement (10) because X ✓ t. Condition 4 follows from line 3 of statement (10). ⇥

Case 1: x 2 A. Condition 1 of Definition 7 follows from line 1 of statement (10) because X ✓ t. Condition 2 follows from line 2 of statement (10). Conditions 3 and 4 trivially follow from δx 2 Dsx by statement (7).

The statement of this lemma follows from Claim 2.

6.2 Strong Completeness Theorem

As usual, at the core of the proof of completeness is a truth lemma proven by induction on the structural complexity of a formula. In our case, it is the Lemma 7. The completeness result, as shown in Theorem 4, is proved with Lemma 7 in the standard way. We put the formal proofs in Appendix D of the full version.

Lemma 7. s ⊩ ' if and only if ' 2 s for each state s of the canonical transition system and each formula ' 2 Φ.

Theorem 4 (strong completeness). For each set of formulae X ✓ Φ and each formula ' 2 Φ such that X 0 ', there is a state s of a transition system such that s ⊩ χ for each χ 2 X and s 1 '.

7 Conclusion and Future Research

We are the first to classify the agentive permissions in multiagent settings into permissions to ensure and permissions to admit and cross-discuss them in both weak and strong forms. To do this, we propose and formalise four forms of agentive permissions in multiagent transition systems, analyse the time complexity of the model checking algorithm, prove their semantical undefinability through each other, and give a sound and complete logical system that reveals their interplay.

Future research could be in two directions. One is to extend the deontic constraints from one-step actions to multi-step actions. Indeed, multi-step deontic constraints are commonly seen in application scenarios. For example, if a child is permitted to eat only one ice cream per day, then whether to eat an ice cream in the morning affects whether she is permitted to eat one in the afternoon. This is closely related to conditional norms (e.g. conditional obligations) discussed in the literature [van Fraassen, 1973; Chellas, 1974; DeCew, 1981; Rulli, 2020] but is interpreted in multiagent transition systems instead of possible-world semantics. The other direction could be the interaction between permission and responsibility in multiagent settings. It might have been noticed that our introductory example about factories and fish is a variant of [Halpern, 2015, Example 3.11] and [Halpern, 2016, Example 6.2.5], which talk about causality and responsibility in multiagent settings. Indeed, the connection between obligation and responsibility in linguistic intuition has already been noticed by philosophers [van de Poel, 2011]. However, a formal investigation of the interaction among norm, causation, and responsibility in multiagent settings is still lacking.

Acknowledgements

I would like to express my sincere gratitude to Dr. Pavel Naumov, my PhD supervisor, for his selfless help in completing this paper. The research is funded by the China Scholarship Council (CSC No.202206070014).