arXiv:1707.04298v2 [cs.AI] 14 Nov 2017

Strategic Coalitions with Perfect Recall
Pavel Naumov

Jia Tao

Department of Computer Science
Vassar College
Poughkeepsie, New York 12604
pnaumov@vassar.edu

Department of Computer Science
Lafayette College
Easton, Pennsylvania 18042
taoj@lafayette.edu

Abstract
The paper proposes a bimodal logic that describes an interplay between distributed knowledge modality and coalition
know-how modality. Unlike other similar systems, the one
proposed here assumes perfect recall by all agents. Perfect
recall is captured in the system by a single axiom. The main
technical results are the soundness and the completeness theorems for the proposed logical system.

Introduction
Autonomous agents such as self-driving cars and robotic
vacuum cleaners are facing the challenge of navigating without having complete information about the current situation.
Such a setting could be formally captured by an epistemic
transition system where an agent uses instructions to transition the system between states without being able to distinguish some of these states. In this paper we study properties
of strategies in such systems. An example of such a system
is the epistemic transition system T1 , depicted in Figure 1.
It has six states named w0 , w00 , w1 , w10 , w2 , w20 and two instructions 0 and 1 that an agent a can use to transition the
system from one state to another. For instance, if an instruction 0 is given in state w0 , then the system transitions into
state w1 . The system is called epistemic because the agent
cannot distinguish state wi from state wi0 for each i = 0, 1, 2.
The indistinguishability relation is shown in the figure using
dashed lines. Atomic proposition p is true only in state w2 .
w0

1

w1

0

w2

p

1

a

a

a
1

1
w0'

0

0

w1'

0

w2'

Figure 1: Epistemic Transition System T1 .
The logical system that we propose consists of two modalities. The first is the knowledge modality K. Imagine that
the system starts in state w2 . Since agent a cannot distinguish state w2 from state w20 where statement p is not satisfied, the agent does not know if p is true or not. We write

this as (w2 ) 1 Ka p. Next, suppose that the system started
in state w1 and the agent used instruction 0 to transition
the system into state w2 . In this paper we assume that all
agents have perfect recall, so in state w2 the agent remembers history (w1 , 0, w2 ). However, such a history is indistinguishable from history (w10 , 0, w20 ) because the agent cannot distinguish state w1 from state w10 and state w2 from
state w20 . Thus, the agent does not know that proposition
p is true in the state w2 even with history (w1 , 0, w2 ). We
denote this by (w1 , 0, w2 ) 1 Ka p. Finally, assume that the
system started in state w0 and the agent first used instruction 1 to transition it into state w1 and later instruction 0
to transition it to state w2 . Thus, the history of the system
is (w0 , 1, w1 , 0, w2 ). The only history that the agent cannot
distinguish from this one is history (w00 , 1, w1 , 0, w2 ). Since
both of these histories end in a state where proposition p
is satisfied, agent a does know that proposition p is true in
state w2 , given history (w0 , 1, w1 , 0, w2 ). We write this as
(w0 , 1, w1 , 0, w2 ) Ka p.
The other modality that we consider is the strategic power.
In system T1 , the agent can transition the system from state
w1 to state w2 by using instruction 0. Similarly, the agent
can transition the system from state w10 to state w2 by using
instruction 1. In other words, given either history (w1 ) or
history (w10 ) the agent can transition the system to a state in
which atomic proposition p is satisfied. We say that, given
either history, agent a has a strategy to achieve p. Histories (w1 ) and (w10 ) are the only histories indistinguishable
by agent a from history (w1 ). Since she has a strategy to
achieve p under all histories indistinguishable from history
(w1 ), we say that given history (w1 ) the agent knows that
she has a strategy. Similarly, given history (w10 ), she also
knows that she has a strategy. However, since indistinguishable histories (w1 ) and (w10 ) require different strategies to
achieve p, given history (w1 ) she does not know what the
strategy is. We say that she does not have a know-how strategy. We denote this by (w1 ) 1 Ha p, where H stands for
know-How. Of course, it is also true that (w10 ) 1 Ha p.
The situation changes if the transition system starts in
state w0 instead of state w1 and transitions to state w1 under
instruction 1. Now the history is (w0 , 1, w1 ) and the histories that the agent cannot distinguish from this one are history (w00 , 1, w1 ) and history (w0 , 1, w1 ) itself. Given both of
these two histories, agent a can achieve p using the same

transition 0. Thus, (w0 , 1, w1 ) Ha p.
Finally note that there are only two histories: (w0 ) and
(w00 ) indistinguishable from (w0 ). Given either history,
agent a can achieve Ha p using instruction 1. Thus, (w0 )
Ha Ha p. That is, given history (w0 ) agent a knows how to
transition to a state in which formula Ha p is satisfied.
Multiagent Systems Like many other autonomous agents,
self-driving cars are expected to use vehicle-to-vehicle communication to share traffic information and to coordinate actions (Harding et al. 2014). Thus, it is natural to consider
epistemic transition systems that have more than one agent.
An example of such a system T2 is depicted in Figure 2. This
w1

1

a

0
p

0,1

w3

0

w0

1

1

b

0

w4

0,1

w2

Figure 2: Epistemic Transition System T2 .
system has five epistemic states: w0 , w1 , w2 , w3 , and w4 and
three agents: a, b, and c. In each state the agents vote either
0 or 1 and the system transitions into the next state based
on the majority vote. For example, since the directed edge
from state w0 to state w4 is labelled with 1, if the majority
of agents in state w0 votes 1, then the system transitions into
state w4 . Since coalition {a, b} forms a majority, this coalition has a strategy to transition the system from state w0 to
state w4 and, thus, to achieve p. Note that agent a cannot
distinguish state w0 from state w1 and thus agent a does not
know what she should vote for to achieve p. Similarly, agent
b also does not know what she should vote for to achieve
p because she cannot distinguish state w0 from state w2 . In
this paper, we assume that members of a coalition make the
decisions based on combined (distributed) knowledge of the
whole coalition. In our example, coalition {a, b} can distinguish state w0 from both state w1 and state w2 . Thus, given
history (w0 ) the coalition {a, b} knows how to achieve p. We
denote this by (w0 ) H{a,b} p, or simply as (w0 ) Ha,b p.
Universal Principles We have discussed a statement being true or false given a certain history. This paper focuses
on the logical principles that are true for each history in each
epistemic transition system. An example of such a principle is the strategic positive introspection: HC ϕ → KC HC ϕ.
This principle says that if a coalition knows how to achieve
ϕ, then the coalition knows that it knows how to achieve ϕ.
Informally, this principle is true because in order for statement HC ϕ to be satisfied for a given history h, coalition
C must have a strategy to achieve ϕ that works under any

history h0 indistinguishable from history h by the coalition.
Thus, the same strategy must work for any history h00 indistinguishable from history h0 by the coalition. In other
words, it is also true that h0
HC ϕ. Recall that h0 is an
arbitrary history indistinguishable from history h by coalition C. Hence, h
KC HC ϕ according to the standard semantics of the epistemic modality KC . A similar argument
can be used to justify the strategic negative introspection:
¬HC ϕ → KC ¬HC ϕ.
Another universal principle is the empty coalition principle: K∅ ϕ → H∅ ϕ. Indeed, K∅ ϕ means that statement ϕ is
true under any history indistinguishable from the given history by an empty coalition. Since an empty coalition cannot
distinguish any two histories, the assumption K∅ ϕ means
that statement ϕ is true under any history. In particular, this
statement is true after the next transition no matter how
agents vote. Hence, H∅ ϕ.
The epistemic modality KC also satisfies axioms of
epistemic logic S5 for distributed knowledge. Know-how
modality satisfies the unachievability of falsehood principle: ¬HC ⊥, stating that no coalition can achieve ⊥. Knowhow modality also satisfies a form of cooperation principle (Pauly 2001; Pauly 2002):
HC (ϕ → ψ) → (HD ϕ → HC∪D ψ), where C ∩ D = ∅.
Perfect Recall A complete trimodal logical system describing the interplay between distributed knowledge modality KC , coalition know-how modality HC , and standard (not
know-how) strategic power modality in the imperfect recall setting was proposed by (Naumov and Tao 2017b). We
provide a complete axiomatization of the interplay between
modalities KC and HC in the perfect recall setting. Surprisingly, the assumption of perfect recall by all agents is captured by a single principle that we call the perfect recall
principle: HD ϕ → HD KC ϕ, where D ⊆ C 6= ∅. This
principle says that if a sub-coalition D ⊆ C can achieve ϕ,
then after the vote the whole coalition will know that ϕ is
true. Informally, this principle is true because coalition C is
able to recall how sub-coalition D voted and, thus, will deduce that formula ϕ is true after the transition. As an empty
coalition has no memory even in the perfect recall setting,
it is essential for coalition C to be nonempty. However, the
sub-coalition D can be empty.
Literature Review Non-epistemic logics of coalition
power were developed by (Pauly 2001; Pauly 2002), who
also proved the completeness of the basic logic of coalition
power. His approach has been widely studied in the literature (Goranko 2001; van der Hoek and Wooldridge 2005;
Borgo 2007; Sauro et al. 2006; Ågotnes et al. 2010; Ågotnes,
van der Hoek, and Wooldridge 2009; Belardinelli 2014;
Goranko, Jamroga, and Turrini 2013). An alternative logical system for coalition power was proposed by (More and
Naumov 2012).
(Alur, Henzinger, and Kupferman 2002) introduced
Alternating-Time Temporal Logic (ATL) that combines
temporal and coalition modalities. (van der Hoek and
Wooldridge 2003) proposed to combine ATL with epistemic modality to form Alternating-Time Temporal Epis-

temic Logic. They did not prove the completeness theorem for the proposed logical system. Aminof, Murano,
Rubin and Zuleger (Aminof et al. 2016) studied modelchecking problems of an extension of ATL with epistemic
and “prompt eventually” modal operators.
(Ågotnes and Alechina 2012) proposed a complete logical system that combines the coalition power and epistemic
modalities. Since their system does not have epistemic requirements on strategies, it does not contain any axioms describing the interplay of these modalities. In the extended
version, (Ågotnes and Alechina 2016) added a complete axiomatization of an interplay between single-agent knowledge and know-how modalities.
Know-how strategies were studied before under different names. While (Jamroga and Ågotnes 2007) talked about
“knowledge to identify and execute a strategy”, (Jamroga
and van der Hoek 2004) discussed “difference between an
agent knowing that he has a suitable strategy and knowing the strategy itself”. (van Benthem 2001) called such
strategies “uniform”. (Broersen 2008) investigated a related notion of “knowingly doing”, while (Broersen, Herzig,
and Troquard 2009) studied modality “know they can do”.
(Wang 2015; Wang 2016) captured the “knowing how” as a
binary modality in a complete logical system with a single
agent and without the knowledge modality.
Coalition know-how strategies for enforcing a condition
indefinitely were investigated by (Naumov and Tao 2017a).
Such strategies are similar to (Pauly 2001, p. 80) “goal maintenance” strategies in “extended coalition logic”. A similar
complete logical system in a single-agent setting for knowhow strategies to achieve a goal in multiple steps rather than
to maintain a goal is developed by (Fervari et al. 2017).
(Naumov and Tao 2017b) also proposed a complete
trimodal logical system describing an interplay between
distributed knowledge modality KC , coalition know-how
modality HC , and standard (not know-how) strategic power
modality in the imperfect recall setting.
In this paper we provide a complete axiomatization of an
interplay between modalities KC and HC in the perfect recall setting. The main challenge in proving the completeness, compared to (Ågotnes and Alechina 2016; Fervari et
al. 2017; Naumov and Tao 2017b; Naumov and Tao 2017a),
is the need to construct not only “possible worlds”, but the
entire “possible histories”, see the proof of Lemma 22.
Outline The rest of the paper is organized as follows. First,
we introduce the syntax and semantics of our logical system.
Next, we list the axioms and give examples of proofs in the
system. Then, we prove the soundness and the completeness
of this system.

Syntax and Semantics
Throughout the rest of the paper we assume a fixed set of
agents A. By X Y we denote the set of all functions from set
Y to set X, or in other words, the set of all tuples of elements
from set X indexed by the elements of set Y . If t ∈ X Y is
such a tuple and y ∈ Y , then by (t)y we denote the y-th
component of tuple t.

We now proceed to describe the formal syntax and semantics of our logical system starting with the definition of a
transition system. Although our introductory examples used
voting to decide on the next state of the system, in this paper
we investigate universal properties of an arbitrary nondeterministic action aggregation mechanism.
Definition 1 A tuple (W, {∼a }a∈A , V, M, π) is called an
epistemic transition system, if
1. W is a set of epistemic states,
2. ∼a is an indistinguishability equivalence relation on W
for each a ∈ A,
3. V is a nonempty set called domain of choices,
4. M ⊆ W × V A × W is an aggregation mechanism,
5. π is a function that maps propositional variables into subsets of W .
For example, in the transition system T1 depicted in Figure 1, the set of states W is {w0 , w1 , w2 , w00 , w10 , w20 } and
relation ∼a is a transitive reflexive closure of {(w0 , w00 ),
(w1 , w10 ), (w2 , w20 )}.
Informally, an epistemic transition system is regular if
there is at least one next state for each outcome of the vote.
Definition 2 An epistemic transition system (W, {∼a }a∈A ,
V, M, π) is regular if for each w ∈ W and each s ∈ V A ,
there is w0 ∈ W such that (w, s, w0 ) ∈ M .
A coalition is a subset of A. A strategy profile of coalition
C is any tuple in the set V C .
Definition 3 For any states w1 , w2 ∈ W and any coalition
C, let w1 ∼C w2 if w1 ∼a w2 for each agent a ∈ C.
Lemma 1 For each coalition C, relation ∼C is an equivalence relation on the set of epistemic states W .

Definition 4 For all strategy profiles s1 and s2 of coalitions
C1 and C2 respectively and any coalition C ⊆ C1 ∩ C2 , let
s1 =C s2 if (s1 )a = (s2 )a for each a ∈ C.
Lemma 2 For any coalition C, relation =C is an equivalence relation on the set of all strategy profiles of coalitions
containing coalition C.

Definition 5 A history is an arbitrary sequence h =
(w0 , s1 , w1 , s2 , w2 , . . . , sn , wn ) such that n ≥ 0 and
1. wi ∈ W for each i ≤ n,
2. si ∈ V A for each i ≤ n,
3. (wi , si+1 , wi+1 ) ∈ M for each i < n.
In this paper we assume that votes of all agents are private.
Thus, an individual agent only knows her own votes and the
equivalence classes of the states that the system has been
at. This is formally captured in the following definition of
indistinguishability of histories by an agent.
Definition 6 For any history h = (w0 , s1 , w1 , . . . , sn , wn ),
0
), and any agent
any history h0 = (w00 , s01 , w10 , . . . , s0m , wm
0
a ∈ A, let h ≈a h if n = m and
1. wi ∼a wi0 for each i ≤ n,
2. (si )a = (s0i )a for each i ≤ n.

Definition 7 For any histories h1 , h2 and any coalition C,
let h1 ≈C h2 if h1 ≈a h2 for each agent a ∈ C.
Lemma 3 For any coalition C, relation ≈C is an equivalence relation on the set of histories.

The length |h| of a history h = (w0 , s1 , w1 , . . . , sn , wn ) is
the value of n. By Definition 7, the empty coalition cannot
distinguish any two histories, even of different lengths.
Lemma 4 |h1 | = |h2 | for each histories h1 and h2 such
that h1 ≈C h2 for some nonempty coalition C.

For any sequence x = x1 , . . . , xn and an element y, by
sequence x :: y we mean x1 , . . . , xn , y. If sequence x is
nonempty, then by hd(x) we mean element xn .
Lemma 5 If (h1 :: s1 :: w1 ) ≈C (h2 :: s2 :: w2 ), then
h1 ≈C h2 , s1 =C s2 , and w1 ∼C w2 .

Definition 8 Let Φ be the language specified as follows
ϕ := p | ¬ϕ | ϕ → ϕ | KC ϕ | HC ϕ, where C ⊆ A.
Boolean constants ⊥ and > are defined as usual.
Definition 9 For any history h of an epistemic transition
system (W, {∼a }a∈A , V, M, π) and any formula ϕ ∈ Φ, let
satisfiability relation h ϕ be defined as follows
1. h p if hd(h) ∈ π(p) and p is a propositional variable,
2. h ¬ϕ if h 1 ϕ,
3. h ϕ → ψ if h 1 ϕ or h ψ,
4. h KC ϕ if h0 ϕ for each history h0 s.t. h ≈C h0 ,
5. h HC ϕ if there is a strategy profile s ∈ V C such that
for any history h0 :: s0 :: w0 , if h ≈C h0 and s =C s0 , then
h0 :: s0 :: w0 ϕ.

Axioms
In additional to propositional tautologies in language Φ, our
logical system consists of the following axioms:
1. Truth: KC ϕ → ϕ,
2. Negative Introspection: ¬KC ϕ → KC ¬KC ϕ,
3. Distributivity: KC (ϕ → ψ) → (KC ϕ → KC ψ),
4. Monotonicity: KC ϕ → KD ϕ, if C ⊆ D,
5. Strategic Positive Introspection: HC ϕ → KC HC ϕ,
6. Cooperation: HC (ϕ → ψ) → (HD ϕ → HC∪D ψ), where
C ∩ D = ∅,
7. Empty Coalition: K∅ ϕ → H∅ ϕ,
8. Perfect Recall: HD ϕ → HD KC ϕ, where D ⊆ C 6= ∅,
9. Unachievability of Falsehood: ¬HC ⊥.
We write ` ϕ if formula ϕ is provable from the axioms of
our logical system using Necessitation, Strategic Necessitation, and Modus Ponens inference rules:
ϕ
ϕ
ϕ,
ϕ→ψ
.
KC ϕ
HC ϕ
ψ
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.
The next lemma follows from a well-known observation
that the Positive Introspection axiom is provable from the
other axioms of S5.

Lemma 6 ` KC ϕ → KC KC ϕ.



Proof. Formula ¬KC ϕ → KC ¬KC ϕ is an instance of
the Negative Introspection axiom. Thus, ` ¬KC ¬KC ϕ →
KC ϕ by the law of contrapositive in the propositional logic.
Hence, ` KC (¬KC ¬KC ϕ → KC ϕ) by the Necessitation
inference rule. Thus, by the Distributivity axiom and the
Modus Ponens inference rule,
` KC ¬KC ¬KC ϕ → KC KC ϕ.

(1)

At the same time, KC ¬KC ϕ → ¬KC ϕ is an instance of the Truth axiom. Thus, ` KC ϕ → ¬KC ¬KC ϕ
by contraposition. Hence, taking into account the following instance of the Negative Introspection axiom
¬KC ¬KC ϕ → KC ¬KC ¬KC ϕ, one can conclude that
` KC ϕ → KC ¬KC ¬KC ϕ. The latter, together with
statement (1), implies the statement of the lemma by the
laws of propositional reasoning.


Derivation Examples
This section contains examples of formal proofs in our logical system. The results obtained here are used in the proof
of completeness. The proof of Lemma 7 is based on the one
proposed to us by Natasha Alechina.
Lemma 7 (Alechina) ` ¬HC ϕ → KC ¬HC ϕ.
Proof. By the Positive Strategic Introspection axiom,
` HC ϕ → KC HC ϕ. Thus, ` ¬KC HC ϕ → ¬HC ϕ by
the contrapositive. Hence, ` KC (¬KC HC ϕ → ¬HC ϕ)
by the Necessitation inference rule. Then, by the Distributivity axiom and the Modus Ponens inference rule
` KC ¬KC HC ϕ → KC ¬HC ϕ. Thus, by the Negative Introspection axiom and the laws of propositional reasoning,
` ¬KC HC ϕ → KC ¬HC ϕ. Note that ¬HC ϕ → ¬KC HC ϕ
is the contrapositive of the Truth axiom. Therefore, by the
laws of propositional reasoning, ` ¬HC ϕ → KC ¬HC ϕ. 
Lemma 8 ` HC ϕ → HD ϕ, where C ⊆ D.
Proof. Note that ϕ → ϕ is a propositional tautology. Thus,
` ϕ → ϕ. Hence, ` HD\C (ϕ → ϕ) by the Strategic
Necessitation inference rule. At the same time, by the
Cooperation axiom, ` HD\C (ϕ → ϕ) → (HC ϕ → HD ϕ)
due to the assumption C ⊆ D. Therefore, ` HC ϕ → HD ϕ
by the Modus Ponens inference rule.

Lemma 9 If ϕ1 , . . . , ϕn ` ψ, then
1. KC ϕ1 , . . . , KC ϕn ` KC ψ,
2. HC1 ϕ1 , . . . , HCn ϕn ` HSni=1 Ci ψ, where sets C1 , . . . , Cn
are pairwise disjoint.
Proof. To prove the second statement, apply deduction
lemma for propositional logic n time. Then, we have
` ϕ1 → (· · · → (ϕn → ψ)). Thus, by the Strategic Necessitation inference rule, ` H∅ (ϕ1 → (· · · → (ϕn → ψ)))
Hence, ` HC1 ϕ1 → HC1 (ϕ2 · · · → (ϕn → ψ)) by the
Cooperation axiom and the Modus Ponens inference rule.
Then, HC1 ϕ1 ` HC1 (ϕ2 · · · → (ϕn → ψ)) by the Modus

Ponens inference rule. Thus, again by the Cooperation
axiom and the Modus Ponens inference rule we have
HC1 ϕ1 ` HC2 ϕ2 → HC1 ∪C2 (ϕ3 · · · → (ϕn → ψ)).
Therefore, by repeating the last two steps n − 2 times,
HC1 ϕ1 , . . . , HCn ϕn ` HSni=1 Ci ψ. The proof of the first
statement is similar, but it uses the Distributivity axiom
instead of the Cooperation axiom.


Soundness
In this section we prove the following soundness theorem
for our logical system.
Theorem 1 If ` ϕ, then h
ϕ for each history of each
regular epistemic transition system.
The proof of the soundness of axioms of epistemic logic
S5 with distributed knowledge is standard. Below we prove
the soundness of each remaining axiom as a separate lemma.
Lemma 10 If h

HC ϕ, then h

KC HC ϕ.

Proof. Due to Definition 9, assumption h
HC ϕ implies
that there is a strategy profile s0 of coalition C such that for
any history h0 :: s0 :: w0 , if h ≈C h0 and s0 =C s0 , then
h0 :: s0 :: w0 ϕ.
Consider any history h00 such that h ≈C h00 . By Definition 9, it suffices to show that h00 HC ϕ. Furthermore, by
the same Definition 9, it suffices to prove that for any history h000 :: s000 :: w000 , if h00 ≈C h000 and s0 =C s000 , then
h000 :: s000 :: w000 ϕ.
Suppose that h00 ≈C h000 and s0 =C s000 . By Lemma 3,
statements h ≈C h00 and h00 ≈C h000 imply that h ≈C h000 .
Therefore, h000 :: s000 :: w000 ϕ by the choice of s0 .

Lemma 11 If h
then h HC ψ.

HC (ϕ → ψ), h

HD ϕ, and C∩D = ∅,

Proof. By Definition 9, assumption h
HC (ϕ → ψ) implies that there is a strategy profile s1 of coalition C such
that for any history h0 :: s0 :: w0 , if h ≈C h0 and s1 =C s0 ,
then h0 :: s0 :: w0 ϕ → ψ.
Similarly, assumption h
HD ϕ implies that there is a
profile s2 of coalition D such that for any history h0 :: s0 ::
w0 , if h ≈D h0 and s2 =D s0 , then h0 :: s0 :: w0 ϕ.
Consider strategy profile s of coalition C ∪ D such that

(s1 )a , if a ∈ C,
(s)a =
(s2 )a , if a ∈ D.
Strategy profile s is well-defined because coalitions C and
D are disjoint. By Definition 9, it suffices to show that for
any history h0 :: s0 :: w0 , if h ≈C∪D h0 and s =C∪D s0 , then
h0 :: s0 :: w0 ψ.
Suppose that h ≈C∪D h0 and s =C∪D s0 . Then, h ≈C h0
and s1 =C s =C∪D s0 . Hence, h0 :: s0 :: w0
ϕ → ψ
by the choice of strategy s1 . Similarly, h0 :: s0 :: w0
ϕ.
Therefore, h0 :: s0 :: w0 ψ by Definition 9.

Lemma 12 If h

K∅ ϕ, then h

H∅ ϕ.

Proof. Let s ∈ V ∅ be the empty tuple. By Definition 9, it
suffices to show that for any history h0 :: s0 :: w0 we have
h0 :: s0 :: w0 ϕ. Definition 7 implies h ≈∅ (h0 :: s0 :: w0 ).
Thus, h0 :: s0 :: w0 ϕ by Definition 9 and h K∅ ϕ. 
Lemma 13 If h
and C 6= ∅.

HD ϕ, then h

HD KC ϕ, where D ⊆ C

Proof. By Definition 9, assumption h HD ϕ implies that
there is a strategy profile s of coalition D such that for any
history h0 :: s0 :: w0 , if h ≈D h0 and s =D s0 , then h0 :: s0 ::
w0 ϕ.
Consider any history h1 :: s1 :: w1 such that h ≈D h1
and s =D s1 . By Definition 9, it suffices to prove that h1 ::
s1 :: w1 KC ϕ. Let h2 be any such history that (h1 :: s1 ::
w1 ) ≈C h2 . Again by Definition 9, it suffices to prove that
h2 ϕ.
By Lemma 4, assumptions (h1 :: s1 :: w1 ) ≈C h2 and
C 6= ∅ imply that |h2 | = |h1 :: s1 :: w1 | ≥ 1. Thus,
h2 = h02 :: s02 :: w20 for some history h02 , some complete
strategy profile s02 , and some epistemic state w20 .
Then, (h02 :: s02 :: w20 ) = h2 ≈C (h1 :: s1 :: w1 ). Hence,
h1 ≈C h02 and s1 =C s02 by Lemma 5. Hence, h ≈D h1 ≈C
h02 and s =D s1 =C s02 by the choice of history h1 :: s1 ::
w1 . Then, h ≈D h02 and s =D s02 by Lemma 3, Lemma 2,
and because D ⊆ C. Thus, h02 :: s02 :: w20 ϕ by the choice
of strategy profile s. Therefore, h2 ϕ, because (h02 :: s02 ::
w20 ) = h2 .

Lemma 14 h 1 HC ⊥ for any history h of any regular epistemic transition system.
Proof. Suppose h HC ⊥. By Definition 9, there is a strategy profile s ∈ V C such that for any history h0 :: s0 :: w0 , if
h ≈C h0 and s =C s0 , then h0 :: s0 :: w0 ⊥.
By Definition 1, set V contains at least one element v0 .
Let s0 be a complete strategy profile such that

(s)a , if a ∈ C,
(s0 )a =
(2)
v0 ,
otherwise.
By Definition 2, there is an epistemic state w0 ∈ S such
that (hd(h), s0 , w0 ) ∈ M . Thus, h :: s0 :: w0 is a history by
Definition 5. Note that h ≈C h by Lemma 3 and s =C s0
due to equation (2). Thus, h :: s0 :: w0
⊥ by the choice
of strategy profile s, which contradicts Definition 9 and the
definition of ⊥.

This concludes the proof of Theorem 1.

Completeness
In the rest of this paper we focus on the completeness theorem for our logical system with respect to the class of
regular epistemic transition systems. We start the proof of
completeness by fixing a maximal consistent set of formulae X0 and defining a canonical epistemic transition system
ET S(X0 ) = (W, {∼a }a∈A , Φ, M, π) using the “unravelling” technique (Sahlqvist 1975). Note that the domain of
choices in the canonical model is the set of all formulae Φ.

Canonical Epistemic Transition System
Definition 10 The set of epistemic states W consists of all
sequences X0 , C1 , X1 , . . . , Cn , Xn , such that n ≥ 0 and
1. Xi is a maximal consistent subset of Φ for each i ≥ 1,
2. Ci ⊆ A for each i ≥ 1,
3. {ϕ | KCi ϕ ∈ Xi−1 } ⊆ Xi , for each i ≥ 1.
Definition 11 Suppose that w = X0 , C1 , X1 , . . . , Cn , Xn
0
0
and w0 = X0 , C10 , X10 . . . , Cm
, Xm
are epistemic states. For
0
any agent a ∈ A, let w ∼a w if there is a non-negative
integer k ≤ min{n, m} such that
1.
2.
3.
4.

Xi = Xi0 for each i such that 0 < i ≤ k,
Ci = Ci0 for each i such that 0 < i ≤ k,
a ∈ Ci for each i such that k < i ≤ n,
a ∈ Ci0 for each i such that k < i ≤ m.

Lemma 15 For any epistemic state X0 , C1 , . . . , Cn , Xn
and any integer k ≤ n, if KC ϕ ∈ Xn and C ⊆ Ci for
each integer i such that k < i ≤ n, then KC ϕ ∈ Xk .
Proof. Suppose KC ϕ ∈
/ Xk for some k ≤ n. Let m be
the maximal such k. Note that m < n by the assumption
KC ϕ ∈ Xn of the lemma. Thus, m < m + 1 ≤ n.
Assumption KC ϕ ∈
/ Xm implies ¬KC ϕ ∈ Xm by the
maximality of the set Xm . Hence, Xm ` KC ¬KC ϕ by the
Negative Introspection axiom. Thus, Xm ` KCm+1 ¬KC ϕ
by the Monotonicity axiom and the assumption
C ⊆ Cm+1 of the lemma (recall that m + 1 ≤ n).
Then, KCm+1 ¬KC ϕ ∈ Xm due to the maximality of the
set Xm . Hence, ¬KC ϕ ∈ Xm+1 by Definition 10. Thus,
KC ϕ ∈
/ Xm+1 due to the consistency of the set Xm+1 ,
which contradicts the choice of m.

Lemma 16 For any epistemic state X0 , C1 , . . . , Cn , Xn
and any integer k ≤ n, if KC ϕ ∈ Xk and C ⊆ Ci for
each integer i such that k < i ≤ n, then ϕ ∈ Xn .
Proof. We prove the lemma by induction on the distance between n and k. In the base case n = k. Then the assumption
KC ϕ ∈ Xn implies Xn ` ϕ by the Truth axiom. Therefore,
ϕ ∈ Xn due to the maximality of set Xn .
Suppose that k < n. Assumption KC ϕ ∈ Xk implies
Xk ` KC KC ϕ by Lemma 6. Thus, Xk ` KCk+1 KC ϕ by the
Monotonicity axiom, the condition k < n of the inductive
step, and the assumption C ⊆ Ck+1 of the lemma. Then,
KCk+1 KC ϕ ∈ Xk by the maximality of set Xk . Hence,
KC ϕ ∈ Xk+1 by Definition 10. Therefore, ϕ ∈ Xn by the
induction hypothesis.


of the coalition vote for ϕ, then ϕ must be true after the transition.
Definition 12 For any states w, w0 ∈ W and any complete
strategy profile s ∈ ΦA , let (w, s, w0 ) ∈ M if
{ϕ | (HD ϕ ∈ hd(w)) ∧ ∀a ∈ D((s)a = ϕ)} ⊆ hd(w0 ).
Definition 13 π(p) = {w ∈ W | p ∈ hd(w)}.
This concludes the definition of the canonical epistemic
transition system ET S(X0 ) = (W, {∼a }a∈A , Φ, M, π).
We prove that this system is regular in Lemma 25.
K-child Lemmas The following technical results (Lemmas 18–22) about the knowledge modality K are used in the
proof of completeness.
Lemma 18 For any epistemic state w ∈ W if ¬KC ϕ ∈
hd(w), then there is an epistemic state w0 ∈ W such that
w ∼C w0 and ¬ϕ ∈ hd(w0 ).
Proof. Consider the set X = {¬ϕ} ∪ {ψ | KC ψ ∈ hd(w)}.
First, we show that set X is consistent. Assume the opposite. Then, there exist formulae KC ψ1 , . . . , KC ψn ∈ hd(w)
such that ψ1 , . . . , ψn ` ϕ. Thus, KC ψ1 , . . . , KC ψn ` KC ϕ
by Lemma 9. Therefore, hd(w) ` KC ϕ by the choice of formulae KC ψ1 , . . . , KC ψn , which contradicts the consistency
of the set hd(w) due to the assumption ¬KC ϕ ∈ hd(w).
Let X̂ be a maximal consistent extension of set X
and let w0 be sequence w :: C :: X. Note that w0 ∈ W
by Definition 10 and the choice of set X. Furthermore,
w ∼C w0 by Definition 11. To finish the proof, note that
¬ϕ ∈ X ⊆ X̂ = hd(w0 ) by the choice of set X.

History h is a sequence whose last element hd(h) is an
epistemic state. Epistemic state hd(h), by Definition 10, is
also a sequence. Expression hd(hd(h)) denotes the last element of the sequence hd(h).
Lemma 19 For any history h, if KC ϕ ∈ hd(hd(h)), then
ϕ ∈ hd(hd(h0 )) for each history h0 such that h ≈C h0 .
Proof. Assumption h ≈C h0 by Definition 6 implies
that hd(h) ∼C hd(h0 ). Therefore, ϕ ∈ hd(hd(h0 )) by
Lemma 17 and the assumption KC ϕ ∈ hd(hd(h)).


w1

s

C

C

w4

w2

s'

w3

0

Lemma 17 For any epistemic states w, w ∈ W such that
w ∼C w0 , if KC ϕ ∈ hd(w), then ϕ ∈ hd(w0 ).
Proof. The statement of the lemma follows from Lemma 15
and Lemma 16 as well as Definition 11 because there is a
unique path between any two nodes in a tree.

Next, we specify the aggregation mechanism of the
canonical epistemic transition system. Informally, if a coalition has a know-how strategy to achieve ϕ and all members

Figure 3: Illustration for Lemma 20.
Lemma 20 For any nonempty coalition C, any states
w1 , w2 , w3 ∈ W , and any complete strategy profile s such
that (w1 , s, w2 ) ∈ M and w2 ∼C w3 , see Figure 3, there
is a state w4 and a complete strategy profile s0 such that
w1 ∼C w4 , (w4 , s0 , w3 ) ∈ M , and s =C s0 .

Proof. Let s0 be a complete strategy profile such that

(s)a , if a ∈ C,
0
(s )a =
⊥,
otherwise.

(3)

Consider the set of formulae
X

= {ϕ | KC ϕ ∈ hd(w1 )} ∪
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ ∀a ∈ D((s0 )a = ψ)}.

Finally, let us show that (w4 , s0 , w3 ) ∈ M using Definition 12. Consider any D ⊆ A and any HD ψ ∈ hd(w4 ) = X̂
such that s0 (a) = ψ for each a ∈ D. We need to show that
ψ ∈ hd(w3 ). Suppose the opposite. Then, ¬ψ ∈ hd(w3 )
by the maximality of set hd(w3 ). Thus, ¬HD ψ ∈ X by
the choice of set X. Hence, ¬HD ψ ∈ X ⊆ X̂. Therefore,
HD ψ ∈
/ X̂ due to the consistency of set X̂, which contradicts the choice of formula HD ψ.


First, we show that set X is consistent. Indeed, set
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ ∀a ∈ D((s0 )a = ψ)}
is equal to the union of the following two sets
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)},
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ D * C ∧ ∀a ∈ D((s0 )a = ψ)}.
The second set is a subset of {¬HD ⊥ | D ⊆ A} by the
choice of strategy s0 , see (3). Thus, set X is a subset of
{ϕ | KC ϕ ∈ hd(w1 )} ∪ {¬HD ⊥ | D ⊆ A} ∪
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)}.
Hence, by the Unachievability of Falsehood axiom, to show
the consistency of set X it suffices to prove the consistency
of the union of the set {ϕ | KC ϕ ∈ hd(w1 )} and the set
{¬HD ψ | ¬ψ ∈ hd(w3 ) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)}.
Suppose the opposite. In other words, assume that there are
formulae
formulae
and sets
such that
and

KC ϕ1 , . . . , KC ϕn ∈ hd(w1 ),
(4)
¬ψ1 , . . . , ¬ψm ∈ hd(w3 ),
(5)
D1 , . . . , Dm ⊆ C,
(6)
∀i ≤ m ∀a ∈ Di ((s0 )a = ψi ),
(7)
ϕ1 , . . . , ϕn , ¬HD1 ψ1 , . . . , ¬HDm ψm ` ⊥.

Lemma 21 For any history h, if K∅ ϕ ∈
/ hd(hd(h)), then
there is a history h0 s.t. h ≈∅ h0 and ¬ϕ ∈ hd(hd(h0 )).
Proof. By Lemma 18, there is a state w ∈ W such that
hd(h) ∼C w and ¬ϕ ∈ hd(w). Let h0 be a one-element
sequence w. Note that h ≈∅ h0 by Definition 7. Finally,
¬ϕ ∈ hd(w) = hd(hd(h0 )).

Lemma 22 For any nonempty coalition C and any history
h, if KC ϕ ∈
/ hd(hd(h)), then there is a history h0 such that
h ≈C h0 and ¬ϕ ∈ hd(hd(h0 )).
Proof. Let h = (w0 , s1 , w1 , . . . , sn , wn ). We prove the
lemma by induction on integer n.
Base Case. Let n = 0. By Lemma 18, there is w00 ∈ W such
that w0 ∼C w00 and ¬ϕ ∈ hd(w00 ). Let h0 be a one-element
sequence w00 . Note that w0 ∼C w00 implies that h ≈C h0 by
Definition 6. Also, ¬ϕ ∈ hd(w00 ) = hd(hd(h0 )).

w0

s1

C

w1

wn-1

C

C

w1'

'
wn-1

sn

wn

h_

h

C

By Lemma 9 and the Truth axiom,
KC ϕ1 , . . . , KC ϕn , KC ¬HD1 ψ1 , . . . , KC ¬HDm ψm ` ⊥.
Hence, statement (4) and the consistency of the set hd(w1 )
imply that there exists k ≤ m such that KC ¬HDk ψk ∈
/
hd(w1 ). Thus, ¬KC ¬HDk ψk ∈ hd(w1 ) due to the maximality of the set hd(w1 ). Then, ¬KDk ¬HDk ψk ∈ hd(w1 )
by statement (6) and the contrapositive of the Monotonicity axiom. Then, hd(w1 ) ` HDk ψk by the contrapositive of
Lemma 7. Thus, hd(w1 ) ` HDk KC ψk by the Perfect Recall axiom, statement (6), and the assumption of the lemma
that C 6= ∅. Hence, HDk KC ψk ∈ hd(w1 ) due to the maximality of the set hd(w1 ). Note that statements (3) and (6)
imply s =Dk s0 . Then, (s)a = ψk for each agent a ∈ Dk
by statement (7). Thus, KC ψk ∈ hd(w2 ) by assumption
(w1 , s, w2 ) ∈ M , statement (6), and Definition 12. Hence,
ψk ∈ hd(w3 ) by the assumption w2 ∼C w3 of the lemma
and Lemma 17. This contradicts statement (5) and the consistency of the set hd(w3 ). Therefore, set X is consistent.
Let X̂ be any maximal consistent extension of set X. Define w4 to be the sequence w1 :: C :: X̂. Note that w4 ∈ W
by Definition 10 and the choice of set X. At the same time,
w1 ∼C w4 by Definition 11 and Definition 3.

w0'

'
s1

'
sn

wn'

h_'

h'

Figure 4: Histories h and h0 .
Induction Step. Let h− = (w1 , s2 , . . . , sn , wn ), see Figure 4. By Definition 5, sequence h− is a history. By the induction hypothesis there is a history h0− such that h− ≈C
h0− and ¬ϕ ∈ hd(hd(h0− )). Let h0− = (w10 , s02 , . . . , s0n , wn0 ).
By Lemma 20, there is a state w00 and a complete strategy
profile s01 such that w0 ∼C w00 , (w00 , s01 , w10 ) ∈ M , and
s1 =C s01 .
Define h0 = (w00 , s01 , w10 , s02 , . . . , s0n , wn0 ). By Definition 5, statement (w00 , s01 , w10 ) ∈ M implies that h0 is a history. Note that h ≈C h0 by Definition 6 because h0− ≈C h− ,
w0 ∼C w00 , and s1 =C s01 . Finally, ¬ϕ ∈ hd(hd(h0 ))
because hd(h0 ) = hd(h0− ) and ¬ϕ ∈ hd(hd(h0− )).

H-child Lemmas Lemmas 23 and 24 are about the knowhow modality H. They are used later in the proof.

Lemma 23 For any history h, if HC ϕ ∈ hd(hd(h)), then
there is a strategy profile s of coalition C s.t. for any history
h0 :: s0 :: w0 if h ≈C h0 and s =C s0 , then ϕ ∈ hd(w0 ).
Proof. Consider a strategy profile s of coalition C such that
(s)a = ϕ for each agent a ∈ C. Suppose that HC ϕ ∈
hd(hd(h)) and sequence h0 :: s0 :: w0 is a history such that
h ≈C h0 and s =C s0 . It suffices to show that ϕ ∈ hd(w0 ).
By the Strategic Positive Introspection axiom, assumption
HC ϕ ∈ hd(hd(h)) implies hd(hd(h)) ` KC HC ϕ. Thus,
KC HC ϕ ∈ hd(hd(h)) by the maximality of set hd(hd(h)).
Assumption h ≈C h0 implies hd(h) ∼C hd(h0 ) by Definition 6. Thus, HC ϕ ∈ hd(hd(h0 )) by Lemma 17 and because KC HC ϕ ∈ hd(hd(h)).
By Definition 5, assumption that sequence h0 :: s0 :: w0
is a history implies that (hd(h0 ), s0 , w0 ) ∈ M . Thus,
ϕ ∈ hd(w0 ) by Definition 12 because HC ϕ ∈ hd(hd(h0 ))
and (s0 )a = (s)a = ϕ for each agent a ∈ C.

Lemma 24 For any history h and any strategy profile s of a
coalition C, if ¬HC ϕ ∈ hd(hd(h)), then there is a history
h :: s0 :: w0 such that s =C s0 and ¬ϕ ∈ hd(w0 ).
Proof. Let w = hd(h). Consider a complete strategy profile
s0 and a set of formulae X such that

(s)a , if a ∈ C,
(s0 )a =
(8)
>,
otherwise,
and

X = {¬ϕ} ∪ {χ | K∅ χ ∈ hd(w)} ∪
{ψ | HD ψ ∈ hd(w) ∧ ∀a ∈ D((s0 )a = ψ)}.

First, we show that set X is consistent. Indeed, note that set
{ψ | HD ψ ∈ hd(w) ∧ ∀a ∈ D((s0 )a = ψ)} is equal to the
union of the following two sets
{ψ | HD ψ ∈ hd(w) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)},
{ψ | HD ψ ∈ hd(w) ∧ D * C ∧ ∀a ∈ D((s0 )a = ψ)}.
The second of the two sets is a subset of {>} by the choice
(8) of strategy profile s0 . Thus, set X is a subset of
{>} ∪ {¬ϕ} ∪ {χ | K∅ χ ∈ hd(w)} ∪
{ψ | HD ψ ∈ hd(w) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)}.
Hence, to show the consistency of set X, it suffices to prove
the consistency of the union of {¬ϕ} ∪ {χ | K∅ χ ∈ hd(w)}
and {ψ | HD ψ ∈ hd(w) ∧ D ⊆ C ∧ ∀a ∈ D((s0 )a = ψ)}.
Suppose the opposite. In other words, assume there are
formulae
and formulae
such that

K∅ χ1 , . . . , K∅ χn ∈ hd(w)
HD1 ψ1 , . . . , HDm ψm ∈ hd(w)
D1 , . . . , Dm ⊆ C,
∀i ≤ m ∀a ∈ Di ((s0 )a = ψi ),

(9)
(10)
(11)
(12)

and χ1 , . . . , χn , ψ1 , . . . , ψm ` ϕ. By Lemma 9,
H∅ χ1 , . . . , H∅ χn , HD1 ψ1 , . . . , HDm ψm ` H∪m
ϕ.
i=1 Di
Then, by the Empty Coalition axiom,
K∅ χ1 , . . . , K∅ χn , HD1 ψ1 , . . . , HDm ψm ` H∪m
ϕ.
i=1 Di

Thus, by Lemma 8 and assumption (11),
K∅ χ1 , . . . , K∅ χn , HD1 ψ1 , . . . , HDm ψm ` HC ϕ.
Hence, hd(w) ` HC ϕ by assumption (9) and assumption (10). Then, ¬HC ϕ ∈
/ hd(w) due to the consistency of
the set hd(w), which contradicts the assumption ¬HC ϕ ∈
hd(w) of the lemma. Therefore, set X is consistent.
Let set X̂ be a maximal consistent extension of set X and
w0 be the sequence w :: ∅ :: X̂. Note that w0 ∈ W by
Definition 10 and because {χ | K∅ χ ∈ hd(w)} ⊆ X ⊆
X̂ = hd(w0 ) by the choice of set X.
Also note that (w, s0 , w0 ) ∈ M by Definition 12 and because {ψ | HD ψ ∈ hd(w) ∧ ∀a ∈ D((s0 )a = ψ)} ⊆ X ⊆
X̂ = hd(w0 ) by the choice of set X. Thus, h :: s0 :: w0 is a
history by Definition 5.
Finally, ¬ϕ ∈ hd(w0 ) because ¬ϕ ∈ X ⊆ X̂ = hd(w0 )
by the choice of set X.

Lemma 25 The system ET S(X0 ) is regular.
Proof. Let w ∈ W and s ∈ V A . By Definition 2, it
suffices to show that there is an epistemic state w0 such that
(w, s, w0 ) ∈ M . Indeed, let history h be a single-element
sequence w. Note that ¬HA ⊥ ∈ hd(w) = hd(hd(h)) by
the Unachievability of Falsehood axiom and due to the maximality of set hd(w). Thus, by Lemma 24, there is a history
h :: s0 :: w0 such that s =A s0 . Hence, (hd(h), s0 , w0 ) ∈ M
by Definition 5. At the same time, s =A s0 implies that
s = s0 by Definition 4. Thus, (hd(h), s, w0 ) ∈ M . Therefore, (w, s, w0 ) ∈ M because hd(h) = w.

Completeness: Final Steps
Lemma 26 h ϕ iff ϕ ∈ hd(hd(h)) for each history h and
each formula ϕ ∈ Φ.
Proof. We prove the statement by induction on the structural
complexity of formula ϕ. If ϕ is an atomic proposition p,
then h p iff hd(h) ∈ π(p), by Definition 9. Hence, h p
iff p ∈ hd(hd(h)) by Definition 13.
The cases when formula ϕ is a negation or an implication
follow from Definition 9 and the maximality and the consistency of the set hd(hd(h)) in the standard way.
Next, suppose that formula ϕ has the form KC ψ.
(⇒) : Let KC ψ ∈
/ hd(hd(h)). Then, either by Lemma 21
(when set C is empty) or by Lemma 22 (when set C is
nonempty), there is a history h0 such that h ≈C h0 and
¬ψ ∈ hd(hd(h0 )). Hence, h0 1 ψ by the induction hypothesis. Therefore, h 1 KC ψ by Definition 9.
(⇐) : Let h 1 KC ψ. By Definition 9, there is a history
h0 such that h ≈C h0 and h0 1 ψ. Thus, ψ ∈
/ hd(hd(h0 ))
by the induction hypothesis. Then, KC ϕ ∈
/ hd(hd(h)) by
Lemma 19.
Finally, let formula ϕ be of the form HC ψ.
(⇒) : Assume h HC ψ. Then, by Definition 9, there is a
strategy profile s ∈ ΦC such that for any history h0 :: s0 ::
w0 , if h ≈C h0 and s =C s0 , then h0 :: s0 :: w0 ψ. Thus,
by Lemma 3,
for any history h :: s0 :: w0 , if s =C s0 , then
h :: s0 :: w0 ψ.

(13)

Suppose that HC ψ ∈
/ hd(hd(h)). Then, ¬HC ψ ∈
hd(hd(h)) due to the maximality of the set hd(hd(h)).
Hence, by Lemma 24, there is a history h :: s0 :: w0 such
that s =C s0 and ¬ψ ∈ hd(w0 ). Thus, ψ ∈
/ hd(w0 ) due to
the consistency of set hd(w0 ). Hence, by the induction hypothesis, h :: s0 :: w0 1 ψ, which contradicts statement (13).
(⇐) : Assume that HC ψ ∈ hd(hd(h)). By Lemma 23, there
is a strategy profile s ∈ ΦC such that for any history h0 ::
s0 :: w0 if h ≈C h0 and s =C s0 , then ψ ∈ hd(w0 ). Hence,
by the induction hypothesis, for any history h0 :: s0 :: w0 if
h ≈C h0 and s =C s0 , then h0 :: s0 :: w0
ψ. Therefore,
h HC ψ by Definition 9.

Theorem 2 If h
ϕ for each history h of each regular
epistemic transition system, then ` ϕ.
Proof. Suppose that 0 ϕ. Consider any maximal consistent
set X0 such that ¬ϕ ∈ X0 . Let h0 be a single-element sequence consisting of just set X0 . By Definition 5, sequence
h0 is a history of the canonical epistemic transition system ET S(X0 ). Then, h0
¬ϕ by Lemma 26. Therefore,
h0 1 ϕ by Definition 9.

Theorem 2 can be generalized to the strong completeness
theorem in the standard way. We also believe that the number of states and the domain of choices in the canonical
model can be made finite using filtration on subformulae.

Conclusion
We have extended the recent study of the interplay between knowledge and strategic coalition power (Ågotnes
and Alechina 2016; Fervari et al. 2017; Naumov and Tao
2017b; Naumov and Tao 2017a) to the case of perfect recall.
Our main results are the soundness and the completeness
theorems.

References
[Ågotnes and Alechina 2012] Ågotnes, T., and Alechina, N.
2012. Epistemic coalition logic: completeness and complexity. In Proceedings of the 11th International Conference
on Autonomous Agents and Multiagent Systems-Volume 2
(AAMAS), 1099–1106. International Foundation for Autonomous Agents and Multiagent Systems.
[Ågotnes and Alechina 2016] Ågotnes, T., and Alechina, N.
2016. Coalition logic with individual, distributed and
common knowledge. Journal of Logic and Computation.
exv085.
[Ågotnes et al. 2010] Ågotnes, T.; Balbiani, P.; van Ditmarsch, H.; and Seban, P. 2010. Group announcement logic.
Journal of Applied Logic 8(1):62 – 81.
[Ågotnes, van der Hoek, and Wooldridge 2009] Ågotnes, T.;
van der Hoek, W.; and Wooldridge, M. 2009. Reasoning
about coalitional games. Artificial Intelligence 173(1):45 –
79.
[Alur, Henzinger, and Kupferman 2002] Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time
temporal logic. Journal of the ACM 49(5):672–713.

[Aminof et al. 2016] Aminof, B.; Murano, A.; Rubin, S.; and
Zuleger, F. 2016. Prompt alternating-time epistemic logics.
KR 16:258–267.
[Belardinelli 2014] Belardinelli, F. 2014. Reasoning about
knowledge and strategies: Epistemic strategy logic. In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume
146 of EPTCS, 27–33.
[Borgo 2007] Borgo, S. 2007. Coalitions in action logic.
In 20th International Joint Conference on Artificial Intelligence, 1822–1827.
[Broersen, Herzig, and Troquard 2009] Broersen, J.; Herzig,
A.; and Troquard, N. 2009. What groups do, can do, and
know they can do: an analysis in normal modal logics. Journal of Applied Non-Classical Logics 19(3):261–289.
[Broersen 2008] Broersen, J. 2008. A Logical Analysis of the
Interaction between ‘Obligation-to-do’ and ‘Knowingly Doing’. Berlin, Heidelberg: Springer Berlin Heidelberg. 140–
154.
[Fervari et al. 2017] Fervari, R.; Herzig, A.; Li, Y.; and
Wang, Y. 2017. Strategically knowing how. In Proceedings of the Twenty-Sixth International Joint Conference on
Artificial Intelligence, IJCAI-17, 1031–1038.
[Goranko, Jamroga, and Turrini 2013] Goranko, V.; Jamroga, W.; and Turrini, P. 2013. Strategic games and truly
playable effectivity functions. Autonomous Agents and
Multi-Agent Systems 26(2):288–314.
[Goranko 2001] Goranko, V. 2001. Coalition games and alternating temporal logics. In Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge,
259–272. Morgan Kaufmann Publishers Inc.
[Harding et al. 2014] Harding, J.; Powell, G., R.; Yoon, R.;
Fikentscher, J.; Doyle, C.; Sade, D.; Lukuc, M.; Simons, J.;
and Wang, J. 2014. Vehicle-to-vehicle communications:
Readiness of v2v technology for application. Washington,
DC: National Highway Traffic Safety Administration. (Report No. DOT HS 812 014).
[Jamroga and Ågotnes 2007] Jamroga, W., and Ågotnes, T.
2007. Constructive knowledge: what agents can achieve
under imperfect information. Journal of Applied NonClassical Logics 17(4):423–475.
[Jamroga and van der Hoek 2004] Jamroga, W., and van der
Hoek, W. 2004. Agents that know how to play. Fundamenta
Informaticae 63(2-3):185–219.
[More and Naumov 2012] More, S. M., and Naumov, P.
2012. Calculus of cooperation and game-based reasoning about protocol privacy. ACM Trans. Comput. Logic
13(3):22:1–22:21.
[Naumov and Tao 2017a] Naumov, P., and Tao, J. 2017a.
Coalition power in epistemic transition systems. In Proceedings of the 2017 International Conference on Autonomous
Agents and Multiagent Systems (AAMAS), 723–731.
[Naumov and Tao 2017b] Naumov, P., and Tao, J. 2017b.
Together we know how to achieve: An epistemic logic of
know-how. In 16th conference on Theoretical Aspects of Ra-

tionality and Knowledge (TARK), July 24-26, 2017, EPTCS
251, 441–453.
[Pauly 2001] Pauly, M. 2001. Logic for Social Software.
Ph.D. Dissertation, Institute for Logic, Language, and Computation.
[Pauly 2002] Pauly, M. 2002. A modal logic for coalitional power in games. Journal of Logic and Computation
12(1):149–166.
[Sahlqvist 1975] Sahlqvist, H. 1975. Completeness and
correspondence in the first and second order semantics for
modal logic. Studies in Logic and the Foundations of Mathematics 82:110–143. (Proc. of the 3rd Scandinavial Logic
Symposium, Uppsala, 1973).
[Sauro et al. 2006] Sauro, L.; Gerbrandy, J.; van der Hoek,
W.; and Wooldridge, M. 2006. Reasoning about action and
cooperation. In Proceedings of the Fifth International Joint
Conference on Autonomous Agents and Multiagent Systems,
AAMAS ’06, 185–192. New York, NY, USA: ACM.
[van Benthem 2001] van Benthem, J. 2001. Games in
dynamic-epistemic logic. Bulletin of Economic Research
53(4):219–248.
[van der Hoek and Wooldridge 2003] van der Hoek, W., and
Wooldridge, M. 2003. Cooperation, knowledge, and time:
Alternating-time temporal epistemic logic and its applications. Studia Logica 75(1):125–157.
[van der Hoek and Wooldridge 2005] van der Hoek, W., and
Wooldridge, M. 2005. On the logic of cooperation and
propositional control. Artificial Intelligence 164(1):81 –
119.
[Wang 2015] Wang, Y. 2015. A logic of knowing how. In
Logic, Rationality, and Interaction. Springer. 392–405.
[Wang 2016] Wang, Y. 2016. A logic of goal-directed knowing how. Synthese.

