Introduction
It was a little after 9am on Friday, July 20th 2018, when a fouryearold boy accidentally shot his twoyear old cousin in the town of Muscoy in Southern California. The victim was taken to a hospital, where she died an hour later [Oreskes2018]. The police arrested Cesar Lopez, victim’s grandfather, as a felon in possession of a firearm and for child endangerment [Juarez and Miracle2018].
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 [Goudkamp2004].
We are interested in logical systems for reasoning about different forms of responsibility. Xu (x98jpl) 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 braking California law. Broersen, Herzig, and Troquard (bht09jancl) 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 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 Eddon2013]. Modern works on this topic include [Fields1994, Fischer and Ravizza2000, Nichols and Knobe2007, Mason2015, Widerker2017]. Frankfurt (f69tjop) 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 [Widerker2017], we refer to this principle as the principle of alternative possibilities. Cushman (c15cop) 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 [Halpern2016]. This definition uses the counterfactual requirement which formalizes the principle of alternative possibilities. Halpern and KleimanWeiner (hk18aaai) used a similar setting to define degrees of blameworthiness. Batusov and Soutchanski (bs18aaai) gave a counterfactualbased definition of causality in situation calculus.
Coalitional Power in Strategic Games
Pauly (p01illc,p02) 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 [Goranko2001, van der Hoek and Wooldridge2005, Borgo2007, Sauro et al.2006, Ågotnes et al.2010, Ågotnes, van der Hoek, and Wooldridge2009, Belardinelli2014, Goranko, Jamroga, and Turrini2013, Alechina et al.2011, Galimullin and Alechina2017, Goranko and Enqvist2018].
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 could be blamed for an outcome if is true, but the coalition 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 [Xu1998] and [Broersen, Herzig, and Troquard2009] 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 of agents and a fixed set of propositional variables . By a coalition we mean an arbitrary subset of set .
Definition 1
is the minimal set of formulae such that

for each variable ,

for all formulae ,

, for each coalition and each formula .
In other words, language is defined by grammar:
Formula is read as “statement is true under each play” and formula as “coalition is blamable for ”.
Boolean connectives , , and as well as constants and are defined in the standard way. By formula we mean . For the disjunction of multiple formulae, we assume that parentheses are nested to the left. That is, formula is a shorthand for . As usual, the empty disjunction is defined to be . For any two sets and , by we denote the set of all functions from to .
The formal semantics of modalities and is defined in terms of models, which we call games.
Definition 2
A game is a tuple , where

is a nonempty set of “actions”,

is a set of “outcomes”,

the set of “plays” is an arbitrary set of pairs such that and ,

is a function that maps into subsets of .
The example from the introduction can be captured in our setting by assuming that Lopez is the only actor who has two possible actions: and the gun in the game with two outcomes and . 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 we mean action profile that maps agent Lopez into action . The set of possible plays of this game consists of pairs .
The above definition of a game is very close but not identical to the definition of a game frame in Pauly (p01illc,p02) and the definition of a concurrent game structure, the semantics of ATL [Alur, Henzinger, and Kupferman2002]. 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 . 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: 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 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 and are action profiles of coalitions and , respectively, and is any coalition such that , then we write to denote that for each agent .
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 of a game and any formula , the satisfiability relation is defined recursively as follows:

if , where ,

if ,

if or ,

if for each play ,

if and there is such that for each play , if , then .
Axioms
In addition to the propositional tautologies in language , our logical system contains the following axioms.

Truth: and ,

Distributivity: ,

Negative Introspection: ,

None to Blame: ,

Joint Responsibility: if , then
, 
Blame for Cause: ,

Monotonicity: , where ,

Fairness: .
We write if formula is provable from the axioms of our system using the Modus Ponens and the Necessitation inference rules:
We write if formula is provable from the theorems of our logical system and an additional set of axioms using only the Modus Ponens inference rule.
The Truth axiom for modality , the Distributivity axiom, and the Negative Introspection axiom together with the Necessitation inference rule capture the fact that modality , per Definition 3, is an S5 modality and thus satisfies all standard S5 properties.
The Truth axiom for modality 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 and 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 (x98jpl) axiom for independence of individual agents, which in our notations can be stated as
Broersen, Herzig, and Troquard (bht09jancl) captured the independence of disjoint coalitions and in their Lemma 17:
In spite of these similarities, the definition of responsibility used in [Xu1998] and [Broersen, Herzig, and Troquard2009] does not assume the principle of alternative possibilities. The Joint Responsibility axiom is also similar to Marc Pauly (p01illc,p02) Cooperation axiom for logic of coalitional power:
where coalitions and are disjoint and stands for “coalition 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 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 and are equivalent in our system. That is, coalition can be blamed for being blamed for if and only if it can be blamed for .
Lemma 1
.
Proof. Note that by the Truth axiom. Thus, by the Necessitation rule. At the same time,
is an instance of the Blame for Cause axiom. Then, by the Modus Ponens inference rule. Therefore, by the propositional reasoning.
The rest of the examples in this section are used later in the proof of the completeness.
Lemma 2
.
Proof. Note that by the Fairness axiom. Hence, , by the law of contrapositive. Thus, by the Necessitation inference rule. Hence, by the Distributivity axiom and the Modus Ponens inference rule,
At the same time, by the Negative Introspection axiom:
Thus, by the laws of propositional reasoning,
Hence, by the law of contrapositive,
Note that is an instance of the Truth axiom. Thus, by propositional reasoning,
Hence, by the definition of .
Lemma 3
If , then .
Proof. By the Blame for Cause axiom,
Assumption implies by the laws of propositional reasoning. Thus, by the Necessitation inference rule. Hence, by the Modus Ponens rule,
Thus, by the laws of propositional reasoning,
(1) 
Note that by the Truth axiom. At the same time, by the assumption of the lemma. Thus, by the laws of propositional reasoning, . Therefore, by the Modus Ponens inference rule from statement (1).
Lemma 4
.
Proof. By the Truth axioms, . Thus, by the law of contrapositive, . Hence, by the definition of the modality . Therefore, 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 and any pairwise disjoint sets ,
Proof. We prove the lemma by induction on . If , then disjunction is Boolean constant false by definition. Thus, the statement of the lemma is , which is provable in the propositional logic due to the assumption on the lefthand side of .
Next, suppose that . Then, from Lemma 2 it follows that .
Suppose that . By the Joint Responsibility axiom and the Modus Ponens inference rule,
Thus, by Lemma 4,
At the same time, by the induction hypothesis,
Hence,
Since is provable in propositional logic,
(2) 
Similarly, by the Joint Responsibility axiom and the Modus Ponens inference rule,
Since formula is provable in the propositional logic, by Lemma 3,
Thus, by Lemma 4,
At the same time, by the induction hypothesis,
Hence,
Since is provable in propositional logic,
(3) 
Finally, note that the following statement is provable in the propositional logic for ,
Therefore, from statement (2) and statement (3),
by the laws of propositional reasoning.
Lemma 6
If , then .
Proof. By the deduction lemma applied times, assumption implies that
Hence, by the Necessitation inference rule,
Thus, by the Distributivity axiom and the Modus Ponens,
Hence, by the Modus Ponens inference rule,
Therefore, by applying the previous steps more times, .
Lemma 7
.
Proof. Formula is an instance of the Truth axiom. Thus, by contraposition. Hence, taking into account the following instance of the Negative Introspection axiom: , we have
(4) 
At the same time, is an instance of the Negative Introspection axiom. Thus, by the law of contrapositive in the propositional logic. Hence, by the Necessitation inference rule, . Thus, by the Distributivity axiom and the Modus Ponens inference rule, The latter, together with statement (4), implies the statement of the lemma by propositional reasoning.
Lemma 8
For any integer and any disjoint sets ,
Proof. By Lemma 5,
Thus, by the Monotonicity axiom,
Hence, by the Modus Ponens inference rule
By the Truth axiom and the Modus Ponens inference rule,
Note that is an instance of the Blame for Cause axiom. Thus, by the Modus Ponens inference rule applied twice,
By the Modus Ponens inference rule,
By the deduction lemma,
By Lemma 6,
By the definition of modality , the Negative Introspection axiom, and the Modus Ponens inference rule,
Therefore, by Lemma 7 and the Modus Ponens inference rule, the statement of the lemma follows.
Soundness
In the following lemmas, is a play of an arbitrary game and are arbitrary formulae.
Lemma 9
.
Proof. Suppose that . Thus, by Definition 3, we have and there is an action profile such that for each play , if , then .
Consider and . Note that is vacuously true. Hence, . In other words, , which leads to a contradiction.
Lemma 10
For all sets such that , if , , and , then .
Proof. Let and . Thus, by Definition 3 and the definition of modality , there are plays and such that and .
By Definition 3, statement implies that there is such that for each play , if , then .
Similarly, by Definition 3, statement implies that there is such that for each play , if , then .
Consider an action profile of coalition such that
Note that the action profile is welldefined because sets and are disjoint by the assumption of the lemma.
The choice of action profiles , , and implies that for each play , if , then and . Thus, for each play , if , then . Therefore, by Definition 3 and due to the assumption of the lemma.
Lemma 11
If , , and , then .
Proof. By Definition 3, assumption implies that there is such that for each play , if , then .
At the same time, for each play by the assumption of the lemma and Definition 3.
Thus, for each play such that by Definition 3. Hence, by Definition 3 and the assumption of the lemma.
Lemma 12
For all sets such that , if , then .
Proof. By Definition 3, assumption implies that and there is such that for each play , if , then .
By Definition 2, set is not empty. Let . Consider an action profile of coalition such that
Then, by the choice of action profile and because , for each play , if , then . Therefore, by Definition 3 and because , as we have shown earlier.
Lemma 13
If , then .
Completeness
We start the proof of the completeness by defining the canonical game for each maximal consistent set of formulae .
Definition 4
The set of outcomes is the set of all maximal consistent sets of formulae such that for each formula if , 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 and all agents in the coalition veto formula , then is satisfied in the outcome.
Definition 5
The domain of actions is set .
Definition 6
The set consists of all pairs such that for any formula , if for each agent , then .
Definition 7
.
This concludes the definition of the canonical game . The next four lemmas are auxiliary results leading to the proof of the completeness in Theorem 1.
Lemma 14
For any play , any action profile , and any formula , there is a play such that and .
Proof. Consider the following set of formulae:
Claim 1
Set is consistent.
Proof of Claim. Suppose the opposite. Thus, there are
formulae  (5)  
and formulae  (6)  
such that  (8)  
and  (9) 
Without loss of generality, we can assume that formulae are distinct. Thus, assumption (8) implies that sets are pairwise disjoint.
By propositional reasoning, assumption (9) implies that
Thus, by Lemma 6,
Hence, by assumption (5),
Thus, by Lemma 8, using assumptions (6) and the fact that sets are pairwise disjoint,
Hence because set is maximal. Then, by Definition 4, which contradicts the assumption of the lemma because set is consistent. Therefore, set is consistent.
Let be any maximal consistent extension of set . Thus, by the choice of sets and . Also, by Definition 4 and the choice of sets and .
Let the complete action profile be defined as follows:
(10) 
Then, .
Claim 2
.
Proof of Claim. Consider any formula such that for each . By Definition 6, it suffices to show that .
Case I: . Thus, by the definition of set . Therefore, by the choice of set .
Case II: . Consider any . Thus, by equation (10). Also, by the choice of formula . 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 such that .
Proof. Define a complete action profile such that for each agent . To prove , consider any formula
Comments
There are no comments yet.