Together We Know How to Achieve: An Epistemic Logic of Know-How

TL;DR

This paper develops a formal logical framework to analyze the relationship between distributed knowledge, coalition strategies, and coalition 'know-how' strategies, providing a sound and complete system for reasoning about these concepts.

Contribution

It introduces a novel trimodal logical system that captures the interplay between knowledge and strategic ability in coalitions, advancing formal epistemic and strategic reasoning.

Findings

Established a sound and complete logical system.

Clarified the distinction between knowing that a strategy exists and knowing how to implement it.

Provided formal tools for reasoning about coalition knowledge and strategies.

Abstract

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 article 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.

Equations

$${\mathsf{S}}_C(\phi \to \psi )\to ({\mathsf{S}}_D\phi \to {\mathsf{S}}_{C\cup D}\psi ),\text{mbox}whereC\cap D=\varnothing ,$$

$${\mathsf{H}}_C(\phi \to \psi )\to ({\mathsf{H}}_D\phi \to {\mathsf{H}}_{C\cup D}\psi ),\text{mbox}whereC\cap D=\varnothing .$$

$${\mathsf{S}}_C\phi \to {\mathsf{S}}_D\phi ,\text{mbox}whereC\subseteq D,$$

$${\mathsf{H}}_C\phi \to {\mathsf{H}}_D\phi ,\text{mbox}whereC\subseteq D.$$

$${\mathsf{H}}_C\phi \to K_C{\mathsf{H}}_C\phi .$$

$$\neg {\mathsf{H}}_C\phi \to K_C\neg {\mathsf{H}}_C\phi .$$

$${\mathsf{H}}_C\phi \to {\mathsf{S}}_C\phi .$$

$${\mathsf{K}}_{\varnothing }\phi \to {\mathsf{H}}_{\varnothing }\phi .$$

$$\neg {\mathsf{S}}_C\perp .$$

$${\mathsf{K}}_C{\mathsf{S}}_{\varnothing }\phi \to {\mathsf{H}}_C\phi .$$

$${\mathsf{K}}_C{\mathsf{S}}_{\varnothing }\phi \wedge {\mathsf{H}}_C\psi \to {\mathsf{H}}_C(\phi \wedge \psi ).$$

$${\mathsf{H}}_C(\phi \to \psi )\to ({\mathsf{K}}_C{\mathsf{S}}_{\varnothing }\phi \to {\mathsf{H}}_C\psi ).$$

$$\phi :=p|\neg \phi |\phi \to \phi |{\mathsf{K}}_C\phi |{\mathsf{S}}_C\phi |{\mathsf{H}}_C\phi .$$

$$\frac{\phi }{{\mathsf{K}}_C\phi }\frac{\phi }{{\mathsf{H}}_C\phi }\frac{\phi ,\phi \to \psi }{\psi }.$$

$$⊢{\mathsf{K}}_C\neg {\mathsf{K}}_C\neg {\mathsf{H}}_C\phi \to {\mathsf{K}}_C{\mathsf{H}}_C\phi .$$

$$s_a=\{\begin{array}{ll}{s}_a^1,& \text{mbox}ifa\in C,\\ s_a^2,& \text{mbox}ifa\in D.\end{array}$$

$$⊢{\mathsf{K}}_C\neg {\mathsf{K}}_C\neg {\mathsf{K}}_C\phi \to {\mathsf{K}}_C{\mathsf{K}}_C\phi .$$

$$⊢{\phi }_1\to ({\phi }_2\to \dots ({\phi }_n\to \psi )\dots ).$$

$$⊢{\mathsf{K}}_C({\phi }_1\to ({\phi }_2\to \dots ({\phi }_n\to \psi )\dots )).$$

$${\mathsf{K}}_C{\phi }_1⊢{\mathsf{K}}_C({\phi }_2\to \dots ({\phi }_n\to \psi )\dots ).$$

$${\mathsf{K}}_C{\phi }_1,\dots ,{\mathsf{K}}_C{\phi }_n⊢{\mathsf{K}}_C\psi .$$

$$⊢{\phi }_1\to ({\phi }_2\to (\dots ({\phi }_n\to \psi )\dots )).$$

$$⊢{\mathsf{S}}_{D_1}{\phi }_1\to {\mathsf{S}}_{\varnothing \cup D_1}({\phi }_2\to (\dots ({\phi }_n\to \psi )\dots )).$$

$$⊢{\mathsf{S}}_{D_1}{\phi }_1\to {\mathsf{S}}_{D_1}({\phi }_2\to (\dots ({\phi }_n\to \psi )\dots )).$$

$${\mathsf{S}}_{D_1}{\phi }_1⊢{\mathsf{S}}_{D_1}({\phi }_2\to (\dots ({\phi }_n\to \psi )\dots )).$$

$${\mathsf{S}}_{D_1}{\phi }_1⊢{\mathsf{S}}_{D_2}{\phi }_2\to {\mathsf{S}}_{D_1\cup D_2}(\dots ({\phi }_n\to \psi )\dots ).$$

$${\mathsf{S}}_{D_1}{\phi }_1,{\mathsf{S}}_{D_2}{\phi }_2⊢{\mathsf{S}}_{D_1\cup D_2}(\dots ({\phi }_n\to \psi )\dots ).$$

$${\mathsf{S}}_{D_1}{\phi }_1,{\mathsf{S}}_{D_2}{\phi }_2,\dots ,{\mathsf{S}}_{D_n}{\phi }_n⊢{\mathsf{S}}_{D_1\cup D_2\cup \cdots \cup D_n}\psi .$$

$$X,\neg {\mathsf{S}}_{\varnothing }\phi ⊢{\mathsf{S}}_{\varnothing }\neg \wedge Y_1$$

$$X⊢{\mathsf{S}}_{\varnothing }\neg \wedge Y_2.$$

Full text

1 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 ${\sf S}_{a}p$, where statement $p$ is a claim of future prosperity. Furthermore, agent $a$ knows that such a strategy exists. We write this as ${\sf K}_{a}{\sf S}_{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 $\neg{\sf H}_{a}p$, where know-how modality ${\sf H}_{a}$ expresses the fact that agent $a$ knows how to achieve the goal based on the information available to her. In this article we study the interplay between modality ${\sf K}$, representing knowledge, modality ${\sf S}$, representing the existence of a strategy, and modality ${\sf H}$, representing the existence of a know-how strategy. Our main result is a complete trimodal axiomatic system capturing properties of this interplay.

1.1 Epistemic Transition Systems

In this article 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 1.

In this system state $w$ represents the prosperity and state $w^{\prime}$ 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^{\prime}$. 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\Vdash{\sf S}_{a}p$ and $v\Vdash{\sf S}_{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\nVdash{\sf H}_{a}p$ and $v\nVdash{\sf H}_{a}p$. At the same time, since formula ${\sf S}_{a}p$ is satisfied in all states indistinguishable to agent $a$ from state $u$, we can claim that $u\Vdash{\sf K}_{a}{\sf S}_{a}p$ and, similarly, $v\Vdash{\sf K}_{a}{\sf S}_{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^{\prime}$, see Figure 2. 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\Vdash{\sf H}_{a}p$ and $v\Vdash{\sf H}_{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.

1.2 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\Vdash{\sf H}_{a}q$.

A more interesting question is whether $s\Vdash{\sf H}_{a}{\sf H}_{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 article 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\Vdash{\sf H}_{a}{\sf S}_{a}p$. However, she does not know which choice (L or R) it is: $s\nVdash{\sf H}_{a}{\sf H}_{a}p$.

1.3 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 4, 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^{\prime}$ because such a transition requires the consensus of both agents. Thus, $u\Vdash{\sf S}_{a}p\wedge{\sf S}_{b}p\wedge\neg{\sf S}_{a}q\wedge\neg{\sf S}_{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\Vdash{\sf H}_{a}p\wedge{\sf H}_{b}p$.

In Figure 5, 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\Vdash{\sf S}_{a}p\wedge\neg{\sf H}_{a}p\wedge\neg{\sf K}_{a}{\sf S}_{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\Vdash{\sf H}_{b}p$.

1.4 Coalitions

We have talked about strategies, know-hows, and knowledge of individual agents. In this article 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 [8]. Different contexts call for different forms of group knowledge.

As illustrated in the famous Two Generals’ Problem [4, 11] 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 article 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 6. In this system, agents $a$ and $b$ cannot distinguish states $u$ and $v$ while agents $b$ and $c$ cannot distinguish states $v$ and $u^{\prime}$. 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\Vdash{\sf S}_{\{a,b\}}p$, or simply $u\Vdash{\sf S}_{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\Vdash S_{a,b}p\wedge{\sf K}_{a,b}S_{a,b}p\wedge\neg{\sf H}_{a,b}p$.

On the other hand, although agents $b$ and $c$ cannot distinguish states $v$ and $u^{\prime}$, by both voting R in either of states $v$ and $u^{\prime}$, 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^{\prime}$, 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\Vdash{\sf H}_{b,c}p$.

1.5 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 7. 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\nVdash{\sf S}_{a,b}p$. However, they can achieve $p\vee q$. Moreover, since all agents can distinguish all states, we have $u\Vdash{\sf H}_{a,b}(p\vee q)$.

1.6 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 article, 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 ${\sf H}_{C}$ satisfy cooperation properties [17, 18]:

[TABLE]

They also satisfy monotonicity properties

[TABLE]

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

Properties of Interplay

Note that $w\Vdash{\sf H}_{C}\varphi$ means that coalition $C$ has the same strategy to achieve $\varphi$ in all epistemic states indistinguishable by the coalition from state $w$. Hence, the following principle is universally true:

[TABLE]

Similarly, $w\Vdash\neg{\sf H}_{C}\varphi$ means that coalition $C$ does not have the same strategy to achieve $\varphi$ in all epistemic states indistinguishable by the coalition from state $w$. Thus,

[TABLE]

We call properties (3) and (4) 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 (see Lemma 14), the strategic positive introspection principle is also derivable (see Lemma 1).

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

[TABLE]

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 ${\sf K}_{\varnothing}\varphi$ is satisfied in an epistemic state of our transition system, then formula $\varphi$ must be satisfied in every state of this system. Thus, even empty coalition has a trivial strategy to achieve $\varphi$:

[TABLE]

We call this property empty coalition principle. In this article 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

[TABLE]

that we call nontermination principle.

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

For example, consider an epistemic transition system depicted in Figure 8. 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\Vdash{\sf S}_{\varnothing}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^{\prime}$ respectively. Thus, $v\Vdash\neg{\sf K}_{a}{\sf S}_{\varnothing}p\wedge\neg{\sf K}_{b}{\sf S}_{\varnothing}p$.

In the same transition system $T_{8}$, agents $a$ and $b$ together can distinguish state $v$ from states $u$ and $u^{\prime}$. Thus, $v\Vdash{\sf K}_{a,b}{\sf S}_{\varnothing}p$. In general, statement ${\sf K}_{C}{\sf S}_{\varnothing}\varphi$ means that not only $\varphi$ is unavoidable, but coalition $C$ knows about it. Thus, coalition $C$ has a know-how strategy to achieve $\varphi$:

[TABLE]

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 $\varphi$:

[TABLE]

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

[TABLE]

We call this property epistemic determinicity principle. Properties (1), (2), (4), (5), (6), (7), and (8), together with axioms of epistemic logic S5 with distributed knowledge and propositional tautologies constitute the axioms of our sound and complete logical system.

1.7 Literature Review

Logics of coalition power were developed by Marc Pauly [17, 18], who also proved the completeness of the basic logic of coalition power. Pauly’s approach has been widely studied in the literature [10, 23, 7, 20, 2, 3, 6]. An alternative logical system was proposed by More and Naumov [14].

Alur, Henzinger, and Kupferman introduced Alternating-Time Temporal Logic (ATL) that combines temporal and coalition modalities [5]. Van der Hoek and Wooldridge proposed to combine ATL with epistemic modality to form Alternating-Time Temporal Epistemic Logic [22]. 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 [1]. 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” [12], Jamroga and van der Hoek discussed “difference between an agent knowing that he has a suitable strategy and knowing the strategy itself” [13]. Van Benthem called such strategies “uniform” [21]. Wang gave a complete axiomatization of “knowing how” as a binary modality [25, 24], but his logical system does not include the knowledge modality.

In our AAMAS paper, we investigated coalition strategies to enforce a condition indefinitely [15]. Such strategies are similar to “goal maintenance” strategies in Pauly’s “extended coalition logic” [17, p. 80]. We focused on “executable” and “verifiable” strategies. Using the language of the current article, 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 article, the existence of a verifiable strategy could be expressed as ${\sf S}_{C}{\sf K}_{C}\varphi$. In [15], 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 (3) and the strategic negative introspection (4) mentioned above. A similar complete logical system in a single-agent setting for strategies to achieve a goal in multiple steps rather than to maintain a goal is developed by Fervari, Herzig, Li, and Wang [9].

In the current article, we combine know-how modality ${\sf H}$ with strategic modality ${\sf S}$ and epistemic modality ${\sf K}$. The proof of the completeness theorem is significantly more challenging than in [15, 9]. It employs new techniques that construct pairs of maximal consistent sets in “harmony” and in “complete harmony”. See Section 6.3 and Section 6.4 for details. An extended abstract of this article, without proofs, appeared as [16].

1.8 Outline

This article is organized as follows. In Section 2 we introduce formal syntax and semantics of our logical system. In Section 3 we list axioms and inference rules of the system. Section 4 provides examples of formal proofs in our logical systems. Proofs of the soundness and the completeness are given in Section 5 and Section 6 respectively. Section 7 concludes the article.

The key part of the proof of the completeness is the construction of a pair of sets in complete harmony. We discuss the intuition behind this construction and introduce the notion of harmony in Section 6.3. The notion of complete harmony is introduced in Section 6.4.

2 Syntax and Semantics

In this section we present the formal syntax and semantics of our logical system given a fixed finite set of agents $\mathcal{A}$. 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^{\mathcal{A}}$ we mean the set of all functions from set $\mathcal{A}$ to set $V$. Alternatively, the set $V^{\mathcal{A}}$ could be thought of as a set of tuples of elements of $V$ indexed by elements of $\mathcal{A}$.

Definition 1

A tuple $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$ is called an epistemic transition system, where

$W$* is a set of epistemic states,* 2. 2.

$\sim_{a}$* is an indistinguishability equivalence relation on $W$ for each $a\in\mathcal{A}$,* 3. 3.

$V$* is a nonempty set called “domain of choices”,* 4. 4.

$M\subseteq W\times V^{\mathcal{A}}\times W$* is an aggregation mechanism where for each $w\in W$ and each $\mathbf{s}\in V^{\mathcal{A}}$, there is $w^{\prime}\in W$ such that $(w,\mathbf{s},w^{\prime})\in M$,* 5. 5.

$\pi$* is a function that maps propositional variables into subsets of $W$.*

Definition 2

A coalition is a subset of $\mathcal{A}$.

Note that a coalition is always finite due to our assumption that the set of all agents $\mathcal{A}$ 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:

Definition 3

For any epistemic states $w_{1},w_{2}\in W$ and any coalition $C$, let $w_{1}\sim_{C}w_{2}$ if $w_{1}\sim_{a}w_{2}$ for each agent $a\in C$.

Corollary 1

Relation $\sim_{C}$ is an equivalence relation on the set of states $W$ for each coalition $C$.

By a strategy profile $\{s_{a}\}_{a\in C}$ of a coalition $C$ we mean a tuple that specifies vote $s_{a}\in V$ of each member $a\in 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}$:

Definition 4

Any tuple $\{s_{a}\}_{a\in C}\in V^{C}$ is called a strategy profile of coalition $C$.

In addition to a fixed finite set of agents $\mathcal{A}$ we also assume a fixed countable set of propositional variables. We use the assumption that this set is countable in the proof of Lemma 21. The language $\Phi$ of our formal logical system is specified in the next definition.

Definition 5

Let $\Phi$ be the minimal set of formulae such that

$p\in\Phi$* for each propositional variable $p$,* 2. 2.

$\neg\varphi,\varphi\to\psi\in\Phi$* for all formulae $\varphi,\psi\in\Phi$,* 3. 3.

${\sf K}_{C}\varphi,{\sf S}_{C}\varphi,{\sf H}_{C}\varphi\in\Phi$* for each coalition $C$ and each $\varphi\in\Phi$.*

In other words, language $\Phi$ is defined by the following grammar:

[TABLE]

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

According to Definition 1, a mechanism specifies the transition that a system might take for any strategy profile of the set of all agents $\mathcal{A}$. It is sometimes convenient to consider transitions that are consistent with a given strategy profile $\mathbf{s}$ of a give coalition $C\subseteq\mathcal{A}$. We write $w\to_{\mathbf{s}}u$ if a transition from state $w$ to state $u$ is consistent with strategy profile $\mathbf{s}$. The formal definition is below.

Definition 6

For any epistemic states $w,u\in W$, any coalition $C$, and any strategy profile ${\mathbf{s}}=\{s_{a}\}_{a\in C}\in V^{C}$, we write $w\to_{\mathbf{s}}u$ if $(w,\mathbf{s^{\prime}},u)\in M$ for some strategy profile $\mathbf{s^{\prime}}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}\in V^{\mathcal{A}}$ such that $s^{\prime}_{a}=s_{a}$ for each $a\in C$.

Corollary 2

For any strategy profile $\mathbf{s}$ of the empty coalition $\varnothing$, if there are a coalition $C$ and a strategy profile $\mathbf{s^{\prime}}$ of coalition $C$ such that $w\to_{\mathbf{s^{\prime}}}u$, then $w\to_{\mathbf{s}}u$.

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

Definition 7

For any epistemic state $w\in W$ of a transition system $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$ and any formula $\varphi\in\Phi$, let relation $w\Vdash\varphi$ be defined as follows

$w\Vdash p$* if $w\in\pi(p)$ where $p$ is a propositional variable,* 2. 2.

$w\Vdash\neg\varphi$* if $w\nVdash\varphi$,* 3. 3.

$w\Vdash\varphi\to\psi$* if $w\nVdash\varphi$ or $w\Vdash\psi$,* 4. 4.

$w\Vdash{\sf K}_{C}\varphi$* if $w^{\prime}\Vdash\varphi$ for each $w^{\prime}\in W$ such that $w\sim_{C}w^{\prime}$,* 5. 5.

$w\Vdash{\sf S}_{C}\varphi$* if there is a strategy profile $\mathbf{s}\in V^{C}$ such that $w\to_{\mathbf{s}}w^{\prime}$ implies $w^{\prime}\Vdash\varphi$ for every $w^{\prime}\in W$,* 6. 6.

$w\Vdash{\sf H}_{C}\varphi$* if there is a strategy profile $\mathbf{s}\in V^{C}$ such that $w\sim_{C}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$ imply $w^{\prime\prime}\Vdash\varphi$ for all $w^{\prime},w^{\prime\prime}\in W$.*

3 Axioms

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

Truth: ${\sf K}_{C}\varphi\to\varphi$, 2. 2.

Negative Introspection: $\neg{\sf K}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\varphi$, 3. 3.

Distributivity: ${\sf K}_{C}(\varphi\to\psi)\to({\sf K}_{C}\varphi\to{\sf K}_{C}\psi)$, 4. 4.

Monotonicity: ${\sf K}_{C}\varphi\to{\sf K}_{D}\varphi$, if $C\subseteq D$, 5. 5.

Cooperation: ${\sf S}_{C}(\varphi\to\psi)\to({\sf S}_{D}\varphi\to{\sf S}_{C\cup D}\psi)$, where $C\cap D=\varnothing$. 6. 6.

Strategic Negative Introspection: $\neg{\sf H}_{C}\varphi\to{\sf K}_{C}\neg{\sf H}_{C}\varphi$, 7. 7.

Epistemic Cooperation: ${\sf H}_{C}(\varphi\to\psi)\to({\sf H}_{D}\varphi\to{\sf H}_{C\cup D}\psi)$,

where $C\cap D=\varnothing$, 8. 8.

Strategic Truth: ${\sf H}_{C}\varphi\to{\sf S}_{C}\varphi$, 9. 9.

Epistemic Determinicity: ${\sf H}_{C}(\varphi\to\psi)\to({\sf K}_{C}{\sf S}_{\varnothing}\varphi\to{\sf H}_{C}\psi)$, 10. 10.

Empty Coalition: ${\sf K}_{\varnothing}\varphi\to{\sf H}_{\varnothing}\varphi$, 11. 11.

Nontermination: $\neg{\sf S}_{C}\bot$.

We have discussed the informal meaning of these axioms in the introduction. In Section 5 we formally prove the soundness of these axioms with respect to the semantics from Definition 7.

We write $\vdash\varphi$ if formula $\varphi$ is provable from the axioms of our logical system using Necessitation, Strategic Necessitation, and Modus Ponens inference rules:

[TABLE]

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

4 Derivation Examples

In this section we give examples of formal derivations in our logical system. In Lemma 1 we prove the strategic positive introspection principle (3) discussed in the introduction. The proof is similar to the proof of the epistemic positive introspection principle in Lemma 14.

Lemma 1

$\vdash{\sf H}_{C}\varphi\to{\sf K}_{C}{\sf H}_{C}\varphi$.

Proof. Note that formula $\neg{\sf H}_{C}\varphi\to{\sf K}_{C}\neg{\sf H}_{C}\varphi$ is an instance of Strategic Negative Introspection axiom. Thus, $\vdash\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi\to{\sf H}_{C}\varphi$ by the law of contrapositive in the propositional logic. Hence, $\vdash{\sf K}_{C}(\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi\to{\sf H}_{C}\varphi)$ by Necessitation inference rule. Thus, by Distributivity axiom and Modus Ponens inference rule,

[TABLE]

At the same time, ${\sf K}_{C}\neg{\sf H}_{C}\varphi\to\neg{\sf H}_{C}\varphi$ is an instance of Truth axiom. Thus, $\vdash{\sf H}_{C}\varphi\to\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi$ by contraposition. Hence, taking into account the following instance of Negative Introspection axiom $\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi$, one can conclude that $\vdash{\sf H}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\neg{\sf H}_{C}\varphi$. The latter, together with statement (9), implies the statement of the lemma by the laws of propositional reasoning. $\boxtimes\hskip 5.69054pt$

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.

Lemma 2

$\vdash{\sf H}_{C}\varphi\to{\sf K}_{C}{\sf S}_{C}\varphi$.

Proof. By Strategic Truth axiom, $\vdash{\sf H}_{C}\varphi\to{\sf S}_{C}\varphi$. Hence, $\vdash{\sf K}_{C}({\sf H}_{C}\varphi\to{\sf S}_{C}\varphi)$ by Necessitation inference rule. Thus, $\vdash{\sf K}_{C}{\sf H}_{C}\varphi\to{\sf K}_{C}{\sf S}_{C}\varphi$ by Distributivity axiom and Modus Ponens inference rule. At the same time, $\vdash{\sf H}_{C}\varphi\to{\sf K}_{C}{\sf H}_{C}\varphi$ by Lemma 1. Therefore, $\vdash{\sf H}_{C}\varphi\to{\sf K}_{C}{\sf S}_{C}\varphi$ by the laws of propositional reasoning. $\boxtimes\hskip 5.69054pt$

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.

Lemma 3

$\vdash{\sf H}_{C}\varphi\to{\sf H}_{D}\varphi$, where $C\subseteq D$.

Proof. Note that $\varphi\to\varphi$ is a propositional tautology. Thus, $\vdash\varphi\to\varphi$. Hence, $\vdash{\sf H}_{D\setminus C}(\varphi\to\varphi)$ by Strategic Necessitation inference rule. At the same time, by Epistemic Cooperation axiom, $\vdash{\sf H}_{D\setminus C}(\varphi\to\varphi)\to({\sf H}_{C}\varphi\to{\sf H}_{D}\varphi)$ due to the assumption $C\subseteq D$. Therefore, $\vdash{\sf H}_{C}\varphi\to{\sf H}_{D}\varphi$ by Modus Ponens inference rule. $\boxtimes\hskip 5.69054pt$

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.

Lemma 4

For each finite $C\subseteq\mathcal{A}$, inference rule $\dfrac{\varphi}{{\sf S}_{C}\varphi}$ is admissible in our logical system.

Proof. Assumption $\vdash\varphi$ implies $\vdash{\sf H}_{C}\varphi$ by Strategic Necessitation inference rule. Hence, $\vdash{\sf S}_{C}\varphi$ by Strategic Truth axiom and Modus Ponens inference rule. $\boxtimes\hskip 5.69054pt$

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

Lemma 5

$\vdash{\sf S}_{C}\varphi\to{\sf S}_{D}\varphi$, where $C\subseteq D$.

Proof. Note that $\varphi\to\varphi$ is a propositional tautology. Thus, $\vdash\varphi\to\varphi$. Hence, $\vdash{\sf S}_{D\setminus C}(\varphi\to\varphi)$ by Lemma 4. At the same time, by Cooperation axiom, $\vdash{\sf S}_{D\setminus C}(\varphi\to\varphi)\to({\sf S}_{C}\varphi\to{\sf S}_{D}\varphi)$ due to the assumption $C\subseteq D$. Therefore, $\vdash{\sf S}_{C}\varphi\to{\sf S}_{D}\varphi$ by Modus Ponens inference rule. $\boxtimes\hskip 5.69054pt$

5 Soundness

In this section we prove the soundness of our logical system. The proof of the soundness of multiagent S5 axioms and inference rules is standard. Below we show the soundness of each of the remaining axioms and the Strategic Necessitation inference rule as a separate lemma. The soundness theorem for the whole logical system is stated at the end of this section as Theorem 1.

Lemma 6

If $w\Vdash{\sf S}_{C}(\varphi\to\psi)$, $w\Vdash{\sf S}_{D}\varphi$, and $C\cap D=\varnothing$, then $w\Vdash{\sf S}_{C\cup D}\psi$.

Proof. Suppose that $w\Vdash{\sf S}_{C}(\varphi\to\psi)$. Then, by Definition 7, there is a strategy profile $\mathbf{s}^{1}=\{s^{1}_{a}\}_{a\in C}\in V^{C}$ such that $w^{\prime}\Vdash\varphi\to\psi$ for each $w^{\prime}\in W$ where $w\to_{\mathbf{s}^{1}}w^{\prime}$. Similarly, assumption $w\Vdash{\sf S}_{D}\varphi$ implies that there is a strategy $\mathbf{s}^{2}=\{s^{2}_{a}\}_{a\in D}\in V^{D}$ such that $w^{\prime}\Vdash\varphi$ for each $w^{\prime}\in W$ where $w\to_{\mathbf{s}^{2}}w^{\prime}$. Let strategy profile ${\mathbf{s}}=\{s_{a}\}_{a\in C\cup D}$ be defined as follows:

[TABLE]

Strategy profile $\mathbf{s}$ is well-defined due to the assumption $C\cap D=\varnothing$ of the lemma.

Consider any epistemic state $w^{\prime}\in W$ such that $w\to_{\mathbf{s}}w^{\prime}$. By Definition 7, it suffices to show that $w^{\prime}\Vdash\psi$. Indeed, assumption $w\to_{\mathbf{s}}w^{\prime}$, by Definition 6, implies that $w\to_{\mathbf{s}^{1}}w^{\prime}$ and $w\to_{\mathbf{s}^{2}}w^{\prime}$. Thus, $w^{\prime}\Vdash\varphi\to\psi$ and $w^{\prime}\Vdash\varphi$ by the choice of strategies $\mathbf{s}^{1}$ and $\mathbf{s}^{2}$. Therefore, $w^{\prime}\Vdash\psi$ by Definition 7. $\boxtimes\hskip 5.69054pt$

Lemma 7

If $w\Vdash\neg{\sf H}_{C}\varphi$, then $w\Vdash{\sf K}_{C}\neg{\sf H}_{C}\varphi$.

Proof. Consider any epistemic state $u\in W$ such that $w\sim_{C}u$. By Definition 7, it suffices to show that $u\nVdash{\sf H}_{C}\varphi$. Assume the opposite. Thus, $u\Vdash{\sf H}_{C}\varphi$. Then, again by Definition 7, there is a strategy profile $\mathbf{s}\in V^{C}$ where $u^{\prime\prime}\Vdash\varphi$ for all $u^{\prime},u^{\prime\prime}\in W$ such that $u\sim_{C}u^{\prime}$ and $u^{\prime}\to_{\mathbf{s}}u^{\prime\prime}$. Recall that $w\sim_{C}u$. Thus, by Corollary 1, $u^{\prime\prime}\Vdash\varphi$ for all $u^{\prime},u^{\prime\prime}\in W$ such that $w\sim_{C}u^{\prime}$ and $u^{\prime}\to_{\mathbf{s}}u^{\prime\prime}$. Therefore, $w\Vdash{\sf H}_{C}\varphi$, by Definition 7. The latter contradicts the assumption of the lemma. $\boxtimes\hskip 5.69054pt$

Lemma 8

If $w\Vdash{\sf H}_{C}(\varphi\to\psi)$, $w\Vdash{\sf H}_{D}\varphi$, and $C\cap D=\varnothing$, then $w\Vdash{\sf H}_{C\cup D}\psi$.

Proof. Suppose that $w\Vdash{\sf H}_{C}(\varphi\to\psi)$. Thus, by Definition 7, there is a strategy profile $\mathbf{s}^{1}=\{s^{1}_{a}\}_{a\in C}\in V^{C}$ such that $w^{\prime\prime}\Vdash\varphi\to\psi$ for all epistemic states $w^{\prime},w^{\prime\prime}$ where $w\sim_{C}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}^{1}}w^{\prime\prime}$. Similarly, assumption $w\Vdash{\sf H}_{D}\varphi$ implies that there is a strategy $\mathbf{s}^{2}=\{s^{2}_{a}\}_{a\in D}\in V^{D}$ such that $w^{\prime\prime}\Vdash\varphi$ for all $w^{\prime},w^{\prime\prime}$ where $w\sim_{D}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}^{2}}w^{\prime\prime}$. Let strategy profile ${\mathbf{s}}=\{s_{a}\}_{a\in C\cup D}$ be defined as follows:

[TABLE]

Strategy profile $\mathbf{s}$ is well-defined due to the assumption $C\cap D=\varnothing$ of the lemma.

Consider any epistemic states $w^{\prime},w^{\prime\prime}\in W$ such that $w\sim_{C\cup D}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$. By Definition 7, it suffices to show that $w^{\prime\prime}\Vdash\psi$. Indeed, by Definition 3 assumption $w\sim_{C\cup D}w^{\prime}$ implies that $w\sim_{C}w^{\prime}$ and $w\sim_{D}w^{\prime}$. At the same time, by Definition 6, assumption $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$ implies that $w^{\prime}\to_{\mathbf{s}^{1}}w^{\prime\prime}$ and $w^{\prime}\to_{\mathbf{s}^{2}}w^{\prime\prime}$. Thus, $w^{\prime\prime}\Vdash\varphi\to\psi$ and $w^{\prime\prime}\Vdash\varphi$ by the choice of strategies $\mathbf{s}^{1}$ and $\mathbf{s}^{2}$. Therefore, $w^{\prime\prime}\Vdash\psi$ by Definition 7. $\boxtimes\hskip 5.69054pt$

Lemma 9

If $w\Vdash{\sf H}_{C}\varphi$, then $w\Vdash{\sf S}_{C}\varphi$.

Proof. Suppose that $w\Vdash{\sf H}_{C}\varphi$. Thus, by Definition 7, there is a strategy profile $\mathbf{s}\in V^{C}$ such that $w^{\prime\prime}\Vdash\varphi$ for all epistemic states $w^{\prime},w^{\prime\prime}\in W$, where $w\sim_{C}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$. By Corollary 1, $w\sim_{C}w$. Hence, $w^{\prime\prime}\Vdash\varphi$ for each epistemic state $w^{\prime\prime}\in W$, where $w\to_{\mathbf{s}}w^{\prime\prime}$. Therefore, $w\Vdash{\sf S}_{C}\varphi$ by Definition 7. $\boxtimes\hskip 5.69054pt$

Lemma 10

If $w\Vdash{\sf H}_{C}(\varphi\to\psi)$ and $w\Vdash{\sf K}_{C}{\sf S}_{\varnothing}\varphi$, then $w\Vdash{\sf H}_{C}\psi$.

Proof. Suppose that $w\Vdash{\sf H}_{C}(\varphi\to\psi)$. Thus, by Definition 7, there is a strategy profile $\mathbf{s}\in V^{C}$ such that $w^{\prime\prime}\Vdash\varphi\to\psi$ for all epistemic states $w^{\prime},w^{\prime\prime}\in W$ where $w\sim_{C}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$.

Consider any epistemic states $w^{\prime}_{0},w^{\prime\prime}_{0}\in W$ such that $w\sim_{C}w^{\prime}_{0}$ and $w^{\prime}_{0}\to_{\mathbf{s}}w^{\prime\prime}_{0}$. By Definition 7, it suffices to show that $w^{\prime\prime}_{0}\Vdash\psi$.

Indeed, by Definition 7, the assumption $w\Vdash{\sf K}_{C}{\sf S}_{\varnothing}\varphi$ together with $w\sim_{C}w^{\prime}_{0}$ imply that $w^{\prime}_{0}\Vdash{\sf S}_{\varnothing}\varphi$. Hence, by Definition 7, there is a strategy profile $\mathbf{s^{\prime}}$ of empty coalition $\varnothing$ such that $w^{\prime\prime}\Vdash\varphi$ for each $w^{\prime\prime}$ where $w^{\prime}_{0}\to_{\mathbf{s^{\prime}}}w^{\prime\prime}$. Thus, $w^{\prime\prime}_{0}\Vdash\varphi$ due to Corollary 2 and $w^{\prime}_{0}\to_{\mathbf{s}}w^{\prime\prime}_{0}$. By the choice of strategy profile $\mathbf{s}$, statements $w\sim_{C}w^{\prime}_{0}$ and $w^{\prime}_{0}\to_{\mathbf{s}}w^{\prime\prime}_{0}$ imply $w^{\prime\prime}_{0}\Vdash\varphi\to\psi$. Finally, by Definition 7, statements $w^{\prime\prime}_{0}\Vdash\varphi\to\psi$ and $w^{\prime\prime}_{0}\Vdash\varphi$ imply that $w^{\prime\prime}_{0}\Vdash\psi$. $\boxtimes\hskip 5.69054pt$

Lemma 11

If $w\Vdash{\sf K}_{\varnothing}\varphi$, then $w\Vdash{\sf H}_{\varnothing}\varphi$.

Proof. Let $\mathbf{s}=\{s_{a}\}_{a\in\varnothing}$ be the empty strategy profile. Consider any epistemic states $w^{\prime},w^{\prime\prime}\in W$ such that $w\sim_{\varnothing}w^{\prime}$ and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$. By Definition 7, it suffices to show that $w^{\prime\prime}\Vdash\varphi$. Indeed $w\sim_{\varnothing}w^{\prime\prime}$ by Definition 3. Therefore, $w^{\prime\prime}\Vdash\varphi$ by assumption $w\Vdash{\sf K}_{\varnothing}\varphi$ and Definition 7. $\boxtimes\hskip 5.69054pt$

Lemma 12

$w\nVdash{\sf S}_{C}\bot$.

Proof. Suppose that $w\Vdash{\sf S}_{C}\bot$. Thus, by Definition 7, there is a strategy profile $\mathbf{s}=\{s_{a}\}_{a\in\mathcal{A}}\in V^{C}$ such that $u\Vdash\bot$ for each $u\in W$ where $w\to_{\mathbf{s}}u$.

Note that by Definition 1, the domain of choices $V$ is not empty. Thus, strategy profile $\mathbf{s}$ can be extended to a strategy profile $\mathbf{s}^{\prime}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}\in V^{\mathcal{A}}$ such that $s^{\prime}_{a}=s_{a}$ for each $a\in C$.

By Definition 1, there must exist a state $w^{\prime}\in W$ such that $(w,\mathbf{s}^{\prime},w^{\prime})\in M$. Hence, $w\to_{\mathbf{s}}w^{\prime}$ by Definition 6. Therefore, $w^{\prime}\Vdash\bot$ by the choice of strategy $\mathbf{s}$, which contradicts Definition 7. $\boxtimes\hskip 5.69054pt$

Lemma 13

If $w\Vdash\varphi$ for any epistemic state $w\in W$ of an epistemic transition system $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$, then $w\Vdash{\sf S}_{C}\varphi$ for every epistemic state $w\in W$.

Proof. By Definition 1, set $V$ is not empty. Let $v\in V$. Consider strategy profile $\mathbf{s}=\{s_{a}\}_{a\in C}$ of coalition $C$ such that $s_{a}=v$ for each $s\in C$. Note that $w^{\prime}\Vdash\varphi$ for each $w^{\prime}\in W$ due to the assumption of the lemma. Therefore, $w\Vdash{\sf S}_{C}\varphi$ by Definition 7. $\boxtimes\hskip 5.69054pt$

Taken together, the lemmas above imply the soundness theorem for our logical system stated below.

Theorem 1

If $\vdash\varphi$, then $w\Vdash\varphi$ for each epistemic state $w\in W$ of each epistemic transition system $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$. $\boxtimes\hskip 2.84526pt$

6 Completeness

This section is dedicated to the proof of the following completeness theorem for our logical system.

Theorem 2

If $w\Vdash\varphi$ for each epistemic state $w$ of each epistemic transition system, then $\vdash\varphi$.

6.1 Positive Introspection

The proof of Theorem 2 is divided into several parts. In this section we prove the positive introspection principle for distributed knowledge modality from the rest of modality ${\sf K}$ axioms in our logical system. This is a well-known result that we reproduce to keep the presentation self-sufficient. The positive introspection principle is used later in the proof of the completeness.

Lemma 14

$\vdash{\sf K}_{C}\varphi\to{\sf K}_{C}{\sf K}_{C}\varphi$.

Proof. Formula $\neg{\sf K}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\varphi$ is an instance of Negative Introspection axiom. Thus, $\vdash\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi\to{\sf K}_{C}\varphi$ by the law of contrapositive in the propositional logic. Hence, $\vdash{\sf K}_{C}(\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi\to{\sf K}_{C}\varphi)$ by Necessitation inference rule. Thus, by Distributivity axiom and Modus Ponens inference rule,

[TABLE]

At the same time, ${\sf K}_{C}\neg{\sf K}_{C}\varphi\to\neg{\sf K}_{C}\varphi$ is an instance of Truth axiom. Thus, $\vdash{\sf K}_{C}\varphi\to\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi$ by contraposition. Hence, taking into account the following instance of Negative Introspection axiom $\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi$, one can conclude that $\vdash{\sf K}_{C}\varphi\to{\sf K}_{C}\neg{\sf K}_{C}\neg{\sf K}_{C}\varphi$. The latter, together with statement (10), implies the statement of the lemma by the laws of propositional reasoning. $\boxtimes\hskip 5.69054pt$

6.2 Consistent Sets of Formulae

The proof of the completeness consists in constructing a canonical model in which states are maximal consistent sets of formulae. This is a standard technique in modal logic that we modified significantly to work in the setting of our logical system. The standard way to apply this technique to a modal operator $\Box$ is to create a “child” state $w^{\prime}$ such that $\neg\psi\in w^{\prime}$ for each “parent” state $w$ where $\neg\Box\psi\in w$. In the simplest case when $\Box$ is a distributed knowledge modality ${\sf K}_{C}$, the standard technique requires no modification and the construction of a “child” state is based on the following lemma:

Lemma 15

For any consistent set of formulae $X$, any formula $\neg{\sf K}_{C}\psi\in X$, and any formulae ${\sf K}_{C}\varphi_{1},\dots,{\sf K}_{C}\varphi_{n}\in X$, the set of formulae $\{\neg\psi,\varphi_{1},\dots,\varphi_{n}\}$ is consistent.

Proof. Assume the opposite. Then, $\varphi_{1},\dots,\varphi_{n}\vdash\psi$. Thus, by the deduction theorem for propositional logic applied $n$ times,

[TABLE]

Hence, by Necessitation inference rule,

[TABLE]

By Distributivity axiom and Modus Ponens inference rule,

[TABLE]

By repeating the last step $(n-1)$ times,

[TABLE]

Hence, $X\vdash{\sf K}_{C}\psi$ by the choice of formula ${\sf K}_{C}\varphi_{1},\dots,{\sf K}_{C}\varphi_{n}$, which contradicts the consistency of the set $X$ due to the assumption $\neg{\sf K}_{C}\psi\in X$. $\boxtimes\hskip 5.69054pt$

If $\Box$ is the modality ${\sf S}_{C}$, then the standard technique needs to be modified. Namely, while $\neg{\sf S}_{C}\psi\in w$ means that coalition $C$ can not achieve goal $\psi$, its pairwise disjoint sub-coalitions $D_{1},\dots,D_{n}\subseteq C$ might still achieve their own goals $\varphi_{1},\dots,\varphi_{n}$. An equivalent of Lemma 15 for modality ${\sf S}_{C}$ is the following statement.

Lemma 16

For any consistent set of formulae $X$, and any subsets $D_{1},\dots,D_{n}$ of a coalition $C$, any formula $\neg{\sf S}_{C}\psi\in X$, and any ${\sf S}_{D_{1}}\varphi_{1},\dots,{\sf S}_{D_{n}}\varphi_{n}\in X$, if $D_{i}\cap D_{j}=\varnothing$ for all integers $i,j\leq n$ such that $i\neq j$, then the set of formulae $\{\neg\psi,\varphi_{1},\dots,\varphi_{n}\}$ is consistent.

Proof. Suppose that $\varphi_{1},\varphi_{2},\dots,\varphi_{n}\vdash\psi.$ Hence, by the deduction theorem for propositional logic applied $n$ times,

[TABLE]

Then, $\vdash{\sf S}_{D_{1}}(\varphi_{1}\to(\varphi_{2}\to(\dots(\varphi_{n}\to\psi)\dots)))$ by Lemma 4. Hence, by Cooperation axiom and Modus Ponens inference rule,

[TABLE]

In other words,

[TABLE]

Then, by Modus Ponens inference rule,

[TABLE]

By Cooperation axiom and Modus Ponens inference rule,

[TABLE]

Again, by Modus Ponens inference rule,

[TABLE]

By repeating the previous steps $n-2$ times,

[TABLE]

Recall that ${\sf S}_{D_{1}}\varphi_{1},{\sf S}_{D_{2}}\varphi_{2},\dots,{\sf S}_{D_{n}}\varphi_{n}\in X$ by the assumption of the lemma. Thus, $X\vdash{\sf S}_{D_{1}\cup D_{2}\cup\dots\cup D_{n}}\psi$. Therefore, $X\vdash{\sf S}_{C}\psi$ by Lemma 5. Since the set $X$ is consistent, the latter contradicts the assumption $\neg{\sf S}_{C}\psi\in X$ of the lemma. $\boxtimes\hskip 5.69054pt$

6.3 Harmony

If $\Box$ is the modality ${\sf H}_{C}$, then the standard technique needs even more significant modification. Namely, as it follows from Definition 7, assumption $\neg{\sf H}_{C}\psi\in w$ requires us to create not a single child of parent $w$, but two different children referred in Definition 7 as states $w^{\prime}$ and $w^{\prime\prime}$, see Figure 9. Child $w^{\prime}$ is a state of the system indistinguishable from state $w$ by coalition $C$. Child $w^{\prime\prime}$ is a state such that $\neg\psi\in w^{\prime\prime}$ and coalition $C$ cannot prevent the system to transition from $w^{\prime}$ to $w^{\prime\prime}$.

One might think that states $w^{\prime}$ and $w^{\prime\prime}$ could be constructed in order: first state $w^{\prime}$ and then state $w^{\prime\prime}$. It appears, however, that such an approach does not work because it does not guarantee that $\neg\psi\in w^{\prime\prime}$. To solve the issue, we construct states $w^{\prime}$ and $w^{\prime\prime}$ simultaneously. While constructing states $w^{\prime}$ and $w^{\prime\prime}$ as maximal consistent sets of formulae, it is important to maintain two relations between sets $w^{\prime}$ and $w^{\prime\prime}$ that we call “to be in harmony” and “to be in complete harmony”. In this section we define harmony relation and prove its basic properties. The next section is dedicated to the complete harmony relation.

Even though according to Definition 5 the language of our logical system only includes propositional connectives $\neg$ and $\to$, other connectives, including conjunction $\wedge$, can be defined in the standard way. By $\wedge Y$ we mean the conjunction of a finite set of formulae $Y$. If set $Y$ is a singleton, then $\wedge Y$ represents the single element of set $Y$. If set $Y$ is empty, then $\wedge Y$ is defined to be any propositional tautology.

Definition 8

Pair $(X,Y)$ of sets of formulae is in harmony if $X\nvdash{\sf S}_{\varnothing}\neg\wedge Y^{\prime}$ for each finite set $Y^{\prime}\subseteq Y$.

Lemma 17

If pair $(X,Y)$ is in harmony, then set $X$ is consistent.

Proof. If set $X$ is not consistent, then any formula can be derived from it. In particular, $X\vdash{\sf S}_{\varnothing}\neg\wedge\varnothing$. Therefore, pair $(X,Y)$ is not in harmony by Definition 8. $\boxtimes\hskip 5.69054pt$

Lemma 18

If pair $(X,Y)$ is in harmony, then set $Y$ is consistent.

Proof. Suppose that $Y$ is inconsistent. Then, there is a finite set $Y^{\prime}\subseteq Y$ such that $\vdash\neg\wedge Y^{\prime}$. Hence, $\vdash{\sf S}_{\varnothing}\neg\wedge Y^{\prime}$ by Lemma 4. Thus, $X\vdash{\sf S}_{\varnothing}\neg\wedge Y^{\prime}$. Therefore, by Definition 8, pair $(X,Y)$ is not in harmony. $\boxtimes\hskip 5.69054pt$

Lemma 19

For any $\varphi\in\Phi$, if pair $(X,Y)$ is in harmony, then either pair $(X\cup\{\neg{\sf S}_{\varnothing}\varphi\},Y)$ or pair $(X,Y\cup\{\varphi\})$ is in harmony.

Proof. Suppose that neither pair $(X\cup\{\neg{\sf S}_{\varnothing}\varphi\},Y)$ nor pair $(X,Y\cup\{\varphi\})$ is in harmony. Then, by Definition 8, there are finite sets $Y_{1}\subseteq Y$ and $Y_{2}\subseteq Y\cup\{\varphi\}$ such that

[TABLE]

and

[TABLE]

Formula $\neg\wedge Y_{1}\to\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\})))$ is a propositional tautology. Thus, $\vdash{\sf S}_{\varnothing}(\neg\wedge Y_{1}\to\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\}))))$ by Lemma 4. Then, by Cooperation axiom, statement (11), and Modus Ponens inference rule, $X,\neg{\sf S}_{\varnothing}\varphi\vdash{\sf S}_{\varnothing\cup\varnothing}\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\})))$. In other words,

[TABLE]

Finally, formula $\neg\wedge Y_{2}\to(\varphi\to\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\}))))$ is also a propositional tautology. Thus, by Lemma 4,

[TABLE]

Then, by Cooperation axiom, statement (12), and Modus Ponens inference rule, $X\vdash{\sf S}_{\varnothing}(\varphi\to\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\}))))$. Thus, by Cooperation axiom and Modus Ponens inference rule,

[TABLE]

By Modus Ponens inference rule,

[TABLE]

Hence, $X\vdash{\sf S}_{\varnothing}\neg((\wedge Y_{1})\wedge(\wedge(Y_{2}\setminus\{\varphi\})))$ by statement (13) and the laws of propositional reasoning. Recall that $Y_{1}$ and $Y_{2}\setminus\{\varphi\}$ are subsets of $Y$. Therefore, pair $(X,Y)$ is not in harmony by Definition 8. $\boxtimes\hskip 5.69054pt$

The next lemma is an equivalent of Lemma 15 and Lemma 16 for modality ${\sf H}_{C}$.

Lemma 20

For any consistent set of formulae $X$, any formula $\neg{\sf H}_{C}\psi\in X$, and any function $f:C\to\Phi$, pair $(Y,Z)$ is in harmony, where

[TABLE]

Proof. Suppose that pair $(Y,Z)$ is not in harmony. Thus, by Definition 8, there is a finite $Z^{\prime}\subseteq Z$ such that $Y\vdash{\sf S}_{\varnothing}\neg\wedge Z^{\prime}$. Since a derivation uses only finitely many assumptions, there are formulae $K_{C}\varphi_{1},{\sf K}_{C}\varphi_{2}\dots,{\sf K}_{C}\varphi_{n}\in X$ such that

[TABLE]

Then, by the deduction theorem for propositional logic applied $n$ times,

[TABLE]

Hence, by Necessitation inference rule,

[TABLE]

Then, by Distributivity axiom and Modus Ponens inference rule,

[TABLE]

Thus, by Modus Ponens inference rule,

[TABLE]

By repeating the previous two steps $(n-1)$ times,

[TABLE]

Hence, by the choice of formulae $K_{C}\varphi_{1},{\sf K}_{C}\varphi_{2},\dots,{\sf K}_{C}\varphi_{n}$,

[TABLE]

Since set $Z^{\prime}$ is a subset of set $Z$, by the choice of set $Z$, there must exist formulae ${\sf H}_{D_{1}}\chi_{1},\dots,{\sf H}_{D_{n}}\chi_{n}\in X$ such that $D_{1},\dots,D_{n}\subseteq C$,

[TABLE]

and the following formula is a tautology, even if $\neg\psi\notin Z^{\prime}$:

[TABLE]

Without loss of generality, we can assume that formulae $\chi_{1},\dots,\chi_{n}$ are pairwise distinct.

Claim 1

$D_{i}\cap D_{j}=\varnothing$* for each $i,j\leq n$ such that $i\neq j$.*

Proof of Claim. Suppose the opposite. Then, there is $a\in D_{i}\cap D_{j}$. Thus, $\chi_{i}=f(a)=\chi_{j}$ by statement (15). This contradicts the assumption that formulae $\chi_{1},\dots,\chi_{n}$ are pairwise distinct. $\boxtimes\hskip 2.84526pt$

Since formula (16) is a propositional tautology, by the law of contrapositive, the following formula is also a propositional tautology:

[TABLE]

Thus, by Strategic Necessitation inference rule,

[TABLE]

Hence, by Epistemic Cooperation axiom and Modus Ponens inference rule,

[TABLE]

Then, by Modus Ponens inference rule,

[TABLE]

By Epistemic Cooperation axiom, Claim 1, and Modus Ponens inference rule,

[TABLE]

By Modus Ponens inference rule,

[TABLE]

By repeating the previous two steps $(n-2)$ times,

[TABLE]

Recall that ${\sf H}_{D_{1}}\chi_{1},{\sf H}_{D_{2}}\chi_{2},\dots,{\sf H}_{D_{n}}\chi_{n}\in X$ by the choice of ${\sf H}_{D_{1}}\chi_{1}$, …, ${\sf H}_{D_{n}}\chi_{n}$. Thus, $X\vdash{\sf H}_{D_{1}\cup D_{2}\cup\dots\cup D_{n}}(\neg\wedge Z^{\prime}\to\psi)$. Hence, because $D_{1},\dots,D_{n}\subseteq C$, by Lemma 3, $X\vdash{\sf H}_{C}(\neg\wedge Z^{\prime}\to\psi)$. Then, $X\vdash{\sf H}_{C}\psi$ by Epistemic Determinicity axiom and statement (14). Since the set $X$ is consistent, this contradicts the assumption $\neg{\sf H}_{C}\psi\in X$ of the lemma. $\boxtimes\hskip 5.69054pt$

6.4 Complete Harmony

Definition 9

A pair in harmony $(X,Y)$ is in complete harmony if for each $\varphi\in\Phi$ either $\neg{\sf S}_{\varnothing}\varphi\in X$ or $\varphi\in Y$.

Lemma 21

For each pair in harmony $(X,Y)$, there is a pair in complete harmony $(X^{\prime},Y^{\prime})$ such that $X\subseteq X^{\prime}$ and $Y\subseteq Y^{\prime}$.

Proof. Recall that the set of agent $\mathcal{A}$ is finite and the set of propositional variables is countable. Thus, the set of all formulae $\Phi$ is also countable. Let $\varphi_{1},\varphi_{2},\dots$ be an enumeration of all formulae in $\Phi$. We define two chains of sets $X_{1}\subseteq X_{2}\subseteq\dots$ and $Y_{1}\subseteq Y_{2}\subseteq\dots$ such that pair $(X_{n},Y_{n})$ is in harmony for each $n\geq 1$. These two chains are defined recursively as follows:

$X_{1}=X$ and $Y_{1}=Y$, 2. 2.

if pair $(X_{n},Y_{n})$ is in harmony, then, by Lemma 19, either pair $(X_{n}\cup\{\neg{\sf S}_{\varnothing}\varphi_{n}\},Y_{n})$ or pair $(X_{n},Y_{n}\cup\{\varphi_{n}\})$ is in harmony. Let $(X_{n+1},Y_{n+1})$ be $(X_{n}\cup\{\neg{\sf S}_{\varnothing}\varphi_{n}\},Y_{n})$ in the former case and $(X_{n},Y_{n}\cup\{\varphi_{n}\})$ in the latter case.

Let $X^{\prime}=\bigcup_{n}X_{n}$ and $Y^{\prime}=\bigcup_{n}Y_{n}$. Note that $X=X_{1}\subseteq X^{\prime}$ and $Y=Y_{1}\subseteq Y^{\prime}$.

We next show that pair $(X^{\prime},Y^{\prime})$ is in harmony. Suppose the opposite. Then, by Definition 8, there is a finite set $Y^{\prime\prime}\subseteq Y^{\prime}$ such that $X^{\prime}\vdash{\sf S}_{\varnothing}\neg\wedge Y^{\prime\prime}$. Since a deduction uses only finitely many assumptions, there must exist $n_{1}\geq 1$ such that

[TABLE]

At the same time, since set $Y^{\prime\prime}$ is finite, there must exist $n_{2}\geq 1$ such that $Y^{\prime\prime}\subseteq Y_{n_{2}}$. Let $n=\max\{n_{1},n_{2}\}$. Note that $\neg\wedge Y^{\prime\prime}\to\neg\wedge Y_{n}$ is a tautology because $Y^{\prime\prime}\subseteq Y_{n_{2}}\subseteq Y_{n}$. Thus, $\vdash{\sf S}_{\varnothing}(\neg\wedge Y^{\prime\prime}\to\neg\wedge Y_{n})$ by Lemma 4. Then, $\vdash{\sf S}_{\varnothing}\neg\wedge Y^{\prime\prime}\to{\sf S}_{\varnothing}\neg\wedge Y_{n}$ by Cooperation axiom and Modus Ponens inference rule. Hence, $X_{n_{1}}\vdash{\sf S}_{\varnothing}\neg\wedge Y_{n}$ due to statement (17). Thus, $X_{n}\vdash{\sf S}_{\varnothing}\neg\wedge Y_{n}$, because $X_{n_{1}}\subseteq X_{n}$. Then, pair $(X_{n},Y_{n})$ is not in harmony, which contradicts the choice of pair $(X_{n},Y_{n})$. Therefore, pair $(X^{\prime},Y^{\prime})$ is in harmony.

We finally show that pair $(X^{\prime},Y^{\prime})$ is in complete harmony. Indeed, consider any $\varphi\in\Phi$. Since $\varphi_{1},\varphi_{2},\dots$ is an enumeration of all formulae in $\Phi$, there must exist $k\geq 1$ such that $\varphi=\varphi_{k}$. Then, by the choice of pair $(X_{k+1},Y_{k+1})$, either $\neg{\sf S}_{\varnothing}\varphi=\neg{\sf S}_{\varnothing}\varphi_{k}\in X_{k+1}\subseteq X^{\prime}$ or $\varphi=\varphi_{k}\in Y_{k+1}\subseteq Y^{\prime}$. Therefore, pair $(X^{\prime},Y^{\prime})$ is in complete harmony. $\boxtimes\hskip 5.69054pt$

6.5 Canonical Epistemic Transition System

The construction of a canonical model, called the canonical epistemic transition system, for the proof of the completeness is based on the “unravelling” technique [19]. Informally, epistemic states in this system are nodes in a tree. In this tree, each node is labeled with a maximal consistent set of formulae and each edge is labeled with a coalition. Formally, epistemic states are defined as sequences representing paths in such a tree. In the rest of this section we fix a maximal consistent set of formulae $X_{0}$ and define a canonical epistemic transition system $ETS(X_{0})=(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$.

Definition 10

The set of epistemic states $W$ consists of all finite sequences $X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}$, such that

$n\geq 0$, 2. 2.

$X_{i}$* is a maximal consistent subset of $\Phi$ for each $i\geq 1$,* 3. 3.

$C_{i}$* is a coalition for each $i\geq 1$,* 4. 4.

$\{\varphi\;|\;{\sf K}_{C_{i}}\varphi\in X_{i-1}\}\subseteq X_{i}$* for each $i\geq 1$.*

We say that two nodes of the tree are indistinguishable to an agent $a$ if every edge along the unique path connecting these two nodes is labeled with a coalition containing agent $a$.

Definition 11

For any state $w=X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}$ and any state $w^{\prime}=X_{0},C^{\prime}_{1},X^{\prime}_{1},C^{\prime}_{2},\dots,C^{\prime}_{m},X^{\prime}_{m}$, let $w\sim_{a}w^{\prime}$ if there is an integer $k$ such that

$0\leq k\leq\min\{n,m\}$, 2. 2.

$X_{i}=X^{\prime}_{i}$* for each $i$ such that $1\leq i\leq k$,* 3. 3.

$C_{i}=C^{\prime}_{i}$* for each $i$ such that $1\leq i\leq k$,* 4. 4.

$a\in C_{i}$* for each $i$ such that $k<i\leq n$,* 5. 5.

$a\in C^{\prime}_{i}$* for each $i$ such that $k<i\leq m$.*

For any state $w=X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}$, by $hd(w)$ we denote the set $X_{n}$. The abbreviation $hd$ stands for “head”.

Lemma 22

For any $w=X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}\in W$ and any integer $k\leq n$, if ${\sf K}_{C}\varphi\in X_{n}$ and $C\subseteq C_{i}$ for each integer $i$ such that $k<i\leq n$, then ${\sf K}_{C}\varphi\in X_{k}$.

Proof. Suppose that there is $k\leq n$ such that ${\sf K}_{C}\varphi\notin X_{k}$. Let $m$ be the maximal such $k$. Note that $m<n$ due to the assumption ${\sf K}_{C}\varphi\in X_{n}$ of the lemma. Thus, $m<m+1\leq n$.

Assumption ${\sf K}_{C}\varphi\notin X_{m}$ implies $\neg{\sf K}_{C}\varphi\in X_{m}$ due to the maximality of the set $X_{m}$. Hence, $X_{m}\vdash{\sf K}_{C}\neg{\sf K}_{C}\varphi$ by Negative Introspection axiom. Thus, $X_{m}\vdash{\sf K}_{C_{m+1}}\neg{\sf K}_{C}\varphi$ by Monotonicity axiom and the assumption $C\subseteq C_{m+1}$ of the lemma (recall that $m+1\leq n$). Then, ${\sf K}_{C_{m+1}}\neg{\sf K}_{C}\varphi\in X_{m}$ due to the maximality of the set $X_{m}$. Hence, $\neg{\sf K}_{C}\varphi\in X_{m+1}$ by Definition 10. Thus, ${\sf K}_{C}\varphi\notin X_{m+1}$ due to the consistency of the set $X_{m+1}$, which is a contradiction with the choice of integer $m$. $\boxtimes\hskip 5.69054pt$

Lemma 23

For any $w=X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}\in W$ and any integer $k\leq n$, if ${\sf K}_{C}\varphi\in X_{k}$ and $C\subseteq C_{i}$ for each integer $i$ such that $k<i\leq n$, then $\varphi\in X_{n}$.

Proof. We prove the lemma by induction on the distance between $n$ and $k$. In the base case $n=k$. Then the assumption ${\sf K}_{C}\varphi\in X_{n}$ implies $X_{n}\vdash\varphi$ by Truth axiom. Therefore, $\varphi\in X_{n}$ due to the maximality of set $X_{n}$.

Suppose that $k<n$. Assumption ${\sf K}_{C}\varphi\in X_{k}$ implies $X_{k}\vdash{\sf K}_{C}{\sf K}_{C}\varphi$ by Lemma 14. Thus, $X_{k}\vdash{\sf K}_{C_{k+1}}{\sf K}_{C}\varphi$ by Monotonicity axiom, the condition $k<n$ of the inductive step, and the assumption $C\subseteq C_{k+1}$ of the lemma. Then, ${\sf K}_{C_{k+1}}{\sf K}_{C}\varphi\in X_{k}$ by the maximality of set $X_{k}$. Hence, ${\sf K}_{C}\varphi\in X_{k+1}$ by Definition 10. Therefore, $\varphi\in X_{n}$ by the induction hypothesis. $\boxtimes\hskip 5.69054pt$

Lemma 24

If ${\sf K}_{C}\varphi\in hd(w)$ and $w\sim_{C}w^{\prime}$, then $\varphi\in hd(w^{\prime})$.

Proof. The statement follows from Lemma 22, Lemma 23, and Definition 11 because there is a unique path between any two nodes in a tree. $\boxtimes\hskip 5.69054pt$

At the beginning of Section 6.2, we discussed that if a parent node contains a modal formula $\neg\Box\psi$, then it must have a child node containing formula $\neg\psi$. Lemma 15 in Section 6.2 provides a foundation for constructing such a child node for modality ${\sf K}_{C}$. The proof of the next lemma describes the construction of the child node for this modality.

Lemma 25

If ${\sf K}_{C}\varphi\notin hd(w)$, then there is an epistemic state $w^{\prime}\in W$ such that $w\sim_{C}w^{\prime}$ and $\varphi\notin hd(w^{\prime})$.

Proof. Assumption ${\sf K}_{C}\varphi\notin hd(w)$ implies that $\neg{\sf K}_{C}\varphi\in hd(w)$ due to the maximality of the set $hd(w)$. Thus, by Lemma 15, set $Y_{0}=\{\neg\varphi\}\cup\{\psi\;|\;{\sf K}_{C}\psi\in hd(w)\}$ is consistent. Let $Y$ be a maximal consistent extension of set $Y_{0}$ and $w^{\prime}$ be sequence $w,C,Y$. In other words, sequence $w^{\prime}$ is an extension of sequence $w$ by two additional elements: $C$ and $Y$. Note that $w^{\prime}\in W$ due to Definition 10 and the choice of set $Y_{0}$. Furthermore, $w\sim_{C}w^{\prime}$ by Definition 11. To finish the proof, we need to show that $\varphi\notin hd(w^{\prime})$. Indeed, $\neg\varphi\in Y_{0}\subseteq Y=hd(w^{\prime})$ by the choice of $Y_{0}$. Therefore, $\varphi\notin hd(w^{\prime})$ due to the consistency of the set $hd(w^{\prime})$. $\boxtimes\hskip 5.69054pt$

In the next two definitions we specify the domain of votes and the vote aggregation mechanism of the canonical transition system. Informally, a vote $(\varphi,w)$ of each agent consists of two components: the actual vote $\varphi$ and a key $w$. The actual vote $\varphi$ is a formula from $\Phi$ in support of what the agent votes. Recall that the agent does not know in which exact state the system is, she only knows the equivalence class of this state with respect to the indistinguishability relation. The key $w$ is the agent’s guess of the epistemic state where the system is. Informally, agent’s vote has more power to force the formula to be satisfied in the next state if she guesses the current state correctly.

Although each agent is free to vote for any formula she likes, the vote aggregation mechanism would grant agent’s wish only under certain circumstances. Namely, if the system is in state $w$ and set $hd(w)$ contains formula ${\sf S}_{C}\varphi$, then the mechanism guarantees that formula $\varphi$ is satisfied in the next state as long as each member of coalition $C$ votes for formula $\varphi$ and correctly guesses the current epistemic state. In other words, in order for formula $\varphi$ to be guaranteed in the next state all members of the coalition $C$ must cast vote $(\varphi,w)$. This means that if ${\sf S}_{C}\varphi\in hd(w)$, then coalition $C$ has a strategy to force $\varphi$ in the next state. Since the strategy requires each member of the coalition to guess correctly the current state, such a strategy is not a know-how strategy.

The vote aggregation mechanism is more forgiving if the epistemic state $w$ contains formula ${\sf H}_{C}\varphi$. In this case the mechanism guarantees that formula $\varphi$ is satisfied in the next state if all members of the coalition vote for formula $\varphi$; it does not matter if they guess the current state correctly or not. This means that if ${\sf H}_{C}\varphi\in hd(w)$, then coalition $C$ has a know-how strategy to force $\varphi$ in the next state. The strategy consists in each member of the coalition voting for formula $\varphi$ and specifying an arbitrary epistemic state as the key.

Formal definitions of the domain of choices and of the vote aggregation mechanism in the canonical epistemic transition system are given below.

Definition 12

The domain of choices $V$ is $\Phi\times W$.

For any pair $u=(x,y)$, let $pr_{1}(u)=x$ and $pr_{2}(u)=y$.

Definition 13

The mechanism $M$ of the canonical model is the set of all tuples $(w,\{s_{a}\}_{a\in\mathcal{A}},w^{\prime})$ such that for each formula $\varphi\in\Phi$ and each coalition $C$,

if ${\sf S}_{C}\varphi\in hd(w)$ and $s_{a}=(\varphi,w)$ for each $a\in C$, then $\varphi\in hd(w^{\prime})$, and 2. 2.

if ${\sf H}_{C}\varphi\in hd(w)$ and $pr_{1}(s_{a})=\varphi$ for each $a\in C$, then $\varphi\in hd(w^{\prime})$.

The next two lemmas prove that the vote aggregation mechanism specified in Definition 13 acts as discussed in the informal description given earlier.

Lemma 26

Let $w,w^{\prime}\in W$ be epistemic states, ${\sf S}_{C}\varphi\in hd(w)$ be a formula, and $\mathbf{s}=\{s_{a}\}_{a\in C}$ be a strategy profile of coalition $C$. If $w\to_{\mathbf{s}}w^{\prime}$ and $s_{a}=(\varphi,w)$ for each $a\in C$, then $\varphi\in hd(w^{\prime})$.

Proof. Suppose that $w\to_{\mathbf{s}}w^{\prime}$. Thus, by Definition 6, there is a strategy profile $\mathbf{s^{\prime}}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}\in V^{\mathcal{A}}$ such that $s^{\prime}_{a}=s_{a}$ for each $a\in C$ and $(w,\mathbf{s^{\prime}},w^{\prime})\in M$. Therefore, $\varphi\in hd(w^{\prime})$ by Definition 13 and the assumption $s_{a}=(\varphi,w)$ for each $a\in C$. $\boxtimes\hskip 5.69054pt$

Lemma 27

Let $w,w^{\prime},w^{\prime\prime}\in W$ be epistemic states, ${\sf H}_{C}\varphi\in hd(w)$ be a formula, and $\mathbf{s}=\{s_{a}\}_{a\in C}$ be a strategy profile of coalition $C$. If $w\sim_{C}w^{\prime}$, $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$, and $pr_{1}(s_{a})=\varphi$ for each $a\in C$, then $\varphi\in hd(w^{\prime\prime})$.

Proof. Suppose that ${\sf H}_{C}\varphi\in hd(w)$. Thus, $hd(w)\vdash{\sf K}_{C}{\sf H}_{C}\varphi$ by Lemma 1. Hence, ${\sf K}_{C}{\sf H}_{C}\varphi\in hd(w)$ due to the maximality of the set $hd(w)$. Thus, ${\sf H}_{C}\varphi\in hd(w^{\prime})$ by Lemma 24 and the assumption $w\sim_{C}w^{\prime}$. By Definition 6, assumption $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$ implies that there is a strategy profile $\mathbf{s^{\prime}}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}$ such that $s^{\prime}_{a}=s_{a}$ for each $a\in C$ and $(w^{\prime},\mathbf{s^{\prime}},w^{\prime\prime})\in M$. Since ${\sf H}_{C}\varphi\in hd(w^{\prime})$, $pr_{1}(s^{\prime}_{a})=pr_{1}(s_{a})=\varphi$ for each $a\in C$, and $(w^{\prime},\mathbf{s^{\prime}},w^{\prime\prime})\in M$, we have $\varphi\in hd(w^{\prime\prime})$ by Definition 13. $\boxtimes\hskip 5.69054pt$

The lemma below provides a construction of a child node for modality ${\sf S}_{C}$. Although the proof follows the outline of the proof of Lemma 25 for modality ${\sf K}_{C}$, it is significantly more involved because of the need to show that a transition from a parent node to a child node satisfies the constraints of the vote aggregation mechanism from Definition 13.

Lemma 28

For any epistemic state $w\in W$, any formula $\neg{\sf S}_{C}\psi\in hd(w)$, and any strategy profile $\mathbf{s}=\{s_{a}\}_{a\in C}\in V^{C}$, there is a state $w^{\prime}\in W$ such that $w\to_{\mathbf{s}}w^{\prime}$ and $\psi\notin hd(w^{\prime})$.

Proof. Let $Y_{0}$ be the following set of formulae

[TABLE]

We first show that set $Y_{0}$ is consistent. Suppose the opposite. Thus, there must exist formulae $\varphi_{1},\dots,\varphi_{n}\in Y_{0}$ and subsets $D_{1},\dots,D_{n}\subseteq C$ such that (i) ${\sf S}_{D_{i}}\varphi_{i}\in hd(w)$ for each integer $i\leq n$, (ii) $pr_{1}(s_{a})=\varphi_{i}$ for each $i\leq n$ and each $a\in D_{i}$, and (iii) set $\{\neg\psi,\varphi_{1},\dots,\varphi_{n}\}$ is inconsistent. Without loss of generality we can assume that formulae $\varphi_{1},\dots,\varphi_{n}$ are pairwise distinct.

Claim 2

Sets $D_{i}$ and $D_{j}$ are disjoint for each $i\neq j$.

Proof of Claim. Assume that $d\in D_{i}\cap D_{j}$, then $pr_{1}(s_{d})=\varphi_{i}$ and $pr_{1}(s_{d})=\varphi_{j}$. Hence, $\varphi_{i}=\varphi_{j}$, which contradicts the assumption that formulae $\varphi_{1},\dots,\varphi_{n}$ are pairwise distinct. Therefore, sets $D_{i}$ and $D_{j}$ are disjoint for each $i\neq j$. $\boxtimes\hskip 2.84526pt$

By Lemma 16, it follows from Claim 2 that set $Y_{0}$ is consistent. Let $Y$ be any maximal consistent extension of $Y_{0}$ and $w^{\prime}$ be the sequence $w,\varnothing,Y$. In other words, $w^{\prime}$ is an extension of sequence $w$ by two additional elements: $\varnothing$ and $Y$.

Claim 3

$w^{\prime}\in W$.

Proof of Claim. By Definition 10, it suffices to show that, for each formula $\varphi\in\Phi$, if ${\sf K}_{\varnothing}\varphi\in hd(w)$, then $\varphi\in Y$. Indeed, suppose that ${\sf K}_{\varnothing}\varphi\in hd(w)$. Thus, $hd(w)\vdash{\sf H}_{\varnothing}\varphi$ by Empty Coalition axiom. Hence, $hd(w)\vdash{\sf S}_{\varnothing}\varphi$ by Strategic Truth axiom. Then, ${\sf S}_{\varnothing}\varphi\in hd(w)$ due to the maximality of set $hd(w)$. Therefore, $\varphi\in Y_{0}\subseteq Y$ by the choice of sets $Y_{0}$ and $Y$. $\boxtimes\hskip 2.84526pt$

Let $\top$ be any propositional tautology. For example, $\top$ could be formula $\psi\to\psi$. Define strategy profile $\mathbf{s^{\prime}}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}$ as follows

[TABLE]

Claim 4

For any formula $\varphi\in\Phi$ and any $D\subseteq\mathcal{A}$, if ${\sf S}_{D}\varphi\in hd(w)$ and $s^{\prime}_{a}=(\varphi,w)$ for each $a\in D$, then $\varphi\in hd(w^{\prime})$.

Proof of Claim. Consider any formula $\varphi\in\Phi$ and any set $D\subseteq\mathcal{A}$ such that ${\sf S}_{D}\varphi\in hd(w)$ and $s^{\prime}_{a}=(\varphi,w)$ for each agent $a\in D$. We need to show that $\varphi\in hd(w^{\prime})$.

Case 1: $D\subseteq C$. In this case, $s_{a}=s^{\prime}_{a}=(\varphi,w)$ for each $a\in D$ by definition (18). Thus, $\varphi\in Y_{0}\subseteq Y=hd(w^{\prime})$ by the choice of set $Y_{0}$.

Case 2: There is $a_{0}\in D$ such that $a_{0}\notin C$. Then, $s^{\prime}_{a_{0}}=(\top,w)$ by definition (18). Note that $s^{\prime}_{a_{0}}=(\varphi,w)$ by the choice of the set $D$. Thus, $(\top,w)=(\varphi,w)$. Hence, formula $\varphi$ is the tautology $\top$. Therefore, $\varphi\in hd(w^{\prime})$ because set $hd(w^{\prime})$ is maximal. $\boxtimes\hskip 2.84526pt$

Claim 5

*For any formula $\varphi\in\Phi$ and any $D\subseteq\mathcal{A}$, if ${\sf H}_{D}\varphi\in hd(w)$ and $pr_{1}(s^{\prime}_{a})=\varphi$ for each $a\in D$, then $\varphi\in hd(w^{\prime})$. *

Proof of Claim. Consider any formula $\varphi\in\Phi$ and any set $D\subseteq\mathcal{A}$ such that ${\sf H}_{D}\varphi\in hd(w)$ and $pr_{1}(s^{\prime}_{a})=\varphi$ for each agent $a\in D$. We need to show that $\varphi\in hd(w^{\prime})$.

Case 1: $D\subseteq C$. In this case, $pr_{1}(s_{a})=pr_{1}(s^{\prime}_{a})=\varphi$ for each agent $a\in D$ by definition (18) and the choice of set $D$. Thus, $\varphi\in Y_{0}\subseteq Y=hd(w^{\prime})$ by the choice of set $Y_{0}$.

Case 2: There is agent $a_{0}\in D$ such that $a_{0}\notin C$. Then, $s^{\prime}_{a_{0}}=(\top,w)$ by definition (18). Note that $pr_{1}(s^{\prime}_{a_{0}})=\varphi$ by the choice of set $D$. Thus, $\top=\varphi$. Hence, formula $\varphi$ is the tautology $\top$. Therefore, $\varphi\in hd(w^{\prime})$ because set $hd(w^{\prime})$ is maximal. $\boxtimes\hskip 2.84526pt$

By Definition 13, Claim 4 and Claim 5 together imply that $(w,\mathbf{s^{\prime}},w^{\prime})\in M$. Hence, $w\to_{\mathbf{s}}w^{\prime}$ by Definition 6 and definition (18). To finish the proof of the lemma, note that $\psi\notin hd(w^{\prime})$ because set $hd(w^{\prime})$ is consistent and $\neg\psi\in Y_{0}\subseteq Y=hd(w^{\prime})$. $\boxtimes\hskip 5.69054pt$

The next lemma shows the construction of a child node for modality ${\sf H}_{C}$. The proof is similar to the proof of Lemma 28 except that, instead of constructing a single child node, we construct two sibling nodes that are in complete harmony. The intuition was discussed at the beginning of Section 6.3.

Lemma 29

For any state $w\in W$, any formula $\neg{\sf H}_{C}\psi\in hd(w)$, and any strategy profile $\mathbf{s}=\{s_{a}\}_{a\in C}\in V^{C}$, there are epistemic states $w^{\prime},w^{\prime\prime}\in W$ such that $\psi\notin hd(w^{\prime\prime})$, $w\sim_{C}w^{\prime}$, and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$.

Proof. By Definition 12, for each $a\in C$, vote $s_{a}$ is a pair. Let

[TABLE]

By Lemma 20 where $f(x)=pr_{1}(s_{x})$, pair $(Y,Z)$ is in harmony. By Lemma 21, there is a pair $(Y^{\prime},Z^{\prime})$ in complete harmony such that $Y\subseteq Y^{\prime}$ and $Z\subseteq Z^{\prime}$. By Lemma 17 and Lemma 18, sets $Y^{\prime}$ and $Z^{\prime}$ are consistent. Let $Y^{\prime\prime}$ and $Z^{\prime\prime}$ be maximal consistent extensions of sets $Y^{\prime}$ and $Z^{\prime}$, respectively.

Recall that set $\mathcal{A}$ is finite. Thus, set $C\subseteq\mathcal{A}$ is also finite. Let integer $n$ be the cardinality of set $C$. Consider $(n+1)$ sequences $w_{1},w_{2},\dots,w_{n+1}$, where sequence $w_{k}$ is an extension of sequence $w$ that adds $2k$ additional elements:

[TABLE]

Claim 6

$w_{k}\in W$* for each $k\leq n+1$.*

Proof of Claim. We prove the claim by induction on integer $k$.

Base Case: By Definition 10, it suffices to show that if ${\sf K}_{C}\varphi\in hd(w)$, then $\varphi\in hd(w_{1})$. Indeed, if ${\sf K}_{C}\varphi\in hd(w)$, then $\varphi\in Y$ by the choice of set $Y$. Therefore, $\varphi\in Y\subseteq Y^{\prime}\subseteq Y^{\prime\prime}=hd(w_{1})$.

Induction Step: By Definition 10, it suffices to show that if ${\sf K}_{C}\varphi\in hd(w_{k})$, then $\varphi\in hd(w_{k+1})$ for each $k\geq 1$. In other words, we need to prove that if ${\sf K}_{C}\varphi\in Y^{\prime\prime}$, then $\varphi\in Y^{\prime\prime}$, which follows from Truth axiom and the maximality of set $Y^{\prime\prime}$. $\boxtimes\hskip 2.84526pt$

By the pigeonhole principle, there is $i_{0}\leq n$ such that $pr_{2}(s_{a})\neq w_{i_{0}}$ for all $a\in C$. Let $w^{\prime}$ be epistemic state $w_{i_{0}}$. Thus,

[TABLE]

Let $w^{\prime\prime}$ be the sequence $w,\varnothing,Z^{\prime\prime}$. In other words, sequence $w^{\prime\prime}$ is an extension of sequence $w$ by two additional elements: $\varnothing$ and $Z^{\prime\prime}$. Finally, let strategy profile $\mathbf{s^{\prime}}=\{s^{\prime}_{a}\}_{a\in\mathcal{A}}$ be defined as follows

[TABLE]

Claim 7

$w^{\prime\prime}\in W$.

Proof of Claim. By Definition 10, it suffices to show that if ${\sf K}_{\varnothing}\varphi\in hd(w)$, then $\varphi\in hd(w^{\prime\prime})$ for each formula $\varphi\in\Phi$. Indeed, by Empty Coalition axiom, assumption ${\sf K}_{\varnothing}\varphi\in hd(w)$ implies that $hd(w)\vdash{\sf H}_{\varnothing}\varphi$. Hence, ${\sf H}_{\varnothing}\varphi\in hd(w)$ by the maximality of the set $hd(w)$. Thus, $\varphi\in Z$ by the choice of set $Z$. Therefore, $\varphi\in Z\subseteq Z^{\prime}\subseteq Z^{\prime\prime}=hd(w^{\prime\prime})$. $\boxtimes\hskip 2.84526pt$

Claim 8

$w\sim_{C}w^{\prime}$.

Proof of Claim. By Definition 11, $w\sim_{C}w_{i}$ for each integer $i\leq n+1$. In particular, $w\sim_{C}w_{i_{0}}=w^{\prime}$. $\boxtimes\hskip 2.84526pt$

Claim 9

$\psi\notin hd(w^{\prime\prime})$.

Proof of Claim. Note that $\neg\psi\in Z$ by the choice of set $Z$. Thus, $\neg\psi\in Z\subseteq Z^{\prime}\subseteq Z^{\prime\prime}=hd(w^{\prime\prime})$. Therefore, $\psi\notin hd(w^{\prime\prime})$ due to the consistency of the set $hd(w^{\prime\prime})$. $\boxtimes\hskip 2.84526pt$

Claim 10

Let $\varphi$ be a formula in $\Phi$ and $D$ be a subset of $\mathcal{A}$. If ${\sf S}_{D}\varphi\in hd(w^{\prime})$ and $s^{\prime}_{a}=(\varphi,w^{\prime})$ for each $a\in D$, then $\varphi\in hd(w^{\prime\prime})$.

Proof of Claim. Note that either set $D$ is empty or it contains an element $a_{0}$. In the latter case, element $a_{0}$ either belongs or does not belong to set $C$.

Case I: $D=\varnothing$. Recall that pair $(Y^{\prime},Z^{\prime})$ is in complete harmony. Thus, by Definition 9, either $\neg{\sf S}_{\varnothing}\varphi\in Y^{\prime}\subseteq Y^{\prime\prime}=hd(w^{\prime})$ or $\varphi\in Z^{\prime}\subseteq Z^{\prime\prime}=hd(w^{\prime\prime})$. Assumption ${\sf S}_{D}\varphi\in hd(w^{\prime})$ implies that $\neg{\sf S}_{\varnothing}\varphi\notin hd(w^{\prime})$ due to the consistency of the set $hd(w^{\prime})$ and the assumption $D=\varnothing$ of the case. Therefore, $\varphi\in hd(w^{\prime\prime})$.

Case II: there is an element $a_{0}\in C\cap D$. Thus, $a_{0}\in C$. Hence, $pr_{2}(s_{a_{0}})\neq w^{\prime}$ by inequality (19). Then, $s_{a_{0}}\neq(\varphi,w^{\prime})$. Thus, $s^{\prime}_{a_{0}}\neq(\varphi,w^{\prime})$ by definition (20). Recall that $a_{0}\in C\cap D\subseteq D$. This contradicts the assumption that $s^{\prime}_{a}=(\varphi,w^{\prime})$ for each $a\in D$.

Case III: there is an element $a_{0}\in D\setminus C$. Thus, $s^{\prime}_{a_{0}}=(\top,w^{\prime})$ by definition (20). At the same time, $s^{\prime}_{a_{0}}=(\varphi,w^{\prime})$ by the second assumption of the claim. Hence, formula $\varphi$ is the propositional tautology $\top$. Therefore, $\varphi\in hd(w^{\prime\prime})$ due to the maximality of the set $hd(w^{\prime\prime})$. $\boxtimes\hskip 2.84526pt$

Claim 11

Let $\varphi$ be a formula in $\Phi$ and $D$ be a subset of $\mathcal{A}$. If ${\sf H}_{D}\varphi\in hd(w^{\prime})$ and $pr_{1}(s^{\prime}_{a})=\varphi$ for each $a\in D$, then $\varphi\in hd(w^{\prime\prime})$.

Proof of Claim.

Case I: $D\subseteq C$. Suppose that $pr_{1}(s^{\prime}_{a})=\varphi$ for each $a\in D$ and ${\sf H}_{D}\varphi\in hd(w^{\prime})$. Thus, $\varphi\in Z$ by the choice of set $Z$. Therefore, $\varphi\in Z\subseteq Z^{\prime}\subseteq Z^{\prime\prime}=hd(w^{\prime\prime})$.

Case II: $D\nsubseteq C$. Consider any $a_{0}\in D\setminus C$. Note that $s^{\prime}_{a_{0}}=(\top,w^{\prime})$ by definition (20). At the same time, $pr_{1}(s^{\prime}_{a_{a}})=\varphi$ by the second assumption of the claim. Hence, formula $\varphi$ is the propositional tautology $\top$. Therefore, $\varphi\in hd(w^{\prime\prime})$ due to the maximality of the set $hd(w^{\prime\prime})$. $\boxtimes\hskip 2.84526pt$

Claim 10 and Claim 11, by Definition 13, imply that $(w^{\prime},\{s^{\prime}_{a}\}_{a\in\mathcal{A}},w^{\prime\prime})\in M$. Thus, $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$ by Definition 6 and definition (20). This together with Claim 6, Claim 7, Claim 8, and Claim 9 completes the proof of the lemma. $\boxtimes\hskip 5.69054pt$

Definition 14

$\pi(p)=\{w\in W\;|\;p\in hd(w)\}$.

This concludes the definition of tuple $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$.

Lemma 30

Tuple $(W,\{\sim_{a}\}_{a\in\mathcal{A}},V,M,\pi)$ is an epistemic transition system.

Proof. By Definition 1, it suffices to show that for each $w\in W$ and each $\mathbf{s}\in V^{\mathcal{A}}$ there is $w^{\prime}\in W$ such that $(w,\mathbf{s},w^{\prime})\in M$.

Recall that set $\mathcal{A}$ is finite. Thus, $\vdash\neg{\sf S}_{\mathcal{A}}\bot$ by Nontermination axiom. Hence, $\neg{\sf S}_{\mathcal{A}}\bot\in hd(w)$. By Lemma 28, there is $w^{\prime}\in W$ such that $w\to_{\mathbf{s}}w^{\prime}$. Therefore, $(w,\mathbf{s},w^{\prime})\in M$ by Definition 6. $\boxtimes\hskip 5.69054pt$

Lemma 31

$w\Vdash\varphi$* iff $\varphi\in hd(w)$ for each epistemic state $w\in W$ and each formula $\varphi\in\Phi$.*

Proof. We prove the lemma by induction on the structural complexity of formula $\varphi$. If formula $\varphi$ is a propositional variable, then the required follows from Definition 7 and Definition 14. The cases of formula $\varphi$ being a negation or an implication follow from Definition 7, and the maximality and the consistency of the set $hd(w)$ in the standard way.

Let formula $\varphi$ have the form ${\sf K}_{C}\psi$.

$(\Rightarrow)$ Suppose that ${\sf K}_{C}\psi\notin hd(w)$. Then, by Lemma 25, there is $w^{\prime}\in W$ such that $w\sim_{C}w^{\prime}$ and $\psi\notin hd(w^{\prime})$. Hence, $w^{\prime}\nVdash\psi$ by the induction hypothesis. Therefore, $w\nVdash{\sf K}_{C}\psi$ by Definition 7.

$(\Leftarrow)$ Assume that ${\sf K}_{C}\psi\in hd(w)$. Consider any $w^{\prime}\in W$ such that $w\sim_{C}w^{\prime}$. By Definition 7, it suffices to show that $w^{\prime}\Vdash\psi$. Indeed, $\psi\in hd(w^{\prime})$ by Lemma 24. Therefore, by the induction hypothesis, $w^{\prime}\Vdash\psi$.

Let formula $\varphi$ have the form ${\sf S}_{C}\psi$.

$(\Rightarrow)$ Suppose that ${\sf S}_{C}\psi\notin hd(w)$. Then, $\neg{\sf S}_{C}\psi\in hd(w)$ due to the maximality of the set $hd(w)$. Hence, by Lemma 28, for any strategy profile $\mathbf{s}\in V^{C}$, there is an epistemic state $w^{\prime}\in W$ such that $w\to_{\mathbf{s}}w^{\prime}$ and $\psi\notin hd(w^{\prime})$. Thus, by the induction hypothesis, for any strategy profile $\mathbf{s}\in V^{C}$, there is a state $w^{\prime}\in W$ such that $w\to_{\mathbf{s}}w^{\prime}$ and $w^{\prime}\nVdash\psi$. Then, $w\nVdash{\sf S}_{C}\psi$ by Definition 7.

$(\Leftarrow)$ Assume that ${\sf S}_{C}\psi\in hd(w)$. Consider strategy profile ${\mathbf{s}}=\{s_{a}\}_{a\in C}\in V^{C}$ such that $s_{a}=(\psi,w)$ for each $a\in C$. By Lemma 26, for any epistemic state $w^{\prime}\in W$, if $w\to_{\mathbf{s}}w^{\prime}$, then $\psi\in hd(w^{\prime})$. Hence, by the induction hypothesis, for any epistemic state $w^{\prime}\in W$, if $w\to_{\mathbf{s}}w^{\prime}$, then $w^{\prime}\Vdash\psi$. Therefore, $w\Vdash{\sf S}_{C}\psi$ by Definition 7.

Finally, let formula $\varphi$ have the form ${\sf H}_{C}\psi$.

$(\Rightarrow)$ Suppose that ${\sf H}_{C}\psi\notin hd(w)$. Then, $\neg{\sf H}_{C}\psi\in hd(w)$ due to the maximality of the set $hd(w)$. Hence, by Lemma 29, for any strategy profile $\mathbf{s}\in V^{C}$, there are epistemic states $w^{\prime},w^{\prime\prime}\in W$ such that $w\sim_{C}w^{\prime}$, $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$, and $\psi\notin hd(w^{\prime\prime})$. Thus, $w^{\prime\prime}\nVdash\psi$ by the induction hypothesis. Therefore, $w\nVdash{\sf H}_{C}\psi$ by Definition 7.

$(\Leftarrow)$ Assume that ${\sf H}_{C}\psi\in hd(w)$. Consider a strategy profile ${\mathbf{s}}=\{s_{a}\}_{a\in C}\in V^{C}$ such that $s_{a}=(\psi,w)$ for each $a\in C$. By Lemma 27, for all epistemic states $w^{\prime},w^{\prime\prime}\in W$, if $w\sim_{C}w^{\prime}$, and $w^{\prime}\to_{\mathbf{s}}w^{\prime\prime}$, then $\psi\in hd(w^{\prime\prime})$. Hence, by the induction hypothesis, $w^{\prime\prime}\Vdash\psi$. Therefore, $w\Vdash{\sf H}_{C}\psi$ by Definition 7. $\boxtimes\hskip 5.69054pt$

6.6 Completeness: the Final Step

To finish the proof of Theorem 2 stated at the beginning of Section 6, suppose that $\nvdash\varphi$. Let $X_{0}$ be any maximal consistent subset of set $\Phi$ such that $\neg\varphi\in X_{0}$. Consider the canonical epistemic transition system $ETS(X_{0})$ defined in Section 6.5. Let $w$ be the single-element sequence $X_{0}$. Note that $w\in W$ by Definition 10. Thus, $w\Vdash\neg\varphi$ by Lemma 31. Therefore, $w\nVdash\varphi$ by Definition 7.

7 Conclusion

In this article 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.