# blameworthiness_in_strategic_games__749a710d.pdf

The Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19)

Blameworthiness in Strategic Games

Pavel Naumov Department of Mathematical Sciences Claremont Mc Kenna College Claremont, California 91711 pgn2@cornell.edu

Jia Tao Department of Computer Science Lafayette College Easton, Pennsylvania 18042 taoj@lafayette.edu

There are multiple notions of coalitional responsibility. The focus of this paper is on the blameworthiness defined through the principle of alternative possibilities: a coalition is blamable for a statement if the statement is true, but the coalition had a strategy to prevent it. The main technical result is a sound and complete bimodal logical system that describes properties of blameworthiness in one-shot games.

Introduction It was a little after 9am on Friday, July 20th 2018, when a four-year-old boy accidentally shot his two-year old cousin in the town of Muscoy in Southern California. The victim was taken to a hospital, where she died an hour later (Oreskes 2018). The police arrested Cesar Lopez, victim s grandfather, as a felon in possession of a firearm and for child endangerment (Juarez and Miracle 2018). The first charge against Lopez, a previously convicted felon, is based on California Penal Code 29800 (a) (1) that prohibits firearm access to any person who has been convicted of, or has an outstanding warrant for, a felony under the laws of the United States, the State of California, or any other state, government, or country... . We assume that Lopez knew that California state law bans him from owning a gun, but his actions guaranteed that he broke the law. The second charge is different because Lopez clearly never intended for his granddaughter to be killed. He never took any actions that would force her death. Nevertheless, he is blamed for not taking an action (locking the gun) to prevent the tragedy. Blameworthiness is tightly connected to the legal liability for negligence (Goudkamp 2004). We are interested in logical systems for reasoning about different forms of responsibility. Xu (1998) introduced a complete axiomatization of a modal logical system for reasoning about responsibility defined as taking actions that guarantee a certain outcome. In our example, by possessing a gun Lopez guaranteed that he was responsible for breaking California law. Broersen, Herzig, and Troquard (2009) extended Xu s work from individual responsibility to group responsibility. In this paper we propose a complete logical system for reasoning about another form of responsibility

Copyright c 2019, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

that we call blameworthiness: a coalition is blamable for an outcome ϕ if ϕ is true, but the coalition had a strategy to prevent ϕ. In our example, Lopez had a strategy to prevent the death by keeping the gun in a safe place.

Principle of Alternative Possibilities Throughout centuries, blameworthiness, especially in the context of free will and moral responsibility, has been at the focus of philosophical discussions (Singer and Eddon 2013). Modern works on this topic include (Fields 1994; Fischer and Ravizza 2000; Nichols and Knobe 2007; Mason 2015; Widerker 2017). Frankfurt (1969) acknowledges that a dominant role in these discussions has been played by what he calls a principle of alternate possibilities: a person is morally responsible for what he has done only if he could have done otherwise . As with many general principles, this one has many limitations that Frankfurt discusses; for example, when a person is coerced into doing something. Following the established tradition (Widerker 2017), we refer to this principle as the principle of alternative possibilities. Cushman (2015) talks about counterfactual possibility: a person could have prevented their harmful conduct, even though they did not. Halpern and Pearl proposed several versions of a formal definition of causality as a relation between sets of variables (Halpern 2016). This definition uses the counterfactual requirement which formalizes the principle of alternative possibilities. Halpern and Kleiman-Weiner (2018) used a similar setting to define degrees of blameworthiness. Batusov and Soutchanski (2018) gave a counterfactualbased definition of causality in situation calculus. (Alechina, Halpern, and Logan 2017) applied Halpern and Pearl definition of causality to team plans.

Coalitional Power in Strategic Games Pauly (2001; 2002) introduced logics of coalitional power that can be used to describe group abilities to achieve a certain result. His approach has been widely studied in the literature (Goranko 2001; van der Hoek and Wooldridge 2005; Borgo 2007; Sauro et al. 2006; Agotnes et al. 2010; Agotnes, van der Hoek, and Wooldridge 2009; Belardinelli 2014; Goranko, Jamroga, and Turrini 2013; Alechina et al. 2011; Galimullin and Alechina 2017; Goranko and Enqvist 2018). In this paper we use Marc Pauly s framework to define blameworthiness of coalitions of players in strategic (oneshot) games. We say that a coalition C could be blamed for

an outcome ϕ if ϕ is true, but the coalition C had a strategy to prevent ϕ. Thus, just like Halpern and Pearl s formal definition of causality, our definition of blameworthiness is based on the principle of alternative possibilities. However, because Marc Pauly s framework separates agents and outcomes, the proposed definition of blameworthiness is different and, arguably, more succinct. The main technical result of this paper is a sound and complete bimodal logical system describing the interplay between group blameworthiness modality and necessity (or universal truth) modality. Our system is significantly different from earlier mentioned axiomatizations (Xu 1998) and (Broersen, Herzig, and Troquard 2009) because our semantics incorporates the principle of alternative possibilities.

Paper Outline This paper is organized as follows. First, we introduce the formal syntax and semantics of our logical system. Next, we state and discuss its axioms. In the section that follows, we give examples of formal derivations in our system. In the next two sections we prove the soundness and the completeness. The last section concludes with a discussion of possible future work.

Syntax and Semantics In this paper we assume a fixed set A of agents and a fixed set of propositional variables Prop. By a coalition we mean an arbitrary subset of set A.

Definition 1 Φ is the minimal set of formulae such that

1. p Φ for each variable p Prop, 2. ϕ ψ, ϕ Φ for all formulae ϕ, ψ Φ, 3. Nϕ, BCϕ Φ for each coalition C A and each formula ϕ Φ.

Formula Nϕ is read as statement ϕ is true under each play and formula BCϕ as coalition C is blamable for ϕ . Boolean connectives , , and as well as constants and are defined in the standard way. By formula Nϕ we mean N ϕ. For the disjunction of multiple formulae, we assume that parentheses are nested to the left. That is, formula χ1 χ2 χ3 is a shorthand for (χ1 χ2) χ3. As usual, the empty disjunction is defined to be . For any two sets X and Y , by XY we denote the set of all functions from Y to X. The formal semantics of modalities N and B is defined in terms of models, which we call games.

Definition 2 A game is a tuple ( , Ω, P, π), where

1. is a nonempty set of actions , 2. Ωis a set of outcomes , 3. the set of plays P is an arbitrary set of pairs (δ, ω) such that δ A and ω Ω, 4. π is a function that maps Prop into subsets of P.

The example from the introduction can be captured in our setting by assuming that Lopez is the only actor who has two possible actions: hide and expose the gun in the game with two outcomes alive and dead. Although a complete action profile is a function from the set of all agents to

the domain of actions, in a single agent case any such profile can be described by specifying just the action of the single player. Thus, by complete action profile hide we mean action profile that maps agent Lopez into action hide. The set of possible plays of this game consists of pairs {(hide, alive), (expose, alive), (expose, dead)}. The above definition of a game is very close but not identical to the definition of a game frame in Pauly (2001; 2002) and the definition of a concurrent game structure, the semantics of ATL (Alur, Henzinger, and Kupferman 2002). Unlike these works, here we assume that the domain of choices is the same for all states and all agents. This difference is insignificant because all domains of choices in a game frame/concurrent game structure could be replaced with their union. More importantly, we assume that the mechanism is a relation, not a function. Our approach is more general, as it allows us to talk about blameworthiness in nondeterministic games, it also results in fewer axioms. Also, we do not assume that for any complete action profile δ there is at least one outcome ω such that (δ, ω) P. Thus, we allow the system to terminate under some action profiles without reaching an outcome. Without this assumption, we would need to add one extra axiom: BC and to make minor changes in the proof of the completeness. Finally, in this paper we assume that atomic propositions are interpreted as statements about plays, not just outcomes. For example, the meaning of an atomic proposition p could be statement either Lopez locked his gun or his granddaughter is dead . This is a more general approach than the one used in the existing literature, where atomic propositions are usually interpreted as statements about just outcomes. This difference is formally captured in the above definition through the assumption that value of π is a set of plays, not just a set of outcomes. As a result of this more general approach, all other statements in our logical system are also statements about plays, not outcomes. This is why relation in Definition 3 has a play (not an outcome) on the left. If s1 and s2 are action profiles of coalitions C1 and C2, respectively, and C is any coalition such that C C1 C2, then we write s1 =C s2 to denote that s1(a) = s2(a) for each agent a C. Next is the key definition of this paper. Its item 5 formally specifies blameworthiness using the principle of alternative possibilities.

Definition 3 For any play (δ, ω) P of a game ( , Ω, P, π) and any formula ϕ Φ, the satisfiability relation (δ, ω) ϕ is defined recursively as follows:

1. (δ, ω) p if (δ, ω) π(p), where p Prop, 2. (δ, ω) ϕ if (δ, ω) ϕ, 3. (δ, ω) ϕ ψ if (δ, ω) ϕ or (δ, ω) ψ, 4. (δ, ω) Nϕ if (δ , ω ) ϕ for each play (δ , ω ) P, 5. (δ, ω) BCϕ if (δ, ω) ϕ and there is s C such that for each play (δ , ω ) P, if s =C δ , then (δ , ω ) ϕ.

Note that in part 5 of the above definition we do not assume that coalition C is a minimal one that could have prevented the outcome. This is different from the definition of

blameworthiness in (Halpern 2017). Our approach is consistent with how word blame is often used in English. For example, the sentence Millennials being blamed for decline of American cheese (Gant 2018) does not imply that no one in the millennial generation likes American cheese.

Axioms In addition to the propositional tautologies in language Φ, our logical system contains the following axioms.

1. Truth: Nϕ ϕ and BCϕ ϕ, 2. Distributivity: N(ϕ ψ) (Nϕ Nψ), 3. Negative Introspection: Nϕ N Nϕ, 4. None to Blame: B ϕ, 5. Joint Responsibility: if C D = , then

NBCϕ NBDψ (ϕ ψ BC D(ϕ ψ)), 6. Blame for Cause: N(ϕ ψ) (BCψ (ϕ BCϕ)), 7. Monotonicity: BCϕ BDϕ, where C D, 8. Fairness: BCϕ N(ϕ BCϕ).

We write ϕ if formula ϕ is provable from the axioms of our system using the Modus Ponens and the Necessitation inference rules: ϕ, ϕ ψ

We write X ϕ if formula ϕ is provable from the theorems of our logical system and an additional set of axioms X using only the Modus Ponens inference rule. The Truth axiom for modality N, the Distributivity axiom, and the Negative Introspection axiom together with the Necessitation inference rule capture the fact that modality N, per Definition 3, is an S5 modality and thus satisfies all standard S5 properties. The Truth axiom for modality B states that any coalition can be blamed only for a statement which is true. The None to Blame axiom states that the empty coalition cannot be blamed for anything. Intuitively, this axiom is true because the empty coalition has no power to prevent anything. The Joint Responsibility axiom states that if disjoint coalitions C and D can be blamed for statements ϕ and ψ, respectively, on some other (possibly two different) plays of the game and the disjunction ϕ ψ is true on the current play, then the union of the two coalitions can be blamed for this disjunction on the current play. This axiom remotely resembles Xu (1998) axiom for the independence of individual agents, which in our notations can be stated as

NBa1ϕ1 NBanϕn N(Ba1ϕ1 Banϕn).

Broersen, Herzig, and Troquard (2009) captured the independence of disjoint coalitions C and D in their Lemma 17:

NBCϕ NBDψ N(BCϕ BDψ).

In spite of these similarities, the definition of responsibility used in (Xu 1998) and (Broersen, Herzig, and Troquard 2009) does not assume the principle of alternative possibilities. The Joint Responsibility axiom is also similar to Marc

Pauly (2001; 2002) Cooperation axiom for logic of coalitional power:

SCϕ SDψ SC D(ϕ ψ),

where coalitions C and D are disjoint and SCϕ stands for coalition C has a strategy to achieve ϕ . The Blame for Cause axiom states that if formula ϕ universally implies ψ (informally, ϕ is a cause of ψ), then any coalition blamable for ψ should also be blamable for the cause ϕ as long as ϕ is actually true. The Monotonicity axiom states that any coalition is blamed for anything that a subcoalition is blamed for. Finally, the Fairness axiom states that if a coalition C is blamed for ϕ, then it should be blamed for ϕ whenever ϕ is true.

Examples of Derivations The soundness of the axioms of our logical system is established in the next section. In this section we give several examples of formal proofs in our system. Together with the Truth axiom, the first example shows that statements BCBCϕ and BCϕ are equivalent in our system. That is, coalition C can be blamed for being blamed for ϕ if and only if it can be blamed for ϕ. Lemma 1 BCϕ BCBCϕ. PROOF. Note that BCϕ ϕ by the Truth axiom. Thus, N(BCϕ ϕ) by the Necessitation rule. At the same time,

N(BCϕ ϕ) (BCϕ (BCϕ BCBCϕ))

is an instance of the Blame for Cause axiom. Then, BCϕ (BCϕ BCBCϕ) by the Modus Ponens inference rule. Therefore, BCϕ BCBCϕ by the propositional reasoning.

The rest of the examples in this section are used later in the proof of the completeness.

Lemma 2 NBCϕ (ϕ BCϕ). PROOF. Note that BCϕ N(ϕ BCϕ) by the Fairness axiom. Hence, N(ϕ BCϕ) BCϕ, by the law of contrapositive. Thus, N( N(ϕ BCϕ) BCϕ) by the Necessitation inference rule. Hence, by the Distributivity axiom and the Modus Ponens inference rule,

N N(ϕ BCϕ) N BCϕ.

At the same time, by the Negative Introspection axiom:

N(ϕ BCϕ) N N(ϕ BCϕ).

Thus, by the laws of propositional reasoning,

N(ϕ BCϕ) N BCϕ.

Hence, by the law of contrapositive,

N BCϕ N(ϕ BCϕ).

Note that N(ϕ BCϕ) (ϕ BCϕ) is an instance of the Truth axiom. Thus, by propositional reasoning,

N BCϕ (ϕ BCϕ).

Hence, NBCϕ (ϕ BCϕ) by the definition of N.

Lemma 3 If ϕ ψ, then BCϕ BCψ.

PROOF. By the Blame for Cause axiom,

N(ψ ϕ) (BCϕ (ψ BCψ)).

Assumption ϕ ψ implies ψ ϕ by the laws of propositional reasoning. Thus, N(ψ ϕ) by the Necessitation inference rule. Hence, by the Modus Ponens rule,

BCϕ (ψ BCψ).

Thus, by the laws of propositional reasoning,

(BCϕ ψ) (BCϕ BCψ). (1)

Note that BCϕ ϕ by the Truth axiom. At the same time, ϕ ψ by the assumption of the lemma. Thus, by the laws of propositional reasoning, BCϕ ψ. Therefore, BCϕ BCψ by the Modus Ponens inference rule from statement (1).

Lemma 4 ϕ Nϕ.

PROOF. By the Truth axioms, N ϕ ϕ. Thus, by the law of contrapositive, ϕ N ϕ. Hence, ϕ Nϕ by the definition of the modality N. Therefore, ϕ Nϕ by the Modus Ponens inference rule.

The next lemma generalizes the Joint Responsibility axiom from two coalitions to multiple coalitions. Lemma 5 For any integer n 0 and any pairwise disjoint sets D1, . . . , Dn,

{NBDiχi}n i=1, χ1 χn BD1 Dn(χ1 χn).

PROOF. We prove the lemma by induction on n. If n = 0, then disjunction χ1 χn is Boolean constant false by definition. Thus, the statement of the lemma is B , which is provable in the propositional logic due to the assumption on the left-hand side of . Next, suppose that n = 1. Then, from Lemma 2 it follows that NBD1χ1, χ1 BD1χ1. Suppose that n 2. By the Joint Responsibility axiom and the Modus Ponens inference rule,

NBD1 Dn 1(χ1 χn 1), NBDnχn, χ1 χn 1 χn BD1 Dn 1 Dn(χ1 χn 1 χn).

Thus, by Lemma 4,

BD1 Dn 1(χ1 χn 1), NBDnχn, χ1 χn 1 χn BD1 Dn 1 Dn(χ1 χn 1 χn).

At the same time, by the induction hypothesis,

{NBDiχi}n 1 i=1 , χ1 χn 1 BD1 Dn 1(χ1 χn 1).

{NBDiχi}n i=1, χ1 χn 1, χ1 χn 1 χn BD1 Dn 1 Dn(χ1 χn 1 χn).

Since χ1 χn 1 χ1 χn 1 χn is provable in propositional logic,

{NBDiχi}n i=1, χ1 χn 1 BD1 Dn 1 Dn(χ1 χn 1 χn). (2)

Similarly, by the Joint Responsibility axiom and the Modus Ponens inference rule,

NBD1χ1, NBD2 Dn(χ2 χn), χ1 (χ2 χn) BD1 Dn 1 Dn(χ1 (χ2 χn)).

Since formula χ1 (χ2 χn) χ1 χ2 χn is provable in the propositional logic, by Lemma 3,

NBD1χ1, NBD2 Dn(χ2 χn), χ1 χ2 χn BD1 Dn 1 Dn(χ1 χ2 χn).

Thus, by Lemma 4,

NBD1χ1, BD2 Dn(χ2 χn), χ1 χ2 χn BD1 Dn 1 Dn(χ1 χ2 χn).

At the same time, by the induction hypothesis,

{NBDiχi}n i=2, χ2 χn BD2 Dn(χ2 χn).

{NBDiχi}n i=1, χ2 χn, χ1 χ2 χn BD1 D2 Dn(χ1 χ2 χn).

Since χ2 χn χ1 χn 1 χn is provable in propositional logic,

{NBDiχi}n i=1, χ2 χn BD1 Dn 1 Dn(χ1 χ2 χn). (3)

Finally, note that the following statement is provable in the propositional logic for n 2,

χ1 χn (χ1 χn 1) (χ2 χn).

Therefore, from statement (2) and statement (3),

{NBDiχi}n i=1, χ1 χn BD1 Dn(χ1 χn)

by the laws of propositional reasoning.

Note that modality N satisfies all axioms of S5. The following two lemmas state well-known property of S5. Their proofs can be found, for example, in (Naumov and Tao 2018a).

Lemma 6 If ϕ1, . . . , ϕn ψ, then Nϕ1, . . . , Nϕn Nψ.

Lemma 7 Nϕ NNϕ.

Lemma 8 For any integer n 0 and any disjoint sets D1, . . . , Dn C,

{NBDiχi}n i=1, N(ϕ χ1 χn) N(ϕ BCϕ).

PROOF. By Lemma 5,

{NBDiχi}n i=1, χ1 χn BD1 Dn(χ1 χn).

Thus, by the Monotonicity axiom,

{NBDiχi}n i=1, χ1 χn BC(χ1 χn).

Hence, by the Modus Ponens inference rule

{NBDiχi}n i=1, ϕ, ϕ χ1 χn BC(χ1 χn).

By the Truth axiom and the Modus Ponens inference rule,

{NBDiχi}n i=1, ϕ, N(ϕ χ1 χn) BC(χ1 χn).

Note that N(ϕ χ1 χn) (BC(χ1 χn) (ϕ BCϕ)) is an instance of the Blame for Cause axiom. Thus, by the Modus Ponens inference rule applied twice,

{NBDiχi}n i=1, ϕ, N(ϕ χ1 χn) ϕ BCϕ.

By the Modus Ponens inference rule,

{NBDiχi}n i=1, ϕ, N(ϕ χ1 χn) BCϕ.

By the deduction lemma,

{NBDiχi}n i=1, N(ϕ χ1 χn) ϕ BCϕ.

By Lemma 6,

{NNBDiχi}n i=1, NN(ϕ χ1 χn) N(ϕ BCϕ).

By the definition of modality N, the Negative Introspection axiom, and the Modus Ponens inference rule,

{NBDiχi}n i=1, NN(ϕ χ1 χn) N(ϕ BCϕ)

Therefore, by Lemma 7 and the Modus Ponens inference rule, the statement of the lemma follows.

Soundness In the following lemmas, (δ, ω) P is a play of an arbitrary game ( , Ω, P, π) and ϕ, ψ Φ are arbitrary formulae.

Lemma 9 (δ, ω) B ϕ.

PROOF. Suppose that (δ, ω) B ϕ. Thus, by Definition 3, we have (δ, ω) ϕ and there is an action profile s such that for each play (δ , ω ) P, if s = δ , then (δ , ω ) ϕ. Consider δ = δ and ω = ω. Note that s = δ is vacuously true. Hence, (δ , ω ) ϕ. In other words, (δ, ω) ϕ, which leads to a contradiction.

Lemma 10 For all sets C, D A such that C D = , if (δ, ω) NBCϕ, (δ, ω) NBDψ, and (δ, ω) ϕ ψ, then (δ, ω) BC D(ϕ ψ).

PROOF. Let (δ, ω) NBCϕ and (δ, ω) NBDψ. Thus, by Definition 3 and the definition of modality N, there are plays (δ1, ω1) P and (δ2, ω2) P such that (δ1, ω1) BCϕ and (δ2, ω2) BDψ.

By Definition 3, statement (δ1, ω1) BCϕ implies that there is s1 C such that for each play (δ , ω ) P, if s1 =C δ , then (δ , ω ) ϕ. Similarly, by Definition 3, statement (δ2, ω2) BDψ implies that there is s2 D such that for each play (δ , ω ) P, if s2 =D δ , then (δ , ω ) ψ. Consider an action profile s of coalition C D such that

s(a) = s1(a), if a C, s2(a), if a D.

Note that the action profile s is well-defined because sets C and D are disjoint by the assumption of the lemma. The choice of action profiles s1, s2, and s implies that for each play (δ , ω ) P, if s =C D δ , then (δ , ω ) ϕ and (δ , ω ) ψ. Thus, for each play (δ , ω ) P, if s =C D δ , then (δ , ω ) ϕ ψ. Therefore, (δ, ω) BC D(ϕ ψ) by Definition 3 and due to the assumption (δ, ω) ϕ ψ of the lemma.

Lemma 11 If (δ, ω) N(ϕ ψ), (δ, ω) BCψ, and (δ, ω) ϕ, then (δ, ω) BCϕ.

PROOF. By Definition 3, assumption (δ, ω) BCψ implies that there is s C such that for each play (δ , ω ) P, if s =C δ , then (δ , ω ) ψ. At the same time, (δ , ω ) ϕ ψ for each play (δ , ω ) P by the assumption (δ, ω) N(ϕ ψ) of the lemma and Definition 3. Thus, (δ , ω ) ϕ for each play (δ , ω ) P such that s =C δ by Definition 3. Hence, (δ, ω) BCϕ by Definition 3 and the assumption (δ, ω) ϕ of the lemma.

Lemma 12 For all sets C, D A such that C D, if (δ, ω) BCϕ, then (δ, ω) BDϕ.

PROOF. By Definition 3, assumption (δ, ω) BCϕ implies that (δ, ω) ϕ and there is s C such that for each play (δ , ω ) P, if s =C δ , then (δ , ω ) ϕ. By Definition 2, set is not empty. Let d0 . Consider an action profile s of coalition D such that

s (a) = s(a), if a C, d0, if a D \ C.

Then, by the choice of action profile s and because C D, for each play (δ , ω ) P, if s =D δ , then (δ , ω ) ϕ. Therefore, (δ, ω) BDϕ by Definition 3 and because (δ, ω) ϕ, as we have shown earlier.

Lemma 13 If (δ, ω) BCϕ, then (δ, ω) N(ϕ BCϕ).

PROOF. Consider any play (δ , ω ) P. By Definition 3, it suffices to show that if (δ , ω ) ϕ, then (δ , ω ) BCϕ. Thus, again by Definition 3, it suffices to prove there is s C such that for each play (δ , ω ) P, if s =C δ , then (δ , ω ) ϕ. The last statement follows from the assumption (δ, ω) BCϕ and Definition 3.

Completeness We start the proof of the completeness by defining the canonical game G(ω0) = ( , Ω, P, π) for each maximal consistent set of formulae ω0.

Definition 4 The set of outcomes Ωis the set of all maximal consistent sets of formulae ω such that for each formula ϕ Φ if Nϕ ω0, then ϕ ω.

Informally, an action of an agent in the canonical game is designed to veto a formula. The domain of choices of the canonical model consists of all formulae in set Φ. To veto a formula ψ, an agent must choose action ψ. The mechanism of the canonical game guarantees that if NBCψ ω0 and all agents in the coalition C veto formula ψ, then ψ is satisfied in the outcome.

Definition 5 The domain of actions is set Φ.

Definition 6 The set P A Ωconsists of all pairs (δ, ω) such that for any formula NBCψ ω0, if δ(a) = ψ for each agent a C, then ψ ω.

Definition 7 π(p) = {(δ, ω) P | p ω}.

This concludes the definition of the canonical game G(ω0). The next four lemmas are auxiliary results leading to the proof of the completeness in Theorem 1.

Lemma 14 For any play (δ, ω) P, any action profile s C, and any formula (ϕ BCϕ) ω, there is a play (δ , ω ) P such that s =C δ and ϕ ω .

PROOF. Consider the following set of formulae:

X = {ϕ} {ψ | Nψ ω0}

{ χ | NBDχ ω0, D C, a D(s(a) = χ)}.

Claim 1 Set X is consistent.

PROOF OF CLAIM. Suppose the opposite. Thus, there are

formulae Nψ1, . . . , Nψm ω0, (4) and formulae NBD1χ1, . . . , NBDnχn ω0, (5) such that D1, . . . , Dn C, (6) s(a) = χi for all a Di, i n, (7) and ψ1, . . . , ψm, χ1, . . . , χn ϕ. (8)

Without loss of generality, we can assume that formulae χ1, . . . , χn are distinct. Thus, assumption (7) implies that sets D1, . . . , Dn are pairwise disjoint. By propositional reasoning, assumption (8) implies that

ψ1, . . . , ψm ϕ χ1 χn.

Thus, Nψ1, . . . , Nψm N(ϕ χ1 χn), by Lemma 6. Hence, ω0 N(ϕ χ1 χn), by assumption (4), Thus, by Lemma 8, using assumptions (5) and the fact that sets D1, . . . , Dn are pairwise disjoint, ω0 N(ϕ BCϕ). Hence N(ϕ BCϕ) ω0 because set ω0 is maximal. Then, ϕ BCϕ ω by Definition 4, which contradicts the assumption (ϕ BCϕ) ω of the lemma because set ω is consistent. Therefore, set X is consistent.

Let ω be any maximal consistent extension of set X. Thus, ϕ X ω by the choice of sets X and ω . Also, ω Ωby Definition 4 and the choice of sets X and ω . Let the complete action profile δ be defined as follows:

δ (a) = s(a), if a C, , otherwise. (9)

Then, s =C δ .

Claim 2 (δ , ω ) P.

PROOF OF CLAIM. Consider any formula NBDχ ω0 such that δ (a) = χ for each a D. By Definition 6, it suffices to show that χ ω . Case I: D C. Thus, χ X by the definition of set X. Therefore, χ ω by the choice of set ω . Case II: D C. Consider any d0 D \ C. Thus, δ (d0) = by equation (9). Also, δ (d0) = χ because d0 D. Thus, χ and formula χ is a tautology. Hence, χ ω by the maximality of set ω .

This concludes the proof of the lemma.

Lemma 15 For any outcome ω Ω, there is a complete action profile δ A such that (δ, ω) P.

PROOF. Define a complete action profile δ such that δ(a) = for each agent a A. To prove (δ, ω) P, consider any formula NBDχ ω0 such that δ(a) = χ for each a D. By Definition 6, it suffices to show that χ ω. Case I: D = . Thus, BDχ by the None to Blame axiom. Hence, N BDχ by the Necessitation inference rule. Then, N BDχ / ω0 by the consistency of the set ω0. Therefore, NBDχ / ω0 by the definition of the modality N, which contradicts the choice of formula NBDχ. Case II: D = . Thus, there is at least one agent d0 D. Hence, χ = δ(d0) = by the definition of the complete action profile δ. Then, χ is a tautology. Thus, χ ω by the maximality of set ω.

Lemma 16 For any play (δ, ω) P and any formula Nϕ ω, there is a play (δ , ω ) P such that ϕ ω .

PROOF. Consider the set X = { ϕ} {ψ | Nψ ω0}. First, we show that set X is consistent. Suppose the opposite. Thus, there are formulae Nψ1, . . . , Nψn ω0 such that ψ1, . . . , ψn ϕ. Hence, Nψ1, . . . , Nψn Nϕ by Lemma 6. Thus, ω0 Nϕ because Nψ1, . . . , Nψn ω0. Hence, ω0 NNϕ by Lemma 7. Therefore, Nϕ ω by assumption ω Ωand Definition 4. Hence, Nϕ / ω by the consistency of set ω, which contradicts the assumption of the lemma. Thus, set X is consistent. Let ω be any maximal consistent extension of set X. Note that ϕ X ω by the definition of set X. By Lemma 15, there is a complete action profile δ such that (δ , ω ) P.

Lemma 17 (δ, ω) ϕ iff ϕ ω for each play (δ, ω) P and each formula ϕ Φ.

PROOF. We prove the lemma by structural induction on formula ϕ. If ϕ is a propositional variable, then the required follows from Definition 3 and Definition 7. The cases when ϕ is an implication or a negation follow from the maximality and the consistency of set ω in the standard way. Suppose that formula ϕ has the form Nψ. ( ) : Let Nψ / ω. Thus, Nψ ω by the maximality of set ω. Hence, by Lemma 16, there is a play (δ , ω ) P such that ψ ω . Then, ψ / ω by the consistency of set ω . Thus, (δ , ω ) ψ by the induction hypothesis. Therefore, (δ, ω) Nψ by Definition 3. ( ) : Let Nψ ω. Thus, Nψ / ω by the consistency of set ω. Hence, N Nψ / ω0 by Definition 4. Then, ω0 N Nψ by the maximality of set ω0. Thus, ω0 Nψ by the Negative Introspection axiom. Hence, Nψ ω0 by the maximality of set ω0. Then, ψ ω for each ω Ωby Definition 4. Thus, by the induction hypothesis, (δ , ω ) ψ for each (δ , ω ) P. Therefore, (δ, ω) Nψ by Definition 3. Suppose that formula ϕ has the form BCψ. ( ) : Assume that BCψ / ω. First, we consider the case when ψ / ω. Then, (δ, ω) ψ by the induction hypothesis. Hence, (δ, ω) BCψ by Definition 3. Next, assume that ψ ω. Note that ψ BCψ / ω. Indeed, if ψ BCψ ω, then ω BCψ by the Modus Ponens inference rule. Thus, BCψ ω by the maximality of set ω, which contradicts the assumption above. Because ω is a maximal set, statement ψ BCψ / ω implies that (ψ BCψ) ω. Thus, by Lemma 14, for any action profile s C, there is a play (δ , ω ) such that s =C δ ψ ω . Hence, by the induction hypothesis, for any action profile s C there is a play (δ , ω ) such that (δ , ω ) ψ. Therefore, (δ, ω) BCψ by Definition 3. ( ) : Suppose that BCψ ω. Thus, ω ψ by the Truth axiom. Hence, ψ ω by the maximality of the set ω. Thus, (δ, ω) ψ by the induction hypothesis. Next, define an action profile s C to be such that s(a) = ψ for each a C. Consider any play (δ , ω ) P such that s =C δ . By Definition 3, it suffices to show that (δ , ω ) ψ. Statement BCψ ω implies that BCψ / ω because set ω is consistent. Thus, N BCψ / ω0 by Definition 4 and because ω Ω. Hence, N BCψ ω0 due to the maximality of the set ω0. Thus, NBCψ ω0 by the definition of modality N. Also, δ (a) = s(a) = ψ for each a C. Hence, ψ ω by Definition 6 and the assumption (δ , ω ) P. Then, ψ / ω by the consistency of set ω . Therefore, (δ , ω ) ψ by the induction hypothesis.

We are now ready to state and prove the strong completeness of our logical system.

Theorem 1 If X ϕ, then there is a game, a complete action profile δ, and an outcome ω of this game such that (δ, ω) χ for each χ X and (δ, ω) ϕ.

PROOF. Suppose that X ϕ. Thus, set X { ϕ} is consistent. Let ω0 be any maximal consistent extension of set X { ϕ} and G(ω0) = ( , Ω, P, π) be the canonical game defined above. Note that ω0 Ωby Definition 4 and the Truth axiom.

By Lemma 15, there exists a complete action profile δ A such that (δ, ω0) P. Thus, (δ, ω0) χ for each χ X and (δ, ω0) ϕ by Lemma 17 and the choice of set ω0. Therefore, (δ, ω0) ϕ by Definition 3.

In this paper we defined a formal semantics of blameworthiness using the principle of alternative possibilities and Marc Pauly s framework for logics of coalitional power. Our main technical result is a sound and complete bimodal logical system that captures properties of blameworthiness in this setting. This work is meant to be a step towards formal reasoning about blameworthiness and responsibility. Recently, there have been several works combining Marc Pauly s and epistemic logic frameworks to study the interplay between knowledge and know-how strategies ( Agotnes and Alechina 2012; 2016; Naumov and Tao 2017; 2018b; 2018c; 2018a) as well as a study of such strategies in a single-agent case (Fervari et al. 2017). Knowledge is clearly relevant to the study of blameworthiness. Indeed, one can hardly be blamed for not preventing an outcome if one had a strategy to prevent it but did not know what this strategy was. Furthermore, in the legal domain, responsibility is connected to knowledge. For example, US Model Penal Code specifies five types of responsibility based on what the responsible party knew or should have known (Institute 1985 Print). In the future, we plan to explore the interplay between knowledge and blameworthiness/responsibility by introducing epistemic component to the framework of this paper.

References Agotnes, T., and Alechina, N. 2012. Epistemic coalition logic: completeness and complexity. In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems-Volume 2 (AAMAS), 1099 1106.

Agotnes, T., and Alechina, N. 2016. Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation. exv085.

Agotnes, T.; Balbiani, P.; van Ditmarsch, H.; and Seban, P. 2010. Group announcement logic. Journal of Applied Logic 8(1):62 81.

Agotnes, T.; van der Hoek, W.; and Wooldridge, M. 2009. Reasoning about coalitional games. Artificial Intelligence 173(1):45 79. Alechina, N.; Logan, B.; Nguyen, H. N.; and Rakib, A. 2011. Logic for coalitions with bounded resources. Journal of Logic and Computation 21(6):907 937. Alechina, N.; Halpern, J. Y.; and Logan, B. 2017. Causality, responsibility and blame in team plans. In Proceedings of the 16th Conference on Autonomous Agents and Multi Agent Systems, 1091 1099. International Foundation for Autonomous Agents and Multiagent Systems. Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time temporal logic. Journal of the ACM 49(5):672 713.

Batusov, V., and Soutchanski, M. 2018. Situation calculus semantics for actual causality. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI-18). Belardinelli, F. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In Proceedings 2nd International Workshop on Strategic Reasoning, Grenoble, France, April 5-6, 2014, volume 146 of EPTCS, 27 33. Borgo, S. 2007. Coalitions in action logic. In 20th International Joint Conference on Artificial Intelligence, 1822 1827. Broersen, J.; Herzig, A.; and Troquard, N. 2009. What groups do, can do, and know they can do: an analysis in normal modal logics. Journal of Applied Non-Classical Logics 19(3):261 289. Cushman, F. 2015. Deconstructing intent to reconstruct morality. Current Opinion in Psychology 6:97 103. Fervari, R.; Herzig, A.; Li, Y.; and Wang, Y. 2017. Strategically knowing how. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, 1031 1038. Fields, L. 1994. Moral beliefs and blameworthiness: Introduction. Philosophy 69(270):397 415. Fischer, J. M., and Ravizza, M. 2000. Responsibility and control: A theory of moral responsibility. Cambridge University Press. Frankfurt, H. G. 1969. Alternate possibilities and moral responsibility. The Journal of Philosophy 66(23):829 839. Galimullin, R., and Alechina, N. 2017. Coalition and group announcement logic. In Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2017, Liverpool, UK, 24-26 July 2017, 207 220. Gant, M. 2018. Millennials being blamed for decline of American cheese. Fox News. www.foxnews.com/fooddrink/millennials-kraft-american-cheese-sales-decline.amp. Goranko, V., and Enqvist, S. 2018. Socially friendly and group protecting coalition logics. In Proceedings of the 17th International Conference on Autonomous Agents and Multi Agent Systems, 372 380. International Foundation for Autonomous Agents and Multiagent Systems. Goranko, V.; Jamroga, W.; and Turrini, P. 2013. Strategic games and truly playable effectivity functions. Autonomous Agents and Multi-Agent Systems 26(2):288 314. Goranko, V. 2001. Coalition games and alternating temporal logics. In Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge, 259 272. Morgan Kaufmann Publishers Inc. Goudkamp, J. 2004. The spurious relationship between moral blameworthiness and liability for negligence. Melb. UL Rev. 28:343. Halpern, J. Y., and Kleiman-Weiner, M. 2018. Towards formal definitions of blameworthiness, intention, and moral responsibility. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18). Halpern, J. Y. 2016. Actual causality. MIT Press.

Halpern, J. Y. 2017. Reasoning about uncertainty. MIT press. Institute, A. L. 1985 Print. Model Penal Code: Official Draft and Explanatory Notes. Complete Text of Model Penal Code as Adopted at the 1962 Annual Meeting of the American Law Institute at Washington, D.C., May 24, 1962. The Institute. Juarez, L., and Miracle, V. 2018. Toddler dies in Muscoy shooting after 4-year-old cousin gets hold of gun; grandfather arrested. KABC. http://abc7.com/4-year-old-shootskills-toddler-cousin-in-ie;-grandpa-arrested/3794943/. Mason, E. 2015. Moral ignorance and blameworthiness. Philosophical Studies 172(11):3037 3057. Naumov, P., and Tao, J. 2017. Coalition power in epistemic transition systems. In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 723 731. Naumov, P., and Tao, J. 2018a. Second-order know-how strategies. In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 390 398. Naumov, P., and Tao, J. 2018b. Strategic coalitions with perfect recall. In Proceedings of Thirty-Second AAAI Conference on Artificial Intelligence. Naumov, P., and Tao, J. 2018c. Together we know how to achieve: An epistemic logic of know-how. Artificial Intelligence 262:279 300. Nichols, S., and Knobe, J. 2007. Moral responsibility and determinism: The cognitive science of folk intuitions. Nous 41(4):663 685. Oreskes, B. 2018. 4-year-old accidentally shoots and kills toddler cousin in San Bernardino County. Los Angeles Times. http://www.latimes.com/local/lanow/la-me-lnmuscoy-toddler-shooting-20180720-story.html. Pauly, M. 2001. Logic for Social Software. Ph.D. Dissertation, Institute for Logic, Language, and Computation. Pauly, M. 2002. A modal logic for coalitional power in games. Journal of Logic and Computation 12(1):149 166. Sauro, L.; Gerbrandy, J.; van der Hoek, W.; and Wooldridge, M. 2006. Reasoning about action and cooperation. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 06, 185 192. New York, NY, USA: ACM. Singer, P., and Eddon, M. 2013. Moral responsibility, problem of. Encyclopædia Britannica. https://www.britannica.com/topic/problem-of-moralresponsibility. van der Hoek, W., and Wooldridge, M. 2005. On the logic of cooperation and propositional control. Artificial Intelligence 164(1):81 119. Widerker, D. 2017. Moral responsibility and alternative possibilities: Essays on the importance of alternative possibilities. Routledge. Xu, M. 1998. Axioms for deliberative stit. Journal of Philosophical Logic 27(5):505 552.