Shhh! The Logic of 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.

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′ . Propositional variable m denotes the statement "Missiles are deployed in Cuba". It is false in state w and true in state w′ . 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′ . In the diagram, the indistinguishability of these two states to Americans is shown using a dashed line.

Although states w and w′ are indistinguishable to Americans, this does not prevent them from discovering the transition from state w to state w′ 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′ 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; ˚Agotnes and Alechina, 2012; Naumov and Tao, 2017; Naumov and Tao, 2018b; Naumov and Tao, 2018a; ˚Agotnes 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 A. By a coalition we mean any (possibly empty) subset of A. For any coalition C, by C we denote the complement of set C with respect to set A.

Definition 1. Let a clandestine game be any such tuple (W, {∼a}a∈A, ∆, M, π) that

1. W is a set of "states".
2. ∼a is an "indistinguishability" equivalence relation on set W for each agent a ∈ A. We write w ∼C u if w ∼a u for each agent a ∈ C.
3. ∆ is a nonempty set of "operations".
4. M is a set of tuples (w,C, δ, u), where w, u ∈ W are states, C ⊆ A is a coalition, and δ ∈ ∆ is an operation. It is assumed that set M, called "mechanism", satisfies the following two conditions
5. (a) concealment: for any two states w, u ∈ W, any coalition of agents C ⊆ A, any operation δ ∈ ∆, if (w, C, δ, u) ∈ M, then w ∼C u,
6. (b) nontermination: for any state w ∈ W, any coalition of agents C ⊆ A, and any operation δ ∈ ∆, there is at least one state u ∈ W such that (w, C, δ, u) ∈ M.
7. π(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′ , 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 δ 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 full version of this paper [Naumov and Orejola, 2023].

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 expost 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 KC and coalition power modality SC was introduced in [ ˚Agotnes and Alechina, 2012]. Using their language, one can write KCSCϕ to state that coalition C knows ex-ante (before the action) that it has a strategy (joint action) to achieve ϕ. Using the same language, one can write SCKCϕ to state that coalition C has a strategy that would result in ϕ being known ex-post to the coalition. The language of [ ˚Agotnes 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, 2019].

Knowing that a strategy exists, as in KCSCϕ, is different from actually knowing the strategy. If a coalition C knows ex-ante what strategy it can use to achieve ϕ, then we say that the coalition has a know-how strategy to achieve ϕ and denote this by HCϕ. Unless the coalition has a perfect recall, knowing ex-ante a strategy to achieve ϕ does not imply knowing ex-ante a strategy that results in knowing ex-post that ϕ is achieved. The latter, however, could be expressed as HCKCϕ. The interplay between coalitional know-how modality HC and distributed knowledge modality KC has been studied in [Naumov and Tao, 2017; Fervari et al., 2017; Naumov and Tao, 2018b; Naumov and Tao, 2018a; ˚Agotnes and Alechina, 2019; Cao and Naumov, 2020].

In epistemic models, knowledge is usually captured by an indistinguishably relation between states. For example, in Figure 2 (left), w1 ⊩ KCSCp. 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 w1, but also in state w2, indistinguishable to the coalition from w1. Note that this is not a know-how strategy because the required strategy in state w1 (strategy δ1) is different from the required strategy in state w2 (strategy δ2). Thus, w1 ⊩ ¬HCp. Note also that in state w1 coalition C does not have a strategy to achieve ex-post knowledge of p. We write this as w1 ⊩ ¬SCKCp. This is true because state u1 is indistinguishable from state u0 where p is not satisfied.

The situation is different in Figure 2 (centre). Here, coalition C has a strategy in state w1 to achieve p, but the coalition does not know this ex-ante because it cannot distinguish state w1 from state w2 where such a strategy does not exist. Using our notations, w1 ⊩ SCp and w1 ⊩ ¬KCSCp. Note, however, that in this setting coalition also has a strategy to achieve expost knowledge of p because p is satisfied not only in state u1 but also in state u0, indistinguishable to C from state u1. We write this as w1 ⊩ SCKCp

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 knowhow logics as HCKCϕ. 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 C of coalition C. Strategy δ depicted in Figure 2 (right) is a clandestine operation of coalition C to achieve p. In this paper, we introduce a new modality □Cϕ to denote an existence of a clandestine operation of coalition C to achieve ϕ. 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 Φ of our logical system is defined by the grammar

where p is a propositional variable and C is a coalition. We read formula KCϕ as "coalition C knows ϕ", and formula □Cϕ as "coalition C knows which clandestine operation it can execute to achieve ϕ". In both cases, the knowledge is distributed. We assume that Boolean constants ⊤ and ⊥ as well as disjunction ∨ are defined in the standard way. We use KC,Dϕ and □C,Dϕ as shorthand for KC∪Dϕ and □C∪Dϕ respectively.

In the definition below, item 5 gives formal semantics of modality □Cϕ, see Figure 3.

Definition 2. For any state w ∈ W of a clandestine game (W, {∼a}a∈A, ∆, M, π) and any formula ϕ ∈ Φ, satisfiability relation w ⊩ ϕ is defined recursively as

1. w ⊩ p if w ∈ π(p),
2. w ⊩ ¬ϕ if w ⊮ ϕ,
3. w ⊩ ϕ→ψ if w ⊮ ϕ or w ⊩ ψ,
4. w ⊩ KCϕ if u ⊩ ϕ for any u ∈ W such that w ∼C u,
5. w ⊩ □Cϕ if there is a nonempty coalition C ′ ⊆ C and an operation δ ∈ ∆ such that for any states w′ , u, u′ ∈ W, if w ∼C w′ , (w′ ,C ′ , δ, u) ∈ M, and u ∼C u′ , then u′ ⊩ ϕ.

☐C
휑

C
휑

In item 5 of the above definition, we introduce coalition C ′ 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 ′ 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 ′ to nonempty coalitions is significant for our results.

Item 5 of Definition 2 is using state w′ to express that the clandestine operation δ not only exists but it is known to coalition C. Note that this knowledge, captured through statement w ∼C w′ , is the knowledge of the whole coalition C, not just its part C ′ 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 CoalitionInformant-Adversary axiom of our logical system.

Formula □Cϕ states that coalition C knows a clandestine operation to achieve ϕ. Because clandestine games are asynchronous, an important question is for how long ϕ 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 ϕ holds at the very moment the operation is completed. To avoid this, in item 5 of Definition 2, we require ϕ to be satisfied not only in the completion state u of the operation δ, but also in all states u′ indistinguishable from state u by coalition C. In other words, statement ϕ remains true until at least one of the members of coalition C takes part in another clandestine operation 1 .

1 If non-concealed operations are added to Definition 1 as described in the previous section, then ϕ 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,

The assumption □Cϕ 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 ϕ is true. The other assumption KI(KCϕ → KCψ) of this principle refers to ex-ante knowledge of a group of informants I. Because the operation is clandestine and C ∩ I = ∅, the ex-ante and ex-post knowledge of I is the same. Thus, statement KCϕ → KCψ will have to be true after the operation. In other words, after the operation coalition, C will know that not only condition ϕ, but also condition ψ is true. Coalition C alone, however, does not know this ex-ante and thus, it alone does not know an operation to achieve condition ψ. Nevertheless, recall that coalition I knows KCϕ → KCψ ex ante. Thus, it knows ex-ante that KCϕ → KCψ 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 ψ. That is, □C,Iψ.

Note that the purpose of modality KI in the assumption KI(KCϕ → KCψ) of principle (1) is to make sure that statement KCϕ → KCψ 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 KI with KA,I still guarantees that statement KCϕ → KCψ 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:

This statement, however, is not true. Assumptions KA,I (KCϕ → KCψ) and □Cϕ can only guarantee that coalition C knows ex ante an operation to achieve ϕ. If this operation is executed, then coalition C ∪ I will know ex-post that ϕ 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:

Finally, note that if instead of preserving KCϕ → KCψ, it is enough just to be able to preserve statement KCϕ → KC,Iψ:

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 Φ, our logical system contains the following axioms:

1. Truth: KCϕ→ϕ,
2. Negative Introspection: ¬KCϕ→KC¬KCϕ,
3. Distributivity: KC(ϕ→ψ) → (KCϕ→KCψ),
4. Monotonicity: KC′ϕ → KCϕ, where C ′ ⊆ C,
5. Strategic Introspection: □Cϕ→KC□Cϕ,
6. Coalition-Informant-Adversary: if C ∩ (I ∪ A) = ∅,
7. then

1. Nontermination: ¬□C⊥,
2. Empty Coalition: ¬□∅ϕ.

We write ⊢ ϕ if a formula ϕ is provable from the above axioms using the Modus Ponens and the two Necessitation inference rules:

We write X ⊢ ϕ if the formula ϕ 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 K.

The next five lemmas are used in the proof of the completeness of our logical system. We give their proofs in [Naumov and Orejola, 2023].

Lemma 2. ⊢ KCϕ→KCKCϕ.

We show the following soundness theorem in [Naumov and Orejola, 2023]

Theorem 1. For any state w of a clandestine game, if w ⊩ χ for each formula χ ∈ X and X ⊢ ϕ, then w ⊩ ϕ.

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 Ka-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 Ka and Kb formulae. They might have different Ka,b-formulae.

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(X0) = (W, {∼a}a∈A,∆,M, π) for an arbitrary maximal consistent set of formulae X0.

Definition 3. Set W consists of all finite sequences X0, C1, . . . , Cn, Xn, such that n ≥ 0 and

1. Xi is a maximal consistent set of formulae for all i > 1,
2. Ci ⊆ A is a coalition for all i ≤ n,

We define a tree structure on the set of states W by saying that state w = X0,C1,X1,C2, . . . ,Cn,Xn and state w :: Cn+1 :: Xn+1 are connected by an undirected edge labeled with all agents in coalition Cn+1. For example, for the tree depicted in Figure 4, state X0, C2, X2 is adjacent to state X0,C2,X2,C8,X8 and the edge between them is labelled with all agents in coalition C8.

Definition 4. For any two states w,w′ ∈ W and any agent a ∈ A, let w ∼a w′ if all edges along the simple path between w and w′ are labelled with agent a.

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

Lemma 6. Relation ∼a is an equivalence relation on set W. Definition 5. Set of operations ∆ is the set of all formulae in language Φ.

Informally, operation ϕ ∈ ∆ is a clandestine operation in the canonical game that achieves ϕ 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 mechanismM is a set of all tuples (w, C, ϕ, u) where w, u ∈ W are states, C ⊆ A is a coalition, and ϕ ∈ Φ is a formula, such that w ∼C u and if □Cϕ ∈ hd(w), then KCϕ ∈ hd(u).

Note that the requirement w ∼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 ⊆ A, and any formula ϕ ∈ Φ, there is a state u ∈ W such that (w, C, ϕ, u) ∈ M.

Proof. We consider the following two cases separately:

Case I: □Cϕ ∈ hd(w). Let

Claim. Set X is consistent.

Proof of Claim. Assume the opposite. Thus, there are formulae KC ψ1,. . . , KC ψn ∈ hd(w) such that ψ1, . . . , ψn ⊢ ¬KCϕ. Hence, KC ψ1, . . . , KC ψn ⊢ KC ¬KCϕ. by Lemma 1. Then, hd(w) ⊢ KC ¬KCϕ by the assumption KC ψ1, . . . , KC ψn ∈ hd(w). Thus, hd(w) ⊢ ¬□Cϕ by Lemma 4 and the Modus Ponens inference rule. Then, □Cϕ /∈ hd(w) because set hd(w) is consistent, which contradicts the assumption of the case. ⊠

Let X′ be any maximal consistent extension of set X and u be the sequence w :: C :: X′ . Then, w ∈ W by Definition 3 as well as the choice of sets X and X′ .

Finally, note that w ∼C u by Definition 4 because u = w :: C :: X′ . Also, KCϕ ∈ X ⊆ X′ = hd(u) by the choice of sets X and X′ and the choice of sequence u. Therefore, (w, C, ϕ, u) ∈ M by Definition 6.

Case II: □Cϕ /∈ hd(w). Take u to be world w. Therefore, (w, C, ϕ, u) ∈ M by Definition 6. This concludes the proof of the lemma.

This concludes the definition of the canonical model M(X0) = (W, {∼a}a∈A, ∆, M, π).

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. KDϕ ∈ Xn iff KDϕ ∈ Xn+1 for any formula ϕ ∈ Φ, any n ≥ 0, and any state X0,C1,X1,C2, . . . ,Xn,Cn+1,Xn+1 ∈ W, and any coalition D ⊆ Cn+1.

Proof. If KDϕ ∈ Xn, then Xn ⊢ KDKDϕ by Lemma 2. Hence, Xn ⊢ KCn+1 KDϕ by the Monotonicity axiom, the assumption D ⊆ Cn+1, and the Modus Ponens inference rule. Thus, KCn+1 KDϕ ∈ Xn by the maximality of set Xn. Therefore, KDϕ ∈ Xn+1 by Definition 3.

Suppose that KDϕ /∈ Xn. Hence, ¬KDϕ ∈ Xn by the maximality of set Xn. Thus, Xn ⊢ KD¬KDϕ by the Negative Introspection axiom and the Modus Ponens inference rule. Hence, Xn ⊢ KCn+1 ¬KDϕ by the Monotonicity axiom, the assumption D ⊆ Cn+1, and the Modus Ponens inference rule. Then, KCn+1 ¬KDϕ ∈ Xn by the maximality of set Xn. Thus, ¬KDϕ ∈ Xn+1 by Definition 3. Therefore, KDϕ /∈ Xn+1 because set Xn+1 is consistent.

Lemma 9. If KCϕ ∈ hd(w) and w ∼C u, then ϕ ∈ hd(u).

Proof. Assumption w ∼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, KCϕ ∈ hd(u) by Lemma 8. Hence, hd(u) ⊢ ϕ by the Truth axiom and the Modus Ponens inference rule. Therefore, ϕ ∈ hd(u) because set hd(u) is maximal.

Lemma 10. If KCϕ /∈ hd(w), then there is u ∈W such that w ∼C u and ϕ /∈ hd(u).

Claim. Set X is consistent.

Proof of Claim. Suppose the opposite. Thus, there are formulae KCψ1, . . . , KCψn ∈ hd(w) such that ψ1, . . . , ψn ⊢ ϕ. Hence, KCψ1, . . . , KCψn ⊢ KCϕ by Lemma 1. Then, hd(w) ⊢ KCϕ by the assumption KCψ1, . . . , KCψn ∈ hd(w). Thus, KCϕ ∈ hd(w) because set hd(w) is maximal, which contradicts the assumption of the lemma. ⊠ Let X′ be any maximal consistent extension of set X and u be the sequence w :: C :: X′ . Then, w ∈ W by Definition 3 as well as the choice of sets X and X′ .

Finally, ¬ϕ ∈ X ⊆ X′ = hd(u) by the choice of sets X and X′ and the choice of sequence u. Therefore, ϕ /∈ hd(u) because set hd(u) is consistent.

Lemma 11. For any formula □Cϕ ∈ hd(w) and any three states w′ , u, u′ ∈ W, if w ∼C w′ , (w′ ,C, ϕ, u) ∈ M, and u ∼C u′ , then ϕ ∈ hd(u′ ).

Proof. Assumption □Cϕ ∈ hd(w) implies that hd(w) ⊢ KC□Cϕ by the Strategic Introspection axiom and the Modus Ponens inference rule. Hence, KC□Cϕ ∈ hd(w) because set hd(w) is maximal. Thus, □Cϕ ∈ hd(w′ ) by Lemma 9 and the assumption w ∼C w′ . Then, KCϕ ∈ hd(u) by Definition 6 and the assumption (w′ ,C, ϕ, u) ∈ M. Therefore, ϕ ∈ hd(u′ ) by Lemma 9 and the assumption u ∼C u′ .

Lemma 12. If □Fϕ /∈ hd(w), then for any nonempty coalition E ⊆ F and any action δ ∈ ∆, there are states w′ , u, u′ such that w ∼F w′ , (w′ ,E, δ, u) ∈ M, u ∼F u′ , and ϕ /∈ hd(u′ ).

In the proof of this lemma located below, we consecutively construct states w′ , u, and u′ . To guarantee that state u′ could be constructed after state u, we construct a state u such that set hd(u) contains formula ¬KFϕ. In this case, by Lemma 10, there must exist a state u′ such that u ∼F u′ , and ϕ /∈ hd(u′ ).

One might think that state u could be constructed from state w′ in a similar fashion by guaranteeing first that set hd(w′ ) contains formula ¬KE KFϕ. However, there is a problem because Definition 6 states that if set hd(w′ ) contains formula □Eδ, then set hd(u), in addition to formula ¬KFϕ, must also contain formula KEδ. Thus, there are two possible ways sets hd(w′ ) and hd(u) could be constructed:

1. Set hd(u) contains ¬KFϕ and KEδ. In this case, set hd(w′ ) must contain formula ¬KE ¬(¬KFϕ ∧ KEδ). The last formula is equivalent to ¬KE (KEδ →KFϕ),
2. Set hd(u) contains only formula ¬KFϕ. In this case, set hd(w′ ) must contain formulae ¬KE KF ϕ and ¬□Eδ.

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

Unfortunately, there is no way to decide upfront which of these two ways could be used to construct a consistent set hd(w′ ). Thus, in the proof below we attempt to concurrently construct both versions of the set hd(w′ ) 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 ∼F w′ . To achieve this, we include in set hd(w′ ) all such formulae ψ that KFψ ∈ hd(w).

In the proof below, the two different attempts to create a set hd(w′ ) are carried out by defining sets X and Y and proving that at least one of them is consistent. Set hd(w′ ) 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:

Claim. Either set X or set Y is consistent.

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

such that

Then, by the Strategic Introspection axiom,

Hence, by Lemma 1,

Thus, by assumption (2),

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

Then, by the Truth axiom and propositional reasoning,

Recall that set E is nonempty by the assumption of the lemma. Thus, there is at least one e ∈ E. Then, e ∈ F by the assumption E ⊆ F of the lemma. Hence, e ∈ F \ E. Thus, F ⊈ E. Then, ⊢ KFKE KFϕ → □Fϕ by Lemma 3. At the same time, hd(w) ⊬ □Fϕ by the assumption □Fϕ /∈ hd(w) of the lemma and the maximality of the set hd(w). Then, hd(w) ⊬ KFKE KFϕ by the contraposition of the Modus Ponens inference rule. Hence, ¬KFKE KFϕ ∈ hd(w) because set hd(w) is maximal. Thus, by propositional reasoning using statement (4),

At the same time, assumption E ⊆ F of the lemma implies that (F \E)∪F = E. Then, E∩((F \E)∪F ) = E∩E = ∅. Hence, the following formula

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

Note that E ∪ (F \ E) = F and F ∪ (F \ E) = E by the assumption E ⊆ F of the lemma. In other words,

Then, hd(w) ⊢ □F ϕ by statement (3) and the Modus Ponens inference rule. Therefore, □Fϕ ∈ hd(w) because set hd(w) is maximal, which contradicts assumption □Fϕ /∈ hd(w) of the lemma. ⊠

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′ be any maximal consistent extension of the set X and let state w′ be the sequence w :: F :: X′ . Note that w ∈ W by Definition 3 and the choice of set X, set X′ , and sequence w′ . Also, w ∼F w′ by Definition 4 and the choice of sequence w′ .

Note that ¬KE (KEδ → KFϕ) ∈ X ⊆ X′ = hd(w′ ) by the choice of set X, set X′ , and sequence w′ . Thus, KE (KEδ → KFϕ) /∈ hd(w′ ) because set hd(w′ ) is consistent. Hence, by Lemma 10, there is a state u ∈ W such that w′ ∼E u and KEδ → KFϕ /∈ hd(u). Then, KEδ ∈ hd(u) and KFϕ /∈ hd(u) because hd(u) is a maximal consistent set. Statements w′ ∼E u and KEδ ∈ hd(u) imply that (w′ , E, δ, u) ∈ M by Definition 6. Statement KFϕ /∈ hd(u) implies that there is a state u′ ∈ W such that u ∼F u′ and ϕ /∈ hd(u′ ) by Lemma 10.

Case II: set Y is consistent. Let Y ′ be any maximal consistent extension of the set Y and let state w′ be the sequence w :: F :: X′ . As in the previous case, w ∈ W by Definition 3 and the choice of set Y , set Y ′ , and sequence w′ . Also, w ∼F w′ by Definition 4 and the choice of w′ .

Note that ¬KE KFϕ ∈ Y ⊆ Y ′ = hd(w′ ) by the choice of set Y , set Y ′ , and sequence w′ . Thus, KE KFϕ /∈ hd(w′ ) as set hd(w′ ) is maximal consistent. Hence, by Lemma 10, there is a state u ∈ W such that

At the same time, ¬□Eδ ∈ Y ⊆ Y ′ = hd(w′ ) by the choice of set Y , set Y ′ , and sequence w′ . Thus, □Eδ /∈ hd(w′ ) because set hd(w′ ) is consistent. Then, (w′ ,E, δ, u) ∈ M by Definition 6 and because w′ ∼E u by statement (6).

Finally, KFϕ /∈ hd(u) by statement (6). Therefore, by Lemma 10, there exists a state u′ ∈ W such that u ∼F u′ and ϕ /∈ hd(u′ ). 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 [Naumov and Orejola, 2023].

Theorem 1. If X ⊬ ϕ, then there is a state w of a clandestine game such that w ⊩ χ for each formula χ ∈ X and w ⊮ ϕ.

Proof. If X ⊬ ϕ, then set X ∪ {¬ϕ} is consistent. Let w be any maximal consistent extension of this set. Then, w ⊩ χ for each formula χ ∈ X and w ⊢ ¬ϕ by Lemma 13. Therefore, w ⊬ ϕ 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 □Cϕ. A natural generalization of our work could be a study of "partially-clandestine" modality □FC ϕ, that stands for "coalition C knows an operation that it can use to achieve ϕ 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 multistep operations is similar to multi-step strategies studied in know-how logics [Fervari et al., 2017; Li and Wang, 2017; Wang, 2018; Wang, 2015].