Two Forms of Responsibility in Strategic Games

1 Introduction

In this paper we study formal semantics of responsibility. In the literature, there have been two different approaches to defining responsibility.

The first approach is based on what became known as Frankfurt's principle of alternate possibilities: "a person is morally responsible for what he has done only if he could have done otherwise" [Frankfurt, 1969]. The principle of alternate possibilities is widely discussed in the literature [Widerker, 2017]. Although Frankfurt and many others agree that this principle has many exceptions and limitations, the principle is often taken as a starting point in philosophical discussions of responsibility. This principle, sometimes referred to as "counterfactual possibility" [Cushman, 2015], is also used to define causality [Lewis, 2013; Halpern, 2016; Batusov and Soutchanski, 2018]. For the sake of clarity, in this paper we refer to all versions of responsibility based on the principle of alternate possibilities as blameworthiness. Formal logical systems for reasoning about blameworthiness in strategic and security games are proposed in [Naumov and Tao, 2019a] and [Naumov and Tao, 2020a] respectively.

The other approach is to hold a person responsible for the outcome if the person sees to it that it happens. In this paper we refer to this approach as responsibility for seeing to it. This approach to responsibility has been extensively studied in STIT ("seeing-to-it-that") logic [Belnap and Perloff, 1990; Horty, 2001; Horty and Belnap, 1995; Horty and Pacuit, 2017; Olkhovikov and Wansing, 2018].

The rest of this paper is organized as follows. First, we illustrate the difference between the two forms of responsibility on an example. Then, we discuss how these two forms of responsibility could be defined in imperfect information setting. In Section 4 we formally define games with imperfect information. Section 5 defines modalities that capture seeing to it and blameworthiness. In the section that follows, we compare our semantics with epistemic XSTIT frames. Section 7 and Section 8 contain the two main results of this paper. We show that the blameable modality is definable through the seeing to it modality and that seeing to it is not definable through blameable even using the ex ante (before the action) knowledge modality. Section 9 discusses the future work and concludes.

2 Responsibility in Strategic Games

The difference between the two forms of responsibility could be illustrated using two strategic games depicted in Figure 1. We refer to these games as the left and the right game. In these

games, agents mom and dad are trying to prevent their baby from crying. In both games, each parent has three strategies: m1, m2, and m3 for mom and d1, d2, and d3 for dad. The cells of the tables represent action profiles. The crying emoji marks action profiles under which the baby cries. In this paper we consider nondeterministic games that might have multiple outcomes for the same action profile. If an action profile might result in multiple outcomes, we further split the cell into triangles representing these outcomes. For example, in the left game, under action profile (m2, d3) there might be two possible outcomes. Only in one of them the baby cries.

Consider a situation when parents choose actions m2 and d3 in the left game and the baby cries. In this case, according to the principle of alternative possibilities, the mom is blamable for the baby crying because mom could have prevented it by choosing action m1. At the same time, in the right game, under the same profile (m2, d3), the baby also cries, but mom is not blamable for it because in the right game she has no unilateral action that would prevent the baby from crying.

However, mom is responsible for seeing to the baby's crying in the right game under action profile (m2, d3). Indeed, by choosing action m2 mom guarantees that the baby cries. On the other hand, she is not responsible for seeing to it under profile (m2, d3) in the left game because action m2 in the left game does not unavoidably lead to baby crying.

Note that statement 2 + 2 = 4 is true no matter what action the mom chooses. Thus, one can say that the mom sees to it that 2 + 2 = 4. This is the approach taken in STIT logic. However, such an approach is problematic if seeing to it is interpreted as a form of responsibility. One can hold an agent responsible for seeing to it that something happens only if the agent had an alternative action that does not unavoidably leads to it. Horty and Belnap refer to seeing to it in the presence of such an alternative action as seeing to it "deliberately" [Horty and Belnap, 1995]. Since the focus of our paper is on two forms of responsibility, we include the existence of the alternative action in our definition of seeing to it. In the right game from Figure 1, under action profile (m2, d3) such an alternative action of mom not unavoidably leading to baby crying is, for example, action m3.

3 Responsibility and Knowledge

Knowledge is an important factor in ascribing responsibility to agents. The connection between responsibility and knowledge has been discussed by philosophers since Aristotle:

. . . blame is given only to what is voluntary . . . a voluntary act is one which is originated by the doer with knowledge of the particular circumstances of the act. [Aristotle, 1906]

In a legal setting, the responsibility is also commonly defined as a combination of knowledge and actions, often referred to as guilty mind and guilty actions. For example, US Model Penal Code distinguishes five such combinations referred to as strict liability and liability for doing negligently, recklessly, knowingly, and purposefully [Institute, 1985 Print].

If one considers games with imperfect information instead of games with perfect information that we discussed in the last section, then the definitions of both forms of responsibility must be adjusted to incorporate knowledge. In the case of blameworthiness, it is natural to require that the agent could be blamed for an outcome when she not only has a strategy to prevent it, but also knows ex ante (before the action) what this strategy is [Yazdanpanah et al., 2019; Naumov and Tao, 2020c; Naumov and Tao, 2020b]. In the case of seeing to it, it is natural to require that not only should the agent's action unavoidably leads to the outcome, but the agent also must interim (at the time of the action) know this.

To illustrate the two forms of responsibility in imperfect information setting, consider an execution of a death penalty by shooting. If the execution is administered by a single shooter, then the shooter is blameable for the death and sees to it.

Indeed, the shooter is blameable for the death of the prisoner because the prisoner is dead after the shooting, and the shooter knows ex ante that this could be prevented by not firing the lethal shot. The shooter also sees to the death of the prisoner because the shooter knows interim (at the moment the trigger is pulled) that the action will result in death. The shooter also knows that the prisoner would not have to die if the trigger is not pulled.

Most executions by shooting are performed by a firing squad rather than by a single shooter. If multiple shooters are instructed to fire simultaneously, then no single shooter has a strategy to prevent the death of the prisoner. Thus, none of them could be blamed for the death individually 1 . At the same time, each of the agents knows interim that pulling the trigger while aiming at the prisoner will unavoidably result in the death, while not shooting leaves a possibility (if all other shooters do not shoot too) for the prisoner not to be killed. Thus, each member of the firing squad who pulls the trigger while aiming at the prisoner sees to the death of the prisoner.

In some cases, one or more members of the firing squad are issued a weapon containing a blank cartridge 2 , also known as the "conscience bullet". The members of the squad are told that one of them has a blank cartridge, but they are not told which one. Because the blank cartridge has no bullet, it gives no recoil. As a result, each shooter knows ex post (after the trigger is pulled) which cartridge it was, but not ex ante or interim (at the moment the trigger is pulled). If one or more members of the firing squad are issued "conscience bullets", then none of the squad members are blamable for the death. Indeed, even if only one member of the squad is issued the real bullet, then this member has a strategy to prevent the death, but the shooter does not know this. If more than one of them is issued a real bullet, then none of the members have a strategy to prevent the death unilaterally. In the "conscience bullet" setting, none of the agents sees to the death of the prisoner because none of them knows interim that pulling the trigger while aiming at the prisoner will unavoidably result in the death of the prisoner.

Thus, an execution by a single shooter results in the shooter being blamable for the death and also the shooter sees to the death. If an execution by a firing squad is without a "conscience bullet", then none of the squad members is blameable, but each of them sees to the death. If at least one "conscience bullet" is used, none of the members is blamable for the death and none sees to the death.

4 Imperfect Information Strategic Games

In this section we give a formal definition of games with imperfect information used throughout the rest of this paper. Throughout the paper we assume a fixed set of propositional variables and a fixed set of agents A.

1 All shooters could be blamed together as a group under the coalitional blameworthiness definition in [Naumov and Tao, 2019b].

2 "The officer charged with the execution will . . .Cause eight rifles to be loaded in his presence. Not more than three nor less than one will be loaded with blank ammunition. He will place the rifles at random in the rack provided for that purpose." [Witsell and Eisenhower, 1947, p.5]

Definition 1. A game is (I, {∼a}a∈A, {∆αa }α∈I a∈A, Ω, P, π), where

1. I is a set of "initial states",
2. ∼a is an "indistinguishability" equivalence relation on the set of initial states I, for each agent a ∈ A,
3. ∆αa is a nonempty set of "actions" for each agent a ∈ A and each state α ∈ I, where for each agent a ∈ A and all states α, α′ ∈ I, if α ∼a α′ , then ∆αa = ∆α′ a ,
4. Ω is a set of "outcomes",
5. P is a set of triples (α, δ, ω), called "plays", where α ∈ I is an initial state, ω ∈ Ω is an outcome, and
6. (a) function δ, called an "action profile in state α", is such that δ(a) ∈ ∆αa for each initial state α ∈ I and each agent a ∈ A,
7. (b) for each initial state α ∈ I and each action profile δ in state α, there is at least one outcome ω ∈ Ω such that (α, δ, ω) ∈ P ,
8. π(p) is a subset of P for each propositional variable p.

The indistinguishability equivalence relation between initial states ∼a captures the ex ante knowledge of an agent a or the knowledge of the agent before the transition takes place. Knowledge defined through equivalence relation on outcomes is usually called the ex post knowledge. We do not include the ex post knowledge into our system because it is not relevant to responsibility.

The assumption of item 3 in Definition 1 that ∆αa = ∆α′ a when α ∼a α′ states that an agent has the same set of actions in all indistinguishable states. In other words, the set of available actions is known to the agent.

In Definition 1, we distinguish the set of initial states I from the set of outcomes Ω. This is done for convenience only. In particular, we allow I and Ω to be the same set.

The set of plays P captures the mechanism or the set of "rules" of the game. It specifies into which outcome the game can transition from a given initial state under a given action profile. We allow the mechanism to be nondeterministic.

Finally, unlike many other logical systems, we use propositional variables to represent not statements about outcomes, but, more generally, statements about plays. We further discuss the reason for this choice in the next section. Formally, this is captured through the value of π(p) being a set of plays rather than a set of outcomes.

5 Syntax and Semantics

By ΦST,B we denote the language defined by the grammar

where p is a propositional variable and a ∈ A is an agent. We read Kaϕ as "agent a knows ex ante that statement ϕ will be true", Baϕ as "agent a is blameable for ϕ", and STaϕ as "agent a sees to ϕ". By ΦB we denote the fragment of the language ΦST,B that does not include modality ST. Similarly, by ΦST we denote the fragment of ΦST,B without modality B.

Definition 2. The satisfaction relation (α, δ, ω) ⊩ ϕ between a play (α, δ, ω) ∈ P and a formula ϕ ∈ ΦST,B is defined as:

1. (α, δ, ω) ⊩ p, if (α, δ, ω) ∈ π(p),
2. (α, δ, ω) ⊩ ¬ϕ, if (α, δ, ω) ⊮ ϕ,
3. (α, δ, ω) ⊩ ϕ→ψ, if (α, δ, ω) ⊮ ϕ or (α, δ, ω) ⊩ ψ,
4. (α, δ, ω) ⊩ Kaϕ, if (α′ , δ′ , ω′ ) ⊩ ϕ for each play (α′ , δ′ , ω′ ) ∈ P such that α ∼a α′ ,
5. (α, δ, ω) ⊩ STaϕ, if
6. (a) (α′ , δ′ , ω′ ) ⊩ ϕ for each play (α′ , δ′ , ω′ ) ∈ P such that α ∼a α′ and δ(a) = δ′ (a),
7. (b) (α′ , δ′ , ω′ ) ⊮ ϕ for some play (α′ , δ′ , ω′ ) ∈ P such that α ∼a α′ .
8. (α, δ, ω) ⊩ Baϕ if
9. (a) (α, δ, ω) ⊩ ϕ and
10. (b) there is an action d ∈ ∆αa such that for each play (α′ , δ′ , ω′ ) ∈ P if α ∼a α′ and d = δ′ (a), then (α′ , δ′ , ω′ ) ⊮ ϕ.

The formal semantics in Definition 2 specifies satisfaction ⊩ as a relation between a play (α, δ, ω) and a formula ϕ. This is different from the standard semantics of modal logics where satisfaction is a relation between a state and a formula. This change is needed because "seeing to it" is a property not of a state, but rather of a transition between states 3 . Indeed,

consider the game depicted in Figure 2 (left). This game has a single initial state α and two outcome states ω1 and ω2. The only agent Alice of this game has two possible actions in state α: action a and action b. Action a deterministically transitions the game into outcome ω1 and action b nondeterministically leads to either outcome ω1 or outcome ω2. Let statement p stand for "game ends with outcome ω1". Note that if Alice employs action a, then she knows at the time of the action, that statement p will be true and she also knows that p is not unavoidable if she chooses action b instead. Thus, by item 5 of Definition 2, she sees to it that p is true:

At the same time, if the game ends with the same outcome ω1, but Alice uses action b instead of a, then she does see to p because condition 5(a) of Definition 2 is not satisfied:

Hence, whether an agent sees to something depends not only on the outcome, but also on the actions of the agent that lead to that outcome.

3 The same is true about the blameworthiness modality as well.

The game depicted in Figure 2 (right) illustrates that seeing to something also depends on the initial state:

Thus, a statement of the form STaϕ depends not only on the action profile, but also on the initial state. Because formulae in our languages use this modality, we define satisfaction relation ⊩ as a relation between plays 4 and formulae.

Next, let us turn to item 5(b) of the above definition. It is intended to avoid agent a being responsible for unavoidable statements like 2 + 2 = 4. In the perfect information case, this condition was introduced in Delibarative STIT [Horty and Belnap, 1995]. There are at least three possible ways in which this condition can be stated in the imperfect information case:

1. agent a does not know that ϕ is unavoidable,
2. ϕ is avoidable,
3. agent a knows that ϕ is avoidable.

Out of these alternatives, 1 is the weakest and 3 is the strongest. We believe that condition 1 is the best to capture the "guilty mind" aspect of responsibility. For example, shooting a terminally ill person by an agent who does not know that the person is about to die is seeing to the death under alternative 1, but not under alternatives 2 and 3. Item 5(b) of Definition 2 formally captures alternative 1.

6 Games vs Epistemic XSTIT Frames

The original STIT logic does not include a knowledge modality and, thus, its standard semantics does not contain an equivalence relation on states. Broersen, Herzig, and Troquard propose a STIT-extension of ATL and also define an epistemic version of this extension [Broersen et al., 2006]. In [Broersen et al., 2007] they discuss a possibility of adding knowledge modality to NCL, a version of STIT, and claim completeness without a proof. The most detailed account of their epistemic extension of STIT and its semantics in terms of epistemic XSTIT frames is given in [Broersen, 2011]. In this section we compare this work with ours.

The standard semantics of STIT is defined with respect to dynamic states or pairs of a history and a state in the history. History roughly corresponds to our notion of a play. As we mentioned earlier, there are three forms of knowledge that can be considered for any action: ex ante (before action), interim (at the moment of action), and ex post (after outcome is known). Ex ante knowledge is defined in terms of indistinguishable initial states, interim knowledge - in terms of indistinguishable initial states and equal actions, and ex post knowledge - in terms of indistinguishable initial state, equal actions, and indistinguishable outcomes. Item 5(a) of Definition 2 refers to interim knowledge because it requires states α and α′ be indistinguishable and actions δ(a) and δ′ (a) be the same. Item 5(b) of Definition 2 refers to ex ante knowledge because it only requires states to be indistinguishable, but allows actions δ(a) and δ′ (a) to be different.

4 We also include an outcome ω because we want to be able to reason about a more general class of nondeterministic games in which an outcome is not uniquely determined by the actions.

Epistemic XSTIT frames define knowledge through an indistinguishably relation on dynamic states. [Broersen, 2011] states "if we let uncertainty range over dynamic states, as for the present logic, we can talk about knowledge of what agents are doing". However, epistemic XSTIT frames do not include any condition that connects relation Ra, representing agent's actions, with relation ∼a, representing agent's knowledge. As a result, the knowledge modality could be potentially interpreted as capturing any of the three forms of knowledge we discussed above. In fact, because histories include future states, the same knowledge modality could also be interpreted as capturing knowledge of a fortune-teller who can see the future. [Broersen, 2011, p.147] uses this very abstract knowledge modality to express what is supposed to be an equivalent version of our modality ST:

The first conjunct on the right-hand-side of the above formula states that the agent knows (modality K) that her action would unavoidably lead (modality [a xstit]) to statement ϕ being true. This conjunct intends to express condition 5(a) of Definition 2. Since the agent's action is not fixed at ex ante time, modality Ka must refer to interim knowledge, just like our condition 5(a). At the same time, the second conjunct states that the agent does not know (modality K) that her action unavoidably lead (the combination of modalities □X) to statement ϕ being true. This statement intends to express condition 5(b) of Definition 2. Note that knowledge here should be ex ante because once the agent's action is fixed, statement ϕ is guaranteed to be true (as per first conjunct). Therefore, in order to faithfully capture the intended meaning, the two instances of modality K on the right-hand-side of equation (1) must refer to two different forms of knowledge: ex ante and interim, which is not the case for epistemic XSTIT frames.

A version of epistemic STIT logic that distinguishes ex ante, interim, and ex post forms of knowledge is proposed in [Lorini et al., 2014]. Their notion of active agentive responsibility is the one captured by ST modality in the current paper. They study the decidability of the satisfiability problem, but do not propose an axiomatization. In this paper we distinguish the two forms of knowledge in items 5(a) and 5(b) of Definition 2 and we use modality K to represent ex ante knowledge. Our main technical results are the definability of modality B through ST and a sound and complete logical system capturing the properties of modality ST.

7 Definability of B through ST

In this section we show that blameworthiness modality B is expressible through seeing to it modality ST. In the next section, we show that the opposite is false.

Proof. (⇒) : By item 6 of Definition 2, the assumption (α, δ, ω) ⊩ Baϕ implies that

and that there is an action d ∈ ∆αa such that for each play (α′ , δ′ , ω′ ) ∈ P ,

Due to statement (2), it suffices to show that

We prove this statement by verifying the two claims below.

PROOF OF CLAIM. Statement (2) implies that (α′′ , δ′′ , ω′′ ) ⊮ STa¬ϕ by item 5 of Definition 2 because α ∼a α′′ and δ(a) = δ′′ (a). Therefore, (α′′ , δ′′ , ω′′ ) ⊩ ¬STa¬ϕ by item 2 of Definition 2. ⊠

Let δ0 be any action profile in state α such that δ0(a) = d. Such an action profile exists because the domain of actions of each agent in state α is not empty by item 3 of Definition 1. Then, by condition 5(b) of Definition 1, there must exist at least one outcome ω0 such that (α, δ0, ω0) ∈ P .

PROOF OF CLAIM. Recall that δ0(a) = d by the choice of action profile δ0. Thus, (α′ , δ′ , ω′ ) ⊮ ϕ for each play (α′ , δ′ , ω′ ) ∈ P such that α ∼a α′ and δ0(a) = δ′ (a) by statement (3). At the same time (α, δ, ω) ⊩ ϕ by statement (2). Therefore, (α, δ0, ω0) ⊩ STa¬ϕ by item 5 of Definition 2. ⊠

Claims 1 and 2 imply statement (4) by item 5 of Definition 2.

and (α, δ, ω) ⊩ STa¬STa¬ϕ. The latter, by item 5(b) of Definition 2, implies that there is a play (α′ , δ′ , ω′ ) ∈ P such that

and (α′ , δ′ , ω′ ) ⊮ ¬STa¬ϕ. Thus, (α′ , δ′ , ω′ ) ⊩ STa¬ϕ by item 2 of Definition 2. Then, for each play (α′′ , δ′′ , ω′′ ) ∈ P ,

by item 5(a) of Definition 2. Let action d be δ′ (a) ∈ ∆α′ a . Thus, d ∈ ∆αa by item 3 of Definition 1 and statement (6). Then, by statement (6) and statement (7), for any play (α′′ , δ′′ , ω′′ ) ∈ P ,

Therefore, (α, δ, ω) ⊩ Baϕ by item 6 of Definition 2 and statement (5). ⊠

8 Undefinability of ST through B and K

As we have seen in Theorem 1, blameworthiness modality B could be defined through seeing to it modality ST. In this section we show that modality ST cannot be defined in language ΦB . To prove this, we construct two games and define a common play for both games such that a formula ϕ ∈ ΦB is satisfied under this play in the first game if and only if it is satisfied under the same play in the second game. We also give a formula which is satisfied in the first game but not in the second game under the constructed play. The first result, in a more general form, is stated in this section as Lemma 4 and the second as Lemma 5 and Lemma 6. The undefinability is formally stated as Theorem 2 at the end of this section.

The two games are depicted in Figure 3. Each game has a single agent, Alice. In other words, A = {Alice}. Both games have a single initial state α and two outcomes: ω1 and ω2. In both games, Alice has three actions (a, b, and c) in state α. In both games, propositional variable 5 p holds only on plays that result in outcome ω1. In both games, action a leads to outcome ω1 and action c leads (nondeterministically) to outcome ω1 or outcome ω2. The only difference between the two games is how action b is executed. In the first game, action b acts the same way as action a and in the second game it acts the same way as action c, see Figure 3.

We refer to the two games from Figure 3 as the left and the right games. The sets of plays of these two games are denoted by Pl and Pr, respectively. Satisfiability relations corresponding to those games are denoted by ⊩l and ⊩r. Valuation functions for the two games will be denoted by πl and πr. Note that πl(p) = πr(p) = {(α, x, ω1) | x ∈ {a, b, c}} by the choice of the games.

Recall that an action profile is a function that maps agents into actions. Since Alice is the only agent in these two games, we refer to an action profile by the action of Alice under the profile. The play (α, b, ω1) is the common play of these two games that we use to show the undefinability of modality ST in language ΦB .

As mentioned above, Lemma 4 is a key step in the proof of the undefinability. Before proving this lemma, we establish three auxiliary results. First, observe that sets Pl and Pr are not equal because (α, b, ω2) ∈ Pr \ Pl. However, the set of plays that use actions a and c is the same for both games.

Lemma 1. (α, δ, ω) ∈ Pl iff (α, δ, ω) ∈ Pr for any action δ ∈ {a, c} and any outcome ω ∈ {ω1, ω2}. ⊠

5 We assume here that the language contains only one propositional variable. If the language contains more variables, satisfaction relation of all of them should be defined the same way as p.

Second, observe that plays (α, a, ω1) and (α, b, ω1) in the left game are indistinguishabile in language ΦB .

The third lemma establishes that actions b and c in the right game are indistinguishabile in language ΦB . The proof of this lemma is similar to the proof of Lemma 2.

The next lemma is one of the two key steps in the proof of undefinability. It shows that for any common play of the two games, the same formulae are satisfied on this play under both games. Of course, play (α, b, ω2) ∈ Pr \ Pl is excluded.

Lemma 4. (α, δ, ω) ⊩l ϕ iff (α, δ, ω) ⊩r ϕ for each formula ϕ ∈ ΦB and each play (α, δ, ω) ∈ Pl.

Proof. We prove the lemma by structural induction on formula ϕ. If ϕ is a propositional variable p, then (α, δ, ω) ⊩l p iff (α, δ, ω) ⊩r p by Definition 2 and because πl(p) = πr(p). The case when formula ϕ is a negation or an implication follows from the induction hypothesis and items 2 and 3 of Definition 2 respectively.

Suppose that formula ϕ has the form KAliceψ. Recall that there is only one state that Alice cannot distinguish from state α - the state α itself.

(⇒) : Assume that (α, δ, ω) ⊩l KAliceψ. Thus, (α, δ′ , ω′ ) ⊩l ψ for each play (α, δ′ , ω′ ) ∈ Pl by item 4 of Definition 2. Hence, by the induction hypothesis, (α, δ′ , ω′ ) ⊩r ψ for each play (α, δ′ , ω′ ) ∈ Pl. Then, (α, δ′ , ω′ ) ⊩r ψ for each (α, δ′ , ω′ ) ∈ Pr because Pr = Pl ∪ {(α, b, ω2)} and due to Lemma 3.

(⇐) : Suppose that (α, δ, ω) ⊩r KAliceψ. Then, (α, δ′ , ω′ ) ⊩r ψ for each play (α, δ′ , ω′ ) ∈ Pr by item 4 of Definition 2. Hence, (α, δ′ , ω′ ) ⊩r ψ for each play (α, δ′ , ω′ ) ∈ Pl because Pl ⊆ Pr. Thus, by the induction hypothesis, (α, δ′ , ω′ ) ⊩l ψ for each play (α, δ′ , ω′ ) ∈ Pl. Therefore, (α, δ, ω) ⊩l KAliceψ by item 4 of Definition 2.

Finally, suppose that formula ϕ has the form BAliceψ. (⇒) : Let (α, δ, ω) ⊩l BAliceψ for some play (α, δ, ω) ∈ Pl. Hence, by item 6 of Definition 2,

and ∃x ∈ {a, b, c} ∀(α, x, ω′ ) ∈ Pl ((α, x, ω′ ) ⊮l ψ). Thus, by Lemma 2,

Then, by the induction hypothesis,

Hence, by Lemma 1,

In addition, (α, δ, ω) ⊩r ψ also by the induction hypothesis using statement (8). Therefore, (α, δ, ω) ⊩r BAliceψ by item 6 of Definition 2.

(⇐) : Suppose (α, δ, ω) ⊩r BAliceψ. Thus, by item 6 of Definition 2,

and ∃x ∈ {a, b, c} ∀(α, x, ω′ ) ∈ Pr ((α, x, ω′ ) ⊮r ψ). Then, by Lemma 3,

Hence, by Lemma 1,

Thus, by the induction hypothesis,

In addition, (α, δ, ω) ⊩l ψ also by the induction hypothesis using statement (9). Therefore, (α, δ, ω) ⊩l BAliceψ by item 6 of Definition 2. ⊠

Informally, the next two lemmas are true because by choosing action b in the left model the agent knows that statement p will be unavoidably true, while the same is not true about the right model. Formally, statements of the lemmas follow from the definitions of the left and the right models and item 5 of Definition 2.

The statement of the next theorem follows from Lemma 4, Lemma 5, and Lemma 6.

Theorem 2. Modality ST is not definable in the language ΦB .

9 Conclusion

In this paper we study the ex ante knowledge modality and two responsibility modalities: "seeing to it" and "being blamable". We observed that "being blamable" could be defined through "seeing to it" and have shown that the converse is not true.

In the future, we plan to develop a complete logical system describing the interplay between modalities K and ST in language ΦST . Such a logical system would be different from the epistemic version of STIT described in [Broersen, 2011]. This is because our semantics is based on the strategic games with imperfect information semantics rather than properties of epistemic XSTIT frames. Furthermore, as we discussed in Section 6, we interpret K as ex ante knowledge instead of a very general notion of knowledge modeled by epistemic XSTIT frames. As a result, our system would contain new logical principles such as Kaϕ → ¬STaϕ. This axiom is sound if modality Ka represents the ex ante knowledge, as in the proposed system, but is not sound, for example, if Ka represents the interim knowledge.