# Clandestine Strategies in Games with Imperfect Information

Pavel Naumov1 Oliver Orejola2 1University of Southampton, United Kingdom
2Tulane University, United States<EMAIL_ADDRESS><EMAIL_ADDRESS>
(February 2020)

# Logic of Clandestine Operations

Pavel Naumov1 Oliver Orejola2 1University of Southampton, United Kingdom
2Tulane University, United States<EMAIL_ADDRESS><EMAIL_ADDRESS>
(February 2020)

# Strategic Coalitions in Clandestine Games

Pavel Naumov1 Oliver Orejola2 1University of Southampton, United Kingdom
2Tulane University, United States<EMAIL_ADDRESS><EMAIL_ADDRESS>
(February 2020)

# Shhh! The Logic of Clandestine Operations

Pavel Naumov1 Oliver Orejola2 1University of Southampton, United Kingdom
2Tulane University, United States<EMAIL_ADDRESS><EMAIL_ADDRESS>
(February 2020)

###### Abstract

An operation is called covert if it conceals the identity of the actor; it is
called clandestine if the very fact that the operation is conducted is
concealed. The paper proposes a formal semantics of clandestine operations and
introduces a sound and complete logical system that describes the interplay
between the distributed knowledge modality and a modality capturing coalition
power to conduct clandestine operations.

##  1 Clandestine Games

In this paper, we study games in which coalitions can engage in concealed
operations. The US Department of Defense Dictionary of Military and Associated
Terms distinguishes between covert and clandestine operations. Covert
operations are planned and executed to conceal the identity of the actor. An
operation is clandestine when the very fact that the operation is conducted is
concealed Office of the Chairman of the Joint Chiefs of Staff (2020). Thus,
every clandestine operation is covert, but not every covert operation is
clandestine. The focus of the current work is on clandestine operations.

Figure 1: Cuban Missile Crisis Game.

An example of a clandestine operation is 1962 Operation Anadyr conducted by
the Soviet Union arm forces as a prelude to the Cuban Missile Crisis Hansen
(2007). The operation consisted of the delivery and deployment of ballistic
missiles with nuclear warheads in Cuba to prevent an invasion of the island by
the United States. Figure 1 depicts our representation of the Cuban Missile
Crisis as a clandestine game between three players: the Americans ($a$), the
Cubans ($c$), and the Russians ($r$). Operation Anadyr was executed by the
Cubans and the Russians and consisted in transitioning the world from state
$w$ to state $w^{\prime}$. Propositional variable $m$ denotes the statement
“Missiles are deployed in Cuba”. It is false in state $w$ and true in state
$w^{\prime}$. Operation Anadyr was concealed in the sense that the Americans
were not able to detect the transition of the world from state $w$ to state
$w^{\prime}$. In the diagram, the indistinguishability of these two states to
Americans is shown using a dashed line.

Although states $w$ and $w^{\prime}$ are indistinguishable to Americans, this
does not prevent them from discovering the transition from state $w$ to state
$w^{\prime}$ by executing an operation of their own. In fact, they did just
that on October 14th, 1962, by conducting a clandestine operation Mission 3101
McAuliffe (1992). Mission 3101 consisted of a U-2 spy plane secretly flying
over Cuban territory to collect military intelligence. Mission 3101 also was
concealed in the sense that, as shown in the diagram, the Cubans and the
Russians were not able to detect its execution that transitioned the world
from state $w^{\prime}$ to state $v$. If the same Mission 3101 were to be
executed in state $w$, it would hypothetically transition the world from state
$w$ to state $u$. The Americans can distinguish state $v$ from state $u$ based
on the reconnaissance photos taken by the spy plane. This explains how the
Americans were able to detect the execution of Operation Anadyr through
operation Mission 3101.

Coalition power in games with imperfect information has been studied before in
synchronous settings where all agents act at once and, thus, everyone is aware
that something happened van der Hoek and Wooldridge (2003); Ågotnes and
Alechina (2012); Naumov and Tao (2017, 2018b, 2018a); Ågotnes and Alechina
(2019). To capture clandestine operations it is crucial to use semantics in
which an agent might be unaware of the game transitioning from one state to
another as a result of the actions of other agents. Such a behaviour could be
modelled, for example, by extending the semantics of the above logical systems
with a single $sleep$ action. Additionally, it should be required that any
agent executing action $sleep$ should not be able to distinguish the initial
and the final state of any transition during which the agent used $sleep$.
This approach would also need to settle who learns what if two or more
disjoint coalitions execute clandestine operations synchronously.

For the sake of the clarity of presentation, in this paper, we define the
semantics of clandestine operations in terms of a class of asynchronous games
that we call clandestine games that are described in the definition below.

In this paper, we will assume a fixed set of agents $\mathcal{A}$. By a
coalition we mean any (possibly empty) subset of $\mathcal{A}$. For any
coalition $C$, by $\overline{C}$ we denote the complement of set $C$ with
respect to set $\mathcal{A}$.

######  Definition 1.

Let a clandestine game be any such tuple
$(W,\\{\sim_{a}\\}_{a\in\mathcal{A}},\Delta,M,\pi)$ that

  1. 1.

$W$ is a set of “states”.

  2. 2.

$\sim_{a}$ is an “indistinguishability” equivalence relation on set $W$ for
each agent $a\in\mathcal{A}$. We write $w\sim_{C}u$ if $w\sim_{a}u$ for each
agent $a\in C$.

  3. 3.

$\Delta$ is a nonempty set of “operations”.

  4. 4.

$M$ is a set of tuples $(w,C,\delta,u)$, where $w,u\in W$ are states,
$C\subseteq\mathcal{A}$ is a coalition, and $\delta\in\Delta$ is an operation.
It is assumed that set $M$, called “mechanism”, satisfies the following two
conditions

    1. (a)

concealment: for any two states $w,u\in W$, any coalition of agents
$C\subseteq\mathcal{A}$, any operation $\delta\in\Delta$, if
$(w,C,\delta,u)\in M$, then $w\sim_{\overline{C}}u$,

    2. (b)

nontermination: for any state $w\in W$, any coalition of agents
$C\subseteq\mathcal{A}$, and any operation $\delta\in\Delta$, there is at
least one state $u\in W$ such that $(w,C,\delta,u)\in M$.

  5. 5.

$\pi(p)$ is a subset of $W$ for each propositional variable $p$.

The diagram in Figure 1 depicts an example of a clandestine game with four
states ($w$, $w^{\prime}$, $u$, and $v$) and two operations (Anadyr and 3101).
The indistinguishability relations are shown by dashed lines and the mechanism
is depicted by directed lines. The diagram omits loop operations. This means,
for example, that if the Americans execute Operation Anadyr in any of the
states, then the game transitions back to the same state. The nontermination
condition 4(b) guarantees that no operation can terminate a game without
reaching some state.

In a real-world setting, a variety of operations might be performed by any
coalition. Some of them satisfy the concealment condition 4(a) of Definition
1, the others might not. We excluded non-concealed operations from our games
to keep the presentation simple. If such operations are added to the models
and the quantifier over operations $\delta$ in item 5 of Definition 2 below is
simultaneously restricted to concealed operations only, then the soundness and
the completeness results of this paper will remain true and no changes to
their proofs will be necessary.

In this paper, we propose a sound and complete logical system for reasoning
about coalition power to conduct clandestine operations. The rest of the paper
is organized as follows. In the next section, we discuss the interplay between
knowledge and actions and explain why existing coalition power modalities do
not capture the properties of clandestine operations. Then, we define the
syntax and semantics of our logical system. In the section Coalition-
Informant-Adversary Principle, we introduce and discuss the most non-trivial
axiom of our system. In the section that follows, we list the remainder of the
axioms. After that, we sketch the completeness of our logical system. The
proof of soundness and some details of the completeness are in the appendix.

##  2 Knowledge and Actions

In this section, we discuss how different forms of knowledge can be captured
in the existing modal logics for reasoning about coalition power and explain
why the power to perform a clandestine operation is not expressible in these
logics.

When discussing the interplay between knowledge and actions, it is common to
distinguish ex-ante, interim, and ex-post knowledge. They refer to an agent’s
(or a coalition’s) knowledge before the action, at the moment of the action,
and after the action, respectively. One of the first logical systems
describing the interplay between distributed knowledge modality ${\sf K}_{C}$
and coalition power modality ${\sf S}_{C}$ was introduced in Ågotnes and
Alechina (2012). Using their language, one can write ${\sf K}_{C}{\sf
S}_{C}\varphi$ to state that coalition $C$ knows ex-ante (before the action)
that it has a strategy (joint action) to achieve $\varphi$. Using the same
language, one can write ${\sf S}_{C}{\sf K}_{C}\varphi$ to state that
coalition $C$ has a strategy that would result in $\varphi$ being known ex-
post to the coalition. The language of Ågotnes and Alechina (2012) cannot be
used to express interim knowledge. However, this could be done using “seeing
to it” modality Belnap and Perloff (1990); Horty (2001); Horty and Belnap
(1995); Horty and Pacuit (2017); Olkhovikov and Wansing (2018).

Knowing that a strategy exists, as in ${\sf K}_{C}{\sf S}_{C}\varphi$, is
different from actually knowing the strategy. If a coalition $C$ knows ex-ante
what strategy it can use to achieve $\varphi$, then we say that the coalition
has a know-how strategy to achieve $\varphi$ and denote this by ${\sf
H}_{C}\varphi$. Unless the coalition has a perfect recall, knowing ex-ante a
strategy to achieve $\varphi$ does not imply knowing ex-ante a strategy that
results in knowing ex-post that $\varphi$ is achieved. The latter, however,
could be expressed as ${\sf H}_{C}{\sf K}_{C}\varphi$. The interplay between
coalitional know-how modality ${\sf H}_{C}$ and distributed knowledge modality
${\sf K}_{C}$ has been studied in Naumov and Tao (2017); Fervari et al.
(2017); Naumov and Tao (2018b, a); Ågotnes and Alechina (2019); Cao and Naumov
(2020).

Figure 2: Knowledge and Actions.

In epistemic models, knowledge is usually captured by an indistinguishably
relation between states. For example, in Figure 2 (left), $w_{1}\Vdash{\sf
K}_{C}{\sf S}_{C}p$. In other words, coalition $C$ knows ex-ante that it has a
strategy to achieve $p$. This is true because the coalition has such a
strategy not only in state $w_{1}$, but also in state $w_{2}$,
indistinguishable to the coalition from $w_{1}$. Note that this is not a know-
how strategy because the required strategy in state $w_{1}$ (strategy
$\delta_{1}$) is different from the required strategy in state $w_{2}$
(strategy $\delta_{2}$). Thus, $w_{1}\Vdash\neg{\sf H}_{C}p$. Note also that
in state $w_{1}$ coalition $C$ does not have a strategy to achieve ex-post
knowledge of $p$. We write this as $w_{1}\Vdash\neg{\sf S}_{C}{\sf K}_{C}p$.
This is true because state $u_{1}$ is indistinguishable from state $u_{0}$
where $p$ is not satisfied.

The situation is different in Figure 2 (centre). Here, coalition $C$ has a
strategy in state $w_{1}$ to achieve $p$, but the coalition does not know this
ex-ante because it cannot distinguish state $w_{1}$ from state $w_{2}$ where
such a strategy does not exist. Using our notations, $w_{1}\Vdash{\sf S}_{C}p$
and $w_{1}\Vdash\neg{\sf K}_{C}{\sf S}_{C}p$. Note, however, that in this
setting coalition also has a strategy to achieve ex-post knowledge of $p$
because $p$ is satisfied not only in state $u_{1}$ but also in state $u_{0}$,
indistinguishable to $C$ from state $u_{1}$. We write this as $w_{1}\Vdash{\sf
S}_{C}{\sf K}_{C}p$

The clandestine operations that we consider in this paper are know-how
strategies. Furthermore, for the reason we discuss in the next section, they
are know-how strategies to achieve ex-post knowledge. This alone would not
require a new modality because it can be captured in existing know-how logics
as ${\sf H}_{C}{\sf K}_{C}\varphi$. However, the last formula does not account
for the concealed nature of clandestine operations. We capture the late by
requiring the initial and the final state of the operation to be
indistinguishable to the complement $\overline{C}$ of coalition $C$. Strategy
$\delta$ depicted in Figure 2 (right) is a clandestine operation of coalition
$C$ to achieve $p$. In this paper, we introduce a new modality
$\Box_{C}\varphi$ to denote an existence of a clandestine operation of
coalition $C$ to achieve $\varphi$. This modality is not definable through
existing modalities of coalition power, know-how, and seeing-to-it, because
these existing modalities cannot capture the indistinguishably (by the
complement of coalition $C$) of the initial and the final state of the
operation.

##  3 Syntax and Semantics

Language $\Phi$ of our logical system is defined by the grammar

$\varphi:=p\;|\;\neg\varphi\;|\;\varphi\to\varphi\;|\;{\sf
K}_{C}\varphi\;|\;{\Box}_{C}\varphi,$

where $p$ is a propositional variable and $C$ is a coalition. We read formula
${\sf K}_{C}\varphi$ as “coalition $C$ knows $\varphi$”, and formula
$\Box_{C}\varphi$ as “coalition $C$ knows which clandestine operation it can
execute to achieve $\varphi$”. In both cases, the knowledge is distributed. We
assume that Boolean constants $\top$ and $\bot$ as well as disjunction $\vee$
are defined in the standard way. We use ${\sf K}_{C,D}\varphi$ and
$\Box_{C,D}\varphi$ as shorthand for ${\sf K}_{C\cup D}\varphi$ and
$\Box_{C\cup D}\varphi$ respectively.

In the definition below, item 5 gives formal semantics of modality
${\Box}_{C}\varphi$, see Figure 3.

######  Definition 2.

For any state $w\in W$ of a clandestine game
$(W,\\{\sim_{a}\\}_{a\in\mathcal{A}},\Delta,M,\pi)$ and any formula
$\varphi\in\Phi$, satisfiability relation $w\Vdash\varphi$ is defined
recursively as

  1. 1.

$w\Vdash p$ if $w\in\pi(p)$,

  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 $u\Vdash\varphi$ for any $u\in W$ such that
$w\sim_{C}u$,

  5. 5.

$w\Vdash{\Box}_{C}\varphi$ if there is a nonempty coalition
$C^{\prime}\subseteq C$ and an operation $\delta\in\Delta$ such that for any
states $w^{\prime},u,u^{\prime}\in W$, if $w\sim_{C}w^{\prime}$,
$(w^{\prime},C^{\prime},\delta,u)\in M$, and $u\sim_{C}u^{\prime}$, then
$u^{\prime}\Vdash\varphi$.

Figure 3: Towards item 5 of Definition 2.

In item 5 of the above definition, we introduce coalition $C^{\prime}$ to
capture the fact that in order for a coalition $C$ to know a clandestine
operation to achieve a certain goal, not all members of the coalition $C$ have
to take an active part in it.

Recall that Definition 1 allows for some operations to be conducted by the
empty coalition. Such operations can change the state of the game. However,
according to the concealment condition of Definition 1, such change is not
noticeable to any agent in the game. Informally, these operations could be
thought of as nondeterministic transitions of the game that occur
independently from the actions of the agents and are not noticeable to them.
The presence of such transitions is not significant for the results in this
paper. We do not exclude them for the sake of generality. At the same time, in
Definition 2, we require coalition $C^{\prime}$ to be nonempty. Intuitively, a
coalition can ask some of its members to conduct an operation, but the
coalition cannot ask the empty coalition, because operations of the empty
coalition are system transitions not controlled by the agents. The restriction
of $C^{\prime}$ to nonempty coalitions is significant for our results.

Item 5 of Definition 2 is using state $w^{\prime}$ to express that the
clandestine operation $\delta$ not only exists but it is known to coalition
$C$. Note that this knowledge, captured through statement
$w\sim_{C}w^{\prime}$, is the knowledge of the whole coalition $C$, not just
its part $C^{\prime}$ that executes the operation. In other words, we assume
that some members of the coalition $C$ could be passive informants. We explore
this in the Coalition-Informant-Adversary axiom of our logical system.

Formula ${\Box}_{C}\varphi$ states that coalition $C$ knows a clandestine
operation to achieve $\varphi$. Because clandestine games are asynchronous, an
important question is for how long $\varphi$ will remain true after the
operation. If another coalition can “undo” the operation without $C$ even
noticing, then coalition $C$ could only be sure that $\varphi$ holds at the
very moment the operation is completed. To avoid this, in item 5 of Definition
2, we require $\varphi$ to be satisfied not only in the completion state $u$
of the operation $\delta$, but also in all states $u^{\prime}$
indistinguishable from state $u$ by coalition $C$. In other words, statement
$\varphi$ remains true until at least one of the members of coalition $C$
takes part in another clandestine operation111If non-concealed operations are
added to Definition 1 as described in the previous section, then $\varphi$
will remain until at least one of the members of coalition $C$ becomes aware
that another operation took place..

##  4 Coalition-Informant-Adversary Principle

The most interesting axiom of our logical system is a principle that captures
strategic information dynamics between three sets of agents: a coalition that
conducts a clandestine operation, a group of informants who passively
cooperate with the coalition by sharing knowledge but do not participate in
the operation itself, and a group of adversaries who do not cooperate with the
coalition at all. To understand this principle, let us first consider its
simplified form without the adversaries: for any disjoint coalitions $C$ and
$I$,

${\sf K}_{I}({\sf K}_{C}\varphi\to{\sf
K}_{C}\psi)\to({\Box}_{C}\varphi\to{\Box}_{C,I}\psi).$ (1)

The assumption ${\Box}_{C}\varphi$ of this principle states that before the
operation (ex-ante) the coalition knows which clandestine operation it should
conduct in order to know after the operation (ex-post) that $\varphi$ is true.
The other assumption ${\sf K}_{I}({\sf K}_{C}\varphi\to{\sf K}_{C}\psi)$ of
this principle refers to ex-ante knowledge of a group of informants $I$.
Because the operation is clandestine and $C\cap I=\varnothing$, the ex-ante
and ex-post knowledge of $I$ is the same. Thus, statement ${\sf
K}_{C}\varphi\to{\sf K}_{C}\psi$ will have to be true after the operation. In
other words, after the operation coalition, $C$ will know that not only
condition $\varphi$, but also condition $\psi$ is true. Coalition $C$ alone,
however, does not know this ex-ante and thus, it alone does not know an
operation to achieve condition $\psi$. Nevertheless, recall that coalition $I$
knows ${\sf K}_{C}\varphi\to{\sf K}_{C}\psi$ ex ante. Thus, it knows ex-ante
that ${\sf K}_{C}\varphi\to{\sf K}_{C}\psi$ will have to be true after any
clandestine operation that does not involve $I$. Therefore, the union of the
coalitions $C$ and $I$ knows ex-ante the operation that $C$ can conduct to
achieve $\psi$. That is, ${\Box}_{C,I}\psi$.

Note that the purpose of modality ${\sf K}_{I}$ in the assumption ${\sf
K}_{I}({\sf K}_{C}\varphi\to{\sf K}_{C}\psi)$ of principle (1) is to make sure
that statement ${\sf K}_{C}\varphi\to{\sf K}_{C}\psi$ is preserved during the
clandestine operation of coalition $C$. If one were to consider an additional
coalition, that we refer to as an adversary coalition $A$, then replacing
modality ${\sf K}_{I}$ with ${\sf K}_{A,I}$ still guarantees that statement
${\sf K}_{C}\varphi\to{\sf K}_{C}\psi$ is preserved during the operation (as
long as $A$ is also disjoint with $C$). Thus, one might think that the
following form of principle (1) is also valid:

${\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf
K}_{C}\psi)\to({\Box}_{C}\varphi\to{\Box}_{C,I}\psi).$

This statement, however, is not true. Assumptions ${\sf K}_{A,I}({\sf
K}_{C}\varphi\to{\sf K}_{C}\psi)$ and ${\Box}_{C}\varphi$ can only guarantee
that coalition $C$ knows ex ante an operation to achieve $\varphi$. If this
operation is executed, then coalition $C\cup I$ will know ex-post that
$\varphi$ is true, but they might not know ex-ante that they will know this
ex-post. To make sure that they indeed have such ex-ante knowledge, one more
knowledge modality should be added to the formula:

${\sf K}_{C,I}{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf
K}_{C}\psi)\to({\Box}_{C}\varphi\to{\Box}_{C,I}\psi).$

Finally, note that if instead of preserving ${\sf K}_{C}\varphi\to{\sf
K}_{C}\psi$, it is enough just to be able to preserve statement ${\sf
K}_{C}\varphi\to{\sf K}_{C,I}\psi$:

${\sf K}_{C,I}{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf
K}_{C,I}\psi)\to({\Box}_{C}\varphi\to{\Box}_{C,I}\psi).$

As it turns out, the above formula is the final and the most general form of
the Coalition-Informant-Adversary principle. In this paper, we show that this
principle, in combination with several much more straightforward other axioms,
forms a logical system that can derive all universally valid properties of
clandestine operations.

##  5 Axioms

In addition to propositional tautologies in the language $\Phi$, our logical
system contains the following axioms:

  1. 1.

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^{\prime}}\varphi\to{\sf K}_{C}\varphi$, where
$C^{\prime}\subseteq C$,

  5. 5.

Strategic Introspection: ${\Box}_{C}\varphi\to{\sf K}_{C}{\Box}_{C}\varphi$,

  6. 6.

Coalition-Informant-Adversary: if $C\cap(I\cup A)=\varnothing$, then
${\sf K}_{C,I}{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf
K}_{C,I}\psi)\to({\Box}_{C}\varphi\to{\Box}_{C,I}\psi)$,

  7. 7.

Nontermination: $\neg{\Box}_{C}\bot$,

  8. 8.

Empty Coalition: $\neg{\Box}_{\varnothing}\varphi$.

We write $\vdash\varphi$ if a formula $\varphi$ is provable from the above
axioms using the Modus Ponens and the two Necessitation inference rules:

$\dfrac{\varphi,\varphi\to\psi}{\psi}\hskip 22.76219pt\dfrac{\varphi}{{\sf
K}_{C}\varphi}\hskip
22.76219pt\dfrac{\varphi,\;\;\;\;\;C\neq\varnothing}{{\Box}_{C}\varphi}.$

We write $X\vdash\varphi$ if the formula $\varphi$ is provable from the
theorems of our logical system and the set of additional axioms $X$ using only
the Modus Ponens inference rule. The next two lemmas state well-known
properties of S5 modality ${\sf K}$.

The next five lemmas are used in the proof of the completeness of our logical
system. We give their proofs in the appendix.

######  Lemma 1.

If $\varphi_{1},...,\varphi_{n}\\!\vdash\\!\psi$, then ${\sf
K}_{C}\varphi_{1},...,{\sf K}_{C}\varphi_{n}\\!\vdash\\!{\sf K}_{C}\psi$.

######  Lemma 2.

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

######  Lemma 3.

$\vdash{\sf K}_{F}{\sf K}_{E}{\sf K}_{F}\varphi\to{\Box}_{F}\varphi$, where
$F\nsubseteq E$.

######  Lemma 4.

$\vdash{\sf K}_{E}\neg{\sf K}_{F}\varphi\to\neg{\Box}_{F}\varphi$, where
$E\cap F=\varnothing$.

######  Lemma 5.

$\vdash{\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\to{\sf K}_{E}\varphi\vee{\sf
K}_{F}\psi$, where $E\subseteq F$.

We show the following soundness theorem in the appendix.

######  Theorem 1.

For any state $w$ of a clandestine game, if $w\Vdash\chi$ for each formula
$\chi\in X$ and $X\vdash\varphi$, then $w\Vdash\varphi$.

In the rest of this paper, we prove the completeness of our logical system.

##  6 Canonical Model

As usual, the key step in the proof of completeness is the construction of a
canonical model.

The standard canonical model for epistemic logic of individual knowledge S5
defines states as maximal consistent sets of formulae. Two such sets are
indistinguishable to an agent $a$ if they contain the same ${\sf
K}_{a}$-formulae. Unfortunately, this approach does not work for distributed
knowledge because any two sets that are indistinguishable to agents $a$ and
$b$ would then only share ${\sf K}_{a}$ and ${\sf K}_{b}$ formulae. They might
have different ${\sf K}_{a,b}$-formulae.

Figure 4: Tree Construction.

To address this issue, we define the canonical model using a tree whose nodes
are labelled by maximal consistent sets and whose edges are labelled by
coalitions, see Figure 4. Informally, states are the nodes of this tree.
Formally, any state is a sequence of labels along the path leading from the
root of the tree to a node of the tree.

Let us now define canonical clandestine game
$M(X_{0})=(W,\\{\sim_{a}\\}_{a\in\mathcal{A}},\Delta,M,\pi)$ for an arbitrary
maximal consistent set of formulae $X_{0}$.

######  Definition 3.

Set $W$ consists of all finite sequences $X_{0},C_{1},\dots,C_{n},X_{n}$, such
that $n\geq 0$ and

  1. 1.

$X_{i}$ is a maximal consistent set of formulae for all $i>1$,

  2. 2.

$C_{i}\subseteq\mathcal{A}$ is a coalition for all $i\leq n$,

  3. 3.

$\\{\varphi\in\Phi\;|\;{\sf K}_{C_{i}}\varphi\in X_{i-1}\\}\subseteq X_{i}$,
for all $i\leq n$.

We define a tree structure on the set of states $W$ by saying that state
$w=X_{0},C_{1},X_{1},C_{2},\dots,C_{n},X_{n}$ and state $w::C_{n+1}::X_{n+1}$
are connected by an undirected edge labeled with all agents in coalition
$C_{n+1}$. For example, for the tree depicted in Figure 4, state
$X_{0},C_{2},X_{2}$ is adjacent to state $X_{0},C_{2},X_{2},C_{8},X_{8}$ and
the edge between them is labelled with all agents in coalition $C_{8}$.

######  Definition 4.

For any two states $w,w^{\prime}\in W$ and any agent $a\in\mathcal{A}$, let
$w\sim_{a}w^{\prime}$ if all edges along the simple path between $w$ and
$w^{\prime}$ are labelled with agent $a$.

Note that, in the above definition, the path might consist of a single node.

######  Lemma 6.

Relation $\sim_{a}$ is an equivalence relation on set $W$.

######  Definition 5.

Set of operations $\Delta$ is the set of all formulae in language $\Phi$.

Informally, operation $\varphi\in\Delta$ is a clandestine operation in the
canonical game that achieves $\varphi$ unnoticeable to the agents outside of
the coalition that performed the operation and makes the result known to the
coalition. This intuition is captured in the definition below. Throughout the
paper, by $hd(w)$ we denote the last element of the sequence $w$.

######  Definition 6.

Canonical mechanism $M$ is a set of all tuples $(w,C,\varphi,u)$ where $w,u\in
W$ are states, $C\subseteq\mathcal{A}$ is a coalition, and $\varphi\in\Phi$ is
a formula, such that $w\sim_{\overline{C}}u$ and if ${\Box}_{C}\varphi\in
hd(w)$, then ${\sf K}_{C}\varphi\in hd(u)$.

Note that the requirement $w\sim_{\overline{C}}u$ in the above definition
implies that mechanism $M$ satisfies the concealment condition from Definition
1. Next, we show that $M$ also satisfies the nontermination condition.

######  Lemma 7.

For any state $w$, any coalition $C\subseteq\mathcal{A}$, and any formula
$\varphi\in\Phi$, there is a state $u\in W$ such that $(w,C,\varphi,u)\in M$.

###### Proof.

We consider the following two cases separately:

Case I: ${\Box}_{C}\varphi\in hd(w)$. Let

$X=\\{{\sf K}_{C}\varphi\\}\cup\\{\psi\;|\;{\sf K}_{\overline{C}}\psi\in
hd(w)\\}.$

######  Claim.

Set $X$ is consistent.

Proof of Claim. Assume the opposite. Thus, there are formulae ${\sf
K}_{\overline{C}}\psi_{1}$,…, ${\sf K}_{\overline{C}}\psi_{n}\in hd(w)$ such
that $\psi_{1},\dots,\psi_{n}\vdash\neg{\sf K}_{C}\varphi.$ Hence, ${\sf
K}_{\overline{C}}\psi_{1},\dots,{\sf K}_{\overline{C}}\psi_{n}\vdash{\sf
K}_{\overline{C}}\neg{\sf K}_{C}\varphi.$ by Lemma 1. Then, $hd(w)\vdash{\sf
K}_{\overline{C}}\neg{\sf K}_{C}\varphi$ by the assumption ${\sf
K}_{\overline{C}}\psi_{1},\dots,{\sf K}_{\overline{C}}\psi_{n}\in hd(w)$.
Thus, $hd(w)\vdash\neg{\Box}_{C}\varphi$ by Lemma 4 and the Modus Ponens
inference rule. Then, ${\Box}_{C}\varphi\notin hd(w)$ because set $hd(w)$ is
consistent, which contradicts the assumption of the case. $\boxtimes\hskip
5.69054pt$

Let $X^{\prime}$ be any maximal consistent extension of set $X$ and $u$ be the
sequence $w::\overline{C}::X^{\prime}$. Then, $w\in W$ by Definition 3 as well
as the choice of sets $X$ and $X^{\prime}$.

Finally, note that $w\sim_{\overline{C}}u$ by Definition 4 because
$u=w::\overline{C}::X^{\prime}$. Also, ${\sf K}_{C}\varphi\in X\subseteq
X^{\prime}=hd(u)$ by the choice of sets $X$ and $X^{\prime}$ and the choice of
sequence $u$. Therefore, $(w,C,\varphi,u)\in M$ by Definition 6.

Case II: ${\Box}_{C}\varphi\notin hd(w)$. Take $u$ to be world $w$. Therefore,
$(w,C,\varphi,u)\in M$ by Definition 6. This concludes the proof of the lemma.
∎

######  Definition 7.

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

This concludes the definition of the canonical model
$M(X_{0})=(W,\\{\sim_{a}\\}_{a\in\mathcal{A}},\Delta,M,\pi)$.

##  7 Completeness

As usual, the proof of completeness is using an “induction” (or “truth”) lemma
to connect the syntax of our system with the semantics of the canonical model.
In our case, this is Lemma 13. The next five lemmas are auxiliary statements
that will be used in different cases of the induction step in the proof of
Lemma 13.

######  Lemma 8.

${\sf K}_{D}\varphi\in X_{n}$ iff ${\sf K}_{D}\varphi\in X_{n+1}$ for any
formula $\varphi\in\Phi$, any $n\geq 0$, and any state
$X_{0},C_{1},X_{1},C_{2},\dots,X_{n},C_{n+1},X_{n+1}\in W$, and any coalition
$D\subseteq C_{n+1}$.

###### Proof.

If ${\sf K}_{D}\varphi\in X_{n}$, then $X_{n}\vdash{\sf K}_{D}{\sf
K}_{D}\varphi$ by Lemma 2. Hence, $X_{n}\vdash{\sf K}_{C_{n+1}}{\sf
K}_{D}\varphi$ by the Monotonicity axiom, the assumption
$D\subseteq{C_{n+1}}$, and the Modus Ponens inference rule. Thus, ${\sf
K}_{C_{n+1}}{\sf K}_{D}\varphi\in X_{n}$ by the maximality of set $X_{n}$.
Therefore, ${\sf K}_{D}\varphi\in X_{n+1}$ by Definition 3.

Suppose that ${\sf K}_{D}\varphi\notin X_{n}$. Hence, $\neg{\sf
K}_{D}\varphi\in X_{n}$ by the maximality of set $X_{n}$. Thus,
$X_{n}\vdash{\sf K}_{D}\neg{\sf K}_{D}\varphi$ by the Negative Introspection
axiom and the Modus Ponens inference rule. Hence, $X_{n}\vdash{\sf
K}_{C_{n+1}}\neg{\sf K}_{D}\varphi$ by the Monotonicity axiom, the assumption
$D\subseteq C_{n+1}$, and the Modus Ponens inference rule. Then, ${\sf
K}_{C_{n+1}}\neg{\sf K}_{D}\varphi\in X_{n}$ by the maximality of set $X_{n}$.
Thus, $\neg{\sf K}_{D}\varphi\in X_{n+1}$ by Definition 3. Therefore, ${\sf
K}_{D}\varphi\notin X_{n+1}$ because set $X_{n+1}$ is consistent. ∎

######  Lemma 9.

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

###### Proof.

Assumption $w\sim_{C}u$ implies that all edges along the unique simple path
between nodes $w$ and $u$ are labeled with all agents in coalition $C$. Thus,
${\sf K}_{C}\varphi\in hd(u)$ by Lemma 8. Hence, $hd(u)\vdash\varphi$ by the
Truth axiom and the Modus Ponens inference rule. Therefore, $\varphi\in hd(u)$
because set $hd(u)$ is maximal. ∎

######  Lemma 10.

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

###### Proof.

Consider set $X=\\{\neg\varphi\\}\cup\\{\psi\;|\;{\sf K}_{C}\psi\in hd(w)\\}$.

######  Claim.

Set $X$ is consistent.

Proof of Claim. Suppose the opposite. Thus, there are formulae ${\sf
K}_{C}\psi_{1},\dots,{\sf K}_{C}\psi_{n}\in hd(w)$ such that
$\psi_{1},\dots,\psi_{n}\vdash\varphi$. Hence, ${\sf K}_{C}\psi_{1},\dots,{\sf
K}_{C}\psi_{n}\vdash{\sf K}_{C}\varphi$ by Lemma 1. Then, $hd(w)\vdash{\sf
K}_{C}\varphi$ by the assumption ${\sf K}_{C}\psi_{1},\dots,{\sf
K}_{C}\psi_{n}\in hd(w)$. Thus, ${\sf K}_{C}\varphi\in hd(w)$ because set
$hd(w)$ is maximal, which contradicts the assumption of the lemma.
$\boxtimes\hskip 5.69054pt$ Let $X^{\prime}$ be any maximal consistent
extension of set $X$ and $u$ be the sequence $w::C::X^{\prime}$. Then, $w\in
W$ by Definition 3 as well as the choice of sets $X$ and $X^{\prime}$.

Finally, $\neg\varphi\in X\subseteq X^{\prime}=hd(u)$ by the choice of sets
$X$ and $X^{\prime}$ and the choice of sequence $u$. Therefore, $\varphi\notin
hd(u)$ because set $hd(u)$ is consistent. ∎

######  Lemma 11.

For any formula ${\Box}_{C}\varphi\in hd(w)$ and any three states
$w^{\prime},u,u^{\prime}\in W$, if $w\sim_{C}w^{\prime}$,
$(w^{\prime},C,\varphi,u)\in M$, and $u\sim_{C}u^{\prime}$, then $\varphi\in
hd(u^{\prime})$.

###### Proof.

Assumption ${\Box}_{C}\varphi\in hd(w)$ implies that $hd(w)\vdash{\sf
K}_{C}{\Box}_{C}\varphi$ by the Strategic Introspection axiom and the Modus
Ponens inference rule. Hence, ${\sf K}_{C}{\Box}_{C}\varphi\in hd(w)$ because
set $hd(w)$ is maximal. Thus, ${\Box}_{C}\varphi\in hd(w^{\prime})$ by Lemma 9
and the assumption $w\sim_{C}w^{\prime}$. Then, ${\sf K}_{C}\varphi\in hd(u)$
by Definition 6 and the assumption $(w^{\prime},C,\varphi,u)\in M$. Therefore,
$\varphi\in hd(u^{\prime})$ by Lemma 9 and the assumption
$u\sim_{C}u^{\prime}$. ∎

######  Lemma 12.

If ${\Box}_{F}\varphi\notin hd(w)$, then for any nonempty coalition
$E\subseteq F$ and any action $\delta\in\Delta$, there are states
$w^{\prime},u,u^{\prime}$ such that $w\sim_{F}w^{\prime}$,
$(w^{\prime},E,\delta,u)\in M$, $u\sim_{F}u^{\prime}$, and $\varphi\notin
hd(u^{\prime})$.

In the proof of this lemma located below, we consecutively construct states
$w^{\prime}$, $u$, and $u^{\prime}$. To guarantee that state $u^{\prime}$
could be constructed after state $u$, we construct a state $u$ such that set
$hd(u)$ contains formula $\neg{\sf K}_{F}\varphi$. In this case, by Lemma 10,
there must exist a state $u^{\prime}$ such that $u\sim_{F}u^{\prime}$, and
$\varphi\notin hd(u^{\prime})$.

One might think that state $u$ could be constructed from state $w^{\prime}$ in
a similar fashion by guaranteeing first that set $hd(w^{\prime})$ contains
formula $\neg{\sf K}_{\overline{E}}{\sf K}_{F}\varphi$. However, there is a
problem because Definition 6 states that if set $hd(w^{\prime})$ contains
formula $\Box_{E}\delta$, then set $hd(u)$, in addition to formula $\neg{\sf
K}_{F}\varphi$, must also contain formula ${\sf K}_{E}\delta$. Thus, there are
two possible ways sets $hd(w^{\prime})$ and $hd(u)$ could be constructed:

  1. I.

Set $hd(u)$ contains $\neg{\sf K}_{F}\varphi$ and ${\sf K}_{E}\delta$. In this
case, set $hd(w^{\prime})$ must contain formula $\neg{\sf
K}_{\overline{E}}\,\neg(\neg{\sf K}_{F}\varphi\wedge{\sf K}_{E}\delta)$. The
last formula is equivalent to $\neg{\sf K}_{\overline{E}}({\sf
K}_{E}\delta\to{\sf K}_{F}\varphi)$,

  2. II.

Set $hd(u)$ contains only formula $\neg{\sf K}_{F}\varphi$. In this case, set
$hd(w^{\prime})$ must contain formulae $\neg{\sf K}_{\overline{E}}{\sf
K}_{F}\varphi$ and $\neg\Box_{E}\delta$.

We visualise these two cases on the diagram in Figure 5.

Figure 5: Towards the Proof of Lemma 12.

Unfortunately, there is no way to decide upfront which of these two ways could
be used to construct a consistent set $hd(w^{\prime})$. Thus, in the proof
below we attempt to concurrently construct both versions of the set
$hd(w^{\prime})$ and prove that one of the two attempts succeeds by resulting
in a consistent set $hd(w)$. Finally, note that in both cases we must also
guarantee that $w\sim_{F}w^{\prime}$. To achieve this, we include in set
$hd(w^{\prime})$ all such formulae $\psi$ that ${\sf K}_{F}\psi\in hd(w)$.

In the proof below, the two different attempts to create a set
$hd(w^{\prime})$ are carried out by defining sets $X$ and $Y$ and proving that
at least one of them is consistent. Set $hd(w^{\prime})$ is later defined as a
maximal consistent extension of either set $X$ or set $Y$ depending on which
one is consistent.

###### Proof.

Consider the following two sets of formulae:

$\displaystyle X$ $\displaystyle=$ $\displaystyle\\{\neg{\sf
K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf
K}_{F}\varphi)\\}\cup\\{\psi\;|\;{\sf K}_{F}\psi\in hd(w)\\},$ $\displaystyle
Y$ $\displaystyle=$ $\displaystyle\\{\neg{\Box}_{E}\delta,\neg{\sf
K}_{\overline{E}}{\sf K}_{F}\varphi\\}\cup\\{\psi\;|\;{\sf K}_{F}\psi\in
hd(w)\\}.$

######  Claim.

Either set $X$ or set $Y$ is consistent.

Proof of Claim. Suppose the opposite. Thus, there are

${\sf K}_{F}\psi_{1},\dots,{\sf K}_{F}\psi_{m},{\sf
K}_{F}\psi^{\prime}_{1},\dots,{\sf K}_{F}\psi^{\prime}_{n}\in hd(w)$ (2)

such that

$\displaystyle\psi_{1},\dots,\psi_{m}$ $\displaystyle\vdash$
$\displaystyle{\sf K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf K}_{F}\varphi),$
$\displaystyle\psi^{\prime}_{1},\dots,\psi^{\prime}_{n}$ $\displaystyle\vdash$
$\displaystyle{\Box}_{E}\delta\vee{\sf K}_{\overline{E}}{\sf K}_{F}\varphi.$

Then, by the Strategic Introspection axiom,

$\displaystyle\psi_{1},\dots,\psi_{m}$ $\displaystyle\vdash$
$\displaystyle{\sf K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf K}_{F}\varphi),$
$\displaystyle\psi^{\prime}_{1},\dots,\psi^{\prime}_{n}$ $\displaystyle\vdash$
$\displaystyle{\sf K}_{E}{\Box}_{E}\delta\vee{\sf K}_{\overline{E}}{\sf
K}_{F}\varphi.$

Hence, by Lemma 1,

$\displaystyle{\sf K}_{F}\psi_{1},\dots,{\sf K}_{F}\psi_{m}$
$\displaystyle\vdash$ $\displaystyle{\sf K}_{F}{\sf K}_{\overline{E}}({\sf
K}_{E}\delta\to{\sf K}_{F}\varphi),$ $\displaystyle{\sf
K}_{F}\psi^{\prime}_{1},\dots,{\sf K}_{F}\psi^{\prime}_{n}$
$\displaystyle\vdash$ $\displaystyle{\sf K}_{F}({\sf
K}_{E}{\Box}_{E}\delta\vee{\sf K}_{\overline{E}}{\sf K}_{F}\varphi).$

Thus, by assumption (2),

$\displaystyle hd(w)$ $\displaystyle\vdash$ $\displaystyle{\sf K}_{F}{\sf
K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf K}_{F}\varphi),$ (3) $\displaystyle
hd(w)$ $\displaystyle\vdash$ $\displaystyle{\sf K}_{F}({\sf
K}_{E}{\Box}_{E}\delta\vee{\sf K}_{\overline{E}}{\sf K}_{F}\varphi).$

The last statement, by Lemma 5, assumption $E\subseteq F$ of the lemma, and
the Modus Ponens inference rule, implies that

$hd(w)\vdash{\sf K}_{E}{\Box}_{E}\delta\vee{\sf K}_{F}{\sf
K}_{\overline{E}}{\sf K}_{F}\varphi.$

Then, by the Truth axiom and propositional reasoning,

$hd(w)\vdash{\Box}_{E}\delta\vee{\sf K}_{F}{\sf K}_{\overline{E}}{\sf
K}_{F}\varphi.$ (4)

Recall that set $E$ is nonempty by the assumption of the lemma. Thus, there is
at least one $e\in E$. Then, $e\in F$ by the assumption $E\subseteq F$ of the
lemma. Hence, $e\in F\setminus\overline{E}$. Thus, $F\nsubseteq\overline{E}$.
Then, $\vdash{\sf K}_{F}{\sf K}_{\overline{E}}{\sf
K}_{F}\varphi\to{\Box}_{F}\varphi$ by Lemma 3. At the same time,
$hd(w)\nvdash{\Box}_{F}\varphi$ by the assumption ${\Box}_{F}\varphi\notin
hd(w)$ of the lemma and the maximality of the set $hd(w)$. Then,
$hd(w)\nvdash{\sf K}_{F}{\sf K}_{\overline{E}}{\sf K}_{F}\varphi$ by the
contraposition of the Modus Ponens inference rule. Hence, $\neg{\sf K}_{F}{\sf
K}_{\overline{E}}{\sf K}_{F}\varphi\in hd(w)$ because set $hd(w)$ is maximal.
Thus, by propositional reasoning using statement (4),

$hd(w)\vdash{\Box}_{E}\delta.$ (5)

At the same time, assumption $E\subseteq F$ of the lemma implies that
$(F\setminus E)\cup\overline{F}=\overline{E}$. Then, $E\cap((F\setminus
E)\cup\overline{F})=E\cap\overline{E}=\varnothing$. Hence, the following
formula

${\sf K}_{E,F\setminus E}{\sf K}_{\overline{F},F\setminus E}({\sf
K}_{E}\delta\\!\to\\!{\sf K}_{E,F\setminus
E}\varphi)\to({\Box}_{E}\delta\\!\to\\!{\Box}_{E,F\setminus E}\varphi)$

is an instance of the Coalition-Informant-Adversary axiom where $C=E$,
$I=F\setminus E$, and $A=\overline{F}$. Thus, using statement (5) and
propositional reasoning,

$hd(w)\vdash{\sf K}_{E,F\setminus E}{\sf K}_{\overline{F},F\setminus E}({\sf
K}_{E}\delta\\!\to\\!{\sf K}_{E,F\setminus E}\varphi)\to{\Box}_{E,F\setminus
E}\varphi.$

Note that $E\cup(F\setminus E)=F$ and $\overline{F}\cup(F\setminus
E)=\overline{E}$ by the assumption $E\subseteq F$ of the lemma. In other
words,

$hd(w)\vdash{\sf K}_{F}{\sf K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf
K}_{F}\varphi)\to{\Box}_{F}\varphi.$

Then, $hd(w)\vdash{\Box}_{F}\varphi$ by statement (3) and the Modus Ponens
inference rule. Therefore, ${\Box}_{F}\varphi\in hd(w)$ because set $hd(w)$ is
maximal, which contradicts assumption ${\Box}_{F}\varphi\notin hd(w)$ of the
lemma. $\boxtimes\hskip 5.69054pt$

The claim that we just proved states that either set $X$ or set $Y$ is
consistent. We consider these two cases separately.

Case I: set $X$ is consistent. Let $X^{\prime}$ be any maximal consistent
extension of the set $X$ and let state $w^{\prime}$ be the sequence
$w::F::X^{\prime}$. Note that $w\in W$ by Definition 3 and the choice of set
$X$, set $X^{\prime}$, and sequence $w^{\prime}$. Also, $w\sim_{F}w^{\prime}$
by Definition 4 and the choice of sequence $w^{\prime}$.

Note that $\neg{\sf K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf
K}_{F}\varphi)\in X\subseteq X^{\prime}=hd(w^{\prime})$ by the choice of set
$X$, set $X^{\prime}$, and sequence $w^{\prime}$. Thus, ${\sf
K}_{\overline{E}}({\sf K}_{E}\delta\to{\sf K}_{F}\varphi)\notin
hd(w^{\prime})$ because set $hd(w^{\prime})$ is consistent. Hence, by Lemma
10, there is a state $u\in W$ such that $w^{\prime}\sim_{\overline{E}}u$ and
${\sf K}_{E}\delta\to{\sf K}_{F}\varphi\notin hd(u)$. Then, ${\sf
K}_{E}\delta\in hd(u)$ and ${\sf K}_{F}\varphi\notin hd(u)$ because $hd(u)$ is
a maximal consistent set. Statements $w^{\prime}\sim_{\overline{E}}u$ and
${\sf K}_{E}\delta\in hd(u)$ imply that $(w^{\prime},E,\delta,u)\in M$ by
Definition 6. Statement ${\sf K}_{F}\varphi\notin hd(u)$ implies that there is
a state $u^{\prime}\in W$ such that $u\sim_{F}u^{\prime}$ and $\varphi\notin
hd(u^{\prime})$ by Lemma 10.

Case II: set $Y$ is consistent. Let $Y^{\prime}$ be any maximal consistent
extension of the set $Y$ and let state $w^{\prime}$ be the sequence
$w::F::X^{\prime}$. As in the previous case, $w\in W$ by Definition 3 and the
choice of set $Y$, set $Y^{\prime}$, and sequence $w^{\prime}$. Also,
$w\sim_{F}w^{\prime}$ by Definition 4 and the choice of $w^{\prime}$.

Note that $\neg{\sf K}_{\overline{E}}{\sf K}_{F}\varphi\in Y\subseteq
Y^{\prime}=hd(w^{\prime})$ by the choice of set $Y$, set $Y^{\prime}$, and
sequence $w^{\prime}$. Thus, ${\sf K}_{\overline{E}}{\sf K}_{F}\varphi\notin
hd(w^{\prime})$ as set $hd(w^{\prime})$ is maximal consistent. Hence, by Lemma
10, there is a state $u\in W$ such that

$w^{\prime}\sim_{\overline{E}}u\;\;\;\mbox{ and }\;\;\;{\sf
K}_{F}\varphi\notin hd(u).$ (6)

At the same time, $\neg{\Box}_{E}\delta\in Y\subseteq
Y^{\prime}=hd(w^{\prime})$ by the choice of set $Y$, set $Y^{\prime}$, and
sequence $w^{\prime}$. Thus, ${\Box}_{E}\delta\notin hd(w^{\prime})$ because
set $hd(w^{\prime})$ is consistent. Then, $(w^{\prime},E,\delta,u)\in M$ by
Definition 6 and because $w^{\prime}\sim_{\overline{E}}u$ by statement (6).

Finally, $K_{F}\varphi\notin hd(u)$ by statement (6). Therefore, by Lemma 10,
there exists a state $u^{\prime}\in W$ such that $u\sim_{F}u^{\prime}$ and
$\varphi\notin hd(u^{\prime})$. This concludes the proof of the lemma. ∎

The next “truth lemma” follows from the four previous lemmas in the standard
way. Due to the space constraint, we give its proof in the appendix.

######  Lemma 13.

$w\Vdash\varphi$ iff $\varphi\in hd(w)$.

Theorem 1. If $X\nvdash\varphi$, then there is a state $w$ of a clandestine
game such that $w\Vdash\chi$ for each formula $\chi\in X$ and
$w\nVdash\varphi$.

###### Proof.

If $X\nvdash\varphi$, then set $X\cup\\{\neg\varphi\\}$ is consistent. Let $w$
be any maximal consistent extension of this set. Then, $w\Vdash\chi$ for each
formula $\chi\in X$ and $w\vdash\neg\varphi$ by Lemma 13. Therefore,
$w\nvdash\varphi$ by item 2 of Definition 2. ∎

##  8 Conclusion

In this paper, we proposed a sound and complete logical system that describe
properties of clandestine power modality $\Box_{C}\varphi$. A natural
generalization of our work could be a study of “partially-clandestine”
modality $\Box^{F}_{C}\varphi$, that stands for “coalition $C$ knows an
operation that it can use to achieve $\varphi$ unnoticeable to anyone outside
(friendly) coalition $F$”.

It is also possible to consider a broader class of clandestine operations that
achieve a goal through several consecutive clandestine actions of the given
coalition. This type of multi-step operations is similar to multi-step
strategies studied in know-how logics Fervari et al. (2017); Li and Wang
(2017); Wang (2018, 2015).

## References

  * Ågotnes and Alechina [2012] Thomas Ågotnes and Natasha Alechina.  Epistemic coalition logic: completeness and complexity.  In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems-Volume 2 (AAMAS), pages 1099–1106, 2012\.
  * Ågotnes and Alechina [2019] Thomas Ågotnes and Natasha Alechina.  Coalition logic with individual, distributed and common knowledge.  Journal of Logic and Computation, 29:1041–1069, 11 2019.
  * Belnap and Perloff [1990] Nuel Belnap and Michael Perloff.  Seeing to it that: A canonical form for agentives.  In Knowledge representation and defeasible reasoning, pages 167–190. Springer, 1990.
  * Cao and Naumov [2020] Rui Cao and Pavel Naumov.  Knowing the price of success.  Artificial Intelligence, 284:103287, 2020.
  * Fagin et al. [1995] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi.  Reasoning about knowledge.  MIT Press, Cambridge, MA, 1995.
  * Fervari et al. [2017] Raul Fervari, Andreas Herzig, Yanjun Li, and Yanjing Wang.  Strategically knowing how.  In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 1031–1038, 2017.
  * Hansen [2007] James H. Hansen.  Soviet deception in the cuban missile crisis.  Studies in Intelligence, 46(1), 2007.
  * Horty and Belnap [1995] John F Horty and Nuel Belnap.  The deliberative STIT: A study of action, omission, ability, and obligation.  Journal of Philosophical Logic, 24(6):583–644, 1995.
  * Horty and Pacuit [2017] John Horty and Eric Pacuit.  Action types in STIT semantics.  The Review of Symbolic Logic, pages 1–21, 2017.
  * Horty [2001] John F Horty.  Agency and deontic logic.  Oxford University Press, 2001.
  * Li and Wang [2017] Yanjun Li and Yanjing Wang.  Achieving while maintaining: A logic of knowing how with intermediate constraints.  In Logic and Its Applications: Proceedings of 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, pages 154–167. Springer, 2017.
  * McAuliffe [1992] Mary S. McAuliffe.  CIA Documents on the cuban missile crisis 1962, October 1992.  https://www.cia.gov/library/center-for-the-study-of-intelligence/csi-publications/books-and-monographs/Cuban%20Missile%20Crisis1962.pdf.
  * Naumov and Tao [2017] Pavel Naumov and Jia Tao.  Coalition power in epistemic transition systems.  In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 723–731, 2017.
  * Naumov and Tao [2018a] Pavel Naumov and Jia Tao.  Strategic coalitions with perfect recall.  In Proceedings of Thirty-Second AAAI Conference on Artificial Intelligence, 2018.
  * Naumov and Tao [2018b] Pavel Naumov and Jia Tao.  Together we know how to achieve: An epistemic logic of know-how.  Artificial Intelligence, 262:279 – 300, 2018.
  * Office of the Chairman of the Joint Chiefs of Staff [2020] Office of the Chairman of the Joint Chiefs of Staff.  DOD dictionary of military and associated terms, January 2020.
  * Olkhovikov and Wansing [2018] Grigory K Olkhovikov and Heinrich Wansing.  Inference as doxastic agency. part i: The basics of justification STIT logic.  Studia Logica, pages 1–28, 2018.
  * van der Hoek and Wooldridge [2003] Wiebe van der Hoek and Michael Wooldridge.  Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications.  Studia Logica, 75(1):125–157, 2003.
  * Wang [2015] Yanjing Wang.  A logic of knowing how.  In Logic, Rationality, and Interaction, pages 392–405. Springer, 2015.
  * Wang [2018] Yanjing Wang.  A logic of goal-directed knowing how.  Synthese, 195(10):4419–4439, 2018.

Technical Appendix

##  Appendix A Soundness

In this section, we prove the soundness of our logical system. The soundness
of the Truth, the Negative Introspection, the Distributivity, and the
Monotonicity axioms as well as of the Modus Ponens inference rule and the
Necessitation inference rule for modality ${\sf K}$ are well-known results
about epistemic logic of distributed knowledge Fagin et al. [1995]. Below we
prove the soundness of each of the remaining axioms and the Necessitation
inference rule for modality $\Box$ as separate lemmas.

######  Lemma 14.

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

###### Proof.

Consider any state $v$ such that $w\sim_{C}v$. By item 4 of Definition 2, it
suffices to show that $v\Vdash\Box_{C}\varphi$.

By item 5 of Definition 2, assumption $w\Vdash\Box_{C}\varphi$ implies that
there is a nonempty coalition $C^{\prime}\subseteq C$ and an operation
$\delta\in\Delta$ such that for any states $w^{\prime},u,u^{\prime}\in W$,

$w\sim_{C}w^{\prime}\wedge(w^{\prime},C^{\prime},\delta,u)\in M\wedge
u\sim_{C}u^{\prime}\Rightarrow u^{\prime}\Vdash\varphi.$ (7)

Towards the proof of statement $v\Vdash\Box_{C}\varphi$, consider any states
$v^{\prime},z,z^{\prime}\in W$ such that $v\sim_{C}v^{\prime}$,
$(v^{\prime},C^{\prime},\delta,z)\in M$, and $z\sim_{C}z^{\prime}$. By item 5
of Definition 2, it suffices to show that $z^{\prime}\Vdash\varphi$. Indeed,
notice that $w\sim_{C}v^{\prime}$ because $w\sim_{C}v$ and
$v\sim_{C}v^{\prime}$. Therefore, $z^{\prime}\Vdash\varphi$ due to statement
(7). ∎

######  Lemma 15.

If $w\Vdash{\sf K}_{C,I}{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf
K}_{C,I}\psi)$, $w\Vdash{\Box}_{C}\varphi$, and $C\cap(I\cup A)=\varnothing$,
then $w\Vdash{\Box}_{C,I}\psi$.

###### Proof.

Assumption $w\Vdash{\Box}_{C}\varphi$ implies that there is a coalition

$C^{\prime}\subseteq C$ (8)

and an action $\delta\in\Delta$ such that for any states
$w^{\prime},u,u^{\prime}\in W$,

$w\sim_{C}w^{\prime}\wedge(w^{\prime},C^{\prime},\delta,u)\in M\wedge
u\sim_{C}u^{\prime}\Rightarrow u^{\prime}\Vdash\varphi.$ (9)

Towards the proof of statement $w\Vdash\Box_{C,I}\psi$, consider any states
$w^{\prime\prime},v,v^{\prime}\in W$ such that

$w\sim_{C,I}w^{\prime\prime},$ (10) $(w^{\prime\prime},C^{\prime},\delta,v)\in
M,$ (11)

and

$v\sim_{C,I}v^{\prime}.$ (12)

By item 5 of Definition 2, it suffices to show that $v^{\prime}\Vdash\psi$.

######  Claim.

$v\Vdash{\sf K}_{C}\varphi$.

Proof of Claim. Consider any state $v^{\prime\prime}\in W$ such that

$v\sim_{C}v^{\prime\prime}.$ (13)

By item 4 of Definition 2, it suffices to show that
$v^{\prime\prime}\Vdash\varphi$. Indeed, statement (10) implies that
$w\sim_{C}w^{\prime\prime}$. Then, $v^{\prime\prime}\Vdash\varphi$ by
statement (9), statement (11), and assumption (13). $\boxtimes\hskip
5.69054pt$

By item 4(a) of Definition 1, the assumption (11) implies that
$w^{\prime\prime}\sim_{\overline{C^{\prime}}}v$. Thus,
$w^{\prime\prime}\sim_{\overline{C}}v$ because
$\overline{C}\subseteq\overline{C^{\prime}}$, see assumption (8). Hence, by
the assumption $C\cap(I\cup A)=\varnothing$ of the lemma,

$w^{\prime\prime}\sim_{A,I}v.$ (14)

At the same time, by item 4 of Definition 2, assumption $w\Vdash{\sf
K}_{C,I}{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf K}_{C,I}\psi)$ of the lemma
and statement (10) imply that

$w^{\prime\prime}\Vdash{\sf K}_{A,I}({\sf K}_{C}\varphi\to{\sf K}_{C,I}\psi).$

Then, by statement (14) and item 4 of Definition 2,

$v\Vdash{\sf K}_{C}\varphi\to{\sf K}_{C,I}\psi.$

Thus, $v\Vdash{\sf K}_{C,I}\psi$ by the earlier Claim, and part 3 of
Definition 2. Therefore, $v^{\prime}\Vdash\psi$ by statement (12) and part 5
of Definition 2. ∎

######  Lemma 16.

$w\nVdash\Box_{C}\bot$.

###### Proof.

Suppose that $w\Vdash\Box_{C}\bot$. Thus, by item 5 of Definition 2, there is
a nonempty coalition $C^{\prime}\subseteq C$ and an operation
$\delta\in\Delta$ such that for any states $w^{\prime},u,u^{\prime}\in W$, if
$w\sim_{C}w^{\prime}$, $(w^{\prime},C^{\prime},\delta,u)\in M$, and
$u\sim_{C}u^{\prime}$, then $u^{\prime}\Vdash\varphi$. In particular,

$\forall u\in W((w,C^{\prime},\delta,u)\in M\Rightarrow u\Vdash\bot).$ (15)

By item 4(b) of Definition 1, there is a state $v\in W$ such that
$(w,C^{\prime},\delta,v)\in M$. Therefore, $v\Vdash\bot$ by statement (15),
which is a contradiction. ∎

######  Lemma 17.

$w\nVdash\Box_{\varnothing}\varphi$.

###### Proof.

The statement of the lemma holds by item 5 of Definition 2 because the empty
set has no nonempty subsets. ∎

######  Lemma 18.

If $w\Vdash\varphi$ for each state $w$ of each clandestine game and coalition
$C$ is nonempty, then $w\Vdash\Box_{C}\varphi$ for each state $w$ of each
clandestine game.

###### Proof.

Consider any state $w$ of a clandestine game. By item 3 of Definition 1, set
$\Delta$, contains at least one element $\delta$.

Towards the proof of $w\Vdash\Box_{C}\varphi$, consider any states
$w^{\prime},u,u^{\prime}\in W$ such that $w\sim_{C}w^{\prime}$,
$(w^{\prime},C,\delta,u)\in M$, and $u\sim_{C}u^{\prime}$. By item 5 of
Definition 2, because set $C$ is nonempty, it suffices to show that
$u^{\prime}\Vdash\varphi$. The latter is true by the assumption of the lemma.
∎

##  Appendix B Auxiliary Lemmas

In this section of the appendix, we prove Lemma 1, Lemma 2, Lemma 3, Lemma 4,
and Lemma 5 stated in the main part of the paper.

######  Lemma 19 (deduction).

If $X,\varphi\vdash\psi$, then $X\vdash\varphi\to\psi$.

###### Proof.

Suppose that sequence $\psi_{1},\dots,\psi_{n}$ is a proof from set
$X\cup\\{\varphi\\}$ and the theorems of our logical system that uses the
Modus Ponens inference rule only. In other words, for each $k\leq n$, either

  1. 1.

$\vdash\psi_{k}$, or

  2. 2.

$\psi_{k}\in X$, or

  3. 3.

$\psi_{k}$ is equal to $\varphi$, or

  4. 4.

there are integers $i,j<k$ such that formula $\psi_{j}$ is equal to
$\psi_{i}\to\psi_{k}$.

It suffices to show that $X\vdash\varphi\to\psi_{k}$ for each $k\leq n$. We
prove this by induction on $k$ through considering the four cases above
separately.

Case I: $\vdash\psi_{k}$. Note that $\psi_{k}\to(\varphi\to\psi_{k})$ is a
propositional tautology, and thus, is an axiom of our logical system. Hence,
$\vdash\varphi\to\psi_{k}$ by the Modus Ponens inference rule. Therefore,
$X\vdash\varphi\to\psi_{k}$.

Case II: $\psi_{k}\in X$. Then, similar to the previous case,
$X\vdash\varphi\to\psi_{k}$.

Case III: formula $\psi_{k}$ is equal to $\varphi$. Thus, $\varphi\to\psi_{k}$
is a propositional tautology. Therefore, $X\vdash\varphi\to\psi_{k}$.

Case IV: formula $\psi_{j}$ is equal to $\psi_{i}\to\psi_{k}$ for some
$i,j<k$. Thus, by the induction hypothesis, $X\vdash\varphi\to\psi_{i}$ and
$X\vdash\varphi\to(\psi_{i}\to\psi_{k})$. Note that formula

$(\varphi\to\psi_{i})\to((\varphi\to(\psi_{i}\to\psi_{k}))\to(\varphi\to\psi_{k}))$

is a propositional tautology. Therefore, $X\vdash\varphi\to\psi_{k}$ by
applying the Modus Ponens inference rule twice. ∎

######  Lemma 1.

If $\varphi_{1},\\!\dots,\\!\varphi_{n}\vdash\psi$, then ${\sf
K}_{a}\varphi_{1},\\!\dots,\\!{\sf K}_{a}\varphi_{n}\vdash{\sf K}_{a}\psi$.

###### Proof.

By Lemma 19 applied $n$ times, the assumption
$\varphi_{1},\dots,\varphi_{n}\vdash\psi$ implies that

$\vdash\varphi_{1}\to(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Thus,

$\vdash{\sf
K}_{a}(\varphi_{1}\to(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots))$

by the Necessitation inference rule. Hence, by the Distributivity axiom and
the Modus Ponens inference rule,

$\vdash{\sf K}_{a}\varphi_{1}\to{\sf
K}_{a}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Then, ${\sf K}_{a}\varphi_{1}\vdash{\sf
K}_{a}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots)$, again by the Modus
Ponens inference rule. Therefore, ${\sf K}_{a}\varphi_{1},\dots,{\sf
K}_{a}\varphi_{n}\vdash{\sf K}_{a}\psi$ by applying the previous steps $(n-1)$
more times. ∎

######  Lemma 2 (positive introspection).

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

###### Proof.

Formula ${\sf K}_{a}\neg{\sf K}_{a}\varphi\to\neg{\sf K}_{a}\varphi$ is an
instance of the Truth axiom. Thus, by contraposition, $\vdash{\sf
K}_{a}\varphi\to\neg{\sf K}_{a}\neg{\sf K}_{a}\varphi$. Hence, taking into
account the following instance of the Negative Introspection axiom: $\neg{\sf
K}_{a}\neg{\sf K}_{a}\varphi\to{\sf K}_{a}\neg{\sf K}_{a}\neg{\sf
K}_{a}\varphi$,

$\vdash{\sf K}_{a}\varphi\to{\sf K}_{a}\neg{\sf K}_{a}\neg{\sf K}_{a}\varphi.$
(16)

At the same time, $\neg{\sf K}_{a}\varphi\to{\sf K}_{a}\neg{\sf K}_{a}\varphi$
is an instance of the Negative Introspection axiom. Thus, $\vdash\neg{\sf
K}_{a}\neg{\sf K}_{a}\varphi\to{\sf K}_{a}\varphi$ by contraposition. Hence,
by the Necessitation inference rule, $\vdash{\sf K}_{a}(\neg{\sf
K}_{a}\neg{\sf K}_{a}\varphi\to{\sf K}_{a}\varphi)$. Thus, by the
Distributivity axiom and the Modus Ponens inference rule, $\vdash{\sf
K}_{a}\neg{\sf K}_{a}\neg{\sf K}_{a}\varphi\to{\sf K}_{a}{\sf K}_{a}\varphi.$
The latter, together with statement (16), implies the statement of the lemma
by propositional reasoning. ∎

Lemma 3 $\vdash{\sf K}_{F}{\sf K}_{E}{\sf K}_{F}\varphi\to{\Box}_{F}\varphi$,
where $F\nsubseteq E$.

###### Proof.

Note that sets $F\setminus E$, $F\cap E$, and $E\setminus F$ are pairwise
disjoint for any sets $E$ and $F$. Then, by the Coalition-Informant-Adversary
axiom, where $C=F\setminus E$, $I=F\cap E$, and $A=E\setminus F$,

$\displaystyle\vdash{\sf K}_{F\setminus E,F\cap E}{\sf K}_{E\setminus F,F\cap
E}({\sf K}_{F\setminus E}\top\to{\sf K}_{F\setminus E,F\cap E}\varphi)$
$\displaystyle\hskip 14.22636pt\to({\Box}_{F\setminus
E}\top\to{\Box}_{F\setminus E,F\cap E}\varphi).$

In other words,

$\displaystyle\vdash{\sf K}_{F}{\sf K}_{E}({\sf K}_{F\setminus E}\top\to{\sf
K}_{F}\varphi)\to({\Box}_{F\setminus E}\top\to{\Box}_{F}\varphi).$ (17)

At the same time, formula ${\sf K}_{F}\varphi\to({\sf K}_{F\setminus
E}\top\to{\sf K}_{F}\varphi)$ is a propositional tautology. Thus, by the
Necessitation inference rule, $\vdash{\sf K}_{E}({\sf K}_{F}\varphi\to({\sf
K}_{F\setminus E}\top\to{\sf K}_{F}\varphi))$. Then, by the Distributivity
axiom and the Modus Ponens inference rule, $\vdash{\sf K}_{E}{\sf
K}_{F}\varphi\to{\sf K}_{E}({\sf K}_{F\setminus E}\top\to{\sf K}_{F}\varphi)$.
Hence, again by the Necessitation inference rule,

$\vdash{\sf K}_{F}({\sf K}_{E}{\sf K}_{F}\varphi\to{\sf K}_{E}({\sf
K}_{F\setminus E}\top\to{\sf K}_{F}\varphi)).$

Thus, by the Distributivity axiom and the Modus Ponens inference rule,
$\vdash{\sf K}_{F}{\sf K}_{E}{\sf K}_{F}\varphi\to{\sf K}_{F}{\sf K}_{E}({\sf
K}_{F\setminus E}\top\to{\sf K}_{F}\varphi).$ Then, $\vdash{\sf K}_{F}{\sf
K}_{E}{\sf K}_{F}\varphi\to({\Box}_{F\setminus E}\top\to{\Box}_{F}\varphi)$ by
the laws of propositional reasoning using statement (17). Finally, note that
assumption $F\nsubseteq E$ implies that set $F\setminus E$ is not empty.
Hence, $\vdash{\Box}_{F\setminus E}\top$ by the Necessitation inference rule.
Therefore, $\vdash{\sf K}_{F}{\sf K}_{E}{\sf
K}_{F}\varphi\to{\Box}_{F}\varphi$ by the laws of propositional reasoning. ∎

Lemma 4 $\vdash{\sf K}_{E}\neg{\sf K}_{F}\varphi\to\neg{\Box}_{F}\varphi$,
where $E\cap F=\varnothing$.

###### Proof.

Assumption $E\cap F=\varnothing$ implies that set $F$ and set
$E\cup\varnothing$ are disjoint. Then, by the Coalition-Informant-Adversary
axiom, where $C=F$, $I=E$, $A=\varnothing$, and $\psi=\bot$,

$\vdash{\sf K}_{F,E}{\sf K}_{E}({\sf K}_{F}\varphi\to{\sf
K}_{F,E}\bot)\to({\Box}_{F}\varphi\to{\Box}_{F,E}\bot).$ (18)

At the same time, the formula $\neg{\sf K}_{F}\varphi\to({\sf
K}_{F}\varphi\to{\sf K}_{F,E}\bot)$ is a tautology. Thus, $\vdash{\sf
K}_{E}(\neg{\sf K}_{F}\varphi\to({\sf K}_{F}\varphi\to{\sf K}_{F,E}\bot))$ by
the Necessitation inference rule. Hence, by the Distributivity axiom and the
Modus Ponens inference rule,

$\vdash{\sf K}_{E}\neg{\sf K}_{F}\varphi\to{\sf K}_{E}({\sf
K}_{F}\varphi\to{\sf K}_{F,E}\bot).$

Then, $\vdash{\sf K}_{E}\neg{\sf K}_{F}\varphi\to{\sf K}_{E}{\sf K}_{E}({\sf
K}_{F}\varphi\to{\sf K}_{F,E}\bot)$ using propositional reasoning and Lemma 2.
Thus, using the Monotonicity axiom and propositional reasoning,

$\vdash{\sf K}_{E}\neg{\sf K}_{F}\varphi\to{\sf K}_{F,E}{\sf K}_{E}({\sf
K}_{F}\varphi\to{\sf K}_{F,E}\bot).$

Hence, $\vdash{\sf K}_{E}\neg{\sf
K}_{F}\varphi\to({\Box}_{F}\varphi\to{\Box}_{F,E}\bot)$ using statement (18)
and propositional reasoning. Finally, note that $\neg{\Box}_{F,E}\bot$ is an
instance of the Nontermination axiom. Therefore, $\vdash{\sf K}_{E}\neg{\sf
K}_{F}\varphi\to\neg{\Box}_{F}\varphi$ by the laws of propositional reasoning.
∎

Lemma 5 $\vdash{\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\to{\sf
K}_{E}\varphi\vee{\sf K}_{F}\psi$, where $E\subseteq F$.

###### Proof.

Note that ${\sf K}_{E}\varphi\vee\psi\to(\neg{\sf K}_{E}\varphi\to\psi)$ is a
propositional tautology. Thus, $\vdash{\sf K}_{F}({\sf
K}_{E}\varphi\vee\psi\to(\neg{\sf K}_{E}\varphi\to\psi))$ by the Necessitation
inference rule. Hence, by the Distributivity axiom and the Modus Ponens
inference rule,

$\vdash{\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\to{\sf K}_{F}(\neg{\sf
K}_{E}\varphi\to\psi).$

Then, ${\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\vdash{\sf K}_{F}(\neg{\sf
K}_{E}\varphi\to\psi)$ by the Modus Ponens inference rule. Thus, by the
Distributivity axiom and the Modus Ponens, ${\sf K}_{F}({\sf
K}_{E}\varphi\vee\psi)\vdash{\sf K}_{F}\neg{\sf K}_{E}\varphi\to{\sf
K}_{F}\psi.$ Hence, ${\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\vdash{\sf
K}_{E}\neg{\sf K}_{E}\varphi\to{\sf K}_{F}\psi$ by the Monotonicity axiom,
assumption $E\subseteq F$, and the laws of propositional reasoning. Then, by
the Negative Introspection axiom and propositional reasoning, ${\sf
K}_{F}({\sf K}_{E}\varphi\vee\psi)\vdash\neg{\sf K}_{E}\varphi\to{\sf
K}_{F}\psi.$ Thus, by propositional reasoning, ${\sf K}_{F}({\sf
K}_{E}\varphi\vee\psi)\vdash{\sf K}_{E}\varphi\vee{\sf K}_{F}\psi.$ Therefore,
$\vdash{\sf K}_{F}({\sf K}_{E}\varphi\vee\psi)\to{\sf K}_{E}\varphi\vee{\sf
K}_{F}\psi$ by the deduction theorem. ∎

##  Appendix C Completeness

Lemma 13 $w\Vdash\varphi$ iff $\varphi\in hd(w)$.

###### Proof.

We prove the statement of the lemma by structural induction on formula
$\varphi$. If $\varphi$ is a propositional variable, then the statement of the
lemma follows from item 1 of Definition 2 and Definition 7. If formula
$\varphi$ is a negation or an implication, then the required follows from
items 2 and 3 of Definition 2 and the maximality and the consistency of the
set $hd(w)$ in the standard way.

Suppose that formula $\varphi$ has the form ${\sf K}_{C}\psi$.

$(\Rightarrow)$: If ${\sf K}_{C}\psi\notin hd(w)$, then, by Lemma 10, there is
a state $u\in W$ such that $w\sim_{C}u$ and $\psi\notin hd(u)$. Thus,
$u\nVdash\psi$ by the induction hypothesis. Therefore, $w\nVdash{\sf
K}_{C}\psi$ by item 4 of Definition 2.

$(\Leftarrow)$: If ${\sf K}_{C}\psi\in hd(w)$, then $\psi\in hd(u)$ for each
state $u\in W$ such that $w\sim_{C}u$ by Lemma 9. Hence, by the induction
hypothesis, $u\Vdash\psi$ for each state $u\in W$ such that $w\sim_{C}u$.
Therefore, $w\Vdash{\sf K}_{C}\psi$ by item 4 of Definition 2.

Assume that formula $\varphi$ has the form ${\Box}_{C}\psi$.

$(\Rightarrow)$: If ${\Box}_{C}\psi\notin hd(w)$, then, by Lemma 12, for any
nonempty coalition $C^{\prime}\subseteq C$ and any action $\delta\in\Delta$,
there are states $w^{\prime},u,u^{\prime}$ such that $w\sim_{C}w^{\prime}$,
$(w^{\prime},C^{\prime},\delta,u)\in M$, $u\sim_{C}u^{\prime}$, and
$\psi\notin hd(u^{\prime})$. Thus, by the induction hypothesis, for any
nonempty coalition $C^{\prime}\subseteq C$ and any action $\delta\in\Delta$,
there are states $w^{\prime},u,u^{\prime}$ such that $w\sim_{C}w^{\prime}$,
$(w^{\prime},C^{\prime},\delta,u)\in M$, $u\sim_{C}u^{\prime}$, and
$u^{\prime}\nVdash\psi$. Therefore, $w\nVdash{\Box}_{C}\psi$ by item 5 of
Definition 2.

$(\Leftarrow)$: Let ${\Box}_{C}\psi\in hd(w)$. Thus, by Lemma 11, for any
three states $w^{\prime},u,u^{\prime}\in W$, if $w\sim_{C}w^{\prime}$,
$(w^{\prime},C,\psi,u)\in M$, and $u\sim_{C}u^{\prime}$, then $\varphi\in
hd(u^{\prime})$. Hence, by the induction hypothesis, for any three states
$w^{\prime},u,u^{\prime}\in W$, if $w\sim_{C}w^{\prime}$,
$(w^{\prime},C,\psi,u)\in M$, and $u\sim_{C}u^{\prime}$, then
$u^{\prime}\Vdash\psi$. Therefore, $w\Vdash{\Box}_{C}\psi$ by item 5 of
Definition 2. ∎