# intelligence_in_strategic_games__5493507c.pdf

Journal of Artiﬁcial Intelligence Research 71 (2021) 521-556 Submitted 04/2021; published 07/2021

Intelligence in Strategic Games

Pavel Naumov pgn2@cornell.edu King s College, Wilkes-Barre, Pennsylvania, 18711 USA

Yuan Yuan yyuan@vassar.edu Vassar College, Poughkeepsie, New York, 12604 USA

If an agent, or a coalition of agents, has a strategy, knows that she has a strategy, and knows what the strategy is, then she has a know-how strategy. Several modal logics of coalition power for know-how strategies have been studied before. The contribution of the article is three-fold. First, it proposes a new class of know-how strategies that depend on the intelligence information about the opponents actions. Second, it shows that the coalition power modality for the proposed new class of strategies cannot be expressed through the standard know-how modality. Third, it gives a sound and complete logical system that describes the interplay between the coalition power modality with intelligence and the distributed knowledge modality in games with imperfect information.

1. Introduction

The Battle of the Atlantic was a classical example of the matching pennies game. British (and American) admirals were choosing routes of the allied convoys and the Germans picked routes of their U-boats. If their trajectories crossed, the Germans scored a win, if not the allies did. Neither of the players appeared to have a strategy that would guarantee a victory. The truth, however, was that during the most of the battle one of the sides had exactly such a strategy. First, it was the British who broke German Enigma cipher in summer of 1941. Although the Germans did not know about the British success, they changed codebook and added fourth wheel to Enigma in February 1942 thus preventing the British from decoding German messages. The very next month, in March 1942, German navy cryptography unit, B-Dienst, broke the allied code and got access to convoy route information. The Germans lost their ability to read allied communication in December 1942 due to a routine change in the allied codebook. The same month, the British were able to read German communication as a result of capturing codebook from a U-boat in Mediterranean. In March 1943, the Germans changed codebook again and, unknowingly, disabled British ability to read German messages. Simultaneous, the Germans caught up and started to decipher British transmissions again (Budiansky, 2002; Showell, 2003). At almost any moment during these two years one of the sides was able to read the communications of the other side. However, the two sides never have been able to read each other s messages at the same time to notice that the other side knows more than it should have known. As a result, neither of them was able to ﬁgure out that their own code is insecure. Finally, in May 1943, with the help of US Navy, the British cracked German messages while the Germans still were reading British. It was the ﬁrst time the allies

c 2021 AI Access Foundation. All rights reserved.

Pavel Naumov and Yuan Yuan

understood that their code was insecure. A new convoy cipher was immediately introduced and the Germans have never been able to break it again, while the allies continued reading Enigma-encrypted transmissions till the end of the war (Budiansky, 2002). In this article, we study coalition power in strategic games assuming that the coalition has intelligence information about the moves of all or some of its opponents. Throughout the article, we refer to the information about the future actions of the other agents simply as the intelligence . We write [C]Iϕ if a coalition C has a strategy to achieve an outcome ϕ in one step as long as the coalition has the intelligence about the move of each agent in set I. For example, [British]Germans(Convoy is saved).

As another example, consider the road situation depicted in Figure 1. Here, a busy threelane highway is merging into a two-lane one. Drivers of cars a and b need to coordinate in

Figure 1: A road situation.

order to avoid the collision. Each of them has two possible actions: to accelerate or to slow down. If both drivers choose the same action, the cars will collide. If they choose diﬀerent actions, the accident will be avoided. First, suppose that each of the drivers is choosing an action not knowing what the other driver will do. In this case, the drivers might get lucky and avoid the collision, but neither of them has a strategy to avoid it:

[a] (Collision is avoided.) [b] (Collision is avoided.).

Suppose now that cars a and b are self-driving vehicles that can use, for example, radio signals to warn other cars about their chosen course of actions. In this case, self-driving car a has a strategy to unilaterally prevent collision as long as it knows the forthcoming action of car b. The opposite, of course, is also true:

[a]b(Collision is avoided.) [b]a(Collision is avoided.).

An important class of strategic games with intelligence is Stackelberg security games. These games have been used by the U.S. Transportation Security Administration, the U.S. Federal Air Marshal Service, the U.S. Coast Guard, and others (Sinha, Fang, An, Kiekintveld, & Tambe, 2018). An example of a security game is captured in Table 1. Here, one of the two agents, the attacker, is trying to inﬂict the greatest damage on a two-terminal airport. The defender is trying to minimize the damage. The attacker has two strategies: Attack Terminal 1 and Attack Terminal 2. The defender, constrained by the budget, has only a single security oﬃcer who could be placed at either of the two terminals. It is usually assumed in security games that the defender employs a mixed strategy by asking the agent to randomly visit both terminals. The mixed strategy of the defender could be expressed as

Intelligence in Strategic Games

(100,0) (50,50) (0,100)

Attack Terminal 1 10 55 100 Attack Terminal 2 200 110 20

Table 1: Expected values of damage to the airport.

pair (w1, w2), where w1 and w2 are percentages of time the security oﬃcer spends at the ﬁrst and the second terminals, respectively. For the sake of simplicity, we restrict the defender to mixed strategies (100, 0), (50, 50), and (0, 100). The expected value of the damage to the airport under diﬀerent action proﬁles is shown in Table 1. For example, if the defender chooses mixed strategy (50, 50) and the attacker targets the ﬁrst terminal, then, of course, there could be a smaller or a larger damage to the terminal depending on where the security oﬃcer is at the moment of the attack. However, the expected value of this damage, per Table 1, is 55 units. Note that in this setting the attacker has a strategy to guarantee that the expected value of the damage is at least 20 units. The strategy consists in targeting the second terminal and it does not depend on any intelligence:

[Attacker] (Expected value of damages is at least 20 units).

At the same time, the attacker does not have a strategy to guarantee that the expected value of the damage is at least 30 units:

[Attacker] (Expected value of damages is at least 30 units).

It is the standard assumption in security games that the attacker has the intelligence about the mixed strategy used by the defender. In our example, it would be assumed that the attacker visits the airport multiple number of times while preparing for the attack. During these visits the attack observes the frequencies of the placement of the security oﬃcer at the two terminals and learns the mixed strategy used by the defender. If the attacker knows the mixed strategy of the defender, then the attacker has a strategy to force a signiﬁcantly larger expected value of the damages to the airport:

[Attacker]Defender(Expected value of damages is at least 100 units).

In general, security games can be viewed as two-player perfect-information strategic games where one of the players, the attacker, has the intelligence about the other player, the defender. Modality [C] ϕ is the coalitional power modality proposed by Marc Pauly (Pauly, 2001, 2002). He gave a sound and complete axiomatization of this modality in the case of perfect information strategic games. Variations of his logic has been studied before (Goranko, 2001; van der Hoek & Wooldridge, 2005; Sauro, Gerbrandy, van der Hoek, & Wooldridge, 2006; Borgo, 2007; Agotnes, van der Hoek, & Wooldridge, 2009; Agotnes, Balbiani, van Ditmarsch, & Seban, 2010; Goranko, Jamroga, & Turrini, 2013; Belardinelli, 2014; Goranko & Enqvist, 2018). Strategic power modality with intelligence [a1, . . . , an]i1,...,ikϕ can be

Pavel Naumov and Yuan Yuan

expressed in Strategy Logic (Chatterjee, Henzinger, & Piterman, 2010; Mogavero, Murano, Perelli, & Vardi, 2014) as

t1 . . . tk s1, . . . sn(a1, s1) . . . (an, sn)(i1, t1) . . . (ik, tk)Xϕ,

where (a, s) stands for agent a uses strategy s and X stands for on the next step . The literature on the strategy logic covers model checking (Berthon, Maubert, Murano, Rubin, & Vardi, 2017), synthesis (ˇCerm ak, Lomuscio, & Murano, 2015), decidability (Mogavero, Murano, Perelli, & Vardi, 2012, 2017), and bisimulation (Belardinelli, Dima, & Murano, 2018). We are not aware of any completeness results for a strategy logic with quantiﬁers over strategies. At the same time, our approach is diﬀerent from the one in Alternating-time Temporal Logic with Explicit Strategies (ATLES) (Walther, van der Hoek, & Wooldridge, 2007). There, modality C ρ denotes the existence of a strategy of coalition C for a ﬁxed commitment ρ of some of the other agents. Unlike ATLES, our modality [C]B denotes existence of a strategy of a coalition C for any commitment of coalition B, as long as it is known to C. Goranko and Ju proposed several strategic power modalities that are similar to our coalition power with intelligence modality, gave formal semantics of these modalities, and discussed matching notions of bisimulation (Goranko & Ju, 2019). They did not introduce any axioms for these modalities. We compare our work to their in Section 5. Strategic games could be generalized to strategic games with imperfect information. Unlike perfect information strategic games, the initial state in an imperfect information game could be unknown to the players. For example, consider a hypothetical setting in which a British convoy and a German U-boat have to choose between three routes from point A to point B: route 1, route 2, and route 3, see Figure 2. Let us furthermore assume that it is known to both sides that one of these routes is blocked by Russian naval mines. Although the mines are located along route 1, neither the British nor the Germans know this. If the British have an access to the intelligence about German U-boats, then, in theory, they have a strategy to save the convoy. For example, if the Germans will use route 2, then the British can use route 3. However, since the British do not know the location of the Russian mines, even after they receive information about German plans, they still would not know how to save the convoy.

Figure 2: Three routes from point A to point B.

Multiple aspects of games with imperfect information have been studied in the ﬁeld of artiﬁcial intelligence. Liu, Zheng, Li, Bian, Song developed a machine learning algorithm to play real-time strategy games with imperfect information (2019). Sandholm designed an AI agent outperforming professional poker players (2017). Another poker player was developed by Tammelin, Burch, Johanson, and Bowling (2015). Jiang, Li, Du, Chen, and Fang used

Intelligence in Strategic Games

deep reinforcement learning to construct a human-expert level algorithm for Doudizhu, a three-player imperfect information game (2019). Buro, Long, Furtak, and Sturtevant presented world s ﬁrst computer player for Skat, Germany s national card game with imperfect information (2009). Wisser developed a perfect information Monte Carlo sampling agent for playing Schnapsen, a Central European card game with imperfect information (2015). Parker, Nau, and Subrahmanian analysed algorithms for kriegspiel chess, an imperfectinformation variant of chess (2006). Belardinelli, Lomuscio, and Malvone developed perfect information abstraction method for verifying strategic properties in multi-agent systems with imperfect information (2019). Schmid, Moravcik, and Hladik studied the dependency between the level of uncertainty in games with imperfect information and the minimum support size of a Nash equilibrium (2014). Belle and Lakemeyer proposed to model imperfect information games in a multi-agent epistemic variant of the situation calculus (2010). Burch, Johanson, and Bowling proposed a technique for decomposing imperfect information games into subgames (2014). Sevenster studied the complexity of decision making in the Battleships game (2004). Bard et al. explored various properties of the Hanabi game (2020). Van Ditmarsch proposed an extension of the epistemic logic for reasoning about game actions (2002). Van der Hoek and Wooldridge combined ATL with epistemic modality to form Alternating-Time Temporal Epistemic Logic capable of reasoning about games with imperfect information (2003). It has been suggested in several recent works that, in the case of the games with imperfect information, strategic power modality in Marc Pauly logic should be restricted to existence of know-how1 strategies ( Agotnes & Alechina, 2019; Naumov & Tao, 2017a; Fervari, Herzig, Li, & Wang, 2017; Naumov & Tao, 2018b, 2018c, 2018a; Cao & Naumov, 2020). That is, modality [C]ϕ should stand for coalition C has a strategy, it distributively knows that it has a strategy, and it distributively knows what the strategy is . In this article we adopt this approach to strategic power with intelligence. For example, in the imperfect information setting depicted in Figure 2, after receiving the intelligence report, the British have a strategy, they know that they have a strategy, but they do not know what the strategy is: [British]Germans(Convoy is saved).

At the same time, since the Russians presumably know the location of their mines,

[British, Russians]Germans(Convoy is saved).

This article contains two main technical results. First, we show that know-how with intelligence modality [C]Iϕ cannot be deﬁned through the standard know-how modality. Second, we give a complete logical system that describes the interplay between the coalition power with intelligence modality [C]I and the distributed knowledge modality KC in the imperfect information setting. The most interesting axiom of our system is a generalized version of Marc Pauly s (2001, 2002) Cooperation axiom that connects intelligence I

1. Know-how strategies were studied before under diﬀerent names. While Jamroga and Agotnes talked about knowledge to identify and execute a strategy (2007), Jamroga and van der Hoek discussed difference between an agent knowing that he has a suitable strategy and knowing the strategy itself (2004). Van Benthem called such strategies uniform (2001). Wang gave a complete axiomatization of knowing how as a binary modality (2015, 2018), but his logical system does not include the knowledge modality.

Pavel Naumov and Yuan Yuan

and coalition C parameters of the modality [C]I. Our proof of the completeness is significantly diﬀerent from the existing proofs of completeness for games with imperfect information ( Agotnes & Alechina, 2019; Naumov & Tao, 2017a, 2018b, 2018c, 2018a; Cao & Naumov, 2020). We highlight these diﬀerences in the beginning of Section 9.

The rest of the article is organized as follows. In the next section, we give a formal definition of games with imperfect information that serve as models for our logical system. In Section 4, we describe the syntax and the formal semantics of our logical system. In Section 5, we compare our approach to the one in (Goranko & Ju, 2019). In Section 6, we show that modality [C]Bϕ cannot be expressed through the original know-how modality. Section 7 lists the axioms and the inference rules of the system. We discuss the axioms and prove their soundness in Section 8. The proof of the completeness is given in Section 9, respectively. Section 10 concludes.

3. Games with Imperfect Information

For any sets X and Y , by XY we mean the set of all functions from Y to X. Throughout the article we assume a ﬁxed (possibly inﬁnite) set of agents A and a nonempty set of propositional variables.

Deﬁnition 1 A game is a tuple (W, { a}a A, , M, π), where

1. W is a set of states,

2. a is an indistinguishability equivalence relation on set W for each agent a A,

3. is a nonempty set, called the domain of actions ,

4. M W A W is a relation called aggregation mechanism ,

5. π is a function that maps propositional variables to subsets of W.

A function δ from set A is called a complete action proﬁle. Figure 3 depicts a diagram of the Battle of the Atlantic game with imperfect information as described in the introduction. For the sake of simplicity, we treat the British, the Germans, and the Russians as single agents, not groups of agents. The game has ﬁve states: 1, 2, 3, s, and d. States 1, 2, and 3 are three initial states that correspond to possible locations of Russian mines along route 1, route 2, or route 3. Neither the British nor the Germans can distinguish these states, which is shown in the diagram by labels on the dashed lines connecting these three states. The Russians know location of the mines, and, thus, they can distinguish these states. The other two states are ﬁnal states s and d that describe if the convoy made it safe (s) or was destroyed (d) by either a U-boat or a mine. The designation of some states as initial and others as ﬁnal is speciﬁc to the Battle of the Atlantic game. In general, our Deﬁnition 1 does not distinguish between such states and we allow games to take multiple consecutive transitions from one state to another.

Intelligence in Strategic Games

11,22,31,32,33

11,12,13,22,33

11,21,22,23,33

British, Germans

British, Germans

Figure 3: Battle of the Atlantic with imperfect information.

The domain of actions in this game is {1, 2, 3}. For the British and the Germans actions represent the choice of routes that they make for their convoys and U-boats respectively. The Russians are passive players in this game. Their action does not aﬀect the outcome of the game. Technically, a complete action proﬁle is a function δ from set {British, Germans, Russians} into set {1, 2, 3}. Since, there are only three players in the Battle of the Atlantic game, it is more convenient to represent function δ by triple bgr {1, 2, 3}3, where b is the action of the British, g is the action of the Germans, and c is the action of the Russians. The mechanism M of the Battle of the Atlantic game is captured by the directed edges in Figure 3 labeled by complete action proﬁles. Since value r in a proﬁle bgr does not aﬀect the outcome, it is omitted on the diagram. For example, directed edge from state 1 to state s is labeled with 23 and 32. This means that the mechanism M contains triples (1, 231, s), (1, 232, s), (1, 233, s), (1, 321, s), (1, 322, s), and (1, 323, s). The deﬁnition of a game that we use here is more general than the one used in the original Marc Pauly s semantics of the logic of coalition power. Namely, we assume that the mechanism is a relation, not a function. On one hand, this allows us to talk about nondeterministic games where for each initial state and each complete action proﬁle there might be more than one outcome. On the other hand, this also allows no outcome to exist for some combinations of the initial states and the complete action proﬁles. If in a given state under a given complete action proﬁle there is no next state, then we interpret this as termination of the game. This resembles a user choosing to quit a computer application: once the quit button is pressed, the application terminates without reaching any new state. If needed, games with termination can be excluded and an additional axiom [C] be added to the logical system. The proof of the completeness will remain mostly unchanged.

Deﬁnition 2 For any states w, w W and any coalition C, let w C w if w a w for each agent a C.

In particular, w w for any two states of the game.

Lemma 1 For any coalition C, relation C is an equivalence relation on set W.

Pavel Naumov and Yuan Yuan

4. Syntax and Semantics

In this section, we deﬁne the syntax and the semantics of our formal system. By a coalition we mean any ﬁnite subset of the set of all agents A. Finiteness of coalitions will be important for the proof of the completeness.

Deﬁnition 3 Let Φ be the minimal set of formulae such that

1. p Φ for each propositional variable p,

2. ϕ ψ, ϕ Φ for all ϕ, ψ Φ,

3. KCϕ Φ for each formula ϕ Φ and each coalition C A,

4. [C]Bϕ Φ for each formula ϕ Φ and all disjoint coalitions B, C.

In other words, the language of our logical system is deﬁned by grammar:

ϕ := p | ϕ | ϕ ϕ | KCϕ | [C]Bϕ,

where coalitions C and B are disjoint. Formula KCϕ stands for coalition C distributively knows ϕ and formula [C]Bϕ for coalition C distributively knows strategy to achieve ϕ as long as it gets the intelligence on actions of coalition B . We assume that Boolean constants and are deﬁned through negation, implication, and a propositional variable in the standard way. By an action proﬁle of a coalition C we mean any function from set C. For any two functions f, g, we write f =X g if f(x) = g(x) for each x X. Next is the key deﬁnition of this article. Its part 5 gives the semantics of modality [C]B. This part uses state w to capture the fact that the strategy succeeds in each state indistinguishable by coalition C from the current state w. In other words, the coalition C knows that this strategy will succeed. Except for the addition of coalition B and its action proﬁle β, this is essentially the same deﬁnition as the one used in ( Agotnes & Alechina, 2019; Naumov & Tao, 2017a; Fervari et al., 2017; Naumov & Tao, 2017b, 2018c, 2018b, 2018a).

Deﬁnition 4 For any game (W, { a}a A, , M, π), any state w W, and any formula ϕ Φ, let satisﬁability relation w ϕ be deﬁned as follows:

1. w p, if w π(p), where p is a propositional variable,

2. w ϕ, if w ϕ,

3. w ϕ ψ, if w ϕ or w ψ,

4. w KCϕ, if w ϕ for each w W such that w C w ,

5. w [C]Bϕ, if for any action proﬁle β B of coalition B there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ.

Intelligence in Strategic Games

For example, for the game depicted in Figure 3,

1 [British, Russians]Germans(Convoy is saved).

Indeed, statement 1 British, Russians w is true only for one state w W, namely state

1 itself. Then, for any action proﬁle β {1, 2, 3}{Germans} of the single-member coalition {Germans} we can deﬁne action proﬁle γ {1, 2, 3}{British, Russians} as, for example,

3, if a = British and β(Germans) = 2, 2, if a = British and β(Germans) = 3, 1, if a = Russians.

In other words, if proﬁle β assigns the Germans route 2, then proﬁle γ assigns the British route 3 and vice versa. Assignment of an action to the Russians in not important. This way, no matter what the Germans action is, the British convoy will avoid both the German U-boat and the Russian mines in the game that starts from state w = 1. At the same time,

1 [British]Germans(Convoy is saved).

because the British cannot distinguish states 1, 2, and 3 without the Russians. In other words, 1 British w for any state w {1, 2, 3}. Thus, for each action proﬁle β {1, 2, 3}{Germans} we need to have a single action proﬁle γ {1, 2, 3}{British, Russians}

that would bring the convoy to state s from any of the states 1, 2, and 3. Such proﬁle γ does not exist because, even if the British know where the Germans U-boat will be, there is no single strategy to choose path that would avoid Russian mines from all three indistinguishable states 1, 2, and 3. Note that item 4 of Deﬁnition 4 interprets the knowledge modality KC as distributed knowledge of coalition C. Similarly, the knowledge of how , implicitly referred to by item 5 of the same deﬁnition through indistinguishability relation C, is also distributed knowledge of coalition C. Thus, even if a coalition knows how to achieve ϕ, it is possible that no single individual member of the coalition might know how to do this. In order for the coalition to execute a strategy that it knows, its members might need to communicate with each other to assemble the distributed knowledge. The mechanism and the result of such a communication is not a trivial issue. For example, if a statement ϕ is distributively known to a coalition, then ϕ might even be false after such a communication ( Agotnes & W ang, 2017). In this article, following the existing tradition in the logics of distributively knowing strategy, we investigate the properties of distributed knowledge on an abstract level, without considering the communication between the agents required to execute the strategy. Of course, one can potentially consider the other forms of group knowledge such as individual knowledge (each agent in the group knows) and common knowledge. However, know-how strategies based on either of the last two forms of knowledge do not satisfy the Cooperation axiom listed in Section 4. As a result, they are signiﬁcantly less interesting from the logical point of view. Finally, observe that the formula K ϕ means that statement ϕ is satisﬁed in all states of the game. Modality K is sometimes referred to as universal modality.

Pavel Naumov and Yuan Yuan

5. Conditional Strategic Modalities

In this section, we compare our know-how with the intelligence modality and the conditional strategic modalities of Goranko and Ju (2019). Throughout this section, we consider only games with perfect information. In other words, we assume that for each agent a A, equivalence relation a is the equality. We make this assumption because (Goranko & Ju, 2019), unlike us, only considers such a setting. Before proceeding further, let us deﬁne B ϕ to be the set of all action proﬁles of a coalition B that guarantee outcome ϕ.

Deﬁnition 5 B ϕ is the set of all action proﬁles β B of coalition B such that for any complete action proﬁle δ A and any state u W if β =B δ and (w, δ, u) M, then u ϕ.

It is easy to see that, in the perfect information setting, item 4 of Deﬁnition 4 could be rephrased in the following equivalent form:

w [C]Bϕ, if for each action proﬁle β B of coalition B, there is an action proﬁle γ C of coalition C such that β γ B C ϕ .

Modality [C]Bϕ includes ϕ, the goal of coalition C but this modality puts no constrain on the goal (or the actions) of coalition B. Note that the strategic abilities of the coalition C increase if coalition B commits to acting towards a certain goal ψ. Goranko and Ju proposed modalities [C]1 B:ψϕ, [C]2 B:ψϕ, and [C]3 B:ψϕ that capture this observation in three diﬀerent ways. Modality [C]1 B:ψϕ states that coalition C has a strategy to achieve ϕ as long as coalition B is using a strategy to achieve ψ. It is assumed that coalition C does not known ex ante (before it acts) the speciﬁc strategy to be used by coalition B:

w [C]1 B:ψϕ when there is an action proﬁle γ C of coalition C such that for each action proﬁle β B of coalition B, if β B ψ , then β γ B C ϕ .

b1 ϕ, ψ ψ b2 ϕ, ψ ψ b3 ψ

b1 ϕ, ψ ψ b2 ψ ϕ, ψ b3 ψ

b1 ϕ, ψ ψ b2 ψ ψ b3 ψ

Figure 4: A strategic game with three initial states.

As an example, consider the two-player perfect-information deterministic game depicted in Figure 4. Here, the ﬁrst player has strategies: b1, b2, and b3 and the second player has strategies c1 and c2. The game has three initial states, that we refer to as left , middle , and right states. These initial states correspond to the three tables in Figure 4. The game also has 18 ﬁnal states corresponding to the cells of the tables. The tables shows which of the statements ϕ and ψ are true in each ﬁnal state. For example, if the game starts in

Intelligence in Strategic Games

left initial state (see left table), the ﬁrst player uses action b2, and the second player uses action c1, then both formulae, ϕ and ψ, are satisﬁed in the outcome. We refer to the ﬁrst and the second player in this game as agent b and agent c, respectively. Note that in the left state agent c can force ψ to be true in the outcome by using action c1. This is true no matter what action agent b decides to take. We can express this as

left [c]1 b: ψ,

where the true constant represents the trivial goal which is achieved by any action. At the same time, in the left state, agent c does not have a strategy to unilaterally achieve ϕ:

left [c]1 b: ϕ.

However, if agent b has a goal of achieving ψ, then she is guaranteed to use either action b1 or action b2, see Figure 4 (left). Knowledge of this gives agent c a strategy (use action c1) to achieve ϕ from the left state of the game:

left [c]1 b:ψϕ.

Note that the same is not true in the middle state of the game

middle [c]1 b:ψϕ

because, see Figure 4 (middle), in the middle state, even if agent b is using only either action b1 or action b2 agent c does not have a strategy that is guaranteed to achieve ϕ. However, agent c does have such a strategy if she knows ex ante which of the two strategies (b1 or b2) agent b will use. In general,

w [C]2 B:ψϕ when for each action proﬁle β B ψ of coalition B, there is an action proﬁle γ C of coalition C such that β γ B C ϕ .

In our case, if agent b uses action b1, then agent c can choose action c1; if agent b uses action b2, then agent c can choose action c2. In either case, agent c will force ϕ. Thus,

middle [c]2 b:ψϕ.

Note that the same is not true in the right state of the game:

right [c]2 b:ψϕ

because in the right state agent b might use action b1 to achieve ψ, which would prevent agent c from achieving ϕ, see Figure 4 (right). At the same time, in the right state agent b can choose to achieve her goal ψ in such a way that it would allow agent c to achieve her own goal of ϕ. In general,

w [C]3 B:ψϕ when there is an action proﬁle β B ψ of coalition B and an action proﬁle γ C of coalition C such that β γ B C ϕ .

Pavel Naumov and Yuan Yuan

In our example, because agent b can choose action b1 to help c,

right [c]3 b:ψϕ.

Our modality [C]Bϕ could be expressed through [C]2 B:ψϕ as [C]Bϕ [C]2 B: ϕ. In the forthcoming journal version of their work, Goranko and Ju propose axioms for modalities [C]1 B:ψϕ, [C]2 B:ψϕ, and [C]3 B:ψϕ in perfect information setting, but do not prove their completeness (Goranko & Ju, 2021). One of the main contributions of the current article is a complete axiomatization of the interplay between modality [C]Bϕ and distributed knowledge modality KCϕ in the imperfect information setting.

6. Undeﬁnability through Know-How

If subscript B in the formula [C]Bϕ is the empty set, then the formula states that coalition C knows a strategy to achieve ϕ that does not rely on information about actions of any agents. We write this formula simply as [C]ϕ. Modality [C]ϕ is know how modality that has been studied before in diﬀerent settings ( Agotnes & Alechina, 2019; Naumov & Tao, 2017a; Fervari et al., 2017; Naumov & Tao, 2017b, 2018c, 2018b, 2018a; Cao & Naumov, 2020). In this section, we compare the expressive power of modalities [C]ϕ and [C]Bϕ. In (Goranko & Ju, 2019), the authors prove, in particular, undeﬁnability of the mention in the previous section modality [C]2 B:ψϕ through coalition power modality [C]ϕ in the perfect information setting. Their proof of undeﬁnability appears to signiﬁcantly reply on the parameter ψ. Thus, although our modality [C]Bϕ could be deﬁned as [C]2 B: ϕ, their proof of undeﬁnability of [C]2 B:ψϕ through [C]ϕ could not be easily adapted to our result presented in this section. Throughout this section, by Φ we denote the language deﬁned by the following grammar: ϕ := p | ϕ | ϕ ϕ | KCϕ | [C]ϕ.

The semantics of language Φ could be deﬁned by replacing item 5 of Deﬁnition 4 with

5 . w [C]ϕ if there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if γ =C δ, w C w , and (w , δ, u) M, then u ϕ.

As mentioned above, modality [C]ϕ could be expressed through modality [C]Bϕ as [C] ϕ. In this section, we show that the opposite is not true. Namely, we prove that modality [C]Bϕ cannot be expressed in language Φ . To do this, we construct two games that are indistinguishable in language Φ but are distinguishable in language Φ. These two games are depicted in Figure 5. Both of these games have three states: α, ω1, and ω2. Without loss of generality, in this section we assume that the set of agents A contains only two agents: Alice and Bob and the set of propositional variables contains only variable p. Both games are games with perfect information, so any of the two agents cannot distinguish two states only if the states are equal. The set contains two actions: 0 and 1. The mechanism of both games in state α is a variation of the matching pennies game. In the left game, if actions of Alice and Bob match, then game transitions from state α to state ω1; otherwise the game nondeterministically transitions to either state ω1 or ω2. In the right

Intelligence in Strategic Games

00,11,01,10 01,10

00,11,01,10 11, 01,10

Figure 5: Two Games.

game, if Alice and Bob both choose action 0, then the game transitions from state α to state ω1; otherwise the game nondeterministically transitions to either state ω1 or ω2. Thus, the only diﬀerence between the mechanisms of these two games is the case when Alice and Bob both choose action 1. In the left game this results in a deterministic transition to state ω1, in the right game the same complete action proﬁle lead to a nondeterministic transition to either state ω1 or state ω2. We assume that in both games propositional variable p is satisﬁed only in state ω1. We refer to the satisﬁability relation for the left game as l and for the right game as r. In Lemma 4, we show that the left and the right games are indistinguishable in language Φ . In Lemma 5, we show that these two models are distinguishable in language Φ. This implies undeﬁnability of modality [C]Bϕ in language Φ , which is stated as Theorem 1 in the end of this section. Towards the proof of Lemma 4, we introduce two auxiliary notions and two auxiliary lemmas. First, for any coalition C and any action proﬁle γ of this coalition in either of the games depicted in Figure 5, we deﬁne the set of outcomes O(C, γ) reachable under action proﬁle γ.

Deﬁnition 6 O(C, γ) = {ω | (α, δ, ω) M, γ =C δ}.

We use notation Ol(C, γ) and Or(C, γ) to denote the set of outcomes under proﬁle γ in the left and the right games respectively. For example,

Ol({Alice, Bob}, 11) = {ω1},

Or({Alice, Bob}, 11) = {ω1, ω2}

because if Alice and Bob both choose action 1, then in the left game the outcome is state ω1 and in the right game the outcome could be either state ω1 or state ω2. Next, we deﬁne a family of sets of outcomes O(C) that could be reached under at least one action proﬁle of a coalition C:

Deﬁnition 7 O(C) = {O(C, γ) | γ C}.

Pavel Naumov and Yuan Yuan

We use notation Ol(C) and Or(C) to denote the families of sets of outcomes in the left and the right games respectively. For example, Ol({Alice, Bob}) = {{ω1}, {ω1, ω2}}, because

Ol({Alice, Bob}, 00) = {ω1},

Ol({Alice, Bob}, 01) = {ω1, ω2},

Ol({Alice, Bob}, 10) = {ω1, ω2},

Ol({Alice, Bob}, 11) = {ω1}.

The following lemma rephrases the semantics of modality [C]ϕ in terms of family O(C). It follows from item 5 stated in the beginning of this section as well as Deﬁnition 6 and Deﬁnition 7.

Lemma 2 For any formula ϕ Φ , for any coalition C {a, b}, for either of the two games, α [C]ϕ if and only if there is a set Ω O(C) such that ω ϕ for each ω Ω.

The next lemma captures the fundamental reason for the left and the right games to be indistinguishable in the language Φ . The particular choice of these two games has been mostly guided by our desire to make this lemma true.

Lemma 3 Ol(C) = Or(C), for any coalition C {a, b}.

Proof. Since the set of agents contains only Alice and Bob, there are only four possible coalitions in either of the two games. We consider the corresponding cases separately:

Ol({a, b}) = {{ω1}, {ω1, ω2}} = Or({a, b}),

Ol({a}) = {{ω1, ω2}} = Or({a}),

Ol({b}) = {{ω1, ω2}} = Or({b}),

Ol( ) = {{ω1, ω2}} = Or( ).

We are now ready to show that the left and the right games are indistinguishable in language Φ .

Lemma 4 w l ϕ iﬀw r ϕ for any state w {α, ω1, ω2} and any formula ϕ Φ .

Proof. We prove the statement of the lemma by structural induction on formula ϕ. Suppose that formula ϕ is a propositional variable. By the deﬁnition of two games, πl(p) = {ω1} = πr(p), where πl and πr are valuation function of the left and the right games respectively. Hence, w l p iﬀw r p by item 1 of Deﬁnition 4. The case when formula ϕ is either a negation or an implication follows from items 2 and 3 of Deﬁnition 4 and the induction hypothesis in the standard way. Assume now that formula ϕ has the form KCψ. By item 4 of Deﬁnition 4 and because the games are games with perfect information, statements w l KCψ and w r KCψ are equivalent to w l ψ and w r ψ respectively. The last two statements are equivalent by the induction hypothesis.

Intelligence in Strategic Games

Finally, suppose that formula ϕ has the form [C]ψ. We consider the following two cases separately: Case I: w = α. In this case w l [C]ψ and w r [C]ψ are both vacuously true by item 5 of Deﬁnition 4 because in either of the games, there are no states w and u and an action proﬁle δ such that w w is true and (w , δ, u) belongs to the mechanism of the game. Case II: w = α. Suppose that w l [C]ψ. Thus, by Lemma 2, there exists a set Ω Ol(C) such that ω l ϕ for each ω Ω. Hence, by the induction hypothesis, ω r ϕ for each ω Ω. Note also that Ω Or(C) by Lemma 3 because Ω Ol(C). Therefore, w r [C]ψ Lemma 2. The proof in the other direction is similar.

Next, we show that the left and the right games are distinguishable in the original language Φ.

Lemma 5 α l [Alice]Bobp and α r [Alice]Bobp.

Proof. In state α of the left game, for any action β {0, 1} of agent Bob, agent Alice can choose the same action β to guarantee outcome ω1. Therefore, α l [Alice]Bobp by item 5 of Deﬁnition 4 and because ω1 l p. If in state α of the right game agent Bob chooses action 1, then there is no action γ {0, 1} that agent Alice could choose to prevent outcome ω2. Therefore, α r [Alice]Bobp by item 5 of Deﬁnition 4 and because ω2 r p.

Our main result of this section follows from Lemma 4 and Lemma 5:

Theorem 1 The modality [C]Bϕ is not deﬁnable in language Φ .

In the rest of this article we give a sound and complete axiomatization of the logical system containing modalities KC and [C]B.

In this section, we present our formal logical system, Know-How Logic with the Intelligence, for reasoning about the interplay between distributed knowledge modality KC and knowhow with intelligence modality [C]B.

Deﬁnition 8 In addition to the propositional tautologies in language Φ, the axioms of the Know-How Logic with the Intelligence are

1. Truth: KCϕ ϕ,

2. Distributivity: KC(ϕ ψ) (KCϕ KCψ),

3. Negative Introspection: KCϕ KC KCϕ,

4. Epistemic Monotonicity: KCϕ KDϕ, where C D,

5. Strategic Introspection: [C]Bϕ KC[C]Bϕ,

Pavel Naumov and Yuan Yuan

6. Empty Coalition: K ϕ [ ] ϕ,

7. Cooperation: [C]B(ϕ ψ) ([D]B,Cϕ [C, D]Bψ), where sets B, C, and D are pairwise disjoint,

8. Intelligence Monotonicity: [C]Bϕ [C]B ϕ, where B B ,

9. None to Analyze: [ ]Bϕ [ ] ϕ.

Note that in the Cooperation axiom above and often throughout the rest of the article we abbreviate B C as B, C. However, we keep writing B C when notation B, C could be confusing. We discuss the individual axioms in Section 8 before proving their soundness. Next, we deﬁne two derivability relations. A unary relation ϕ and a binary relation X ϕ, where X Φ is a set of formulae and ϕ Φ is a formula.

Deﬁnition 9 ϕ if there is a ﬁnite sequence of formulae that ends with ϕ such that each formula in the sequence is either an axiom or could be obtained from the previous formulae using the Modus Ponens, the Epistemic Necessitation, or the Strategic Necessitation inference rules: ϕ, ϕ ψ

ψ , ϕ KCϕ, ϕ [C]Bϕ.

If ϕ, then we say that ϕ is a theorem of our logical system.

Deﬁnition 10 X ϕ if there is a ﬁnite sequence of formulae that ends with ϕ such that each formula in the sequence is either a theorem, or an element of X, or could be obtained from the previous formulae using only the Modus Ponens inference rules.

Note that if set X is empty, then statement X ϕ is equivalent to ϕ. Thus, instead of ϕ we write ϕ. We say that set X is consistent if X . The next lemma gives an example of a formal proof in our logical system. This lemma is used later in the proof of the completeness.

Lemma 6 [C]Bϕ [C ]Bϕ, where C C .

Proof. Formula ϕ ((ϕ ϕ) ϕ) is a tautology. Thus, by the Strategic Necessitation inference rule, [ ]B(ϕ ((ϕ ϕ) ϕ)). At the same time, the following formula is an instance of the Cooperation axiom:

[ ]B(ϕ ((ϕ ϕ) ϕ)) ([C]Bϕ [C]B((ϕ ϕ) ϕ)).

Then, by the Modus Ponens inference rule,

[C]Bϕ [C]B((ϕ ϕ) ϕ). (1)

Note that formula ϕ ϕ is also a tautology. Hence, by the Strategic Necessitation inference rule, [C \ C]B,C(ϕ ϕ). In addition, observe that the following formula is an instance of the Cooperation axiom:

[C]B((ϕ ϕ) ϕ) ([C \ C]B,C(ϕ ϕ) [C, C \ C]Bϕ).

Intelligence in Strategic Games

Thus, by the laws of propositional reasoning,

[C]B((ϕ ϕ) ϕ) [C, C \ C]Bϕ.

Hence, by the laws of propositional reasoning using statement (1),

[C]Bϕ [C, C \ C]Bϕ.

Note that C (C \ C) = C by the assumption C C . Therefore, [C]Bϕ [C ]Bϕ.

The following two lemmas state well-known logical principles. For the beneﬁt of the reader, we reproduce their proofs in the appendix.

Lemma 7 KCϕ KCKCϕ.

Lemma 8 (deduction) If X, ϕ ψ, then X ϕ ψ.

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

Proof. The standard proof of Lindenbaum s lemma (Mendelson, 2009, Proposition 2.14) applies here too.

8. Axiom Discussion and Soundness

In this section, we discuss the axioms of our logical system and prove their soundness with respect to the semantics given in Section 4.

Theorem 2 (soundness) For any state w W of any game (W, { a}a A, , M, π), any set of formulae X Φ, and any formula ϕ Φ, if w χ for each formula χ X and X ϕ, then w ϕ.

As usual, the soundness of the Truth, the Distributivity, the Negative Introspection, and the Monotonicity axiom follows from the assumption that a is an equivalence relation (Fagin, Halpern, Moses, & Vardi, 1995). Below we discuss each of the remaining axioms and prove its soundness as a separate lemma. The Strategic Introspection axiom states that if a coalition C has a know-how strategy, then it knows that it has such a strategy. A version of this axiom without intelligence was ﬁrst introduced in ( Agotnes & Alechina, 2019).

Lemma 10 If w [C]Bϕ, then w KC[C]Bϕ.

Proof. Consider any state w W such that w C w . By Deﬁnition 4, it suﬃces to show that w [C]Bϕ. Indeed, consider any action proﬁle β B of coalition B. By the same Deﬁnition 4, it suﬃces to show that there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ.

Pavel Naumov and Yuan Yuan

Since w C w , by Lemma 1, it suﬃces to show that there is an action proﬁle γ C

of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ. The last statement is true by Deﬁnition 4 and the assumption w [C]Bϕ.

The Empty Coalition axiom says that if statement ϕ is satisﬁed in each state of the model, then the empty coalition has a strategy to achieve it. This axiom ﬁrst appeared in (Naumov & Tao, 2017b).

Lemma 11 If w K ϕ, then w [ ] ϕ.

Proof. Let β be an action proﬁle of the empty coalition. Such action proﬁle is unique, but this is not important for our proof. By Deﬁnition 4, it suﬃces to show that there is an action proﬁle γ of the empty coalition such that for any complete action proﬁle δ A and all states w , u W if β = δ, γ = δ, w w , and (w , δ, u) M, then u ϕ. Indeed, let γ = β. Thus, it suﬃces to prove that u ϕ for each state u W. The last statement follows from the assumption w K ϕ by Deﬁnition 4.

The Cooperation axiom for strategies without intelligence:

[C](ϕ ψ) ([D]ϕ [C, D]ψ),

where sets C and D are disjoint, was introduced in (Pauly, 2001, 2002). This is the signature axiom that appears in all subsequent works on the logics of coalition power. The version of this axiom with intelligence is one of the key contributions of the current article. Our version states that if a coalition C knows how to achieve ϕ ψ assuming it has the intelligence about the actions of a coalition B and a coalition D knows how to achieve ϕ assuming it has the intelligence about actions of the coalitions B and C, then the coalitions C and D know how together they can achieve ψ if they have the intelligence about the actions of the coalition B.

Lemma 12 If w [C]B(ϕ ψ), w [D]B,Cϕ, and sets B, C, and D are pairwise disjoint, then w [C, D]Bψ.

Proof. Consider any action proﬁle β B of coalition B. By Deﬁnition 4, it suﬃces to show that there is an action proﬁle γ C D of coalition C D such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C,D δ, w C,D w , and (w , δ, u) M, then u ψ. Assumption w [C]B(ϕ ψ), by Deﬁnition 4, implies that there is an action proﬁle γ1 C of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ1 =C δ, w C w , and (w , δ, u) M, then u ϕ ψ. Deﬁne action proﬁle β1 B C of coalition B C as follows:

( β(a), if a B, γ1(a), if a C.

Action proﬁle β1 is well-deﬁned because sets B and C are disjoint.

Intelligence in Strategic Games

By Deﬁnition 4, the assumption w [D]B,Cϕ implies that there is an action proﬁle γ2 D of coalition D such that for any complete action proﬁle δ A and any states w , u W if β1 =B,C δ, γ2 =D δ, w D w , and (w , δ, u) M, then u ϕ. Deﬁne action proﬁle γ C D of coalition C D as follows:

( γ1(a), if a C, γ2(a), if a D.

Action proﬁle γ is well-deﬁned because sets C and D are disjoint. Consider any complete action proﬁle δ A and any states w , u W such that β =B δ, γ =C D δ, w C D w , and (w , δ, u) M. Recall from the ﬁrst paragraph of this proof that it suﬃces to show that u ϕ. Note that β =B δ, γ1 =C γ =C δ, w C w , and (w , δ, u) M. Thus, u ϕ ψ by the choice of the action proﬁle γ1. Similarly, β1 =B β =B δ and β1 =C γ1 =C γ =C δ. Hence, β1 =B C δ. Also, γ2 =D γ =D δ, w C w , and (w , δ, u) M. Thus, u ϕ by the choice of the action proﬁle γ2. Therefore, u ψ by Deﬁnition 4 because u ϕ ψ and u ϕ.

The remaining two axioms are original to this article. The Intelligence Monotonicity axiom states if a coalition C has a strategy based on the intelligence about the actions of a coalition B, then the coalition C has such a strategy based on the intelligence about any larger coalition. The other form of monotonicity for modality [C]B, monotonicity on the coalition C is also true. It is not listed among our axioms because it is provable in our system, see Lemma 6.

Lemma 13 If w [C]Bϕ, B B , and sets B and C are disjoint, then w [C]B ϕ.

Proof. Consider any action proﬁle β B of coalition B . By Deﬁnition 4, it suﬃces to show that there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ. Deﬁne action proﬁle β B of coalition B to be such that β(a) = β (a) for each agent a B. Action proﬁle β is well-deﬁned due to the assumption B B of the lemma. By Deﬁnition 4, the assumption w [C]Bϕ implies that there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ. Note that β =B β by the choice of action proﬁle β. Thus, for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ. Finally, observe that condition β =B δ implies condition β =B δ by the assumption B B of the lemma. Therefore, for any complete action proﬁle δ A and any states w , u W if β =B δ, γ =C δ, w C w , and (w , δ, u) M, then u ϕ.

The None to Analyze axiom says that if there is no one to interpret the intelligence information about coalition B, then this intelligence might as well not exist.

Lemma 14 If w [ ]Bϕ, then w [ ] ϕ.

Pavel Naumov and Yuan Yuan

Proof. By Deﬁnition 4, the assumption w [ ]Bϕ implies that for any action proﬁle β B of coalition B there is an action proﬁle γ of the empty coalition such that for any complete action proﬁle δ A and any states w , u W if β =B δ, γ = δ, w w , and (w , δ, u) M, then u ϕ. Thus, for any action proﬁle β B of coalition B, any complete action proﬁle δ A

and any states w , u W if β =B δ and (w , δ, u) M, then u ϕ. Hence, for any complete action proﬁle δ A and any states w , u W if (w , δ, u) M, then u ϕ. Then, for any action proﬁle β of the empty coalition there is an action proﬁle γ of the empty coalition such that for any complete action proﬁle δ A and any states w , u W, if β = δ, γ = δ, w w , and (w , δ, u) M, then u ϕ. Therefore, w [ ] ϕ by Deﬁnition 4.

9. Completeness

In this section, we prove the completeness of our logical system. As usual, the completeness theorem is using a canonical model. There are two major challenges that we need to overcome while deﬁning the canonical model. The ﬁrst of them is a well-known complication related to the presence of the distributed knowledge modality in our logical system. The second is a unique challenge speciﬁc to strategies with intelligence. To understand the ﬁrst challenge, recall that, in the case of individual knowledge, states of a canonical model are usually deﬁned as maximal consistent sets of formulae. Two such sets are a-equivalent if the sets contain the same Ka-formulae. Unfortunately, this construction can not be easily adapted to distributed knowledge because if two sets share Kaand Kb-formulae, then they not necessarily share Ka,b-formulae. To overcome this challenge we use the tree construction in which each state is a node of a labeled tree. Nodes of the tree are labeled with maximal consistent sets and edges are labeled with coalitions. This construction has been used in logics of distributed knowledge before (Naumov & Tao, 2017a, 2017b, 2018c, 2018b, 2018a; W ang & Agotnes, 2020; Baltag & van Benthem, 2021). To understand the second challenge, let us ﬁrst recall the way the canonical game is sometimes constructed for the logics of the coalition power. The often used construction deﬁnes the domain of actions to be the set of all formulae (Goranko & van Drimmelen, 2006; Naumov & Tao, 2017a; Goranko & Enqvist, 2018; Naumov & Tao, 2018b). Informally, it means that each agent votes for a formula that the agent wants to be true in the next state. Of course, not all requests of the agents are granted. The canonical game mechanism speciﬁes which requests are granted and which are ignored. There also are canonical game constructions in which a voting ballot in addition to a formula must also contain some additional information that acts as a key verifying that the voting agent has certain information (Naumov & Tao, 2018c, 2018a). So, it is natural to assume that in case of formula [C]Bϕ, coalition C should vote for formula ϕ and provide the vote of coalition B as a key. This approach, however, turns out to be problematic. Indeed, in order to satisfy some other formula, say [B]Dψ, the vote of coalition B would need to include the vote of coalition D as a key. Thus, it appears, that the vote of C would need to include the vote of D as well. The situation is further complicated by a mutual recursion when one attempts to satisfy formulae [C]Bϕ and [B]Cχ simultaneously. The solution that we propose in this

Intelligence in Strategic Games

article avoids this recursion. It turns out that it is not necessary for the key to contain the complete intelligence information. Namely, we assume that each agent votes for a formula and signs her vote with an integer key. To satisfy formula [C]Bϕ, the mechanism will guarantee that if all members of coalition C vote for ϕ and sign with integer keys that are larger than keys of all members in coalition B, then ϕ will be true in the next state. The larger key beats smaller key idea is formalized later in Deﬁnition 14. This idea itself, the notion of rank from the proof of Lemma 18, as well as the ﬁrst six claims in the proof of Lemma 18 are original contributions of this article that have no counterpart in any of the existing works on the logics of know-how. We now start the formal proof of the completeness by deﬁning the canonical game G(X0) = (W, { a}a A, , M, π) for a ﬁxed maximal consistent set of formulae X0.

Deﬁnition 11 A ﬁnite sequence X0, C1, X1, C2, . . . , Cn, Xn is a state of the canonical game if

2. X1, . . . , Xn are maximal consistent sets of formulae,

3. C1, . . . , Cn are coalitions of agents,

4. {ϕ Φ | KCkϕ Xk 1} Xk for each integer k such that 1 k n.

We say that sequence w = X0, C1, X1, . . . , Cn 1, Xn 1 and sequence u = X0, C1, X1, . . . , Cn, Xn are adjacent. The adjacency relation deﬁnes an undirected labeled graph whose nodes are elements of set W and whose edges are speciﬁed by the adjacency relation. We say that the node u is labeled by set Xn and that edge (w, u) is labeled by each agent in set Cn, see Figure 6. Note that this graph has no cycles. Thus, it is a tree. As usual, by a simple path we mean any path without repeating vertices. We allow single-vertex simple paths that connect a node to itself.

X4 X5 X6 X7 X8

C4 C5 C6 C7 C8

Figure 6: Fragment of the tree formed by the states.

Deﬁnition 12 For any agent a A and any nodes v, v W, let v a v if all edges along the unique simple path connecting nodes v and v are labeled by agent a.

Lemma 15 Relation a is an equivalence relation for each agent a A.

Pavel Naumov and Yuan Yuan

Recall from Deﬁnition 2, that we write v C v if v a v for each agent a C. Throughout the rest of the article, for any nonempty sequence w = x1, . . . , xn, by hd(w) we denote the element xn and by w :: y we denote sequence x1, . . . , xn, y. The next lemma shows that the tree construction solves the challenge of the distributed knowledge discussed in the preamble to this section.

Lemma 16 If w C w , then KCϕ hd(w) iﬀKCϕ hd(w ).

Proof. The assumption w C w implies that each edge along the unique simple path between nodes w and w is labeled with all agents in coalition C. Thus, it suﬃces to show that KCϕ hd(w) iﬀKCϕ hd(w ) for any two adjacent nodes along this path. Indeed, without loss of generality, let

w = X0, C1, X1, . . . , Cn 1, Xn 1 w = X0, C1, X1, . . . , Cn 1, Xn 1, Cn, Xn.

The assumption that the edge between w and w is labeled with all agents in coalition C implies that C Cn. Next, we show that KCϕ hd(w) iﬀKCϕ hd(w ). ( ) : Suppose that KCϕ hd(w) = Xn 1. Thus, Xn 1 KCKCϕ by Lemma 7. Hence, Xn 1 KCn KCϕ by the Epistemic Monotonicity axiom and because C Cn. Hence, KCn KCϕ Xn 1 because set Xn 1 is maximal. Then, KCϕ Xn = X(w ) by Deﬁnition 11. ( ) : Suppose that KCϕ / hd(w) = Xn 1. Thus, KCϕ Xn 1 because set Xn 1 is maximal. Hence, Xn 1 KC KCϕ by the Negative Introspection axiom. Hence, Xn 1 KCn KCϕ by the Epistemic Monotonicity axiom and because C Cn. Hence, KCn KCϕ Xn 1 because set Xn 1 is maximal. Then, KCϕ Xn by Deﬁnition 11. Therefore, KCϕ / Xn = hd(w ) because set Xn is consistent.

This deﬁnes the states of the canonical game G(X0) and the indistinguishability relations { a}a A on these states. We now will deﬁne the domain of actions and the mechanism of the canonical game. Recall from the introduction to this section that each action ( vote ) of an agent has two parts: the actual vote (a statement that the agent wants to achieve) and an integer key . The domain of actions consists of all such pairs:

Deﬁnition 13 is a set of all pairs (ϕ, z) such that ϕ Φ is a formula, and z Z is an integer number.

As with the most proofs of completeness, the key step in our proof is an induction or a truth lemma. In our case, this is Lemma 19. In particular, this lemma states that if [C]Bϕ hd(w), then w [C]Bϕ. In other words, if [C]Bϕ hd(w), then coalition C must have a strategy to achieve ϕ that might rely on the intelligence about the actions of coalition B. The deﬁnition of the canonical mechanism below provides coalition C with such a strategy. It guarantees that if (i) [C]Bϕ hd(w), (ii) all members of coalition C vote for ϕ, and (iii) each member of the coalition C signs her vote with a key which is larger than the key of each member of coalition B, then statement ϕ will be true after the transition. If u is a pair (x, y), then by pr1(u) and pr2(u) we mean elements x and y respectively.

Intelligence in Strategic Games

Deﬁnition 14 Mechanism M is the set of all triples (w, δ, u), where w and u are states and δ is a complete action proﬁle, such that for any formula [C]Bϕ hd(w) if

1. pr1(δ(c)) = ϕ, for each agent c C,

2. pr2(δ(b)) < pr2(δ(c)) for each agent b B and each agent c C,

then ϕ hd(u).

For example, suppose that [a]bϕ hd(w) and [b]a ϕ hd(w). The ﬁrst of these assumptions implies that agent a must have a strategy to achieve ϕ as long as she has the intelligence about agent b action. Similarly, [b]a ϕ w means that agent b must have a strategy to achieve ϕ as long as he has the intelligence about agent a action. If agent a uses action (ϕ, 3) and agent b uses action ( ϕ, 2), then the mechanism guarantees that ϕ will be satisﬁed in the outcome because 2 < 3. However, if agent a uses action (ϕ, 3) while agent b uses action ( ϕ, 4), then the mechanism guarantees that ϕ will be satisﬁed in the outcome because 3 < 4. If agent a knows that the action of agent b will be (x, y), then agent a can use action (ϕ, y + 1) to guarantee that ϕ is satisﬁed. This is the strategy of agent a that relies on the intelligence about the action of agent b.

Deﬁnition 15 π(p) = {w W | p hd(w)}.

This concludes the deﬁnition of the canonical game G(X0) = (W, { a}a A, , M, π). The next important milestone in the proof of the completeness is the mentioned above truth Lemma 19. Before that lemma, however, we state and prove two auxiliary statements that are used in the induction step of the proof of Lemma 19. The ﬁrst of these lemmas will be used to show that if KCϕ / hd(w), then w KCϕ.

Lemma 17 If KCϕ hd(w), then there is a state u W such that w C u and ϕ hd(u).

Proof. Consider the set of formulae X = { ϕ} {ψ | KCψ w}. First, we prove that set X is consistent. Suppose the opposite. Thus, there are formulae KCψ1, . . . , KCψn hd(w) such that ψ1, . . . , ψn ϕ.

Hence, by Lemma 8 applied n times,

ψ1 (ψ2 . . . (ψn ϕ) . . . ).

Then, by the Epistemic Necessitation inference rule,

KC(ψ1 (ψ2 . . . (ψn ϕ) . . . )).

Thus, by the Distributivity axiom and the Modus Ponens inference rule,

KCψ1 KC(ψ2 . . . (ψn ϕ) . . . )).

Pavel Naumov and Yuan Yuan

Recall that KCψ1 hd(w) by the choice of formula KCψ1. Hence, by the Modus Ponens inference rule, hd(w) KC(ψ2 . . . (ψn ϕ) . . . )).

By repeating the previous step n 1 more times,

Hence, KCϕ / hd(w) due to the consistency of the set hd(w). This contradicts the assumption of the lemma. Therefore, set X is consistent. By Lemma 9, there is a maximal consistent extension b X of set X. Let u be the sequence w :: C :: b X. Note that u W by Deﬁnition 11 and the choices of the set X, the set b X, and the sequence u. Furthermore, w C u by the deﬁnition of the relation a on the set W. Finally, ϕ X b X = hd(u) again by the choices of the set X, the set b X and the sequence u.

The next lemma is used in Lemma 19 to show that if [C]Bϕ / hd(w), then w [C]Bϕ. In other words, in this proof we show that if [C]Bϕ / hd(w), then no matter what know-how strategy with intelligence coalition C decide to use, there is a situation when the strategy fails. The proof of the next lemma is the longest among all proofs in this article. To improve the readability, we structured some parts of the proof as claims.

Lemma 18 If [C]Bϕ hd(w), then there exists an action proﬁle β B of coalition B such that for each action proﬁle γ C of coalition C there is a complete action proﬁle δ A and states w , u W such that β =B δ, γ =C δ, w C w , (w , δ, u) M, and ϕ hd(u).

Proof. Let action proﬁle β B of coalition B be such that β(b) = ( , 0) for each agent b B. Informally, the ﬁrst component of each action is the formula for which the agent is voting. By choosing the ﬁrst component to be Boolean constant , we minimize the number of statements that we must satisfy in state u. The second component of the action is the key with which the agent signs the vote. Since coalition C has the access to the intelligence about actions of coalition B, coalition C will easily be able to pick keys larger than those chosen by us for the members of coalition B. Thus, there is no point in choosing large keys. We decided to default the key to 0, but any other value would do. Consider any action proﬁle γ C of coalition C. Choose an integer z0 such that for each a C pr2(γ(a)) < z0. (2)

Such z0 exists because coalition C is a ﬁnite set of agents. Deﬁne complete action proﬁle δ A as follows

β(a), if a B, γ(a), if a C, ( , z0), otherwise.

Note that sets B and C are disjoint by Deﬁnition 3 because [C]Bϕ is a formula. Hence, complete action proﬁle δ is well-deﬁned.

Intelligence in Strategic Games

To understand the intuition behind this choice of δ, note that an important part of the deﬁnition of the complete action proﬁle δ is choosing how agents outside of the coalition C B are voting. Just like in the case of action proﬁle β, we minimize the number of statements that we must satisfy in state u by choosing the vote of each such agent to be Boolean constant . We signed the votes of all agents outside of the coalition C B with key z0, which is larger than any of the keys used by the members of coalition C to contain the power of the coalition C to achieve its goal. Indeed, if set hd(w ) contains a formula of the form [D]Eψ, where D C and E A\(C B), then, coalition C can try to force ψ by asking all agents in set D to vote for ψ. By Deﬁnition 14, this tactic will succeed as long as keys of agents in coalition D are higher than keys of agents in coalition E. To prevent this tactic of coalition C from being successful, we set the keys of all agents outside of the coalition C B to be higher than the keys of the agents in coalition C. State w will be later deﬁned to be state w. We are now starting to construct state u, which will be later deﬁned in such a way that hd(w ) is a maximal consistent extension of the set X:

X = { ϕ} {σ | [ ] σ hd(w)} (4)

{ψ | [P]Qψ hd(w), P = , p P(pr1(δ(p)) = ψ),

q Q p P(pr2(δ(q)) < pr2(δ(p)))}.

Informally, the set X contains formula ϕ and all other formulae that must belong to set hd(u) according to Deﬁnition 14. We separated the formulae for the case of P = into a separate set because these formulae are treated diﬀerently later in the proof. Next we show that set X is consistent. Suppose the opposite. Hence,

σ1, . . . , σm, ψ1, ψ2, ψ3, . . . , ψn ϕ (5)

for some formulae [ ] σ1, . . . , [ ] σm hd(w) (6)

and some formulae [P1]Q1ψ1, . . . , [Pn]Qnψn hd(w) (7)

such that pr2(δ(q)) < pr2(δ(p)), i n, q Qi, p Pi (8)

Pi = , i n (9)

and pr1(δ(p)) = ψi i n, p Pi. (10)

Note that, if present, repeated assumptions and assumption can be omitted from statement (5). Thus, we can assume that formulae ψ1, ψ2, ψ3, . . . , ψn are distinct and none of them is equal to : ψi = ψj, (11)

for each i n and each j = i. Next, we state and prove basic properties of the sets of agents Pi and Qi.

Pavel Naumov and Yuan Yuan

rank(P1) rank(P2) rank(P3)

Figure 7: Sets P1, P2, P3, . . . and their ranks.

Claim 1 Sets P1, . . . , Pn are pairwise disjoint.

Proof. Consider any agent a Pi Pj. Then, ψi = pr1(δ(a)) = ψj by equation (10), which contradicts assumption (11).

Claim 2 Pi C for each i n.

Proof. Consider any agent a Pi. Suppose that a / C. Then, pr1(δ(a)) = by equation (3). At the same time, pr1(δ(a)) = ψi by equality (10) because a Pi. Hence, ψi = , which contradicts assumption (12).

Claim 3 Qi B C.

Proof. Consider any agent q Qi. Statement (9) implies that there is at least one agent p Pi. Then, p C by Claim 2. Thus, pr2(δ(p)) = pr2(γ(p)) < z0 due to equality (3) and inequality (2). Hence, pr2(δ(q)) < z0 by inequality (8). Therefore, q B C due to equality (3).

For any nonempty ﬁnite set of agents P A, let

rank(P) = min p P pr2(δ(p)). (13)

Informally, rank(P) is the minimal key used by an agent from set Pi to sign her vote under action proﬁle δ. Sets P1, . . . , Pn are nonempty by statement (9). Thus, rank(Pi) is deﬁned for each i n. Without loss of generality, we can assume that, see Figure 7,

rank(P1) rank(P2) rank(Pn). (14)

To understand the intuition behind this step, recall that in order for a coalition P to use a strategy with the intelligence whose existence is expressed by formula [P]Qψ, all agents in set P must sign with keys higher than those used by the agents in set Q. Thus, informally, the higher rank of a coalition is, the more powerful its vote is. Ordering (14) sorts coalitions P1, . . . , Pn by the power of the keys they used under action proﬁle δ. We now show more advanced properties of coalitions Pi and Qi that are true because of assumption (14).

Intelligence in Strategic Games

Claim 4 Sets Qi and Pj are disjoint for 1 i j.

Proof. For any q Qi and any p Pj, by inequality (8) and deﬁnition (13); assumption (14); and again deﬁnition (13),

pr2(δ(q)) < min p Pi pr2(δ(p )) = rank(Pi) rank(Pj)

= min p Pj pr2(δ(p )) pr2(δ(p)).

Therefore, sets Qi and Pj are disjoint.

Let R = C \ (P1 Pn). (15)

Claim 5 Sets B, R, P1, . . . , Pn are pairwise disjoint.

Proof. Sets B and C are disjoint by Deﬁnition 3 because [C]Bϕ is a formula. Hence, complete action proﬁle δ is well-deﬁned. Hence, sets B and R are disjoint because of equation (15) and set B is disjoint with each of sets P1, . . . , Pn by Claim 2 and because sets B and C are disjoint. Also, set R is disjoint with each of sets P1, . . . , Pn by equation (15). Finally, sets P1, . . . , Pn are pairwise disjoint by Claim 1.

Claim 6 Qi B R P1 Pi 1 for 1 i n.

Proof. Consider any agent q Qi such that q / B R. It suﬃces to show that q P1 Pi 1. Indeed, assumptions q Qi and q / B imply that q C by Claim 3. Thus, q P1 Pn by the assumption q / R and the deﬁnition of set R. Therefore, q P1 Pi 1 by Claim 4 because q Qi.

Let us now return to the proof of the lemma. Statement (5), by the Lemma 8 applied m + n times, implies that

σ1 (. . . (σm (ψ1 . . . (ψn ϕ) . . . )) . . . ).

Hence, by the Strategic Necessitation inference rule,

[ ] (σ1 (. . . (σm (ψ1 . . . (ψn ϕ) . . . )) . . . )).

Thus, by the Cooperation axiom (where B = C = D = ) and the Modus Ponens inference rule, [ ] σ1 [ ] (σ2 (. . . (σm (ψ1 . . . (ψn ϕ) . . . )) . . . )).

Then, by the Modus Ponens inference rule and assumption (6),

hd(w) [ ] (σ2 (. . . (σm (ψ1 . . . (ψn ϕ) . . . )) . . . )).

By repeating the previous step m 1 times,

hd(w) [ ] (ψ1 (ψ2 (ψ3 . . . (ψn ϕ) . . . ))).

Pavel Naumov and Yuan Yuan

Hence, by the Intelligence Monotonicity axiom and the Modus Ponens inference rule,

hd(w) [ ]B(ψ1 (ψ2 (ψ3 . . . (ψn ϕ) . . . ))).

Thus, by Lemma 6, Claim 5, and the Modus Ponens inference rule,

hd(w) [R]B(ψ1 (ψ2 (ψ3 . . . (ψn ϕ) . . . ))).

Then, by the Cooperation axiom, Claim 5, and the Modus Ponens inference rule,

hd(w) [P1]B,Rψ1 [R, P1]B(ψ2 (ψ3 . . . (ψn ϕ) . . . )).

At the same time, recall that [P1]Q1ψ1 hd(w) by assumption (7). Thus, hd(w) [P1]B,Rψ1 by the Intelligence Monotonicity axiom and because Q1 B R due to Claim 6. Hence, by the Modus Ponens inference rule,

hd(w) [R, P1]B(ψ2 (ψ3 . . . (ψn ϕ) . . . )).

Then, by the Cooperation axiom, Claim 5, and the Modus Ponens inference rule,

hd(w) [P2]B,R,P1ψ2 [R, P1, P2]B(ψ3 . . . (ψn ϕ) . . . )).

Also, recall that [P2]Q2ψ2 hd(w) by assumption (7). Thus, hd(w) [P2]B,R,P1ψ2 by the Intelligence Monotonicity axiom and because Q2 B, R, P1 due to Claim 6. Hence, by the Modus Ponens inference rule,

hd(w) [R, P1, P2]B(ψ3 . . . (ψn ϕ) . . . )).

By repeating the previous step n 2 more times,

hd(w) [R, P1, P2, . . . , Pn]Bϕ.

Equation (15) implies that R C. Thus, R, P1, P2, . . . , Pn C by Claim 2. Then, hd(w) [C]Bϕ by Lemma 6, which contradicts the assumption [C]Bϕ hd(w) and the consistency of the set hd(w). Therefore, set X, as deﬁned by equation (4), is consistent. By Lemma 9, there exists a maximal consistent extension b X of the set X. Let w be state w and u to be the sequence w :: :: b X.

Claim 7 u W.

Proof. By Deﬁnition 11, it suﬃces to prove that

{ϕ Φ | K ϕ hd(w)} hd(u).

Indeed, let K ϕ hd(w). Thus, hd(w) [ ] ϕ by the Empty Coalition axiom. Hence, [ ] ϕ hd(w) due to the maximality of the set hd(w). Then, ϕ X by equation (4). Thus, ϕ b X by the choice of set b X. Therefore, ϕ hd(u) by the choice of sequence u.

Intelligence in Strategic Games

Note that β =B δ because of equation (3) and the assumption β B of the lemma. Similarly, γ =C δ. Also, w C w by Deﬁnition 12 and the choice of w = w. Additionally, ϕ hd(u) because, due to equation (4), we have ϕ X b X = hd(u). Since w = w , to ﬁnish the proof of the lemma, we need to show that (w, δ, u) M. Consider any formula [P]Qψ hd(w) such that pr1(δ(p)) = ψ for each agent p P and pr2(δ(q)) < pr2(δ(p)) for each agent q Q and each agent p P. By Deﬁnition 14, it suﬃces to prove that ψ hd(u). We consider the following two cases separately. Case I: P = . Thus, ψ X by equation (4). Therefore, ψ X b X = hd(u). Case II: P = . Then, the assumption [P]Qψ hd(w) can be rewritten as [ ]Qψ hd(w). Thus, hd(w) [ ] ψ by the None to Analyze axiom. Hence, [ ] ψ hd(w) because of the maximality of the set hd(w). Thus, ψ X by equation (4). Therefore, ψ X b X = hd(u). This concludes the proof of Lemma 18.

We are now ready to state and to prove the truth lemma. This lemma is the key step in most proofs of completeness.

Lemma 19 w ϕ iﬀϕ hd(w) for each formula ϕ Φ.

Proof. We prove the lemma by induction on the structural complexity of formula ϕ. The base case follows from Deﬁnition 4 and Deﬁnition 15. The case when formula ϕ is a negation or an implication follows from Deﬁnition 4 and the assumption that set hd(w) is a maximal consistent set of formulae in the standard way. Suppose that formula ϕ has the form KCψ. ( ): Assume that KCψ / hd(w). Thus, KCψ hd(w) due to the maximality of the set hd(u). Hence, by Lemma 17, there is a state u W such that w C u and ψ hd(u). Then, ψ / hd(u) due to the consistency of the set hd(u). Thus, u ψ by the induction hypothesis. Therefore, w KCψ by Deﬁnition 4. ( ): Assume that KCψ hd(w). Consider any state u W such that w C u. By Deﬁnition 4, it suﬃces to show that u ψ. Indeed, by Lemma 16, assumptions KCψ hd(w) and w C u imply that KCψ hd(u). Hence, hd(u) ψ by the Truth axiom and the Modus Ponens inference rule. Thus, ψ hd(u) due to the maximality of the set hd(u). Therefore, u ψ by the induction hypothesis. Suppose that formula ϕ has the form [C]Bψ. ( ): Assume that [C]Bψ / hd(w). Hence, [C]Bψ hd(w) due to the maximality of the set hd(w). Thus, by Lemma 18, there exists an action proﬁle β B of coalition B such that for each action proﬁle γ C of coalition C there is a complete action proﬁle δ A

and states w , u W such that β =B δ, γ =C δ, w C w , (w , δ, u) M, and ψ hd(u). Note that ψ hd(u) implies ψ / hd(u) due to the consistency of the set hd(u), which, in term implies u ψ by the induction hypothesis. Thus, for each action proﬁle γ C of coalition C there is a complete action proﬁle δ A and states w , u W such that β =B δ, γ =C δ, w C w , (w , δ, u) M, and u ψ. Therefore, w [C]Bψ by Deﬁnition 4. ( ): Assume that [C]Bψ hd(w). Consider any action proﬁle β B of coalition B. Set B is ﬁnite because it is a coalition. Let z0 be any integer number such that pr2(β(b)) < z0 for each agent b B. Deﬁne action proﬁle γ C as γ(c) = (ϕ, z0) for each c C.

Pavel Naumov and Yuan Yuan

Consider any complete action proﬁle δ A, any state w W, and any state u W such that β =B δ, γ =C δ, w C w , and (w , δ, u) M. By Deﬁnition 4, it suﬃces to show that u ψ. The assumption [C]Bψ hd(w) implies that hd(w) KC[C]Bψ by the Strategic Introspection axiom and the Modus Ponens inference rule. Thus, KC[C]Bψ hd(w) by the maximality of the set hd(w). Hence, KC[C]Bψ hd(w ) by the assumption w C w and Lemma 16. Then, hd(w ) [C]Bψ by the Truth axiom and the Modus Ponens inference rule. Hence, [C]Bψ hd(w ) due to the maximality of the set hd(w ). By the choice of action proﬁle γ and the assumption γ =C δ, for each agent c C, we have pr1(δ(c)) = pr1(γ(c)) = ϕ. At the same time, by the assumption β =B δ, the choice of integer z0, the choice of action proﬁle γ, and the assumption γ =C δ,

pr2(δ(b)) = pr2(β(b)) < z0 = pr2(γ(c)) = pr2(δ(c))

for each agent b B and each agent c C. Thus, ψ hd(u) by Deﬁnition 14 and the assumption (w , δ, u) M. Therefore, u ψ by the induction hypothesis.

Now we are ready to state and to prove the strong completeness of our logical system.

Theorem 3 If Y ϕ, then there is a state w of a game such that w χ for each χ Y and w ϕ.

Proof. Suppose that Y ϕ. By Lemma 9, there exists a maximal consistent set of formulae X0 such that Y { ϕ} X0. Let w be the single-element sequence X0. By Deﬁnition 11, sequence w is a state of the canonical game G(X0). Note that χ X0 = hd(w) for each formula χ Y and ϕ X0 = hd(w) by the choice of set X0 and the choice of sequence w. Thus, w χ for each χ Y and w ϕ by Lemma 19. Therefore, w ϕ by Deﬁnition 4.

10. Conclusion

In this article, we proposed the notion of a strategy with intelligence, proved that corresponding know-how modality is not deﬁnable through the standard know-how modality, and gave a sound and complete axiomatization of a bimodal logic that describes the interplay between the strategic power with intelligence and the distributed knowledge modalities in the setting of strategic games with imperfect information. A natural question is decidability of the proposed logical system. Unfortunately, the standard ﬁltration technique (Gabbay, 1972) can not be easily applied here to produce a ﬁnite model. Indeed, it is crucial for the proof of the completeness, see Deﬁnition 14, that for each action there is another action with a higher value of the key component. Thus, for the proposed construction to work, the domain of choices must be inﬁnite. One perhaps might be able to overcome this by changing the second component of the action from an inﬁnite linear ordered set to a ﬁnite circularly ordered set as in rock-paper-scissors game, but we have not been able to prove this.

Intelligence in Strategic Games

In this article, we refer to the additional information about actions of coalition B in modality [C]Bϕ as the intelligence , to emphasize that C knows ex ante (before actions are taken) a strategy that depends on (future) intelligence about the actions of coalition B. Alternatively, one can consider a situation when coalition C knows the strategy interim (after coalition B commits to speciﬁc actions). For example, the Germans might have a technical capability to attack a British convoy along route 1, but not along route 2. In such a situation, they do not know ex ante a strategy to attack convoy even if they know ex ante that they will be given the intelligence about the convoy itinerary. However, the Germans will have interim knowledge of such a strategy if British decide to use route 1. We refer to such interim knowledge of the strategy as a knowledge of a conditional strategy because it could be viewed as ex ante knowledge of a strategy that only works when a certain condition on the actions of coalition B is satisﬁed. A logical system for reasoning about such conditional strategies will require a new language in which such conditions on actions of a coalition B could be expressed. An example of such an approach is mentioned earlier Alternating-time Temporal Logic with Explicit Strategies (Walther et al., 2007). Another type of conditional strategies are those where the condition is not on the actions of other coalitions, but on the current state. We denote corresponding modality by [C]ϕψ and read it as coalition C knows a strategy that achieves ψ as along as condition ϕ is satisﬁed (which might be unknown to C) in the current state . This modality can be deﬁned in the setting of Deﬁnition 4 as follows:

w [C]ϕψ if there is an action proﬁle γ C of coalition C such that for any complete action proﬁle δ A and any states w , u W if γ =C δ, w C w , w ϕ, and (w , δ, u) M, then u ψ.

An interesting property of conditional strategies expressible through the last modality is [C]ϕψ ([D] ϕψ [C, D]ψ),

where coalitions C and D are disjoint. Or, more generally,

[C]ϕ1ψ1 ([D]ϕ2ψ2 [C, D]ϕ1 ϕ2(ψ1 ψ2)).

The complete axiomatization of the properties of this modality remains an open question.

Appendix A. Auxiliary Lemmas

Lemma 7 KCϕ KCKCϕ.

Proof. Formula KC KCϕ KCϕ is an instance of the Truth axiom. Thus, KCϕ KC KCϕ by contraposition. Hence, taking into account the following instance of the Negative Introspection axiom: KC KCϕ KC KC KCϕ, we have

KCϕ KC KC KCϕ. (16)

At the same time, KCϕ KC KCϕ is an instance of the Negative Introspection axiom. Thus, KC KCϕ KCϕ by the law of contrapositive in the propositional logic. Hence, by the Necessitation inference rule, KC( KC KCϕ KCϕ). Thus, by the Distributivity axiom and the Modus Ponens inference rule, KC KC KCϕ KCKCϕ. Therefore,

Pavel Naumov and Yuan Yuan

KCϕ KCKCϕ by propositional reasoning using statement (16).

Lemma 8 If X, ϕ ψ, then X ϕ ψ. Proof. Suppose that a sequence ψ1, . . . , ψn is a

proof from set X {ϕ} and the theorems of our logical system that uses the Modus Ponens inference rule only. In other words, for each k n, either

2. ψk X, or

3. ψk is equal to ϕ, or

4. there are i, j < k such that formula ψj is equal to ψi ψk.

It suﬃces to show that X ϕ ψk for each k n. We prove this by induction on k through considering the four cases above separately.

Case I: ψk. Note that ψk (ϕ ψk) is a propositional tautology, and thus, is an axiom of our logical system. Hence, ϕ ψk by the Modus Ponens inference rule. Therefore, X ϕ ψk.

Case II: ψk X. Then, similar to the previous case, X ϕ ψk.

Case III: formula ψk is equal to ϕ. Thus, ϕ ψk is a propositional tautology. Hence, ϕ ψk. Therefore, X ϕ ψk.

Case IV: formula ψj is equal to ψi ψk for some i, j < k. Thus, by the induction hypothesis, X ϕ ψi and X ϕ (ψi ψk). Note that formula (ϕ ψi) ((ϕ (ψi ψk)) (ϕ ψk)) is a propositional tautology. Therefore, X ϕ ψk by applying the Modus Ponens inference rule twice.

Agotnes, T., & Alechina, N. (2019). Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation, 29, 1041 1069.

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

Agotnes, T., van der Hoek, W., & Wooldridge, M. (2009). Reasoning about coalitional games. Artiﬁcial Intelligence, 173(1), 45 79.

Agotnes, T., & W ang, Y. N. (2017). Resolving distributed knowledge. Artiﬁcial Intelligence, 252, 1 21.

Baltag, A., & van Benthem, J. (2021). A simple logic of functional dependence. Journal of Philosophical Logic, (to appear).

Bard, N., Foerster, J. N., Chandar, S., Burch, N., Lanctot, M., Song, H. F., Parisotto, E., Dumoulin, V., Moitra, S., Hughes, E., Dunning, I., Mourad, S., Larochelle, H., Bellemare, M. G., & Bowling, M. (2020). The Hanabi challenge: A new frontier for AI research. Artiﬁcial Intelligence, 280, 103216.

Intelligence in Strategic Games

Belardinelli, F. (2014). Reasoning about knowledge and strategies: Epistemic strategy logic. In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, Vol. 146 of EPTCS, pp. 27 33.

Belardinelli, F., Dima, C., & Murano, A. (2018). Bisimulations for logics of strategies: A study in expressiveness and veriﬁcation. In Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning, pp. 425 434.

Belardinelli, F., Lomuscio, A., & Malvone, V. (2019). An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information. In Proceedings of the AAAI Conference on Artiﬁcial Intelligence, Vol. 33, pp. 6030 6037.

Belle, V., & Lakemeyer, G. (2010). Reasoning about imperfect information games in the epistemic situation calculus. In Twenty-Fourth AAAI Conference on Artiﬁcial Intelligence.

Berthon, R., Maubert, B., Murano, A., Rubin, S., & Vardi, M. Y. (2017). Strategy logic with imperfect information. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pp. 1 12. IEEE.

Borgo, S. (2007). Coalitions in action logic. In 20th International Joint Conference on Artiﬁcial Intelligence, pp. 1822 1827.

Budiansky, S. (2002). German vs. allied codebreakers in the battle of the atlantic. International Journal of Naval History, 1(1).

Burch, N., Johanson, M., & Bowling, M. (2014). Solving imperfect information games using decomposition. In Twenty-Eighth AAAI Conference on Artiﬁcial Intelligence.

Buro, M., Long, J. R., Furtak, T., & Sturtevant, N. R. (2009). Improving state evaluation, inference, and search in trick-based card games.. In IJCAI, pp. 1407 1413.

Cao, R., & Naumov, P. (2020). Knowing the price of success. Artiﬁcial Intelligence, 284, 103287. ˇCerm ak, P., Lomuscio, A., & Murano, A. (2015). Verifying and synthesising multi-agent systems against one-goal strategy logic speciﬁcations. In Twenty-Ninth AAAI Conference on Artiﬁcial Intelligence.

Chatterjee, K., Henzinger, T. A., & Piterman, N. (2010). Strategy logic. Information and Computation, 208(6), 677 693.

Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995). Reasoning about knowledge. MIT Press, Cambridge, MA.

Fervari, R., Herzig, A., Li, Y., & Wang, Y. (2017). Strategically knowing how. In Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence, IJCAI17, pp. 1031 1038.

Gabbay, D. M. (1972). A general ﬁltration method for modal logics. Journal of Philosophical Logic, 1(1), 29 34.

Goranko, V. (2001). Coalition games and alternating temporal logics. In Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge, pp. 259 272. Morgan Kaufmann Publishers Inc.

Pavel Naumov and Yuan Yuan

Goranko, V., & Enqvist, S. (2018). Socially friendly and group protecting coalition logics. In Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems, pp. 372 380. International Foundation for Autonomous Agents and Multiagent Systems.

Goranko, V., Jamroga, W., & Turrini, P. (2013). Strategic games and truly playable eﬀectivity functions. Autonomous Agents and Multi-Agent Systems, 26(2), 288 314.

Goranko, V., & Ju, F. (2019). Towards a logic for conditional local strategic reasoning. In International Workshop on Logic, Rationality and Interaction, pp. 112 125. Springer.

Goranko, V., & Ju, F. (2021). A logic for conditional local strategic reasoning. Journal of Logic, Language and Information, (to appear). ar Xiv:2102.06148.

Goranko, V., & van Drimmelen, G. (2006). Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science, 353(1), 93 117.

Jamroga, W., & Agotnes, T. (2007). Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics, 17(4), 423 475.

Jamroga, W., & van der Hoek, W. (2004). Agents that know how to play. Fundamenta Informaticae, 63(2-3), 185 219.

Jiang, Q., Li, K., Du, B., Chen, H., & Fang, H. (2019). Delta Dou: Expert-level Doudizhu AI through self-play.. In IJCAI, pp. 1265 1271.

Liu, T., Zheng, Z., Li, H., Bian, K., & Song, L. (2019). Playing card-based RTS games with deep reinforcement learning. In IJCAI, pp. 4540 4546.

Mendelson, E. (2009). Introduction to mathematical logic. CRC press.

Mogavero, F., Murano, A., Perelli, G., & Vardi, M. Y. (2012). What makes ATL* decidable? a decidable fragment of strategy logic. In International Conference on Concurrency Theory, pp. 193 208. Springer.

Mogavero, F., Murano, A., Perelli, G., & Vardi, M. Y. (2014). Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic (TOCL), 15(4), 34.

Mogavero, F., Murano, A., Perelli, G., & Vardi, M. Y. (2017). Reasoning about strategies: on the satisﬁability problem. Logical Methods in Computer Science, 13.

Naumov, P., & Tao, J. (2017a). Coalition power in epistemic transition systems. In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 723 731.

Naumov, P., & Tao, J. (2017b). Together we know how to achieve: An epistemic logic of know-how. In Proceedings of 16th conference on Theoretical Aspects of Rationality and Knowledge (TARK), July 24-26, 2017, EPTCS 251, pp. 441 453.

Naumov, P., & Tao, J. (2018a). Second-order know-how strategies. In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 390 398.

Naumov, P., & Tao, J. (2018b). Strategic coalitions with perfect recall. In Proceedings of Thirty-Second AAAI Conference on Artiﬁcial Intelligence.

Intelligence in Strategic Games

Naumov, P., & Tao, J. (2018c). Together we know how to achieve: An epistemic logic of know-how. Artiﬁcial Intelligence, 262, 279 300.

Parker, A., Nau, D., & Subrahmanian, V. (2006). Overconﬁdence or paranoia? Search in imperfect-information games. In Proceedings Of The National Conference On Artiﬁcial Intelligence. Menlo Park, CA; Cambridge, MA; London; AAAI Press; MIT Press; 1999.

Pauly, M. (2001). Logic for Social Software. Ph.D. thesis, 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.

Sandholm, T. (2017). Super-human AI for strategic reasoning: Beating top pros in heads-up no-limit Texas Hold em. In IJCAI, pp. 24 25.

Sauro, L., Gerbrandy, J., van der Hoek, W., & Wooldridge, M. (2006). Reasoning about action and cooperation. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 06, pp. 185 192, New York, NY, USA. ACM.

Schmid, M., Moravcik, M., & Hladik, M. (2014). Bounding the support size in extensive form games with imperfect information. In Twenty-Eighth AAAI Conference on Artiﬁcial Intelligence.

Sevenster, M. (2004). Battleships as a decision problem. ICGA Journal, 27(3), 142 149.

Showell, J. P. M. (2003). German Naval Code Breakers (1st edition). Naval Inst Pr.

Sinha, A., Fang, F., An, B., Kiekintveld, C., & Tambe, M. (2018). Stackelberg security games: Looking beyond a decade of success.. In IJCAI, pp. 5494 5501.

Tammelin, O., Burch, N., Johanson, M., & Bowling, M. (2015). Solving heads-up limit Texas Hold em. In Twenty-Fourth International Joint Conference on Artiﬁcial Intelligence.

van Benthem, J. (2001). Games in dynamic-epistemic logic. Bulletin of Economic Research, 53(4), 219 248.

van der Hoek, W., & Wooldridge, M. (2003). Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, 75(1), 125 157.

van der Hoek, W., & Wooldridge, M. (2005). On the logic of cooperation and propositional control. Artiﬁcial Intelligence, 164(1), 81 119.

van Ditmarsch, H. P. (2002). Descriptions of game actions. Journal of Logic, Language and Information, 11(3), 349 365.

Walther, D., van der Hoek, W., & Wooldridge, M. (2007). Alternating-time temporal logic with explicit strategies. In Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge, pp. 269 278. ACM.

Wang, Y. (2015). A logic of knowing how. In Logic, Rationality, and Interaction, pp. 392 405. Springer.

Wang, Y. (2018). A logic of goal-directed knowing how. Synthese, 195(10), 4419 4439.

Pavel Naumov and Yuan Yuan

W ang, Y. N., & Agotnes, T. (2020). Simpler completeness proofs for modal logics with intersection. In International Workshop on Dynamic Logic, pp. 259 276. Springer.

Wisser, F. (2015). An expert-level card playing agent based on a variant of perfect information monte carlo sampling. In Twenty-Fourth International Joint Conference on Artiﬁcial Intelligence.