The Limits of Morality in Strategic Games

1 Introduction

With humans delegating more and more decision power to autonomous systems such as self-driving cars, automated stock traders, and war robots, there is a need to adapt the notion of responsibility which would be applicable to artificial agents. In addition, autonomous agents must be able to reason about their own and human responsibility in a hybrid humanmachine environment. Towards this goal, in this paper we study the responsibility of agents and coalitions of agents in a strategic game setting.

As an example, consider the strategic game depicted in Figure 1. This game has two players that we refer to as Alice and Bob. In this game, Alice has actions a1, a2, and a3, while Bob has actions b1, b2, and b3. The outcome of each action profile is depicted in the corresponding cell of the table. For example, if Alice chooses action a2 while Bob picks b3, fire starts. Note that we allow games to be nondeterministic. For example, if Alice and Bob choose strategies a3 and b2, respectively, then the fire might start or it might not. In this case we say that action profile (a3, b2) has two different outcomes: "fire" and "no fire" depicted as half-cells of the tables.

∗Contact Author

We say that an agent (or a coalition) is blameable for ϕ if statement ϕ is true and the agent (or the coalition) had a strategy to prevent ϕ. This definition is often referred to as Frankfurt's [1969] principle of alternative possibilities [Widerker, 2017]. In our example, if Alice and Bob choose actions a2 and b3 respectively, then fire starts. In this case, Alice is blamable for the fire:

! ! ! because fire happened and Alice had a strategy (use action a1) that would prevent the statement "Fire started" from being true. In the same situation, Bob is not blamable for the start of the fire because he had no strategy to prevent it:

Note that according to the principle of alternative possibilities, in the case of the action profile (a3, b2), whether Alice is blamable or not depends on the outcome of the actions:

Naumov and Tao proposed complete logical systems that describe the properties of blameworthiness as a modality in perfect information strategic games [2019], imperfect information strategic games [2020c; 2020b], and security games (2020a).

In many real world situations humans are not blamed for the outcome if preventing it would require sacrificing too much. Can you shoot your neighbour's dog if it is attacking your child? Should you share your house with homeless people? Should you donate $1000 for a good cause? Can you use a cell phone in a movie theater if you are having a heart attack? Should you lend your calculator during an exam if you need it too? Should you proof-read a research paper for your friend? Do you have to finish a job assignment if it requires you to work overtime? Should you climb on a roof to save a kitten?

In the words of Shelly Kagan in The Limits of Morality, The greater the sacrifice which morality requires, obviously enough, the more significantly it will decrease the agent's ability to mold his life as he chooses and to promote his interests. The moderate may want to argue that more than a certain loss of such autonomy is morally intolerable. Hence, morality can exact so much, and no more. [Kagan, 1991, p.21]

In this paper we consider limited blameworthiness modality Bsaϕ which means that formula ϕ is true and agent a had a strategy with cost at most s to prevent it. Let us return to our example depicted in Figure 1 and to assume that the cost of each action for each agent is as shown in the figure. For example, the cost of action a1, that Alice can use to prevent the fire, is 100. Thus, if Alice chooses action a2, Bob chooses b3, and fire starts, then Alice can be blamed for the fire if the moral limit on her sacrifice is 100

because she has an action with cost at most 100 to prevent the fire. At the same time, if the moral limit on Alice's sacrifice is set to 50, then she cannot be blamed for the fire

because she has no action with cost at most 50 to prevent the fire. Finally, note that, as a coalition, Alice and Bob can prevent the fire if Alice chooses action a2 and Bob chooses action b2 with total cost 5 + 3 = 8. Thus, we say that their coalition is blameable with sacrifice 8,

In this paper we propose a sound and complete logical system that captures the universal properties of limited blameworthiness modality BsC ϕ. The axioms of the proposed systems are variations of the axioms for blameworthiness modality BCϕ without sacrifice limit [Naumov and Tao, 2019]. However, the proof of the completeness in the current paper is very different from [Naumov and Tao, 2019]; it is closer to the proof of the completeness for Resource-Bounded Coalition Logic [Alechina et al., 2011]. We further discuss the relation between these works in the beginning of Completeness section.

2 Other Related Literature

The other form of responsibility discussed in the literature is responsibility for seeing to ϕ. An agent is responsible for seeing to ϕ if the action taken by the agent unavoidably leads to ϕ being true. This notion of responsibility is captured in the logic of seeing-to-it-that (STIT) [Belnap and Perloff, 1990; Horty, 2001; Horty and Belnap, 1995; Horty and Pacuit, 2017; Olkhovikov and Wansing, 2018]. The cost of sacrifice could be potentially added to responsibility for seeing to it and interpreted as a degree of praiseworthiness. In many situation, the more an agent had to sacrifice to see to ϕ, the more she should be praised for ϕ.

Naumov and Yew proposed a dilemma modality that captures a hard choice that an agent faces between two or more undesirable alternatives [2021]. Although this modality in itself does not represent a form of responsibility, it also contains a cost of sacrifice. In their case, the sacrifice is the limit on the cost of actions that eliminates costly actions that could have been used to avoid making the hard choice.

3 Strategic Games with Cost of Actions

In this section, we describe the class of games that will be used as a semantics of our logical system. Throughout this paper, we assume a fixed finite set A of agents and a fixed set of propositional variables. By a coalition we mean an arbitrary subset of A. By XY we denote the set of all functions from set Y to set X.

Definition 1. A game is a tuple (∆, ‖ · ‖, d0, Ω, P, π), where

1. ∆ is a nonempty set of "actions", any function from set ∆A is called a "complete action profile",
2. ‖d‖ is a nonnegative real number, called the cost of action d ∈ ∆,
3. d0 ∈ ∆ is a zero-cost action: ‖d0‖ = 0,
4. Ω is a set of "outcomes",
5. a set of "plays" P is an arbitrary subset of ∆A × Ω satisfying the following nontermination condition: for each complete action profile δ ∈ ∆A there is at least one outcome ω ∈ Ω such that (δ, ω) ∈ P ,
6. π is a function that maps propositional variables into subsets of P .

In the introductory example, Alice and Bob had different sets of actions. In Definition 1, we assume that each agent has the same set of actions ∆. This assumption is not significant. We made it to simplify the notations. We interpret the cost of any action ‖d‖ as the amount of "sacrifice" that this action requires. We will reflect on the reasons for considering only nonnegative sacrifice in Syntax and Semantics section when we discuss sacrifice of a coalition. Although in this paper we assume that the cost of an action does not depend on the agent, this restriction is also not significant.

In game theory, strategic games are usually assumed to be deterministic in the sense that the outcomes (pay-offs) are uniquely determined by the complete action profile. Nondeterminacy in such games is usually modeled through an additional player, often interpreted as "nature" or "god". In this paper we have chosen to model nondeterminacy by explicitly assuming that a complete action profile might correspond to multiple outcomes. In addition to simplifying our axiomatic system, this choice also avoids the necessity to assign blame to the "nature".

The game depicted in Figure 1 has 9 complete action profiles corresponding to possible combinations of Alice's and Bob's strategies. This game has 10 outcomes defined by the "regions" of the table (eight squares and 2 triangles). In that game, each outcome corresponds to a unique complete action profile. In general, it will be convenient to assume that different complete action profiles might result in the same outcome. Thus, we introduce the set of "plays" P that specifies which complete action profiles are consistent with which outcomes.

Informally, this set captures the rules of the game. The nontermination condition requires each complete action profile to lead to at least one outcome.

The existence of a zero-cost action in the game is important for capturing the notion of limited blameworthiness. Indeed, consider an agent that has a choice of just two actions: not to save somebody's life at cost 99 or to save the life at cost 100. Intuitively, the sacrifice in such a setting is 1, not 100. By requiring that there exists a zero-cost action, we, in essence, "normalize" the costs of all actions available to the agent.

Recall from the introductory examples that we place a play, not a state, on the left side of ⊩. In other words, statements in our logical systems are not about states, but about plays. Similarly, we interpret propositional variables as statements about plays. This is why valuation function π in Definition 1 maps propositional variables into sets of plays rather than sets of outcomes.

Definition 2. For any action profile γ ∈ ∆C of a coalition C, by ‖γ‖ we mean the total cost of the action profile to the coalition: ‖γ‖ = ∑a∈C ‖γ(a)‖.

By defining the cost to a coalition as a sum of the costs of actions of the individual members of the coalition, we ignore the distribution of the burden between the individual members. Although this makes sense in many real-world situations, it is also easy to see that in some cases this approach might be problematic. For example, one probably should blame a coalition of 10 people for breaking a rule if it cost only $19 to all of them together to follow the rule. Indeed, it is less than $2 per person. Similarly, one might argue that 1,000,000 people should be blamed for breaking the rule if it costs them total of $1,999,999 to follow the rule. But what if it costs $1,000,000 to one person and just $1 to each of the remaining 999,999 people?

In this paper we decided to disallow negative costs of actions because they lead to even more paradoxical situations. For example, consider a situation when to prevent ϕ one needs a joint effort of Alice and Bob. Suppose that the action required of Alice will cost her $1,000,000, while Bob will make a profit (negative cost) on his action in the amount of $1,000,000. Should we blame them, as a coalition, for not preventing ϕ at zero cost?

4 Syntax and Semantics

The language Φ of our system is defined by the grammar

where p is a propositional variable, s ≥ 0 is a real number, and C is a coalition. We read BsC ϕ as "coalition C is blameable for statement ϕ because it would have to sacrifice at most s to prevent ϕ". We read Nϕ as "statement ϕ is universally true in the given game". By Nϕ we denote formula ¬N¬ϕ. Thus, Nϕ means that statement ϕ is true on at least one play of the game. We assume that conjunction ∧, disjunction ∨, biconditional ↔, and truth constant ⊤ are defined as usual.

For any functions f and g, we write f =X g, if f(x) = g(x) for each x ∈ X. The following is the key definition of this paper. Item 5 of this definition formally specifies the meaning of the blameworthiness modality BsC ϕ.

Definition 3. For any formula ϕ in language Φ and any play (δ, ω) ∈ P of a game (∆, ‖ · ‖, d0, Ω, P, π), the satisfaction relation (δ, ω) ⊩ ϕ is defined recursively as follows:

1. (δ, ω) ⊩ p if (δ, ω) ∈ π(p), where p is a propositional variable,
2. (δ, ω) ⊩ ¬ϕ if (δ, ω) ⊮ ϕ,
3. (δ, ω) ⊩ ϕ→ψ if (δ, ω) ⊮ ϕ or (δ, ω) ⊩ ψ,
4. (δ, ω) ⊩ Nϕ if (δ′ , ω′ ) ⊩ ϕ for each play (δ′ , ω′ ) ∈ P,
5. (δ, ω) ⊩ BsC ϕ if
6. (a) (δ, ω) ⊩ ϕ,
7. (b) there is a profile γ ∈ ∆C such that ‖γ‖ ≤ s and for each (δ′ , ω′ ) ∈ P, if γ =C δ′ , then (δ′ , ω′ ) ⊮ ϕ,
8. (c) for each proper subset D of set C and each action profile γ ∈ ∆D where ‖γ‖ ≤ s, there is a play (δ′ , ω′ ) ∈ P such that γ =D δ′ and (δ′ , ω′ ) ⊩ ϕ.

Note that if a coalition had a strategy to prevent condition ϕ, then every superset of the coalition had such strategy as well. To avoid blaming a coalition for a failure of its subset, the above definition includes the minimality condition captured by item 5(c). Namely, we say that a coalition C is blamable for statement ϕ with sacrifice limit s if ϕ is true, coalition C had a strategy to prevent it at cost no more than s, and no subset of C had a strategy to prevent ϕ at cost no more than s.

Although the intended meaning of the sacrifice s in modal formula BsC ϕ is to capture the limit of the blameworthiness, it can also be interpreted as a degree of blameworthiness. Intuitively, the lower the cost of prevention is, the more blamable the coalition should be for the outcome. Halpern and Kleiman-Weiner use the cost of prevention to define one of the degrees of blameworthiness that they propose (2018). An important difference between Definition 3 and Halpern and Kleiman-Weiner's approach is that we use absolute sacrifice while they use relative sacrifice. Relative sacrifice is the difference between the current costs encountered by a coalition and the costs required to prevent the undesirable outcome. For example, consider a business company that spent $100,000 on a safety device that does not completely prevent a certain type of accident, but the company could have spent $100,001 on a more expensive version of the device that completely prevents this type of accident. If the accident happens, should the degree of blame be computed based on absolute cost $100,001 or the relative cost of $1? In the former case the degree of blame will be low, in the second case it will be high. In this example, it probably makes sense to use the relative sacrifice as proposed in [Halpern and Kleiman-Weiner, 2018]. However, if in the same setting the original $100,000 were spent not on a safety device, but on a new warehouse, then the absolute sacrifice of $100,001 is probably a better measure of the degree of company's blameworthiness for the accident. The logical system proposed in this paper is suitable for reasoning about the latter, but not the former setting.

Finally, the discussed above degree of blameworthiness of a group should not be confused with the degree of responsibility within the group. The latter is concerned with how the blame should be divided between several members of the group. In the spirit of this paper, one might suggest that degree within the group could be defined as a ratio of total costs that would be imposed on the whole group to the cost imposed on an individual. For example, if prevention would require a joint effort of Alice and Bob and the cost of the appropriate actions is $2 for Alice and $5 for Bob, then Alice is responsible for the outcome to a higher degree than Bob. However, this approach is problematic because there might be two different ways to prevent outcome: one of them would cost $2 to Alice and $5 to Bob, while the other would cost $5 to Alice and $2 to Bob. Thus, the cost-based approach explored in this paper in some situations might be used to define the degree of blameworthiness of a group but it is not likely to be appropriate to define the degree of responsibility within the group.

In this paper we use abbreviation BsC ϕ for the disjunction ∨D⊆C BsD ϕ. Informally, BsC ϕ means "statement ϕ is true and one of subsets of C could be blamed for it with sacrifice s". As shown in the full version of the paper [Cao and Naumov, 2019], it is equivalent to statement "ϕ is true and coalition C could have prevented it at cost no more than s".

5 Axioms

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

1. Truth: Nϕ→ϕ and BsC ϕ→ϕ,
2. Distributivity: N(ϕ→ψ) → (Nϕ→Nψ),
3. Euclidicity: ¬Nϕ→N¬Nϕ,
4. None to Blame: ¬Bs∅ϕ,
5. Blamelessness of Truth: ¬BsC ⊤,
6. Monotonicity: BsC ϕ → BtC ϕ, where s ≤ t,
7. Minimality: BsC ϕ → ¬BsD ϕ, where D ⊊ C,
8. Joint Responsibility: if C ∩D = ∅, then NBsC ϕ ∧ NBtD ψ → (ϕ ∨ ψ → Bs+t C∪D (ϕ ∨ ψ)),
9. Strict Conditional: N(ϕ → ψ) → (BsC ψ → (ϕ → BsC ϕ)),
10. Fairness: BsC ϕ→N(ϕ→BsC ϕ),
11. Substitution: N(ϕ↔ψ) → (BsC ϕ→BsC ψ).

The Truth, the Distributivity, and the Euclidicity axioms for modality N capture the fact that this is an S5-modality [Fagin et al., 1995]. The Truth axiom for modality B states that a coalition can only be blamed for something which is true. The None to Blame axiom says that the empty coalition can not be blamed for anything. The Blamelessness of Truth axioms says that none can be blamed for a tautology. Informally, this axiom is sound because there could be no strategy to prevent a tautology. The Monotonicity axiom states that if a coalition C can be blamed for not preventing an outcome at cost at most s, then either the coalition itself or at least one of its subsets can also be blamed for not preventing the outcome at cost at most t, where t ≥ s. The Minimality axiom says that if a coalition can be blamed for ϕ, then no proper subset of this coalition can be blamed for ϕ. The Joint Responsibility axiom shows how blames of two disjoint coalitions can be combined into a blame of their union. To understand the Strict Conditional axiom, note that formula N(ϕ → ψ) means that ϕ implies ψ for each play of the game. The axiom says that if a coalition is responsible for statement ψ, then either the coalition itself or at least one of its subsets is responsible for a stronger statement ϕ as long as ϕ is true. The Fairness axiom states that if a coalition is blamed for ϕ, then it should be blamed for ϕ each time when ϕ is true.

We write ⊢ ϕ if formula ϕ is provable from the axioms of our system using the Modus Ponens and the Necessitation

formula ϕ is a theorem of our logical system. In addition to unary relation ⊢ ϕ, we also consider a binary relation X ⊢ ϕ. We write X ⊢ ϕ if formula ϕ is provable from all theorems of our logical system and the set of additional formulae X using the Modus Ponens inference rule only. It is easy to see that statement ∅ ⊢ ϕ is equivalent to ⊢ ϕ. A set of formulae X is consistent if there is no formula ϕ such that X ⊢ ϕ and X ⊢ ¬ϕ.

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

6 Completeness

We show the soundness of our logical system in the full version of this paper [Cao and Naumov, 2019]. In the rest of this paper, we prove its completeness.

We will use modality □sC ϕ as an abbreviation for statement N(¬ϕ → BsC ¬ϕ). Informally, formula □sC ϕ means that coalition C or one of its subsets is blamable for ¬ϕ in each outcome of the game in which statement ϕ is false. In other words, □sC ϕ is a counterfactual modality that means that coalition C could have prevented ¬ϕ at cost s. This modality is different from the "coalition C has a strategy to achieve ϕ at costs s" modality of Resource-Bounded Coalition Logic (RBCL) [Alechina et al., 2011] denoted here by SsC ϕ. For example, statement ϕ∧□sC ¬ϕmeans that ϕ is true now, but coalition C could have prevented it at cost s. At the same time, statement ϕ∧SsC ¬ϕ in RBCL means that ϕ is true now but C could make it false in the future. In spite of this semantical difference between modalities □sC ϕ and SsC ϕ, they share many common properties. In the full version of this paper [Cao and Naumov, 2019], we prove the following basic properties of the modalities □sC ϕ and N. Some of these properties are listed as axioms in [Alechina et al., 2011].

In the rest of the paper we use these properties to prove the completeness of our logical system.

Compared to this paper, the blameworthiness modality in [Naumov and Tao, 2019] is missing not only the sacrifice constraint, but also the minimality condition of item 5(c) in Definition 3. As a result, the blameworthiness modality in [Naumov and Tao, 2019] is, essentially, a sacrifice-free version of modality B. The proof of the completeness in [Naumov and Tao, 2019] does not introduce anything similar to abbreviations □sC ϕ. Instead, it constructs the canonical game using the blameworthiness modality directly.

6.1 Canonical Model

As usual in modal logic, the proof of the completeness relies on the construction of a canonical model. In our case, we define the canonical game G(ω0) = (∆, ‖ · ‖, d0, Ω, P, π) for each maximal consistent set of formulae ω0. We define each component of the canonical game G(ω0) separately.

Definition 4. Set ∆ consists of a zero-cost action d0, which is not a triple, and all triples (ϕ,C, s) such that ϕ ∈ Φ is a formula, C is a nonempty coalition, and s is a non-negative real number.

Informally, we consider actions as "votes" of agents. Zerocost action d0 could be interpreted as abstaining from voting. Action (ϕ,C, s) by an agent a means that agent a is voting as a part of coalition C to force ϕ at the total cost s to the whole coalition. If agent a votes (ϕ,C, s), then statement ϕ is not necessarily true in the outcome. The vote aggregation mechanism is given in Definition 7. Definition 4 is substantially different from a similar definition in [Naumov and Tao, 2019], where each action consists of just a single formula ϕ.

Informally, ‖d‖ = s |C| means that the cost of each joint action is divided evenly between all members of the coalition. Note that size |C| of coalition C is non-zero by Definition 4.

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

Definition 7. The set P ⊆ ∆A ×Ω consists of all pairs (δ, ω) such that for any □sC ψ ∈ ω0, if δ(a) = (ψ,C, s) for each agent a ∈ C, then ψ ∈ ω.

In other words, for each formula □sC ψ ∈ ω0, if each member of coalition C votes as a part of C to force ψ at cost s, then ψ is guaranteed to be true in the outcome.

Definition 8. π(p) = {(δ, ω) ∈ P | p ∈ ω} for each propositional variable p.

This concludes the definition of the canonical game G(ω0). In Lemma 5, we prove the nontermination condition from item 5 of Definition 1 is satisfied for game G(ω0).

As usual, the key part of the proof of the completeness is the induction, or "truth", lemma. In our case this is Lemma 7.

The next three lemmas are auxiliary lemmas used in the proof of Lemma 7.

Lemma 2. For any play (δ, ω) ∈ P and any formula □sC ¬ϕ ∈ ω there is a profile γ ∈ ∆C where ‖γ‖ ≤ s such that for any play (δ′ , ω′ ) ∈ P if γ =C δ′ , then ϕ /∈ ω′ .

Proof. Define γ ∈ ∆C to be an action profile of coalition C such that for each agent a ∈ C,

Claim 1. ‖γ‖ ≤ s.

PROOF OF CLAIM. If set C is not empty, then, by Definition 2 and Definition 5, ‖γ‖ = ∑a∈C ‖(ϕ,C, s)‖ = ∑a∈C s |C| = s.

If set C is empty, then ‖γ‖ = 0 by Definition 2. At the same time, s ≥ 0 by the definition of Φ. Thus, ‖γ‖ ≤ s. ⊠

Consider any play (δ′ , ω′ ) ∈ P such that γ =C δ′ . Recall that □sC ¬ϕ ∈ ω by the assumption of the lemma. Hence ω ⊢ N□sC ¬ϕ by Property P0. Thus, ¬N□sC ¬ϕ /∈ ω because set ω is maximal. Then, N¬N□sC ¬ϕ /∈ ω0 by Definition 6. Hence, because set ω0 is maximal,

At the same time, formula ¬N□sC ¬ϕ → N¬N□sC ¬ϕ is an instance of the Euclidicity axiom. Thus, by contraposition, ⊢ ¬N¬N□sC ¬ϕ → N□sC ¬ϕ. Hence, by the Truth axiom and the propositional reasoning, ⊢ ¬N¬N□sC ¬ϕ → □sC ¬ϕ. Then, ω0 ⊢ □sC ¬ϕ by the Modus Ponens inference rule using statement (2). Hence, □sC ¬ϕ ∈ ω0 because set ω0 is maximal. Thus, ¬ϕ ∈ ω′ by Definition 7, the assumption γ =C δ′ and statement (1). Then, ϕ /∈ ω′ because ω′ is consistent. ⊠

Lemma 3. For any play (δ, ω) ∈ P , any profile γ ∈ ∆C , and any formula ¬□sC ¬ϕ ∈ ω, if ‖γ‖ ≤ s, then there is a play (δ′ , ω′ ) ∈ P such that γ =C δ′ and ϕ ∈ ω′ .

Proof. Consider the following set X of formulae:

Claim 2. Set X is consistent.

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

Without loss of generality, we can assume that formulae χ1, . . . , χn are distinct. Thus, assumption (5) implies that sets D1, . . . , Dn are pairwise disjoint. Hence, by Definition 5 and formula (5),

Thus, t1 + · · · + tn ≤ s by the assumption ‖γ‖ ≤ s of the lemma. Then, assumption (6) by Property P1 implies

Hence, by Property P3 and the Modus Ponens rule applied m times, Nψ1, . . . , Nψm, □t1D1 χ1, . . . , □tn Dn χn ⊢ □sC ¬ϕ. Thus, ω0 ⊢ □sC ¬ϕ due to statement (3). Hence, ω0 ⊢ N□sC ¬ϕ by Property P0 and the Modus Ponens inference rule. Then, N□sC ¬ϕ ∈ ω0 because set ω0 is maximal. Thus, □sC ¬ϕ ∈ ω by Definition 6 and because ω ∈ Ω. Thus, ¬□sC ¬ϕ /∈ ω because set ω is consistent, which contradicts assumption ¬□sC ¬ϕ ∈ ω of the lemma. Then, set X is consistent. ⊠

By Lemma 1, set X can be extended to a maximal consistent set ω′ . Thus, ϕ ∈ X ⊆ ω′ by the choice of sets X and ω′ . Also, ω′ ∈ Ω by Definition 6 and the choice of sets X and ω′ . Let the complete action profile δ′ be defined as follows:

Then, γ =C δ′ .

Claim 3. (δ′ , ω′ ) ∈ P.

PROOF OF CLAIM. Consider any formula □tD χ ∈ ω0 such that δ′ (a) = (χ,D, t) for each a ∈ D. By Definition 7, 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 a ∈ D \ C. Thus, δ′ (a) = d0 by equation (7). At the same time, δ′ (a) = (χ,D, t) because a ∈ D. Thus, d0 = (χ,D, t), which is a contradiction, because d0 is not a triple by Definition 4. ⊠ This concludes the proof of the lemma. ⊠

Lemma 4. For each outcome ω ∈ Ω, there is a complete action profile δ ∈ ∆A such that (δ, ω) ∈ P .

Proof. Consider a complete action profile δ where δ(a) = d0 for all a ∈ A. To show (δ, ω) ∈ P , consider any such formula □tD χ ∈ ω0 that δ(a) = (χ,D, t) for all a ∈ D. Due to Definition 7, it enough to prove that χ ∈ ω.

Case I: D = ∅. Thus, assumption □tD χ ∈ ω0 implies ω0 ⊢ Nχ by Property P3 and the Modus Ponens inference rule. Hence, Nχ ∈ ω0 because set ω0 is maximal. Thus, χ ∈ ω by Definition 6 because ω ∈ Ω.

Case II: D ̸= ∅. Hence, set D contains at least one agent a. Then, (χ, D, t) = δ(a) = d0 by the definition of profile δ. Thus, d0 = (χ,D, t), which is a contradiction, because d0 is not a triple by Definition 4. ⊠

Next, we show that canonical game G(ω0) satisfies the nontermination property from item 5 of Definition 1.

Lemma 5. For any complete action profile δ ∈ ∆A there is an outcome ω ∈ Ω such that (δ, ω) ∈ P .

Proof. Recall that game G(ω0) is defined for a given maximal consistent set ω0. Then, ω0 ∈ Ω by Definition 6 and the Truth axiom. Hence, by Lemma 4, there is a complete action profile δ0 ∈ ∆A such that (δ0, ω0) ∈ P .

Note that ‖δ‖ is a finite number because the set of all agents A is finite. Thus, ⊢ ¬□‖δ‖ A ¬⊤ by Property P4. Hence, ¬□‖δ‖ A ¬⊤ ∈ ω0 because set ω0 is maximal. Thus, by Lemma 3 in the case of the play (δ0, ω0), there is a play (δ′ , ω′ ) ∈ P such that δ =A δ′ and ⊤ ∈ ω′ . Note that δ =A δ′ implies that complete action profiles δ and δ′ are the same. Then, (δ, ω′ ) ∈ P . Choose ω to be ω′ . ⊠

Lemma 6. For each play (δ, ω) ∈ P and each formula ¬Nϕ ∈ ω, there is a play (δ′ , ω′ ) ∈ P such that ¬ϕ ∈ ω′ .

Proof. Let X be the set {¬ϕ} ∪ {ψ | Nψ ∈ ω0}. Next, we prove the consistency of set X. Assume the opposite. Hence, there are formulae Nψ1, . . . , Nψn ∈ ω0 where ψ1, . . . , ψn ⊢ ϕ. Thus, Nψ1, . . . ,Nψn ⊢ Nϕ due to Property P6. Then, ω0 ⊢ Nϕ because Nψ1, . . . , Nψn ∈ ω0. Thus, ω0 ⊢ NNϕ by Property P5. Hence, it follows from assumption ω ∈ Ω and Definition 6 that Nϕ ∈ ω. Thus, ¬Nϕ /∈ ω by the consistency of set ω, which contradicts the assumption ¬Nϕ ∈ ω of the lemma. Therefore, set X is consistent. By Lemma 1, set X could be extended to a maximal consistent set ω′ . Observe that ¬ϕ ∈ X ⊆ ω′ due to the definition of set X. Finally, by Lemma 4, there is a profile δ′ where (δ′ , ω′ ) ∈ P . ⊠

Next is the "truth" lemma for our proof of the completeness theorem, whose proof can be found in the full version of this paper [Cao and Naumov, 2019].

Lemma 7. (δ, ω) ⊩ ϕ iff ϕ ∈ ω for any play (δ, ω) ∈ P and any formula ϕ ∈ Φ.

6.2 Strong Completeness

Theorem 1. If X ⊬ ϕ, then there is a game and a play (δ, ω) of the game where (δ, ω) ⊩ χ for all χ ∈ X and (δ, ω) ⊮ ϕ.

Proof. Assume that X ⊬ ϕ. Hence, set X ∪ {¬ϕ} is consistent. By Lemma 1, set X ∪ {¬ϕ} can be extended to a maximal consistent set ω0. Let G(ω0) = (∆, ‖ · ‖, d0,Ω, P, π) to be the canonical game defined above. Then, ω0 ∈ Ω by Definition 6 and the Truth axiom.

By Lemma 4, there exists an action profile δ ∈ ∆A such that (δ, ω0) ∈ P. Hence, (δ, ω0) ⊩ χ for all χ ∈ X and (δ, ω0) ⊩ ¬ϕ by Lemma 7 and the choice of set ω0. Therefore, (δ, ω0) ⊮ ϕ by Definition 3. ⊠

7 Conclusion

In this paper we combine the ideas from the logics of resource bounded coalitions [Alechina et al., 2011] and blameworthiness [Naumov and Tao, 2019] into a logical system that captures the properties of limits of blameworthiness. The main technical result is a strongly complete logical system describing the limited blameworthiness modality.