Together We Know How to Achieve: An Epistemic Logic of Know-How (Extended Abstract)
Pavel Naumov Jia Tao
cs.AI cs.LO


Equivariant extensions of 𝔾_a-torsors over punctured
surfaces
    Takashi Kishimoto 
    
=============================================================




The existence of a coalition strategy to achieve a goal does not necessarily mean that the coalition has enough information to know how to follow the strategy. Neither does it mean that the coalition knows that such a strategy exists. The paper studies an interplay between the distributed knowledge, coalition strategies, and coalition “know-how" strategies. The main technical result is a sound and complete trimodal logical system that describes the properties of this interplay.




















































Equivariant extensions of 𝔾_a-torsors over punctured
surfaces
    Takashi Kishimoto 
    
=============================================================





§ INTRODUCTION




An agent a comes to a fork in a road. There is a sign that says that one of the two roads leads to prosperity, another to death. The agent must take the fork, but she does not know which road leads where. Does the agent have a strategy to get to prosperity? On one hand, since one of the roads leads to prosperity, such a strategy clearly exists. We denote this fact by modal formula _a p, where statement p is a claim of future prosperity. Furthermore, agent a knows that such a strategy exists. We write this as _a_a p. Yet, the agent does not know what the strategy is and, thus, does not know how to use the strategy. We denote this by _a p, where know-how modality _a expresses the fact that agent a knows how to achieve the goal based on the information available to her.  In this paper we study the interplay between modality , representing knowledge, modality , representing the existence of a strategy, and modality , representing the existence of a know-how strategy. Our main result is a complete trimodal axiomatic system capturing properties of this interplay.



 §.§ Epistemic Transition Systems


In this paper we use epistemic transition systems to capture knowledge and strategic behavior. Informally, epistemic transition system is a directed labeled graph supplemented by an indistinguishability relation on vertices. For instance, our motivational example above can be captured by epistemic transition system T_1 depicted in Figure <ref>. 

In this system state w represents the prosperity and state w' represents death. The original state is u, but it is indistinguishable by the agent a from state v. Arrows on the diagram represent possible transitions between the states. Labels on the arrows represent the choices that the agents make during the transition. For example, if in state u agent chooses left (L) road, she will transition to the prosperity state w and if she chooses right (R) road, she will transition to the death state w'. In another epistemic state v, these roads lead the other way around. States u and v are not distinguishable by agent a, which is shown by the dashed line between these two states. In state u as well as state v the agent has a strategy to transition to the state of prosperity: u⊩_a p and v⊩_a p. In the case of state u this strategy is L, in the case of state v the strategy is R. Since the agent cannot distinguish states u and v, in both of these states she does not have a know-how strategy to reach prosperity: u⊮_a p and v⊮_a p. At the same time, since formula _a p is satisfied in all states  indistinguishable to agent a from state u, we can claim that u⊩_a_a p and, similarly, v⊩_a_a p. 



As our second example, let us consider the epistemic transition system T_2 obtained from T_1 by swapping labels on transitions from v to w and from v to w', see Figure <ref>. Although in system T_2 agent a still cannot distinguish states u and v, she has a know-how strategy from either of these states to reach state w. We write this as u⊩_a p and v⊩_a p. The strategy is to choose L. This strategy is know-how because it does not require to make different choices in the states that the agent cannot distinguish. 



 §.§ Imperfect Recall

For the next example, we consider a transition system T_3 obtained from system T_1 by adding a new epistemic state s. From state s, agent a can choose label L to reach state u or choose label R to reach state v. Since proposition q is satisfied in state u, agent a has a know-how strategy to transition from state s to a state (namely, state u) where q is satisfied. Therefore, s⊩_a q. 



A more interesting question is whether s⊩_a_a p is true. In other words, does agent a know how to transition from state s to a state in which she knows how to transition to another state in which p is satisfied? One might think that such a strategy indeed exists: in state s agent a chooses  label L to transition to state u. Since there is no transition labeled by L that leads from state s to state v, upon ending the first transition the agent would know that she is in state u, where she needs to choose label L to transition to state w. This argument, however, is based on the assumption that agent a has a perfect recall. Namely, agent a in state u remembers the choice that she made in the previous state. We assume that the agents do not have a perfect recall and that an epistemic state description captures whatever memories the agent has in this state. In other words, in this paper we assume that the only knowledge that an agent possesses is the knowledge captured by the indistinguishability relation on the epistemic states. Given this assumption, upon reaching the state u (indistinguishable from state v) agent a knows that there exists a choice that she can make to transition to state in which p is satisfied: s⊩_a_a p. However, she does not know which choice (L or R) it is: s⊮_a_a p. 



 §.§ Multiagent Setting




So far, we have assumed that only agent a has an influence on which transition the system takes. In transition system T_4 depicted in Figure <ref>, we introduce another agent b and assume both agents a and b have influence on the transitions. In each state, the system takes the transition labeled D by default unless there is a consensus of agents a and b to take the transition labeled C. In such a setting, each agent has a strategy to transition system from state u into state w by voting D, but neither of them alone has a strategy to transition from state u to state w' because such a transition requires the consensus of both agents. Thus, u⊩_a p∧_b p∧_a q∧_b q. Additionally, both agents know how to transition the system from state u into state w, they just need to vote D. Therefore, u⊩_a p∧_b p.



In Figure <ref>, we show a more complicated transition system obtained from T_1 by renaming label L to D and renaming label R to C. Same as in transition system T_4, we assume that there are two agents a and b voting on the system transition. We also assume that agent a cannot distinguish states u and v while agent b can. By default, the system takes the transition labeled D unless there is a consensus to take transition labeled C. As a result, agent a has a strategy (namely, vote D) in state u to transition system to state w, but because agent a cannot distinguish state u from state v, not only does she not know how to do this, but she is not aware that such a strategy exists: u⊩_a p∧_a p ∧_a_a p. Agent b, however, not only has a strategy to transition the system from state u to state w, but also knows how to achieve this: u⊩_b p.




 §.§ Coalitions


We have talked about strategies, know-hows, and knowledge of individual agents. In this paper we consider knowledge, strategies, and know-how strategies of coalitions. There are several forms of group knowledge that have been studied before. The two most popular of them are common knowledge and distributed knowledge <cit.>. Different contexts call for different forms of group knowledge.

As illustrated in the famous Two Generals' Problem <cit.> where communication channels between the agents are unreliable, establishing a common knowledge between agents might be essential for having a strategy. 

In some settings, the distinction between common and distributed knowledge is insignificant. For example, if members of a political fraction get together to share all their information and to develop a common strategy, then the distributed knowledge of the members becomes the common knowledge of the fraction during the in-person meeting.

Finally, in some other situations the distributed knowledge makes more sense than the common knowledge. For example, if a panel of experts is formed to develop a strategy, then this panel achieves the best result if it relies on the combined knowledge of its members rather than on their common knowledge.

In this paper we focus on distributed coalition knowledge and distributed-know-how strategies. We leave the common knowledge for the future research.

To illustrate how distributed knowledge of coalitions interacts with strategies and know-hows, consider epistemic transition system T_6 depicted in Figure <ref>. In this system, agents a and b cannot distinguish states u and v while agents b and c cannot distinguish states v and u'. In every state, each of agents a, b and c votes either L or R, and the system transitions according to the majority vote. In such a setting, any coalition of two agents can fully control the transitions of the system. 



For example, by both voting L, agents a and b form a coalition {a,b} that forces the system to transition from state u to state w no matter how agent c votes. Since proposition p is satisfied in state w, we write u⊩_{a,b} p, or simply u⊩_a,b p. Similarly, coalition {a,b} can vote R to force the system to transition from state v to state w. Therefore, coalition {a,b} has strategies to achieve p in states u and v, but the strategies are different. Since they cannot distinguish states u and v, agents a and b know that they have a strategy to achieve p, but they do not know how to achieve p. In our notations, v⊩ S_a,bp∧_a,bS_a,bp ∧_a,b p.   

On the other hand, although agents b and c cannot distinguish states v and u', by both voting R in either of states v and u', they form a coalition {b, c} that forces the system to transition to state w where p is satisfied. Therefore, in any of states v and u', they not only have a strategy to achieve p, but also know that they have such a strategy, and more importantly, they know how to achieve p, that is, v⊩_b,c p. 




 §.§ Nondeterministic Transitions


In all the examples that we have discussed so far, given any state in a system, agents' votes uniquely determine the transition of the system. Our framework also allows nondeterministic transitions. Consider transition system T_7 depicted in Figure <ref>. In this system, there are two agents a and b who can vote either C or D. If both agents vote C, then the system takes one of the consensus transitions labeled with C. Otherwise, the system takes the transition labeled with D. Note that there are two consensus transitions starting from state u. Therefore, even if both agents vote C, they do not have a strategy to achieve p, i.e., u⊮_a,bp. However, they can achieve p∨ q. Moreover, since all agents can distinguish all states, we have u ⊩_a,b(p∨ q).








 §.§ Universal Principles


In the examples above we focused on specific properties that were either satisfied or not satisfied in particular states of epistemic transition systems T_1 through T_7.
In this paper, we study properties that are satisfied in all states of all epistemic transition systems. Our main result is a sound and complete axiomatization of all such properties. We finish the introduction with an informal discussion of these properties.




  
Properties of Single Modalities
Knowledge modality K_C satisfies the axioms of epistemic logic S5 with distributed knowledge. Both strategic modality S_C and know-how modality _C satisfy cooperation properties <cit.>:  

    _C(ϕ→ψ)→(_Dϕ→_C∪ Dψ),  C∩ D=∅,
       _C(ϕ→ψ)→(_Dϕ→_C∪ Dψ),  C∩ D=∅.

They also satisfy monotonicity properties

    _Cϕ→_Dϕ,  C⊆ D,
    _Cϕ→_Dϕ,  C⊆ D.

The two monotonicity properties are not among the axioms of our logical system because, as we show in Lemma <ref> and Lemma <ref>, they are derivable.



  
Properties of Interplay

Note that w⊩_Cϕ means that coalition C has the same strategy to achieve ϕ in all epistemic states indistinguishable by the coalition from state w. Hence, the following principle is universally true:

    _Cϕ→ K_C_Cϕ.

Similarly, w⊩_Cϕ means that coalition C does not have the same strategy to achieve ϕ in all epistemic states indistinguishable by the coalition from state w. Thus,

    _Cϕ→ K_C_Cϕ.

We call properties (<ref>) and (<ref>) strategic positive introspection and strategic negative introspection, respectively. 
The strategic negative introspection is one of our axioms. Just as how the positive introspection principle follows from the rest of the axioms in S5, the strategic positive introspection principle is also derivable (see Lemma <ref>).

Whenever a coalition knows how to achieve something, there should exist a strategy for the coalition to achieve. In our notation,

    _Cϕ→_Cϕ.

We call this formula strategic truth property and it is one of the axioms of our logical system.

The last two axioms of our logical system deal with empty coalitions. First of all, if formula _∅ϕ is satisfied in an epistemic state of our transition system, then formula ϕ must be satisfied in every state of this system. Thus, even empty coalition has a trivial strategy to achieve ϕ:

    _∅ϕ→_∅ϕ.

We call this property empty coalition principle. In this paper we assume that an epistemic transition system never halts. That is, in every state of the system no matter what the outcome of the vote is, there is always a next state for this vote. This restriction on the transition systems yields property 

    _C.

that we call nontermination principle.

Let us now turn to the most interesting and perhaps most unexpected property of interplay. Note that _∅ϕ means that an empty coalition has a strategy to achieve ϕ. Since the empty coalition has no members, nobody has to vote in a particular way. Statement ϕ is guaranteed to happen anyway. Thus, statement _∅ϕ simply means that statement ϕ is unavoidably satisfied after any single transition. 


For example, consider an epistemic transition system depicted in Figure <ref>. As in some of our earlier examples, this system has agents a and b who vote either C or D. If both agents vote C, then the system takes one of the consensus transitions labeled with C. Otherwise, the system takes the default transition labeled with D. Note that in state v it is guaranteed that statement p will happen after a single transition. Thus, v⊩_∅ p. At the same time, neither agent a nor agent b knows about this because they cannot distinguish state v from states u and u' respectively. Thus, v⊩_a_∅ p ∧_b_∅ p. 

In the same transition system T_8, agents a and b together can distinguish state v from states u and u'. Thus, v⊩_a,b_∅ p. 
In general,  statement _C_∅ϕ means that not only ϕ is unavoidable, but coalition C knows about it. Thus, coalition C has a know-how strategy to achieve ϕ:

    _C_∅ϕ→_Cϕ.

In fact, the coalition would achieve the result no matter which strategy it uses. Coalition C can even use a strategy that simultaneously achieves another result in addition to ϕ: 

    _C_∅ϕ∧_Cψ→_C(ϕ∧ψ).

In our logical system we use an equivalent form of the above principle that is stated using only implication:

    _C(ϕ→ψ)→(_C_∅ϕ→_Cψ).

We call this property epistemic determinicity principle. Properties (<ref>), (<ref>), (<ref>), (<ref>), (<ref>), (<ref>), and (<ref>), together with axioms of epistemic logic S5 with distributed knowledge and propositional tautologies constitute the axioms of our sound and complete logical system. 



 §.§ Literature Review


Logics of coalition power were developed by Marc Pauly <cit.>, who also proved the completeness of the basic logic of coalition power. 
Pauly's approach has been widely studied in the literature <cit.>. An alternative logical system  was proposed by More and Naumov <cit.>. 

Alur, Henzinger, and Kupferman introduced Alternating-Time Temporal Logic (ATL) that combines temporal and coalition modalities <cit.>.
Van der Hoek and Wooldridge proposed to combine ATL with epistemic modality to form Alternating-Time Temporal Epistemic Logic <cit.>. They did not prove the completeness theorem for the proposed logical system. 

Ågotnes and Alechina proposed a complete logical system that combines the coalition power and epistemic modalities <cit.>. Since this system does not have epistemic requirements on strategies, it does not contain any axioms describing the interplay of these modalities. 




Know-how strategies were studied before under different names. While Jamroga and Ågotnes talked about “knowledge to identify and execute a strategy" <cit.>,  Jamroga and van der Hoek discussed “difference between an agent knowing that he has a suitable strategy and knowing the strategy itself" <cit.>. Van Benthem called such strategies “uniform" <cit.>. Wang gave a complete axiomatization of “knowing how" as a binary modality <cit.>, but his logical system does not include the knowledge modality.  

In our AAMAS'17 paper, we investigated coalition strategies to enforce a condition indefinitely <cit.>. Such strategies are similar to “goal maintenance" strategies in Pauly's “extended coalition logic" <cit.>. We focused on “executable" and “verifiable" strategies. Using the language of the current paper, executability means that a coalition remains “in the know-how" throughout the execution of the strategy. Verifiability means that the coalition can verify that the enforced condition remains true. In the notations of the current paper, the existence of a verifiable strategy could be expressed as _C_Cϕ.  In <cit.>, we provided a complete logical system that describes the interplay between the modality representing the existence of an “executable" and “verifiable" coalition strategy to enforce and the modality representing knowledge. This system can prove principles similar to the strategic positive introspection (<ref>) and the strategic negative introspection (<ref>) mentioned above.  

In the current paper, we combine know-how modality  with strategic modality  and epistemic modality . The proof of the completeness theorem is significantly more challenging than the one in <cit.>. It employs new techniques that construct pairs of maximal consistent sets in “harmony" and in “complete harmony", which are discussed in the full version of this paper <cit.>. 



 §.§ Paper Outline


This paper is organized as follows. In Section <ref> we introduce formal syntax and semantics of our logical system. In Section <ref> we list axioms and inference rules of the system. Section <ref> provides examples of formal proofs in our logical systems. Section <ref> concludes the paper.

The proofs of the soundness and the completeness can be found in the full version of this paper <cit.>. The key part of the proof of the completeness is the construction of a pair of sets in complete harmony.



§ SYNTAX AND SEMANTICS


In this section we present the formal syntax and semantics of our logical system given a fixed finite set of agents 𝒜. Epistemic transition system could be thought of as a Kripke model of modal logic S5 with distributed knowledge to which we add transitions controlled by a vote aggregation mechanism. Examples of vote aggregation mechanisms that we have considered in the introduction are the consensus/default mechanism and the majority vote mechanism. Unlike the introductory examples, in the general definition below we assume that at different states the mechanism might use different rules for vote aggregation. The only restriction on the mechanism that we introduce is that there should be at least one possible transition that the system can take no matter what the votes are. In other words, we assume that the system can never halt.  

For any set of votes V, by V^𝒜 we mean the set of all functions from set 𝒜 to set V. Alternatively, the set V^𝒜 could be thought of as a set of tuples of elements of V indexed by elements of 𝒜.


A tuple (W,{∼_a}_a∈𝒜,V,M,π) is called an epistemic transition system, where

    
  * W is a set of epistemic states,
    
  * ∼_a is an indistinguishability equivalence relation on W for each a∈𝒜,
    
  * V is a nonempty set called “domain of choices", 
    
  * M⊆ W× V^𝒜× W is an aggregation mechanism where for each w∈ W and each 𝐬∈ V^𝒜, there is w'∈ W  such that (w,𝐬,w')∈ M,
    
  * π is a function that maps propositional variables into subsets of W.




A coalition is a subset of 𝒜.


Note that a coalition is always finite due to our assumption that the set of all agents 𝒜 is finite. Informally, we say that two epistemic states are indistinguishable by a coalition C if they are indistinguishable by every member of the coalition. Formally, coalition indistinguishability is defined as follows:



For any epistemic states w_1,w_2∈ W and any coalition C, let w_1∼_C w_2 if w_1∼_a w_2 for each agent a∈ C.



Relation ∼_C is an equivalence relation on the set of states W for each coalition C. 


By a strategy profile {s_a}_a∈ C of a coalition C we mean a tuple that specifies vote s_a∈ V of each member a∈ C. Since such a tuple can also be viewed as a function from set C to set V, we denote the set of all strategy profiles of a coalition C by V^C:


Any tuple {s_a}_a∈ C∈ V^C is called a strategy profile of coalition C.


In addition to a fixed finite set of agents 𝒜 we  also assume a fixed countable set of propositional variables.  The language Φ of our formal logical system is specified in the next definition.   


Let Φ be the minimal set of formulae such that

    
  * p∈Φ for each propositional variable p,
    
  * ϕ,ϕ→ψ∈Φ for all formulae ϕ,ψ∈Φ,
    
  * _Cϕ,_Cϕ,_Cϕ∈Φ for each coalition C and each ϕ∈Φ.



In other words, language Φ is defined by the following grammar:

    ϕ := p | ϕ | ϕ→ϕ | _Cϕ | _Cϕ | _Cϕ.


By  we denote the negation of a tautology. For example, we can assume that  is (p→ p) for some fixed propositional variable p. 

According to Definition <ref>, a mechanism specifies the transition that a system might take for any strategy profile of the set of all agents 𝒜. It is sometimes convenient to consider transitions that are consistent with a given strategy profile 𝐬 of a give coalition C⊆𝒜. We write w→_𝐬u if a transition from state w to state u is consistent with strategy profile 𝐬. The formal definition is below. 



For any epistemic states w,u∈ W, any coalition C, and any strategy profile 𝐬={s_a}_a∈ C∈ V^C, we write w→_𝐬u if (w,𝐬',u)∈ M for some strategy profile 𝐬'={s'_a}_a∈𝒜∈ V^𝒜  such that s'_a=s_a for each a∈ C.


For any strategy profile 𝐬 of the empty coalition ∅, if there are a coalition C and a strategy profile 𝐬' of coalition C such that w→_𝐬' u, then w→_𝐬u.



 The next definition is the key definition of this paper. It formally specifies the meaning of the three modalities in our logical system.
















For any epistemic state w∈ W of a transition system (W,{∼_a}_a∈𝒜,V,M,π) and any formula ϕ∈Φ, let relation w⊩ϕ be defined as follows

    
  * w⊩ p if w∈π(p) where p is a propositional variable,
    
  * w⊩ϕ if w⊮ϕ,
    
  * w⊩ϕ→ψ if w⊮ϕ or w⊩ψ,
    
  * w⊩_Cϕ if w'⊩ϕ for each w'∈ W such that w∼_C w',
    
  * w⊩_Cϕ if there is a strategy profile 𝐬∈ V^C such that  w→_𝐬 w' implies w'⊩ϕ for every w'∈ W,
    
  * w⊩_Cϕ if there is a strategy profile 𝐬∈ V^C such that w∼_C w' and w'→_𝐬 w” imply w”⊩ϕ for all w',w”∈ W.





§ AXIOMS


In additional to propositional tautologies in language Φ, our logical system consists of the following axioms. 

    
  * Truth: _Cϕ→ϕ,
    
  * Negative Introspection: _Cϕ→_C_Cϕ,
    
  * Distributivity: _C(ϕ→ψ)→(_Cϕ→_Cψ),
    
  * Monotonicity: _Cϕ→_Dϕ, if C⊆ D,
    
    
    
  * Cooperation: _C(ϕ→ψ)→(_Dϕ→_C∪ Dψ), where C∩ D=∅.
    
  * Strategic Negative Introspection: _Cϕ→_C_Cϕ,
    
  * Epistemic Cooperation: _C(ϕ→ψ)→(_Dϕ→_C∪ Dψ), where C∩ D=∅,
    
  * Strategic Truth: _Cϕ→_Cϕ,
    
  * Epistemic Determinicity:
 _C(ϕ→ψ)→(_C_∅ϕ→_Cψ),
    
  * Empty Coalition: _∅ϕ→_∅ϕ,
    
  * Nontermination: _C.

We have discussed the informal meaning of these axioms in the introduction. In the full version of this paper <cit.>, we formally prove the soundness of these axioms with respect to the semantics from Definition <ref>.

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

    ϕ_Cϕϕ_Cϕϕ,ϕ→ψψ.

We write X⊢ϕ if formula ϕ is provable from the theorems of our logical system and a set of additional axioms X using only Modus Ponens inference rule.



§ DERIVATION EXAMPLES


In this section we give examples of formal derivations in our logical system. In Lemma <ref> we prove the strategic positive introspection principle (<ref>) discussed in the introduction. 


⊢_Cϕ→_C_Cϕ.


Note that formula _Cϕ→_C_Cϕ is an instance of Strategic Negative Introspection axiom. Thus, ⊢_C_Cϕ→_Cϕ by the law of contrapositive in the propositional logic. Hence,
⊢_C(_C_Cϕ→_Cϕ) by  Necessitation inference rule. Thus, by  Distributivity axiom and Modus Ponens inference rule, 

    ⊢_C_C_Cϕ→_C_Cϕ.


At the same time, _C_Cϕ→_Cϕ is an instance of Truth axiom. Thus, ⊢_Cϕ→_C_Cϕ by contraposition. Hence, taking into account the following instance of Negative Introspection axiom _C_Cϕ→_C_C_Cϕ,
one can conclude that ⊢_Cϕ→_C_C_Cϕ. The latter, together with statement (<ref>), implies the statement of the lemma by the laws of propositional reasoning.


In the next example, we show that the existence of a know-how strategy by a coalition implies that the coalition has a distributed knowledge of the existence of a strategy.


⊢_Cϕ→_C_Cϕ.


By Strategic Truth axiom, ⊢_Cϕ→_Cϕ. Hence, ⊢_C(_Cϕ→_Cϕ) by Necessitation inference rule. Thus, ⊢_C_Cϕ→_C_Cϕ by Distributivity axiom and Modus Ponens inference rule. At the same time, ⊢_Cϕ→_C_Cϕ by Lemma <ref>. Therefore, ⊢_Cϕ→_C_Cϕ by the laws of propositional reasoning.


The next lemma shows that the existence of a know-how strategy by a sub-coalition implies the existence of a know-how strategy by the entire coalition.


⊢_Cϕ→_Dϕ, where C⊆ D.


Note that ϕ→ϕ is a propositional tautology. Thus, ⊢ϕ→ϕ. Hence, ⊢_D∖ C(ϕ→ϕ) by Strategic Necessitation inference rule. At the same time, by Epistemic Cooperation axiom,
⊢_D∖ C(ϕ→ϕ)→(_Cϕ→_Dϕ)
due to the assumption C⊆ D.  Therefore, ⊢_Cϕ→_Dϕ by Modus Ponens inference rule.


Although our logical system has three modalities, the system contains necessitation inference rules 
only for two of them. The lemma below shows that the necessitation rule for the third modality is admissible.

For each finite C⊆𝒜, inference rule ϕ_Cϕ is admissible in our logical system.


Assumption ⊢ϕ implies ⊢_Cϕ by Strategic Necessitation inference rule. Hence, ⊢_Cϕ by Strategic Truth axiom and Modus Ponens inference rule.


The next result is a counterpart of Lemma <ref>. It states that the existence of a strategy by a sub-coalition implies the existence of a strategy by the entire coalition.


⊢_Cϕ→_Dϕ, where C⊆ D.


Note that ϕ→ϕ is a propositional tautology. Thus, ⊢ϕ→ϕ. Hence,  ⊢_D∖ C(ϕ→ϕ) by Lemma <ref>.
At the same time, by Cooperation axiom,
⊢_D∖ C(ϕ→ϕ)→(_Cϕ→_Dϕ)
due to the assumption C⊆ D.  Therefore, ⊢_Cϕ→_Dϕ by Modus Ponens inference rule.






§ CONCLUSION


In this paper we proposed a sound and complete logic system that captures an interplay between the  distributed knowledge, coalition strategies, and how-to strategies. In the future work we hope to explore know-how strategies of non-homogeneous coalitions in which different members contribute differently to the goals of the coalition. For example, “incognito" members of a coalition might contribute only by sharing information, while “open" members also contribute by voting.

eptcs


 






