# AAAI Press Formatting Instructions
for Authors Using LaTeX — A Guide

Junli Jiang,1 Pavel Naumov2

# We Think We Can!: Doxastic Strategies

Junli Jiang,1 Pavel Naumov2

# Doxastic Strategies

Junli Jiang,1 Pavel Naumov2

# Doxastic Strategies and the Triumph of American Technology

Junli Jiang,1 Pavel Naumov2

# The Triumph of American Technology: Doxastic Strategies

Junli Jiang,1 Pavel Naumov2

# Doxastic Coalition Power

Junli Jiang,1 Pavel Naumov2

# Doxastic Coalitional Strategies

Junli Jiang,1 Pavel Naumov2

# The Logic of Doxastic Strategies

Junli Jiang,1 Pavel Naumov2

###### Abstract

In many real-world situations, there is often not enough information to know
that a certain strategy will succeed in achieving the goal, but there is a
good reason to believe that it will. The paper introduces the term “doxastic”
for such strategies.

The main technical contribution is a sound and complete logical system that
describes the interplay between doxastic strategy and belief modalities.

##  1 Introduction

During the 1991 Gulf War, American troops successfully used surface-to-air
Patriot missiles to intercept Iraqi-modified Scud tactical ballistic missiles
originally designed by the Soviet Union in the 1950s. In fact, on 15 February
1991, President George H. W. Bush travelled to the Patriot manufacturing plant
in Andover, Massachusetts to praise the missiles’ capability:

> You see, what has taken place here is a triumph of American technology …we
> are witnessing a revolution in modern warfare, a revolution that will shape
> the way that we defend ourselves for decades to come. For years, we’ve heard
> that antimissile defenses won’t work, that shooting down a ballistic missile
> is impossible – like trying to “hit a bullet with a bullet.” Some people
> called it impossible; you called it your job. They were wrong, and you were
> right …Patriot is 41 for 42: 42 Scuds engaged, 41 intercepted. (Bush 1991)

Just 10 days after this speech, an American radar detected an Iraqi Scud
approaching Dhahran, Saudi Arabia.

Traditionally, knowledge is modelled through an indistinguishability relation
that captures an agent’s own observations. However, modern autonomous agents
often obtain their knowledge from the data that they receive from other
systems. This was the case on 25 February 1991. By analysing the position,
$\vec{x}$, and the velocity, $\vec{v}$, of the Scud, the Patriot concluded
that intercepting the Scud was within its capabilities. We write this as

${\sf K}_{\vec{x},\vec{v}}(\text{``The Patriot has a strategy to destroy the
Scud''})$ (1)

and say that dataset $\\{\vec{x},\vec{v}\\}$ informs the knowledge of the
statement “The Patriot has a strategy to destroy the Scud”. In general, we
write ${\sf K}_{X}\varphi$ if knowing the values of all variables in set $X$
is enough to conclude that statement $\varphi$ is true. We refer to sets of
data variables, like $X$, as datasets. Modality ${\sf K}_{X}$ for a set $X$ of
Boolean variables is introduced by Grossi, Lorini, and Schwarzentruber (2015).
For arbitrary datasets, it is proposed by Baltag and van Benthem (2021). The
name “data-informed knowledge” is suggested by us in (Jiang and Naumov 2022a).
We also proposed a dynamic logic for this modality (Deuser et al. 2024).

Of course, for the Patriot to know that it has a strategy is not the same as
to know what the strategy is. The distinction between “knowing that a strategy
exists” and “knowing what the strategy is”, in the case of the traditional
(indistinguishability-relation-based) knowledge, has been studied in various
logics of know-how strategies (Ågotnes and Alechina 2019; Naumov and Tao 2017;
Fervari et al. 2017; Naumov and Tao 2018c, b, a; Fervari, Velázquez-Quesada,
and Wang 2021; Li and Wang 2021).

In our data-informed setting, in order for the Patriot to know the strategy
(direction in which to launch a surface-to-air missile), it also must know the
exact time, $t$, since the position, $\vec{x}$, and the velocity, $\vec{v}$,
of the Scud has been measured. We write this as

$[\text{Patriot}]_{\vec{x},\vec{v},t}(\text{``Scud is destroyed''})$ (2)

and say that the dataset $\\{\vec{x},\vec{v},t\\}$ informs the strategy of
Patriot to achieve the condition “Scud is destroyed”. In general, we write
$[C]_{X}\varphi$ if knowing the values of all variables in dataset $X$ is
enough to know a strategy for coalition $C$ to achieve condition $\varphi$. We
introduced this modality in (Jiang and Naumov 2022a).

The values in the dataset $\\{\vec{x},\vec{v},t\\}$, obtained from the radar,
gave the Patriot enough information to compute the strategy (direction of
missile launch) that was guaranteed to destroy the Scud. Upon computing the
strategy, the Patriot sent it to the launcher…Seconds later, Scud hit the
barracks of the 14th Quartermaster Detachment of the US Army’s 99th Infantry
Division.

To understand what went wrong that day in the skies above Dhahran, Saudi
Arabia, one needs to acknowledge the fact that data does not always correctly
reflect the state-of-affairs of the real world. Even if the Patriot knows the
“true” values of $\vec{x}$ and $\vec{v}$ as measured by the radar, these
values might not reflect the correct position and velocity of Scud due to, for
example, failure in the radar operation. In the case of our statement (1), it
is perhaps more sensible to say that by analysing the radar-provided values of
$\vec{x}$ and $\vec{v}$ and trusting those values, the Patriot formed a belief
that intercepting the Scud is within its capabilities:

${\sf B}^{\vec{x},\vec{v}}_{\vec{x},\vec{v}}(\text{``The Patriot has a
strategy to destroy the Scud''}).$ (3)

In general, we write ${\sf B}^{T}_{X}\varphi$ if under the assumption of the
trust in dataset $T$, the values of variables in the dataset $X$ inform belief
$\varphi$. We proposed this trust-based belief modality in (Jiang and Naumov
2022b).

As it turns out, the statement ${\sf B}^{\varnothing}_{X}\varphi$ is
equivalent to the statement ${\sf K}_{X}\varphi$. In other words, any belief,
which is not based on trust, is knowledge. Any such belief, of course, is
true. In general, just like the other types of beliefs, trust-based beliefs
are not always true. They might be false if they are based on trust in non-
trustworthy data. This, however, was not the case on 25 February 1991. The
position and the velocity of the Scud communicated by the radar correctly
reflected the physical characteristics of the approaching ballistic missile.
Thus, the Patriot indeed had the capability to intercept the Scud.

As we have just observed, when the trust in data is taken into account, the
knowledge statement (1) becomes a belief statement (3). Of course, a similar
adjustment should be made to statement (2). The Patriot did not actually know
the strategy to destroy the Scud, it only had a belief that a particular
strategy will work. This belief was based on the trust in the dataset
$\\{\vec{x},\vec{v},t\\}$. We write this as:

$[\text{Patriot}]^{\vec{x},\vec{v},t}_{\vec{x},\vec{v},t}(\text{``Scud is
destroyed''}).$ (4)

In general, we write $[C]^{T}_{X}\varphi$ if, under the assumption of trust in
dataset $T$, dataset $X$ informs a belief about some strategy of coalition $C$
that it will achieve condition $\varphi$. We call such strategies “doxastic”
(related to beliefs). Doxastic strategies are guaranteed to work if dataset
$T$ is not only trusted but also trustworthy.

The Patriot system clock stored time (since boot) measured in tenths of a
second. The actual time was computed by multiplying the stored value by $0.1$
using a 24-bit fixed point register. This introduced an error of about
0.000000095 seconds. By the time the Scud appeared in Dhahran, the system had
been running for over 100 hours, creating an accumulated time difference
between the radar’s and the launcher’s clocks of about $0.34$ seconds. A Scud
travels over 500 meters in this time (Mignotte 2010). The strategy that the
Patriot believed would destroy the Scud was based on trusted but non-
trustworthy time data. The “triumph of American technology” pointed the
missile launcher in a completely wrong direction, killing 28 American soldiers
(Mignotte 2010) and wounding close to 100 (Apple 1991). A year later, on 11
November 1992, in Greensburg, Pennsylvania, a memorial was dedicated to the
soldiers killed by the Scud attack. The monument is facing in the direction of
Dhahran, Saudi Arabia (Legion 2017).

In this paper, we introduce formal semantics for doxastic strategies and a
sound and complete logical system that describes the interplay between
modalities ${\sf B}^{T}_{X}$ and $[C]^{T}_{X}$.

The paper is structured as follows. In the next section, we define the class
of games that we use to model multiparty interactions. Next, we define the
syntax and the formal semantics of our logical system. In Section 4, we list
its axioms and inference rules. Section 5 contains the proof of the
completeness. Section 6 discusses ex ante and ex post trust. Section 7
concludes. The proof of soundness and one of the lemmas from Section 5 can be
found in the appendix.

##  2 Games

In this section, we introduce the class of games that is used later to give a
formal semantics of our logical system. Throughout the paper, we assume a
fixed set of atomic propositions and a fixed set of data variables $V$. In
addition, we assume a fixed set of actors $\mathcal{A}$. We use the term
“actor” instead of the more traditional “agent” to emphasise the fact that in
our setting knowledge and beliefs come from data and they are not related to
actors, who are only endowed with an ability to act.

By a dataset we mean any subset of $V$. Informally, given a game, we think
about each data variable as having a value in each state of the game. However,
formally, it is only important to know, for each two given states, if a
variable has the same or different values in those states. Thus, we only need
to associate an indistinguishability relation $\sim_{x}$ with each data
variable $x\in V$. Informally, $w\sim_{x}u$ if data variable $x$ has the same
value in states $w$ and $u$.

To model the trustworthiness of data variables, for each state $w$ of a game
we specify a dataset $\mathcal{T}_{w}\subseteq V$ consisting of the variables
that are trustworthy (but not necessarily trusted) in the state $w$. We
introduced this way to model the trustworthiness of data in (Jiang and Naumov
2022b).

Finally, in the definition below and throughout the paper, by $Y^{X}$ we mean
the set of all functions from set $X$ to set $Y$.

###### Definition 1

A tuple $(W,\\{\sim_{x}\\}_{x\in V},\\{\mathcal{T}_{w}\\}_{w\in
W},\Delta,M,\pi)$ is called a game if

  1. 1.

$W$ is a (possibly empty) set of states,

  2. 2.

$\sim_{x}$ is an indistinguishability equivalence relation on set $W$ for each
data variable $x\in V$,

  3. 3.

$\mathcal{T}_{w}$ the set of data variables that are “trustworthy” in state
$w\in W$,

  4. 4.

$\Delta$ is a nonempty set of “actions”,

  5. 5.

$M\subseteq W\times\Delta^{\mathcal{A}}\times W$ is a “mechanism” of the game,

  6. 6.

$\pi(p)\subseteq W$ for each atomic proposition $p\in P$.

By a complete action profile we mean an arbitrary element of the set
$\Delta^{\mathcal{A}}$. By a coalition we mean an arbitrary subset
$C\subseteq\mathcal{A}$ of actors. By an action profile of a coalition $C$ we
mean an arbitrary element of the set $\Delta^{C}$.

The mechanism of the game $M$ specifies possible transitions of the game from
one state to another. If $(w,\delta,u)\in M$, then under complete action
profile $\delta$ from state $w$ the game can transition to state $u$. Note
that we do not require the mechanism to be deterministic. We also do not
require that for each state $w\in W$ and each complete action profile $\delta$
there is at least one state $u$ such that $(w,\delta,u)\in M$. If such state
$u$ does not exist, then we interpret this as a termination of the game upon
the execution of profile $\delta$ in state $w$.

##  3 Syntax and Semantics

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

$\varphi::=p\;|\;\neg\varphi\;|\;(\varphi\to\varphi)\;|\;{\sf
B}^{T}_{X}\varphi\;|\;[C]^{T}_{X}\varphi,$

where $p$ is an atomic proposition, $C\subseteq\mathcal{A}$ is a coalition,
and $T,X\subseteq V$ are datasets. We read expression ${\sf B}^{T}_{X}\varphi$
as “under the assumption of trust in dataset $T$, dataset $X$ informs belief
$\varphi$”. And we read expression $[C]^{T}_{X}\varphi$ as “under the
assumption of trust in dataset $T$, dataset $X$ informs a doxastic strategy of
coalition $C$ to achieve $\varphi$”.

We write $f=_{C}g$ if $f(x)=g(x)$ for each element $x\in C$ and $w\sim_{X}u$
if $w\sim_{x}u$ for each data variable $x\in X$.

###### Definition 2

For any formula $\varphi\in\Phi$, and any state $w\in W$ of a game
$(W,\\{\sim_{x}\\}_{x\in V},\\{\mathcal{T}_{w}\\}_{w\in W},\Delta,M,\pi)$, the
satisfaction relation $w\Vdash\varphi$ is defined as follows

  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 B}^{T}_{X}\varphi$, if $u\Vdash\varphi$ for each state $u\in W$
such that $w\sim_{X}u$ and $T\subseteq\mathcal{T}_{u}$,

  5. 5.

$w\Vdash[C]^{T}_{X}\varphi$, when there is an action profile $s\in\Delta^{C}$
of coalition $C$ such that for all states $u,v\in W$ and each complete action
profile $\delta\in\Delta^{\mathcal{A}}$, if $w\sim_{X}u$,
$T\subseteq\mathcal{T}_{u}$, $s=_{C}\delta$, $(u,\delta,v)\in M$, and
$T\subseteq\mathcal{T}_{v}$, then $v\Vdash\varphi$.

Note that, by item 4 of the above definition, $w\Vdash{\sf
B}^{\varnothing}_{X}\varphi$ states that condition $\varphi$ is satisfied in
each state $u\in W$ indistinguishible from state $w$ by dataset $X$. Thus,
$B^{\varnothing}_{X}$ is equivalent to data-informed knowledge modality ${\sf
K}_{X}$ discussed in the introduction.

Item 5 above captures our informal intuition that $[C]^{T}_{X}\varphi$ means
that dataset $X$ informs the knowledge of a strategy that guarantees the
achievement of $\varphi$ in states where dataset $T$ is trustworthy. Note that
there are multiple ways to formalise this: we can require $T$ to be
trustworthy in state $u$ (before the transition), in state $v$ (after the
transition), or in both of these states. By including conditions
$T\subseteq\mathcal{T}_{u}$ and $T\subseteq\mathcal{T}_{v}$ in item 5, we
require $T$ to be trustworthy ex ante (before transition) and ex post (after
transition). We discuss an alternative approach in Section 6.

Figure 1: A game. Data variables $\vec{x}$ and $\vec{v}$ are trustworthy in
all states. Data variable $t$ is trustworthy in states $w_{2}$, $w_{3}$,
$w_{4}$.

Figure 1 depicts a (very simplistic) game capturing our introductory game.
This game has a single actor, the Patriot. The actual state is $w_{1}$, in
which data variable $t$ is not trustworthy. The only state which is
$\\{\vec{x},\vec{v},t\\}$-indistinguishable from the current state and in
which all variables in dataset $\\{\vec{x},\vec{v},t\\}$ are trustworthy is
state $w_{2}$. Note that, in state $w_{2}$, strategy $s_{1}$ can be used to
destroy the Scud. Thus, in the current state $w_{1}$, dataset
$\\{\vec{x},\vec{v},t\\}$ informs the belief that the Patriot can use strategy
$s_{1}$ to destroy the Scud. Hence, in this game, formula (4) is satisfied in
state $w_{1}$.

##  4 Axioms

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

  1. 1.

Truth: ${\sf B}^{\varnothing}_{X}\varphi\to\varphi$,

  2. 2.

Negative Introspection: $\neg{\sf B}^{T}_{X}\varphi\to{\sf
B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi$,

  3. 3.

Distributivity: ${\sf B}^{T}_{X}(\varphi\to\psi)\to({\sf
B}^{T}_{X}\varphi\to{\sf B}^{T}_{X}\psi)$,

  4. 4.

Trust: ${\sf B}^{T}_{X}({\sf B}^{T}_{Y}\varphi\to\varphi)$,

  5. 5.

Monotonicity: ${\sf B}^{T}_{X}\varphi\to{\sf
B}^{T^{\prime}}_{X^{\prime}}\varphi$ and
$[C]^{T}_{X}\varphi\to[C^{\prime}]^{T^{\prime}}_{X^{\prime}}\varphi$, where
$T\subseteq T^{\prime}$, $X\subseteq X^{\prime}$, and $C\subseteq C^{\prime}$,

  6. 6.

Cooperation:
$[C]^{T}_{X}(\varphi\\!\to\\!\psi)\to([D]^{T}_{X}\varphi\\!\to\\![C\cup
D]^{T}_{X}\psi)$, where $C\cap D=\varnothing$,

  7. 7.

Strategic Introspection: $[C]^{T}_{X}\varphi\leftrightarrow{\sf
B}^{T}_{X}[C]^{T}_{X}\varphi$,

  8. 8.

Belief in Unavoidability: ${\sf
B}^{T}_{X}[\varnothing]^{T}_{Y}\varphi\to[\varnothing]^{T}_{X}\varphi$,

  9. 9.

Public Belief: ${\sf
B}^{T}_{\varnothing}\varphi\to[\varnothing]^{T}_{\varnothing}\varphi$.

The Truth axiom, the Negative Introspection axiom, the Distributivity axiom,
the Trust axiom and the belief part of the Monotonicity axiom are the axioms
for the trust-based beliefs as stated in (Jiang and Naumov 2022b). The most
non-trivial among them is the Trust axiom. To understand the meaning of this
axiom, note that although the principle ${\sf B}^{T}_{X}\varphi\to\varphi$ is
not universally true, it is true in all states where dataset $T$ is
trustworthy. This observation is captured in the Trust axiom.

The Cooperation axiom is a variation of the axiom from the Logic of Coalition
Power (Pauly 2002). The Strategic Introspection axiom states that dataset $X$
informs a doxastic strategy iff $X$ informs a belief in having a doxastic
strategy. The Strategic Introspection axiom and the Belief in Unavoidability
axiom (which we discuss below) can both be stated in alternative forms where
the superscript of modality ${\sf B}$ is the empty set $\varnothing$.

To understand the meaning of the Belief in Unavoidability axiom, note that
statement $[\varnothing]^{\varnothing}_{X}\varphi$ means that dataset $X$
informs the knowledge that condition $\varphi$ is unavoidably true in the next
state. Similarly, $[\varnothing]^{T}_{X}\varphi$ means that, under the
assumption of trust in dataset $T$, dataset $X$ informs the belief that
condition $\varphi$ is unavoidably true in the next state. The Belief in
Unavoidability axiom states that if $X$ informs the belief that $Y$ informs
the belief in unavoidability of $\varphi$, then $X$ itself informs this belief
in unavoidability of $\varphi$.

Finally, observe that ${\sf B}^{\varnothing}_{\varnothing}\varphi$ means that
statement $\varphi$ is true in all states of the game. In other words,
$\varphi$ is public knowledge in the game. The Public Belief axiom states that
if condition $\varphi$ holds in all words where $T$ is trustworthy, then it is
believed to be unavoidably true in the next state.

We write $\vdash\varphi$ and say that formula $\varphi\in\Phi$ is a theorem of
our system if it is derivable from the above axioms using the Modus Ponens and
the Necessitation inference rules:

$\dfrac{\varphi,\varphi\to\psi}{\psi}\hskip 56.9055pt\dfrac{\varphi}{{\sf
B}^{\varnothing}_{\varnothing}\varphi}.$

In addition to the unary relation $\vdash\varphi$, we also consider a binary
relation $F\vdash\varphi$. We write $F\vdash\varphi$ if formula
$\varphi\in\Phi$ is provable from the set of formulae $F\subseteq\Phi$ and the
theorems of our logical system using only the Modus Ponens inference rule. It
is easy to see that statement $\varnothing\vdash\varphi$ is equivalent to
$\vdash\varphi$. We say that set $F$ is inconsistent if there is a formula
$\varphi\in F$ such that $F\vdash\varphi$ and $F\vdash\neg\varphi$.

The proof of the following theorem is in the appendix.

######  Theorem 1 (soundness)

If $\vdash\varphi$, then $w\Vdash\varphi$ for each state $w$ of an arbitrary
game.

We conclude this section with two auxiliary results that will be used later in
the proof of the completeness. The first of them is a form of the Positive
Introspection principle for our belief modality ${\sf B}$.

###### Lemma 1

$\vdash{\sf B}^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}{\sf
B}^{T}_{X}\varphi$.

  * Proof. Formula ${\sf B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi\to\neg{\sf B}^{T}_{X}\varphi$ is an instance of the Truth axiom. Thus, $\vdash{\sf B}^{T}_{X}\varphi\to\neg{\sf B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi$, by contraposition. Hence, taking into account the following instance $\neg{\sf B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}\neg{\sf B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi$ of the Negative Introspection axiom, we have

$\vdash{\sf B}^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}\neg{\sf
B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi.$ (5)

Also, the formula $\neg{\sf B}^{T}_{X}\varphi\to{\sf
B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi$ is an instance of the Negative
Introspection axiom. Thus, by contraposition, $\vdash\neg{\sf
B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi\to{\sf B}^{T}_{X}\varphi$.
Hence, by the Necessitation inference rule, $\vdash{\sf
B}^{\varnothing}_{\varnothing}(\neg{\sf B}^{\varnothing}_{X}\neg{\sf
B}^{T}_{X}\varphi\to{\sf B}^{T}_{X}\varphi)$. Thus, $\vdash{\sf
B}^{\varnothing}_{X}(\neg{\sf B}^{\varnothing}_{X}\neg{\sf
B}^{T}_{X}\varphi\to{\sf B}^{T}_{X}\varphi)$ by the Monotonicity axiom and the
Modus Ponens inference rule. Thus, by the Distributivity axiom and the Modus
Ponens inference rule it follows that $\vdash{\sf B}^{\varnothing}_{X}\neg{\sf
B}^{\varnothing}_{X}\neg{\sf B}^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}{\sf
B}^{T}_{X}\varphi$. The latter, together with statement (5), implies the
statement of the lemma by propositional reasoning. $\boxtimes\hskip 5.69054pt$

The proof of the following lemma is in the appendix.

###### Lemma 2

If $\varphi_{1},..,\varphi_{n}\vdash\psi$, then ${\sf
B}^{T}_{X}\varphi_{1},..,{\sf B}^{T}_{X}\varphi_{n}\vdash{\sf B}^{T}_{X}\psi$.

##  5 Strong Completeness

The proof of the completeness theorem is split into four subsections. In
Subsection 5.1, we define the canonical game. The truth lemma for the
canonical game and the final step of the proof are given in Subsection 5.4. In
the two subsections before, we state and prove auxiliary lemmas used in the
proof of the truth lemma. A highly non-trivial proof of one of these auxiliary
lemmas is located in the appendix.

###  5.1 Canonical Game

Throughout the rest of the paper, we assume that $\mathcal{B}$ is any set of
cardinality larger than $\mathcal{A}$, such as, for example, the powerset
$\mathcal{P}(\mathcal{A})$. We explain the need for $\mathcal{B}$ after
Definition 3 below.

In this section, towards the proof of completeness, for an arbitrary maximal
consistent set of formulae $F_{0}\subseteq\Phi$ and an arbitrary dataset
$T_{0}\subseteq V$, we define a “canonical” game
$G(T_{0},F_{0})=(W,\\{\sim_{x}\\}_{x\in V},\\{\mathcal{T}_{w}\\}_{w\in
W},\Delta,M,\pi)$.

The set of states in the canonical game is defined using the tree construction
which goes back to the proof of the completeness theorem for epistemic logic
of distributed knowledge (Fagin, Halpern, and Vardi 1992). Informally, in the
tree construction, the states are the nodes of a tree. Formally, the states
are defined first as finite sequences; the tree structure on these sequences
is specified later.

###### Definition 3

$W$ is the set of all sequences $T_{0},F_{0},X_{1}$, $b_{1},T_{1},F_{1}$,
$\dots,X_{n},b_{n},T_{n},F_{n}$ such that $n\geq 0$ and

  1. 1.

$F_{i}\subseteq\Phi$ is a maximal consistent set of formulae for each integer
$i\geq 1$,

  2. 2.

$T_{i},X_{i}\subseteq V$ are datasets for each integer $i\geq 1$,

  3. 3.

$b_{i}\in\mathcal{B}$ for each integer $i\geq 1$,

  4. 4.

$\\{\varphi\;|\;{\sf B}^{\varnothing}_{X_{i}}\varphi\in F_{i-1}\\}\subseteq
F_{i}$ for each integer $i\geq 1$,

  5. 5.

${\sf B}^{T_{i}}_{Y}\psi\to\psi\in F_{i}$ for each dataset $Y\subseteq V$,
each formula $\psi\in\Phi$, and each integer $i\geq 0$.

For any two states $u,w\in W$ of the form

$\displaystyle u$ $\displaystyle\\!\\!=\\!\\!$ $\displaystyle
T_{0},F_{0},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1}$ $\displaystyle w$
$\displaystyle\\!\\!=\\!\\!$ $\displaystyle
T_{0},F_{0},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n},$

we say that the states are adjacent. Note that the adjacency relation forms a
tree structure (undirected graph without cycles) on set $W$. We say that the
edge $(u,w)$ is labelled with each data variable in set $X_{n}$. By $F(w)$ and
$T(w)$ we denote sets $F_{n}$ and $T_{n}$, respectively. Informally, it is
convenient to visualise this tree with the edge marked by the pair
$X_{n},b_{n}$ and node $w$ marked by the pair $T_{n},F_{n}$. Figure 2 depicts
a fragment of such visual representation. In this figure, the node
$T_{0},F_{0},X_{1},b_{1},T_{1},F_{1}$ is adjacent to the node
$T_{0},F_{0},X_{1},b_{1},T_{1},F_{1},X_{3},b_{3},T_{3},F_{3}$. The edge
between them is labelled with each variable in set $X_{3}$.

By clones we call any two nodes

$\displaystyle w_{1}$ $\displaystyle\\!\\!\\!=\\!\\!\\!$ $\displaystyle
T_{0},F_{0},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n}$
$\displaystyle w_{2}$ $\displaystyle\\!\\!\\!=\\!\\!\\!$ $\displaystyle
T_{0},F_{0},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X_{n},b^{\prime}_{n},T_{n},F_{n}$

that differ only by the last $b$-value. For example, in Figure 2, nodes
$T_{0},F_{0},X_{1},b_{1},T_{1},F_{1},X_{3},b_{3},T_{3},F_{3}$ and
$T_{0},F_{0},X_{1}$, $b_{1},T_{1},F_{1},X_{3},b_{6},T_{3},F_{3}$ are clones.
The purpose of set $\mathcal{B}$ in our construction is to guarantee that each
node (except for the root) has more clones than the cardinality of set
$\mathcal{A}$.

Figure 2: Fragment of a canonical tree.

Recall that a simple path in a graph is a path without self-intersections and
that in any tree there is a unique simple path between any two nodes.

###### Definition 4

For any states $w,w^{\prime}\in W$ and any variable $x\in V$, let
$w\sim_{x}w^{\prime}$ if every edge along the unique simple path between nodes
$w$ and $w^{\prime}$ is labelled with variable $x$.

###### Lemma 3

Relation $\sim_{x}$ is an equivalence relation on set $W$ for each data
variable $x\in V$.

As we prove later in Lemma 9, for any state $w\in W$, set $F(w)$ is the set of
all formulae that are satisfied in state $w$ of our canonical model. At the
same time, set $T(w)$ is the set of all data variables that are trustworthy in
state $w$:

###### Definition 5

$\mathcal{T}_{w}=T(w)$ for any state $w\in W$.

The above definition explains the intuition behind item 5 of Definition 3.
Indeed, the item states ${\sf B}^{T(w)}_{Y}\varphi\to\varphi\in F(w)$.
Intuitively, this means that if ${\sf B}^{T(w)}_{Y}\varphi$ is true in a state
$w$, where set $T(w)$ is trustworthy by Definition 5, then statement $\varphi$
must be true in state $w$.

In this paper, as in several other works that extend Marc Pauly’s logic of
coalitional power (Goranko and van Drimmelen 2006; Naumov and Tao 2017;
Goranko and Enqvist 2018), the mechanism of the canonical game is using the
voting construction. In the standard version of this construction, if the goal
of the coalition is to achieve $\varphi$, then all members of the coalition
use action $\varphi$. Informally, this could be interpreted as “voting for
$\varphi$”. In our case, a strategy is informed by a dataset $X$. Thus, for
the strategy to work the coalition should somehow prove that it has access to
the values of dataset $X$ in the current state. To achieve this, we require
each vote to be “signed” by naming a state that belongs to the same
$X$-equivalence class as the current state. Thus, each action consists of a
formula and a state (“signature”). Similar constructions are used in (Naumov
and Tao 2018c; Jiang and Naumov 2022a).

###### Definition 6

$\Delta=\Phi\times W$.

If $d$ is a pair $(x,y)$, then by $pr_{1}(d)$ and $pr_{2}(d)$ we mean elements
$x$ and $y$, respectively.

###### Definition 7

Mechanism $M$ consists of all triples $(w,\delta,v)\in
W\times\Delta^{\mathcal{A}}\times W$ such that for each formula
$[C]^{T}_{X}\varphi\in F(w)$, if

  1. 1.

$pr_{1}(\delta(a))=\varphi$ for each actor $a\in C$ and

  2. 2.

$w\sim_{X}pr_{2}(\delta(a))$ for each actor $a\in C$,

  3. 3.

$T\subseteq\mathcal{T}_{w}$,

  4. 4.

$T\subseteq\mathcal{T}_{v}$,

then $\varphi\in F(v)$.

###### Definition 8

$\pi(p)=\\{w\in W\;|\;p\in F(w)\\}$ for each atomic proposition $p\in P$.

This concludes the definition of the canonical game. As usual, the key step in
the proof of a completeness is a “truth lemma” proven by induction on
structural complexity of a formula. In our case, this is Lemma 9. To improve
readability of the proof of Lemma 9, we separate the non-trivial induction
steps into separate lemmas stated in the next two subsections.

###  5.2 Properties of the belief modality

In this subsection, we state and prove lemmas for modality ${\sf B}$ used in
the induction step of the proof of Lemma 9.

###### Lemma 4

For any formula ${\sf B}^{T}_{Y}\varphi\in\Phi$ and any states

$\displaystyle w^{\prime}$ $\displaystyle=$ $\displaystyle
T_{0},F_{0},\dots,b_{n-1},T_{n-1},F_{n-1},$ $\displaystyle w$ $\displaystyle=$
$\displaystyle
T_{0},F_{0},\dots,b_{n-1},T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n}$

if $Y\subseteq X_{n}$, then ${\sf B}^{T}_{Y}\varphi\in F(w^{\prime})$ iff
${\sf B}^{T}_{Y}\varphi\in F(w)$.

  * Proof. $(\Rightarrow):$ Let ${\sf B}^{T}_{Y}\varphi\in F(w^{\prime})$. Then, ${\sf B}^{T}_{Y}\varphi\in F_{n-1}$. Thus, by Lemma 1 and the Modus Ponens inference rule, $F_{n-1}\vdash{\sf B}^{\varnothing}_{Y}{\sf B}^{T}_{Y}\varphi$. Hence, $F_{n-1}\vdash{\sf B}^{\varnothing}_{X_{n}}{\sf B}^{T}_{Y}\varphi$ by the assumption $Y\subseteq X_{n}$ of the lemma, the Monotonicity axiom, and the Modus Ponens inference rule. Thus, ${\sf B}^{\varnothing}_{X_{n}}{\sf B}^{T}_{Y}\varphi\in F_{n-1}$ because $F_{n-1}$ is a maximal consistent set. Then, ${\sf B}^{T}_{Y}\varphi\in F_{n}$ by item 4 of Definition 3. Therefore, ${\sf B}^{T}_{Y}\varphi\in F(w)$.

$(\Leftarrow):$ Let ${\sf B}^{T}_{Y}\varphi\notin F(w^{\prime})$. Thus, ${\sf
B}^{T}_{Y}\varphi\notin F_{n-1}$. Hence, $\neg{\sf B}^{T}_{Y}\varphi\in
F_{n-1}$ because $F_{n-1}$ is a maximal consistent set of formulae. Then,
$F_{n-1}\vdash{\sf B}^{\varnothing}_{Y}\neg{\sf B}^{T}_{Y}\varphi$ by the
Negative Introspection axiom and the Modus Ponens inference rule. Thus,
$F_{n-1}\vdash{\sf B}^{\varnothing}_{X_{n}}\neg{\sf B}^{T}_{Y}\varphi$ by the
assumption $Y\subseteq X_{n}$ of the lemma, the Monotonicity axiom, and the
Modus Ponens inference rule. Hence, because set $F_{n-1}$ is maximal, ${\sf
B}^{\varnothing}_{X_{n}}\neg{\sf B}^{T}_{Y}\varphi\in F_{n-1}$. Then,
$\neg{\sf B}^{T}_{Y}\varphi\in F_{n}$ by item 4 of Definition 3. Thus, ${\sf
B}^{T}_{Y}\varphi\notin F_{n}$, because set $F_{n}$ is consistent. Therefore,
${\sf B}^{T}_{Y}\varphi\notin F(w)$. $\boxtimes\hskip 5.69054pt$

###### Lemma 5

For any states $w,u\in W$ and any formula ${\sf B}^{T}_{X}\varphi\in F(w)$, if
$w\sim_{X}u$ and $T\subseteq\mathcal{T}_{u}$, then $\varphi\in F(u)$.

  * Proof. By Definition 4, the assumption $w\sim_{X}u$ implies that each edge along the unique path between nodes $w$ and $u$ is labelled with each variable in dataset $X$. Then, the assumption ${\sf B}^{T}_{X}\varphi\in F(w)$ implies ${\sf B}^{T}_{X}\varphi\in F(u)$ by applying Lemma 4 to each edge along this path. Note that the assumption $T\subseteq\mathcal{T}_{u}$ of the lemma implies that $T\subseteq T(u)$ by Definition 5. Hence, $F(u)\vdash{\sf B}^{T(u)}_{X}\varphi$ by the Monotonicity axiom and the Modus Ponens inference rule. Thus, $F(u)\vdash\varphi$ by item 5 of Definition 3 and the Modus Ponens inference rule. Therefore, $\varphi\in F(u)$ because the set $F(u)$ is maximal. $\boxtimes\hskip 5.69054pt$

###### Lemma 6

For any $w\in W$ and any formula ${\sf B}^{T}_{X}\varphi\notin F(w)$, there
exists a state $u\in W$ such that $w\sim_{X}u$, $T=\mathcal{T}_{u}$, and
$\varphi\notin F(u)$.

  * Proof. Consider the set of formulae

$\displaystyle H$ $\displaystyle=$
$\displaystyle\\{\neg\varphi\\}\cup\\{\psi\;|\;{\sf
B}^{\varnothing}_{X}\psi\in F(w)\\}$ (6) $\displaystyle\cup\\{{\sf
B}^{T}_{Y}\chi\to\chi\;|\;Y\subseteq V,\chi\in\Phi\\}.$

###### Claim 1

Set $H$ is consistent.

    * Proof of Claim. Assume the opposite. Hence, there are formulae $\chi_{1},..,\chi_{n}\\!\in\\!\Phi$, datasets $Y_{1},..,Y_{n}\\!\subseteq\\!V$, and formulae

${\sf B}^{\varnothing}_{X}\psi_{1},\dots,{\sf B}^{\varnothing}_{X}\psi_{m}\in
F(w)$ (7)

such that

${\sf B}^{T}_{Y_{1}}\chi_{1}\to\chi_{1},\dots,{\sf
B}^{T}_{Y_{n}}\chi_{n}\to\chi_{n},\psi_{1},\dots,\psi_{m}\vdash\varphi.$

Thus, by Lemma 2,

$\displaystyle{\sf B}^{T}_{X}({\sf
B}^{T}_{Y_{1}}\chi_{1}\to\chi_{1}),\dots,{\sf B}^{T}_{X}({\sf
B}^{T}_{Y_{n}}\chi_{n}\to\chi_{n}),$ $\displaystyle\hskip 85.35826pt{\sf
B}^{T}_{X}\psi_{1},\dots,{\sf B}^{T}_{X}\psi_{m}\vdash{\sf B}^{T}_{X}\varphi.$

Hence, ${\sf B}^{T}_{X}\psi_{1},\dots,{\sf B}^{T}_{X}\psi_{m}\vdash{\sf
B}^{T}_{X}\varphi$ by the Trust axiom applied $n$ times. Then, ${\sf
B}^{\varnothing}_{X}\psi_{1},\dots,{\sf B}^{\varnothing}_{X}\psi_{m}\vdash{\sf
B}^{T}_{X}\varphi$ by the Monotonicity axiom and the Modus Ponens inference
rule applied $m$ times. Thus, $F(w)\vdash{\sf B}^{T}_{X}\varphi$ due to
statement (7). Hence, ${\sf B}^{T}_{X}\varphi\in F(w)$ because the set $F(w)$
is maximal, which contradicts the assumption ${\sf B}^{T}_{X}\varphi\notin
F(w)$ of the lemma. $\boxtimes\hskip 5.69054pt$

Let $H^{\prime}$ be any maximal consistent extension of set $H$ and $b$ be any
element of set $\mathcal{B}$. Suppose that $w=T_{0},F_{0}$, …,
$X_{n},b_{n},T_{n},F_{n}$. Consider sequence

$u=T_{0},F_{0},\dots,X_{n},b_{n},T_{n},F_{n},X,b,T,H^{\prime}.$ (8)

Note that $u\in W$ by Definition 3, equation (6), and the choice of set
$H^{\prime}$ as an extension of set $H$. Also, observe that $w\sim_{X}u$ by
Definition 4 and equation (8). In addition, $T=T(u)=\mathcal{T}_{u}$ by
equation (8) and Definition 5. Finally, $\neg\varphi\in H\subseteq
H^{\prime}=F(u)$ by equation (6), the choice of $H^{\prime}$ as an extension
of $H$, and equation (8). Therefore, $\varphi\notin F(u)$ because the set
$F(u)$ is consistent. This concludes the proof of the lemma. $\boxtimes\hskip
5.69054pt$

###  5.3 Properties of the doxastic strategy modality

We now state lemmas for modality $[C]$ that will be used in the induction step
of the proof of Lemma 9.

###### Lemma 7

For an arbitrary state $w\in W$ and any formula $[C]^{T}_{X}\varphi\in F(w)$
there is an action profile $s\in\Delta^{C}$ such that for all states
$w^{\prime},v\in W$ and each complete action profile
$\delta\in\Delta^{\mathcal{A}}$ if $w\sim_{X}w^{\prime}$, $s=_{C}\delta$,
$T\subseteq\mathcal{T}_{w^{\prime}}$, $T\subseteq\mathcal{T}_{v}$, and
$(w^{\prime},\delta,v)\in M$, then $\varphi\in F(v)$.

  * Proof. Let action profile $s\in\Delta^{C}$ be such that

$s(a)=(\varphi,w)$ (9)

for each actor $a\in C$. Consider any states $w^{\prime},v\in W$ and any
complete action profile $\delta\in\Delta^{\mathcal{A}}$ such that

$\displaystyle w\sim_{X}w^{\prime},$ (10) $\displaystyle
s=_{C}\delta,\;T\subseteq\mathcal{T}_{w^{\prime}},\;T\subseteq\mathcal{T}_{v},\;\mbox{and}\;(w^{\prime},\delta,v)\in
M.$ (11)

It suffices to show that $\varphi\in F(v)$.

The assumption $[C]^{T}_{X}\varphi\in F(w)$ of the lemma implies
$F(w)\vdash{\sf B}^{T}_{X}[C]^{T}_{X}\varphi$ by the Strategic Introspection
axiom and propositional reasoning. Hence, ${\sf
B}^{T}_{X}[C]^{T}_{X}\varphi\in F(w)$ because set $F(w)$ is maximal. Thus,
$[C]^{T}_{X}\varphi\in F(w^{\prime})$ by Lemma 5 and assumption (10) and the
part $T\subseteq\mathcal{T}_{w^{\prime}}$ of assumption (11). Therefore,
$\varphi\in F(v)$ by Definition 7, and assumptions (9) and (11).
$\boxtimes\hskip 5.69054pt$

The proof of the next lemma can be found in the appendix.

###### Lemma 8

For an arbitrary state $w\in W$, any formula $\neg[C]^{T}_{X}\varphi\in F(w)$,
and any action profile $s\in\Delta^{C}$, there are states $w^{\prime},v\in W$
and a complete action profile $\delta\in\Delta^{\mathcal{A}}$ such that
$w\sim_{X}w^{\prime}$, $s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, $(w^{\prime},\delta,v)\in M$, and $\varphi\notin
F(v)$.

###  5.4 Final Steps

We are now ready to prove the truth lemma for our logical system and the
strong completeness of the system.

###### Lemma 9

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

  * Proof. We prove the statement by induction on the complexity of formula $\varphi$. Suppose that formula $\varphi$ is an atomic proposition $p$. Note that $w\Vdash p$ iff $w\in\pi(p)$ by item 1 of Definition 2. At the same time, $w\in\pi(p)$ iff $p\in F(w)$ by Definition 8. Therefore, $w\Vdash p$ iff $p\in F(w)$.

If formula $\varphi$ is a negation or an implication, then the statement of
the lemma follows from the maximality and the consistency of the set $F(w)$,
items 2 and 3 of Definition 2, and the induction hypothesis in the standard
way.

Suppose that formula $\varphi$ has the form ${\sf B}^{T}_{X}\psi$.

$(\Rightarrow):$ Assume that ${\sf B}^{T}_{X}\psi\notin F(w)$. Then, $\neg{\sf
B}^{T}_{X}\psi\in F(w)$ because $F(w)$ is a maximal consistent set of
formulae. Thus, by Lemma 6, there is a state $w^{\prime}\in W$ such that
$w\sim_{X}w^{\prime}$, $T\subseteq\mathcal{T}_{w^{\prime}}$, and $\neg\psi\in
F(w^{\prime})$. Hence, $\psi\notin F(w^{\prime})$ because set $F(w^{\prime})$
is consistent. Then, $w^{\prime}\nVdash\psi$ by the induction hypothesis.
Therefore, $w\nVdash{\sf B}^{T}_{X}\psi$ by item 4 of Definition 2 and
statements $w\sim_{X}w^{\prime}$ and $T\subseteq\mathcal{T}_{w^{\prime}}$.

$(\Leftarrow):$ Assume that ${\sf B}^{T}_{X}\psi\in F(w)$. Consider any state
$w^{\prime}$ such that $w\sim_{X}w^{\prime}$ and
$T\subseteq\mathcal{T}_{w^{\prime}}$. By item 4 of Definition 2, it suffices
to show that $w^{\prime}\Vdash\psi$, which is true by Lemma 5.

Finally, suppose that formula $\varphi$ has the form $[C]^{T}_{X}\psi$.

$(\Rightarrow):$ Assume that $[C]^{T}_{X}\psi\notin F(w)$. Thus,
$\neg[C]^{T}_{X}\psi\in F(w)$ because set $F(w)$ is maximal. Hence, by Lemma
8, for any action profile $s\in\Delta^{C}$, there are states $w^{\prime},v\in
W$ and a complete action profile $\delta\in\Delta^{\mathcal{A}}$ such that
$w\sim_{X}w^{\prime}$, $s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, $(w^{\prime},\delta,v)\in M$, and $\psi\notin
F(v)$. Then, by the induction hypothesis, for any action profile
$s\in\Delta^{C}$, there are states $w^{\prime},v\in W$ and a complete action
profile $\delta\in\Delta^{\mathcal{A}}$ such that $w\sim_{X}w^{\prime}$,
$s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, $(w^{\prime},\delta,v)\in M$, and $v\nVdash\psi$.
Therefore, $w\nVdash[C]^{T}_{X}\psi$ by item 5 of Definition 2.

$(\Leftarrow):$ Assume $[C]^{T}_{X}\psi\in F(w)$. Thus, by Lemma 7, there is
an action profile $s\in\Delta^{C}$ such that for all states $w^{\prime},v\in
W$ and each complete action profile $\delta\in\Delta^{\mathcal{A}}$ if
$w\sim_{X}w^{\prime}$, $s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, and $(w^{\prime},\delta,v)\in M$, then $\psi\in
F(v)$. Hence, by the induction hypothesis, there is an action profile
$s\in\Delta^{C}$ such that for all states $w^{\prime},v\in W$ and each
complete action profile $\delta\in\Delta^{\mathcal{A}}$ if
$w\sim_{X}w^{\prime}$, $s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, and $(w^{\prime},\delta,v)\in M$, then
$v\Vdash\psi$. Therefore, $w\Vdash[C]^{T}_{X}\psi$ by item 5 of Definition 2.
$\boxtimes\hskip 5.69054pt$

######  Theorem 2 (strong completeness)

For any set of formulae $F\subseteq\Phi$ and any formula $\varphi\in\Phi$, if
$F\nvdash\varphi$, then there is a state $w$ of a game such that $w\Vdash f$
for each formula $f\in F$ and $w\nVdash\varphi$.

  * Proof. The assumption $F\nvdash\varphi$ implies that the set $F\cup\\{\neg\varphi\\}$ is consistent. Let $F_{0}$ be any maximal consistent extension of this set. Consider the canonical game $G(\varnothing,F_{0})$.

First, we show that the sequence $\varnothing,F_{0}$ is a state of this
canonical game. By Definition 3, it suffices to show that ${\sf
B}^{\varnothing}_{Y}\psi\to\psi\in F_{0}$ for each dataset $Y\subseteq V$ and
each formula $\psi\in\Phi$. The last statement is true by the Truth axiom and
because set $F_{0}$ is maximal.

Finally, note that $\varphi\notin F_{0}$ because set $F_{0}$ is consistent and
$\neg\varphi\in F_{0}$. Therefore, by Lemma 9 and because $F\subseteq F_{0}$,
it follows that $\varnothing,F_{0}\Vdash f$ for each formula $f\in F$ and also
$\varnothing,F_{0}\nVdash\varphi$. $\boxtimes\hskip 5.69054pt$

##  6 Ex Ante and Ex Post Trust

In item 5 of Definition 2, we require that $T\subseteq\mathcal{T}_{u}$ and
$T\subseteq\mathcal{T}_{v}$. In other words, we apply the assumption of
trustworthiness of dataset $T$ ex ante (before action) and ex post (after
action). In general, one can consider that different datasets, $A$ and $P$,
are required to be trustworthy ex ante and ex post, respectively. That leads
to a more general modality $[C]^{A,P}_{X}\varphi$, defined below:

$w\Vdash[C]^{A,P}_{X}\varphi$, when there is an action profile
$s\in\Delta^{C}$ of coalition $C$ such that for all states $u,v\in W$ and each
complete action profile $\delta\in\Delta^{\mathcal{A}}$ if $w\sim_{X}u$,
$A\subseteq\mathcal{T}_{u}$, $s=_{C}\delta$, $(u,\delta,v)\in M$, and
$P\subseteq\mathcal{T}_{v}$, then $v\Vdash\varphi$.

One might wonder which of the data variables among $\vec{x}$, $\vec{v}$, and
$t$ should be trusted ex ante and which ex post for statement (4) to be true
in our introductory example. Unfortunately, we do not have access to Patriot
code to answer this question, but we suspect that the Patriot missile
constantly adjusts the trajectory based on the current speed and position of
the target. To model such behaviour one would need to use multi-step games
instead of one-shot (strategic) games that we consider in this paper.

To illustrate ex ante and ex post trust, let us consider a different example
where a governing body consisting of 25 members is about to vote on passing a
certain regulation. Suppose that each of them votes yes or no by a paper
ballot. After the vote, the ballots are counted by a tallyman and the number
of yes votes, denoted by $n$, is announced. If $n$ is more than 12, then the
regulation is approved, see Figure 3.

Figure 3: Voting game.

Let us now further assume that a newspaper contacts all 25 members and ask
them how they plan to vote. Suppose that 10 members state that they plan to
support the proposal, 10 members say that they plan to vote against the
proposal, and 5 members are undecided. Alice, Bob, and Cathy are among those 5
who are undecided. It appears that the coalition consisting of the three of
them has a strategy to sway the outcome of the vote either way. If all three
of them vote yes, then the regulation is approved. If they vote no, then it is
rejected. Note, however, that both of these strategies are doxastic: they rely
on the ex ant trust in the newspaper data and on the ex post trust in the
tallyman computing $n$ correctly. Let data variables $yea$ and $nay$ represent
the number of members, according to the newspaper, who plan to vote for and
against, respectively. Note that, in the current world $w$, $yea=nay=10$.
Thus,

$\displaystyle w\Vdash$
$\displaystyle[\text{Alice,Bob,Cathy}]^{\\{yea\\},\\{n\\}}_{\\{yea\\}}\,\text{``Approved''},$
(12) $\displaystyle w\Vdash$
$\displaystyle[\text{Alice,Bob,Cathy}]^{\\{nay\\},\\{n\\}}_{\\{nay\\}}\,\text{``Rejected''}.$

All subscripts and superscripts are important in both formulae above. For
example, if subscript $yea$ is dropped in statement (12), then the statement
is no longer true:

$w\nVdash[\text{Alice,Bob,Cathy}]^{\\{yea\\},\\{n\\}}_{\varnothing}\,\text{``Approved''}.$

This is because, although the doxastic strategy exists, the empty dataset does
not inform its existence.

If $yea$ is removed from the superscript, then the statement is also not true

$w\nVdash[\text{Alice,Bob,Cathy}]^{\varnothing,\\{n\\}}_{\\{yea\\}}\,\text{``Approved''}$

because the newspaper’s information is no longer assumed to be trusted.
Without the ex ante trust in the existence of at least 10 members who are
ready to support the regulation, the coalition consisting of Alice, Bob, and
Cathy does not have a strategy to pass the regulation.

Finally, without the ex post trust that the votes will be counted correctly,
such strategy does not exist either:

$w\nVdash[\text{Alice,Bob,Cathy}]^{\\{yea\\},\varnothing}_{\\{yea\\}}\,\text{``Approved''}.$

Note that formula $[C]^{T,T}_{X}\varphi$ is equivalent to our original
modality $[C]^{T}_{X}\varphi$.

The axioms of our logical system could be modified in a straightforward way
for this more general modality. The most significant change is for the Public
Belief axiom: ${\sf
B}^{T}_{\varnothing}\varphi\to[\varnothing]^{\varnothing,T}_{\varnothing}\varphi$.
Although we did not check the details, we believe that our soundness and
completeness results can be adjusted for this more general modality.

##  7 Conclusion

In this paper, we proposed the notion of doxastic strategies. We gave a sound
and complete logical system for reasoning about such strategies and outlined a
possible extension of this work that separates ex ante and ex post trust.

## Acknowledgment

Junli Jiang acknowledges the support of the Innovation Research 2035 Pilot
Plan of Southwest University (NO. SWUPilotPlan018).

## References

  * Ågotnes and Alechina (2019) Ågotnes, T.; and Alechina, N. 2019.  Coalition Logic with Individual, Distributed and Common Knowledge.  _Journal of Logic and Computation_ , 29: 1041–1069.
  * Apple (1991) Apple, R. W., Jr. 1991.  War in the Gulf: Scud Attack; Scud Missile Hits a U.S. Barracks, Killing 27.  _New York Times_ , February 26th.  https://www.nytimes.com/1991/02/26/world/war-in-the-gulf-scud-attack-scud-missile-hits-a-us-barracks-killing-27.html.
  * Baltag and van Benthem (2021) Baltag, A.; and van Benthem, J. 2021.  A simple logic of functional dependence.  _Journal of Philosophical Logic_ , 50: 1–67.
  * Bush (1991) Bush, G. H. 1991.  Remarks to Raytheon Missile Systems Plant Employees in Andover, Massachusetts.  https://bush41library.tamu.edu/archives/public-papers/2711.  Accessed: 2022-08-20.
  * Deuser et al. (2024) Deuser, K.; Jiang, J.; Naumov, P.; and Zhang, W. 2024.  A Dynamic Logic of Data-Informed Knowledge.  _Journal of Philosophical Logic_.  (to appear).
  * Fagin, Halpern, and Vardi (1992) Fagin, R.; Halpern, J. Y.; and Vardi, M. Y. 1992.  What can machines know? On the properties of knowledge in distributed systems.  _Journal of the ACM (JACM)_ , 39(2): 328–376.
  * Fervari et al. (2017) Fervari, R.; Herzig, A.; Li, Y.; and Wang, Y. 2017.  Strategically knowing how.  In _Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17_ , 1031–1038.
  * Fervari, Velázquez-Quesada, and Wang (2021) Fervari, R.; Velázquez-Quesada, F. R.; and Wang, Y. 2021.  Bisimulations for Knowing How Logics.  _The Review of Symbolic Logic_ , 1–37.
  * Goranko and Enqvist (2018) Goranko, V.; and Enqvist, S. 2018.  Socially Friendly and Group Protecting Coalition Logics.  In _Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems_ , 372–380. International Foundation for Autonomous Agents and Multiagent Systems.
  * Goranko and van Drimmelen (2006) Goranko, V.; and van Drimmelen, G. 2006.  Complete axiomatization and decidability of Alternating-time temporal logic.  _Theoretical Computer Science_ , 353(1): 93 – 117.
  * Grossi, Lorini, and Schwarzentruber (2015) Grossi, D.; Lorini, E.; and Schwarzentruber, F. 2015.  The ceteris paribus structure of logics of game forms.  _Journal of Artificial Intelligence Research_ , 53: 91–126.
  * Jiang and Naumov (2022a) Jiang, J.; and Naumov, P. 2022a.  Data-Informed Knowledge and Strategies.  _Artificial Intelligence_ , 309: 103727.
  * Jiang and Naumov (2022b) Jiang, J.; and Naumov, P. 2022b.  In Data We Trust: The Logic of Trust-Based Beliefs.  In _the 31st International Joint Conference on Artificial Intelligence (IJCAI-22)_.
  * Legion (2017) Legion, T. A. 2017.  14th Quartermaster Detachment Memorial.  https://www.legion.org/memorials/238236/14th-quartermaster-detachment-memorial.  Accessed: 2022-08-20.
  * Li and Wang (2021) Li, Y.; and Wang, Y. 2021.  Planning-based knowing how: A unified approach.  _Artificial Intelligence_ , 103487.
  * Mendelson (2009) Mendelson, E. 2009.  _Introduction to mathematical logic_.  Boca Raton, Florida: CRC press.
  * Mignotte (2010) Mignotte, M. 2010.  The Patriot Missile Failure.  https://www.iro.umontreal.ca/~mignotte/IFT2425/Disasters.html.  Accessed: 2022-08-20.
  * Naumov and Tao (2017) Naumov, P.; and Tao, J. 2017.  Coalition Power in Epistemic Transition Systems.  In _Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS)_ , 723–731.
  * Naumov and Tao (2018a) Naumov, P.; and Tao, J. 2018a.  Second-Order Know-How Strategies.  In _Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS)_ , 390–398.
  * Naumov and Tao (2018b) Naumov, P.; and Tao, J. 2018b.  Strategic Coalitions with Perfect Recall.  In _Proceedings of Thirty-Second AAAI Conference on Artificial Intelligence_.
  * Naumov and Tao (2018c) Naumov, P.; and Tao, J. 2018c.  Together We Know How to Achieve: An Epistemic Logic of Know-How.  _Artificial Intelligence_ , 262: 279 – 300.
  * Pauly (2002) Pauly, M. 2002.  A Modal Logic for Coalitional Power in Games.  _Journal of Logic and Computation_ , 12(1): 149–166.

Technical Appendix

This appendix is not a part of AAAI proceedings.

##  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 is straightforward. Below, we show the soundness of each
of the remaining axioms for an arbitrary game $(W,\\{\sim_{x}\\}_{x\in
V},\\{\mathcal{T}_{w}\\}_{w\in W},\Delta,M,\pi)$ as a separate lemma. We state
the strong soundness for the whole system as Theorem 1 at the end of this
section.

######  Lemma 10 (Trust)

$w\Vdash{\sf B}^{T}_{X}({\sf B}^{T}_{Y}\varphi\to\varphi)$.

  * Proof. Consider any state $u\in W$ such that $w\sim_{X}u$ and $T\subseteq\mathcal{T}_{u}$. By item 4 of Definition 2, it suffices to show that $u\Vdash{\sf B}^{T}_{Y}\varphi\to\varphi$. Suppose that $u\Vdash{\sf B}^{T}_{Y}\varphi$. By item 3 of Definition 2, it is enough to prove that $u\Vdash\varphi$.

Note that $u\sim_{Y}u$ because relation $\sim_{Y}$ is reflexive. Also,
$T\subseteq\mathcal{T}_{u}$ by the choice of world $u$. Then, the assumption
$u\Vdash{\sf B}^{T}_{Y}\varphi$ implies that $u\Vdash\varphi$ by item 4 of
Definition 2. $\boxtimes\hskip 5.69054pt$

######  Lemma 11 (Cooperation)

If $w\Vdash[C]^{T}_{X}(\varphi\to\psi)$, $w\Vdash[D]^{T}_{X}\varphi$, and sets
$C$ and $D$ are disjoint, then $w\Vdash[C\cup D]^{T}_{X}\psi$.

  * Proof. By item 5 of Definition 2, the assumptions $w\Vdash[C]^{T}_{X}(\varphi\to\psi)$ and $w\Vdash[D]^{T}_{X}\varphi$ imply that there are action profiles $s_{1}\in\Delta^{C}$ and $s_{2}\in\Delta^{D}$ such that

$\displaystyle\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(w\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s_{1}=_{C}\delta,$
$\displaystyle\hskip 28.45274pt(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi\to\psi)$ (13)

and

$\displaystyle\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(w\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s_{2}=_{D}\delta,$
$\displaystyle\hskip 28.45274pt(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi)$ (14)

Consider action profile

$s(a)=\begin{cases}s_{1}(a),&\mbox{if }a\in C,\\\ s_{2}(a),&\mbox{if }a\in
D,\\\ \end{cases}$ (15)

of coalition $C\cup D$. Note that profile $s$ is well-defined because sets $C$
and $D$ are disjoint by the assumption of the lemma. Consider any states
$w^{\prime},v\in W$ and any complete action profile
$\delta\in\Delta^{\mathcal{A}}$ such that $w\sim_{X}w^{\prime}$,
$T\subseteq\mathcal{T}_{w^{\prime}}$, $s=_{C\cup D}\delta$,
$(w^{\prime},\delta,v)\in M$, and $T\subseteq\mathcal{T}_{v}$. By item 5 of
Definition 2, it suffices to show that $v\Vdash\psi$.

Assumption $s=_{C\cup D}\delta$ implies that $s_{1}=_{C}\delta$ and
$s_{2}=_{D}\delta$ by equation (15). Thus, $v\Vdash\varphi\to\psi$ and
$v\Vdash\varphi$ by statements (13) and (14) and assumptions
$w\sim_{X}w^{\prime}$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$(w^{\prime},\delta,v)\in M$, and $T\subseteq\mathcal{T}_{v}$. Therefore,
$v\Vdash\psi$ by item 3 of Definition 2. $\boxtimes\hskip 5.69054pt$

######  Lemma 12 (Strategic Introspection)

$w\Vdash[C]^{T}_{X}\varphi$ iff $w\Vdash{\sf B}^{T}_{X}[C]^{T}_{X}\varphi$.

  * Proof. $(\Rightarrow):$ By item 5 of Definition 2, the assumption $w\Vdash[C]^{T}_{X}\varphi$ implies that there is an action profile $s\in\Delta^{C}$ of coalition $C$ such that

$\displaystyle\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(w\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s=_{C}\delta,$
$\displaystyle\hskip 28.45274pt(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$ (16)

Consider any state $u\in W$ such that $w\sim_{X}u$ and
$T\subseteq\mathcal{T}_{u}$. By item 4 of Definition 2, it suffices to show
that $u\Vdash[C]^{T}_{X}\varphi$. Indeed, the assumption $w\sim_{X}u$ and
statement (16) imply that

$\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(u\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s=_{C}\delta,(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$

Therefore, $u\Vdash[C]^{T}_{X}\varphi$ by item 5 of Definition 2.

$(\Leftarrow):$ We consider the following two cases separately:

Case I: There is at least one state $u\in W$ such that
$T\subseteq\mathcal{T}_{u}$ and

$w\sim_{X}u.$ (17)

Hence, by item 4 of Definition 2, the assumption $w\Vdash{\sf
B}^{T}_{X}[C]^{T}_{X}\varphi$ implies that $u\Vdash[C]^{T}_{X}\varphi$. Hence,
by item 5 of Definition 2, there is an action profile $s\in\Delta^{C}$ of
coalition $C$ such that

$\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(u\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s=_{C}\delta,(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$

Thus, by assumption (17),

$\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(w\sim_{X}w^{\prime},T\subseteq\mathcal{T}_{w^{\prime}},s=_{C}\delta,(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$

Therefore, $w\Vdash[C]^{T}_{X}\varphi$ by item 5 of Definition 2.

Case II: There are no states $u\in W$ such that $T\subseteq\mathcal{T}_{u}$
and $w\sim_{X}u$. Thus, $w\Vdash[C]^{T}_{X}\varphi$ by item 5 of Definition 2.
$\boxtimes\hskip 5.69054pt$

######  Lemma 13 (Belief in Unavoidability)

If $w\Vdash{\sf B}^{T}_{X}[\varnothing]^{T}_{Y}\varphi$, then
$w\Vdash[\varnothing]^{T}_{X}\varphi$.

  * Proof. Note that there is only one action profile $s\in\Delta^{\varnothing}$ of the empty coalition. As a function, this action profile consists of the empty set of pairs. We denote this profile by $s_{0}$.

Consider any state $u\in W$ such that $w\sim_{X}u$ and
$T\subseteq\mathcal{T}_{u}$. By item 5 of Definition 2, it suffices to prove
that

$\forall v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(s_{0}=_{\varnothing}\delta,(u,\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$ (18)

Indeed, by item 4 of Definition 2, the assumptions $w\sim_{X}u$ and
$T\subseteq\mathcal{T}_{u}$ and the assumption $w\Vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{Y}\varphi$ of the lemma imply that
$u\Vdash[\varnothing]^{T}_{Y}\varphi$. Hence, by item 5 of Definition 2, there
is an action profile $s_{1}\in\Delta^{\varnothing}$ of the empty coalition
such that

$\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(u\sim_{Y}w^{\prime},s_{1}=_{\varnothing}\delta,(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$

Recall that the action profile of the empty coalition is unique. Thus,
$s_{0}=s_{1}$. Hence,

$\forall w^{\prime},v\in
W\,\forall\delta\in\Delta^{\mathcal{A}}(u\sim_{Y}w^{\prime},s_{0}=_{\varnothing}\delta,(w^{\prime},\delta,v)\in
M,T\subseteq\mathcal{T}_{v}\Rightarrow v\Vdash\varphi).$

The last statement in the case $w^{\prime}=u$ is equivalent to statement (18).
$\boxtimes\hskip 5.69054pt$

######  Lemma 14 (Public Belief)

If $w\Vdash{\sf B}^{T}_{\varnothing}\varphi$, then
$w\Vdash[\varnothing]^{T}_{\varnothing}\varphi$.

  * Proof. To prove $w\Vdash[\varnothing]^{T}_{X}\varphi$, by item 5 of Definition 2, it suffices to show that $v\Vdash\varphi$ for each state $v\in W$ such that $T\subseteq\mathcal{T}_{v}$. Indeed, consider any such state $v\in W$. Note that, vacuously, $w\sim_{\varnothing}v$. Therefore, $v\Vdash\varphi$ by item 4 of Definition 2, the assumption $T\subseteq\mathcal{T}_{v}$, and the assumption $w\Vdash{\sf B}^{T}_{\varnothing}\varphi$ of the lemma. $\boxtimes\hskip 5.69054pt$

The soundness theorem below follows from the lemmas above.

Theorem 1. If $\vdash\varphi$, then $w\Vdash\varphi$ for each state $w$ of an
arbitrary game.

##  Appendix B Auxiliary Lemmas

######  Lemma 15 (deduction)

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

  * Proof. Suppose that sequence $\psi_{1},\dots,\psi_{n}$ is a proof from set $F\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 F$, or

    3. 3.

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

    4. 4.

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

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

Case 1: $\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,
$F\vdash\varphi\to\psi_{k}$.

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

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

Case 4: formula $\psi_{j}$ is equal to $\psi_{i}\to\psi_{k}$ for some $i,j<k$.
Thus, by the induction hypothesis, $F\vdash\varphi\to\psi_{i}$ and
$F\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, $F\vdash\varphi\to\psi_{k}$ by
applying the Modus Ponens inference rule twice. $\boxtimes\hskip 5.69054pt$

######  Lemma 16 (Lindenbaum)

Any consistent set of formulae can be extended to a maximal consistent set of
formulae.

  * Proof. The standard proof of Lindenbaum’s lemma (Mendelson 2009, Proposition 2.14) applies here. $\boxtimes\hskip 5.69054pt$

###### Lemma 17

Inference rule $\dfrac{\varphi}{[\varnothing]^{T}_{X}\varphi}$ is derivable.

  * Proof. Suppose $\vdash\varphi$. Thus, $\vdash{\sf B}^{\varnothing}_{\varnothing}\varphi$ by the Necessitation inference rule. Hence, $\vdash[\varnothing]^{\varnothing}_{\varnothing}\varphi$ by the Public Belief axiom and the Modus Ponens inference rule. Therefore, $\vdash[\varnothing]^{T}_{X}\varphi$ by the Monotonicity axiom and the Modus Ponens inference rule. $\boxtimes\hskip 5.69054pt$

###### Lemma 18

$\vdash[C]^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}[C]^{T}_{X}\varphi$.

  * Proof. The Strategic Introspection axiom, by the laws of propositional reasoning, implies $\vdash{\sf B}^{T}_{X}[C]^{T}_{X}\varphi\to[C]^{T}_{X}\varphi$. Thus, $\vdash{\sf B}^{\varnothing}_{\varnothing}({\sf B}^{T}_{X}[C]^{T}_{X}\varphi\to[C]^{T}_{X}\varphi)$ by the Necessitation inference rule. Hence, $\vdash{\sf B}^{\varnothing}_{X}({\sf B}^{T}_{X}[C]^{T}_{X}\varphi\to[C]^{T}_{X}\varphi)$ by the Monotonicity axiom and the Modus Ponens inference rule. Then, by the Distributivity axiom and the Modus Ponens inference rule,

$\vdash{\sf B}^{\varnothing}_{X}{\sf B}^{T}_{X}[C]^{T}_{X}\varphi\to{\sf
B}^{\varnothing}_{X}[C]^{T}_{X}\varphi.$ (19)

At the same time, by Lemma 1,

$\vdash{\sf B}^{T}_{X}[C]^{T}_{X}\varphi\to{\sf B}^{\varnothing}_{X}{\sf
B}^{T}_{X}[C]^{T}_{X}\varphi.$ (20)

Also, by the Strategic Introspection axiom and propositional reasoning,

$\vdash[C]^{T}_{X}\varphi\to{\sf B}^{T}_{X}[C]^{T}_{X}\varphi.$ (21)

Finally, $\vdash[C]^{T}_{X}\varphi\to{\sf
B}^{\varnothing}_{X}[C]^{T}_{X}\varphi$, by the laws of propositional
reasoning from statements (19), (20), and (21). $\boxtimes\hskip 5.69054pt$

Lemma 2. If $\varphi_{1},\dots,\varphi_{n}\vdash\psi$, then ${\sf
B}^{T}_{X}\varphi_{1},\dots,{\sf B}^{T}_{X}\varphi_{n}\vdash{\sf
B}^{T}_{X}\psi$.

  * Proof. By Lemma 15 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, by the Necessitation inference rule,

$\vdash{\sf
B}^{\varnothing}_{\varnothing}(\varphi_{1}\to(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots)).$

By the Monotonicity axiom and the Modus Ponens inference rule,

$\vdash{\sf
B}^{T}_{X}(\varphi_{1}\to(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots)).$

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

$\vdash{\sf B}^{T}_{X}\varphi_{1}\to{\sf
B}^{T}_{X}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Then, again by the Modus Ponens inference rule,

${\sf B}^{T}_{X}\varphi_{1}\vdash{\sf
B}^{T}_{X}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Thus, ${\sf B}^{T}_{X}\varphi_{1},\dots,{\sf B}^{T}_{X}\varphi_{n}\vdash{\sf
B}^{T}_{X}\psi$ by applying the previous steps $(n-1)$ more times.
$\boxtimes\hskip 5.69054pt$

###### Lemma 19

If $\varphi_{1},\dots,\varphi_{n}\vdash\psi$, then
$[\varnothing]^{T}_{X}\varphi_{1},\dots,[\varnothing]^{T}_{X}\varphi_{n}\vdash[\varnothing]^{T}_{X}\psi$.

  * Proof. By Lemma 15 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, by Lemma 17,

$\vdash[\varnothing]^{T}_{X}(\varphi_{1}\to(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots)).$

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

$\vdash[\varnothing]^{T}_{X}\varphi_{1}\to[\varnothing]^{T}_{X}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Then, by the Modus Ponens inference rule,

$[\varnothing]^{T}_{X}\varphi_{1}\vdash[\varnothing]^{T}_{X}(\varphi_{2}\to\dots(\varphi_{n}\to\psi)\dots).$

Thus, again by the Cooperation axiom and the Modus Ponens inference rule,

$[\varnothing]^{T}_{X}\varphi_{1}\vdash[\varnothing]^{T}_{X}\varphi_{2}\to[\varnothing]^{T}_{X}(\varphi_{3}\to\dots(\varphi_{n}\to\psi)\dots).$

Hence, by the Modus Ponens inference rule,

$[\varnothing]^{T}_{X}\varphi_{1},[\varnothing]^{T}_{X}\varphi_{2}\vdash[\varnothing]^{T}_{X}(\varphi_{3}\to\dots(\varphi_{n}\to\psi)\dots).$

Therefore,
$[\varnothing]^{T}_{X}\varphi_{1},\dots,[\varnothing]^{T}_{X}\varphi_{n}\vdash[\varnothing]^{T}_{X}\psi$
by applying the previous steps $(n-2)$ more times. $\boxtimes\hskip 5.69054pt$

##  Appendix C Proof of Lemma 8

The rest of this appendix contains a highly non-trivial proof of Lemma 8 from
the main part of the paper. For the convenience of the reader, we have divided
this proof into three subsections.

###  C.1 $T$-Harmony

We start the proof with an auxiliary notion of harmony, which has been used in
(Naumov and Tao 2018c; Jiang and Naumov 2022a). Here, we modify this notion
into $T$-harmony.

###### Definition 9

For any dataset $T\subseteq V$, a pair of sets of formulae $(F,G)$ is in
$T$-harmony if $F\nvdash[\varnothing]^{T}_{V}\neg\bigwedge G^{\prime}$ for
each finite set $G^{\prime}\subseteq G$.

###### Lemma 20

If pair of sets of formulae $(F,G)$ is in $T$-harmony, then sets $F$ and $G$
are consistent.

  * Proof. If set $F$ is inconsistent, then $F\vdash\varphi$ for any formula $\varphi\in\Phi$. In particular, $F\vdash[\varnothing]^{T}_{V}\neg\bigwedge\varnothing$. Therefore, the pair $(F,G)$ is not in harmony by Definition 9.

Next, let set $G$ be inconsistent. Thus, by Lemma 15 and propositional
reasoning, $\vdash\neg\bigwedge G^{\prime}$ for some finite set
$G^{\prime}\subseteq G$. Hence, $\vdash[\varnothing]^{T}_{V}\neg\bigwedge
G^{\prime}$ by Lemma 17. Thus, $F\vdash[\varnothing]^{T}_{V}\neg\bigwedge
G^{\prime}$. Therefore, the pair $(F,G)$ is not in harmony by Definition 9.
$\boxtimes\hskip 5.69054pt$

Next, we show that certain initial sets are in $T$-harmony.

###### Lemma 21

For any consistent set $E\subseteq\Phi$, any formula
$\neg[C]^{T}_{X}\varphi\in E$, any family $\\{D_{i}\\}_{i\in I}$ of pairwise
disjoint subsets of $C$, and any set $\\{[D_{i}]^{T}_{X}\psi_{i}\\}_{i\in I}$
of formulae from set $E$, if

$\displaystyle F$ $\displaystyle=$ $\displaystyle\\{\chi\;|\;{\sf
B}^{\varnothing}_{X}\chi\in E\\}\cup\\{{\sf
B}^{T}_{Y}\tau\to\tau\;|\;\tau\in\Phi,Y\subseteq V\\},$ (22) $\displaystyle G$
$\displaystyle=$ $\displaystyle\\{\neg\varphi\\}\cup\\{\psi_{i}\\}_{i\in
I}\cup\\{\sigma\;|\;{\sf B}^{\varnothing}_{\varnothing}\sigma\in E\\}$ (23)
$\displaystyle\cup\\{{\sf B}^{T}_{Z}\eta\to\eta\;|\;\eta\in\Phi,Z\subseteq
V\\},$

then the pair $(F,G)$ is in $T$-harmony.

  * Proof. Suppose that the pair $(F,G)$ is not in $T$-harmony. Thus, by Definition 9, there is a finite set $G^{\prime}\subseteq G$ such that

$F\vdash[\varnothing]^{T}_{V}\neg\bigwedge G^{\prime}.$ (24)

The assumption that set $G^{\prime}$ is finite and equation (23) imply that
there are formulae

${\sf B}^{\varnothing}_{\varnothing}\sigma_{1},\dots\sf
B^{\varnothing}_{\varnothing}\sigma_{m}\in E,$ (25)

formulae

${\sf B}^{T}_{Z_{1}}\eta_{1},\dots,{\sf B}^{T}_{Z_{k}}\eta_{k}\in\Phi,$

and indices $i_{1},\dots,i_{n}\in I$ such that

$\\{\sigma_{i}\\}_{i\leq m},\\{{\sf
B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j}\\}_{j\leq k},\\{\psi_{i_{s}}\\}_{s\leq
n},\neg\varphi\vdash\bigwedge G^{\prime}.$

Thus, by Lemma 15 and the laws of propositional reasoning,

$\neg\bigwedge G^{\prime},\\{\sigma_{i}\\}_{i\leq m},\\{{\sf
B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j}\\}_{j\leq k},\\{\psi_{i_{s}}\\}_{s\leq
n}\vdash\varphi.$

Again by Lemma 15 and the laws of propositional reasoning,

$\neg\bigwedge G^{\prime},\\{\sigma_{i}\\}_{i\leq m},\\{{\sf
B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j}\\}_{j\leq
k}\vdash\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots).$

Thus, by Lemma 19,

$\displaystyle[\varnothing]^{T}_{V}\neg\bigwedge
G^{\prime},\\{[\varnothing]^{T}_{V}\sigma_{i}\\}_{i\leq
m},\\{[\varnothing]^{T}_{V}({\sf B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j})\\}_{j\leq
k}$ $\displaystyle\hskip
85.35826pt\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

By the Monotonicity axiom and the Modus Ponens inference rule applied $m+k$
times,

$\displaystyle[\varnothing]^{T}_{V}\neg\bigwedge
G^{\prime},\\{[\varnothing]^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq
m},\\{[\varnothing]^{T}_{\varnothing}({\sf
B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j})\\}_{j\leq k}$ $\displaystyle\hskip
85.35826pt\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

By the Public Belief axiom and the Modus Ponens inference rule applied $m+k$
times,

$\displaystyle[\varnothing]^{T}_{V}\neg\bigwedge G^{\prime},\\{{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m},\\{{\sf
B}^{T}_{\varnothing}({\sf B}^{T}_{Z_{j}}\eta_{j}\to\eta_{j})\\}_{j\leq k}$
$\displaystyle\hskip
85.35826pt\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

By the Trust axiom,

$\displaystyle[\varnothing]^{T}_{V}\neg\bigwedge G^{\prime},\\{{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq
m}\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Hence, by statement (24),

$\displaystyle F,\\{{\sf B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq
m}\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Thus, by equation (22), there are formulae

${\sf B}^{\varnothing}_{X}\chi_{1},\dots,{\sf B}^{\varnothing}_{X}\chi_{p}\in
E$ (26)

and formulae

${\sf B}^{T}_{Y_{1}}\tau_{1},\dots,{\sf B}^{T}_{Y_{q}}\tau_{q}$

such that

$\displaystyle\\{\chi_{t}\\}_{t\leq p},\\{{\sf
B}^{T}_{Y_{r}}\tau_{r}\to\tau_{r}\\}_{r\leq q},\,\\{{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m}$ $\displaystyle\hskip
42.67912pt\vdash[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Then, by Lemma 2,

$\displaystyle\\{{\sf B}^{T}_{X}\chi_{t}\\}_{t\leq p},\\{{\sf B}^{T}_{X}({\sf
B}^{T}_{Y_{r}}\tau_{r}\to\tau_{r})\\}_{r\leq q},\,\\{{\sf B}^{T}_{X}{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m}$ $\displaystyle\hskip
42.67912pt\vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Thus, by the Trust axiom,

$\displaystyle\\{{\sf B}^{T}_{X}\chi_{t}\\}_{t\leq p},\,\\{{\sf B}^{T}_{X}{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m}\vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Hence, by the Monotonicity axiom and the Modus Ponens inference rule applied
$p+m$ times,

$\displaystyle\\{{\sf B}^{\varnothing}_{X}\chi_{t}\\}_{t\leq p},\,\\{{\sf
B}^{\varnothing}_{\varnothing}{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m}\vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Then, by Lemma 1 and the Modus Ponens inference rule applied $m$ times,

$\displaystyle\\{{\sf B}^{\varnothing}_{X}\chi_{t}\\}_{t\leq p},\,\\{{\sf
B}^{\varnothing}_{\varnothing}\sigma_{i}\\}_{i\leq m}\vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Thus, by statements (25) and (26),

$\displaystyle E\vdash{\sf
B}^{T}_{X}[\varnothing]^{T}_{V}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Hence, by the Belief in Unavoidability axiom and the Modus Ponens inference
rule,

$\displaystyle
E\vdash[\varnothing]^{T}_{X}(\psi_{i_{1}}\to(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Then, by the Cooperation axiom and the Modus Ponens inference rule,

$\displaystyle
E\vdash[D_{i_{1}}]^{T}_{X}\psi_{i_{1}}\to[D_{i_{1}}]^{T}_{X}(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots).$

Thus, by the assumption $[D_{i_{1}}]^{T}_{X}\psi_{i_{1}}\in E$ of the lemma
and the Modus Ponens inference rule,

$\displaystyle
E\vdash[D_{i_{1}}]^{T}_{X}(\psi_{i_{2}}\to\dots(\psi_{i_{n}}\to\varphi)\dots).$

Hence, by the Cooperation axiom, the Modus Ponens inference rule, and the
assumption of the lemma that family $\\{D_{i}\\}_{i\in I}$ consists of
pairwise disjoint sets,

$\displaystyle E\vdash[D_{i_{2}}]^{T}_{X}\psi_{i_{2}}\to[D_{i_{1}}\cup
D_{i_{2}}]^{T}_{X}(\psi_{i_{3}}\to\dots(\psi_{i_{n}}\to\varphi)\dots).$

Then, by the assumption $[D_{i_{2}}]^{T}_{X}\psi_{i_{2}}\in E$ of the lemma
and the Modus Ponens inference rule,

$\displaystyle E\vdash[D_{i_{1}}\cup
D_{i_{2}}]^{T}_{X}(\psi_{i_{3}}\to\dots(\psi_{i_{n}}\to\varphi)\dots)).$

Thus, by repeating the last step $n-2$ more times,

$\displaystyle E\vdash[D_{i_{1}}\cup\dots\cup D_{i_{n}}]^{T}_{X}\varphi.$

Hence, $E\vdash[C]^{T}_{X}\varphi$ by the Monotonicity axiom, the Modus Ponens
inference rule, and the assumption of the lemma that family $\\{D_{i}\\}_{i\in
I}$ are subsets of $C$. Then, $\neg[C]^{T}_{X}\varphi\notin E$ because set $E$
is consistent, which contradicts the assumption $\neg[C]^{T}_{X}\varphi\in E$
of the lemma. $\boxtimes\hskip 5.69054pt$

The next lemma shows that any pair in harmony can be extended.

###### Lemma 22

For any pair of sets of formulae $(F,G)$ in $T$-harmony, any formula
$[\varnothing]^{T}_{X}\varphi\in\Phi$, either the pair
$(F\cup\\{\neg[\varnothing]^{T}_{X}\varphi\\},G)$ or the pair
$(F,G\cup\\{\varphi\\})$ is in $T$-harmony.

  * Proof. Suppose that neither the pair $(F\cup\\{\neg[\varnothing]^{T}_{X}\varphi\\},G)$ nor the pair $(F,G\cup\\{\varphi\\})$ is in $T$-harmony. Thus, by Definition 9,

$\displaystyle
F,\neg[\varnothing]^{T}_{X}\varphi\vdash[\varnothing]^{T}_{V}\neg\bigwedge
G_{1},$ (27) $\displaystyle F\vdash[\varnothing]^{T}_{V}\neg\bigwedge G_{2},$
(28)

for some finite sets $G_{1}\subseteq G$ and $G_{2}\subseteq
G\cup\\{\varphi\\}$. Then, there must exist a finite set of formulae
$G^{\prime}\subseteq G$ such that,

$\displaystyle\vdash\bigwedge G^{\prime}\to\bigwedge G_{1},$
$\displaystyle\vdash\varphi\to\left(\bigwedge G^{\prime}\to\bigwedge
G_{2}\right).$

Hence, by the laws of propositional reasoning,

$\displaystyle\vdash\neg\bigwedge G_{1}\to\neg\bigwedge G^{\prime},$
$\displaystyle\vdash\neg\bigwedge G_{2}\to\left(\varphi\to\neg\bigwedge
G^{\prime}\right).$

Thus, by Lemma 17,

$\displaystyle\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G_{1}\to\neg\bigwedge G^{\prime}\right),$
$\displaystyle\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G_{2}\to\left(\varphi\to\neg\bigwedge G^{\prime}\right)\right).$

Then, by the Cooperation axiom and the Modus Ponens inference rule,

$\displaystyle\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G_{1}\right)\to[\varnothing]^{T}_{V}\left(\neg\bigwedge G^{\prime}\right),$
$\displaystyle\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G_{2}\right)\to[\varnothing]^{T}_{V}\left(\varphi\to\neg\bigwedge
G^{\prime}\right).$

Hence, by assumptions (27) and (28) and the Modus Ponens inference rule,

$\displaystyle
F,\neg[\varnothing]^{T}_{X}\varphi\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right),$ $\displaystyle
F\vdash[\varnothing]^{T}_{V}\left(\varphi\to\neg\bigwedge G^{\prime}\right).$

Hence, by the contraposition of the Monotonicity axiom,

$\displaystyle
F,\neg[\varnothing]^{T}_{V}\varphi\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right),$ $\displaystyle
F\vdash[\varnothing]^{T}_{V}\left(\varphi\to\neg\bigwedge G^{\prime}\right).$

Then, by the Cooperation axiom and the Modus Ponens inference rule,

$\displaystyle
F,\neg[\varnothing]^{T}_{V}\varphi\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right),$ $\displaystyle
F\vdash[\varnothing]^{T}_{V}\varphi\to[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right).$

Hence, by Lemma 15,

$\displaystyle
F\vdash\neg[\varnothing]^{T}_{V}\varphi\to[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right),$ $\displaystyle
F\vdash[\varnothing]^{T}_{V}\varphi\to[\varnothing]^{T}_{V}\left(\neg\bigwedge
G^{\prime}\right).$

Then, by the laws of propositional reasoning,

$F\vdash[\varnothing]^{T}_{V}\left(\neg\bigwedge G^{\prime}\right).$

Therefore, by Definition 9 and the assumption $G^{\prime}\subseteq G$, the
pair $(F,G)$ is not in $T$-harmony, which contradicts the assumption of the
lemma that it is in $T$-harmony. $\boxtimes\hskip 5.69054pt$

###### Definition 10

A pair of sets of formulae $(F,G)$ is in complete $T$-harmony if this pair is
in $T$-harmony and, for any formula $[\varnothing]^{T}_{X}\varphi\in\Phi$,
either $\neg[\varnothing]^{T}_{X}\varphi\in F$ or $\varphi\in G$.

The next lemma follows from Lemma 22 and Definition 10.

###### Lemma 23

For any pair $(F,G)$ in $T$-harmony, there is a pair $(F^{\prime},G^{\prime})$
in complete $T$-harmony such that $F\subseteq F^{\prime}$, $G\subseteq
G^{\prime}$. $\boxtimes\hskip 5.69054pt$

###  C.2 Cones

###### Definition 11

For any state $w\in W$, let $Cone(w)$ be the set of all states $u\in W$ such
that either $w=u$ or sequence $w$ is a prefix of sequence $u$.

Figure 4: States $w$, $u$, and $v$ belong to $Cone(w)$.

We call set $Cone(w)$ the cone of a state $w\in W$. Informally, $Cone(w)$ is a
subtree of the canonical tree that starts at node $w$, see Figure 4. The next
two lemmas state an auxiliary property of cones used later.

###### Lemma 24

$Cone(w)\cap Cone(w^{\prime})=\varnothing$ for any two states $w,w^{\prime}\in
W$ such that

$\displaystyle w$ $\displaystyle=$ $\displaystyle
T_{0},F_{0},X_{1},b_{1},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n},$
$\displaystyle w^{\prime}$ $\displaystyle=$ $\displaystyle
T_{0},F_{0},X_{1},b_{1},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X^{\prime}_{n},b^{\prime}_{n},T^{\prime}_{n},F^{\prime}_{n},$

and
$(X_{n},b_{n},T_{n},F_{n})\neq(X^{\prime}_{n},b^{\prime}_{n},T^{\prime}_{n},F^{\prime}_{n})$.

###### Lemma 25

For any states $w,u\in W$ and any data variable $y\in V$, if

$w=T_{0},F_{0},X_{1},b_{1},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n}\in
W,$

$u\notin Cone(w)$, and $w\sim_{y}u$, then $y\in X_{n}$.

  * Proof. Let $w_{0}=T_{0},F_{0},X_{1},b_{1},\dots,X_{n-1},b_{n-1},T_{n-1},F_{n-1}$. Consider simple path between vertices $w$ and $u$. The assumption $u\notin Cone(w)$ of the lemma implies that this path must contain edge $(w_{0},w)$. Hence, by the assumption $w\sim_{y}u$ of the lemma and Definition 4, edge $(w_{0},w)$ is labeled with variable $y$. Hence, $y\in X_{n}$. $\boxtimes\hskip 5.69054pt$

###  C.3 Final Steps

###### Lemma 26

For any set $A$ and any pairwise disjoint family of sets $\\{R_{b}\\}_{b\in
B}$, if the cardinality of set $A$ is less than the cardinality of set $B$,
then there is an index $b\in B$ such that $A\cap R_{b}=\varnothing$.
$\boxtimes\hskip 5.69054pt$

We are now ready to finish the proof of Lemma 8.

Lemma 8 For an arbitrary state $w\in W$, any formula
$\neg[C]^{T}_{X}\varphi\in F(w)$, and any action profile $s\in\Delta^{C}$,
there are states $w^{\prime},v\in W$ and a complete action profile
$\delta\in\Delta^{\mathcal{A}}$ such that $w\sim_{X}w^{\prime}$,
$s=_{C}\delta$, $T\subseteq\mathcal{T}_{w^{\prime}}$,
$T\subseteq\mathcal{T}_{v}$, $(w^{\prime},\delta,v)\in M$, and $\varphi\notin
F(v)$.

  * Proof. Consider any state $w\in W$, any formula $\neg[C]^{T}_{X}\varphi\in F(w)$, and any action profile $s\in\Delta^{C}$. For each formula $\psi\in\Phi$, define coalition

$D_{\psi}=\\{a\in C\;|\;pr_{1}(s(a))=\psi\\}.$ (29)

###### Claim 2

$\\{D_{\psi}\\}_{\psi\in\Phi}$ is a family of pairwise disjoint subsets of
$C$.

    * Proof of Claim. By equation (29), set $D_{\psi}$ is a subset of $C$ for each formula $\psi\in\Phi$. To show that sets $\\{D_{\psi}\\}_{\psi\in\Phi}$ are disjoint, suppose that there is an actor $a\in C$ such that $a\in D_{\psi_{1}}\cap D_{\psi_{2}}$ for some formulae $\psi_{1},\psi_{2}\in\Phi$. Therefore, $\psi_{1}=pr_{1}(s(a))=\psi_{2}$ by equation (29). $\boxtimes\hskip 5.69054pt$

Consider the set of formulae

$\Psi=\\{\psi\in\Phi\;|\;[D_{\psi}]^{T}_{X}\psi\in F(w)\\}.$ (30)

Next, we are going to apply Lemma 21. Note that $F(w)$ is a consistent subset
of $\Phi$ and that $\neg[C]^{T}_{X}\varphi\in F(w)$ by the assumption of the
lemma. Also, observe that
$\\{D_{\psi}\\}_{\psi\in\Psi}\subseteq\\{D_{\psi}\\}_{\psi\in\Phi}$ is a
family of pairwise disjoint subsets of $C$ by Claim 2. Finally, note that
$\\{[D_{\psi}]^{T}_{X}\psi\\}_{\psi\in\Psi}\subseteq F(w)$ by equation (30).
Therefore, by Lemma 21, the pair $(F,G)$ is in $T$-harmony, where

$\displaystyle F$ $\displaystyle=$ $\displaystyle\\{\chi\;|\;{\sf
B}^{\varnothing}_{X}\chi\in F(w)\\}\cup\\{{\sf
B}^{T}_{Y}\tau\to\tau\;|\;\tau\in\Phi,Y\subseteq V\\},$ (31) $\displaystyle G$
$\displaystyle=$ $\displaystyle\\{\neg\varphi\\}\cup\Psi\cup\\{\sigma\;|\;{\sf
B}^{\varnothing}_{\varnothing}\sigma\in F(w)\\}$ (32)
$\displaystyle\cup\\{{\sf B}^{T}_{Z}\eta\to\eta\;|\;\eta\in\Phi,Z\subseteq
V\\}.$

Then, by Lemma 23, there is a pair $(F^{\prime},G^{\prime})$ in complete
$T$-harmony such that $F\subseteq F^{\prime}$ and $G\subseteq G^{\prime}$.
Hence, by Definition 10, pair $(F^{\prime},G^{\prime})$ in $T$-harmony. Thus,
by Lemma 20, sets $F^{\prime}$ and $G^{\prime}$ are consistent. Then, by Lemma
16, sets $F^{\prime}$ and $G^{\prime}$ can be further extended to maximal
consistent sets of formulae $F^{\prime\prime}$ and $G^{\prime\prime}$,
respectively, such that

$F\subseteq F^{\prime}\subseteq
F^{\prime\prime}\;\;\;\mbox{and}\;\;\;G\subseteq G^{\prime}\subseteq
G^{\prime\prime}.$ (33)

Let state $w\in W$ be the sequence
$T_{0},F_{0},X_{1},b_{1},\dots,X_{n},b_{n},T_{n},F_{n}$. For each
$b\in\mathcal{B}$, define sequence,

$w_{b}=T_{0},F_{0},X_{1},b_{1},\dots,X_{n},b_{n},T_{n},F_{n},X,b,T,F^{\prime\prime}.$
(34)

Recall that we previously referred to such nodes as “clones”.

###### Claim 3

$w_{b}\in W$, $w\sim_{X}w_{b}$, and $T=\mathcal{T}_{w_{b}}$ for each
$b\in\mathcal{B}$.

    * Proof of Claim. By Definition 3 and the assumption $w\in W$ of the lemma, to show that $w_{b}\in W$, it suffices to show that $\\{\chi\;|\;{\sf B}^{\varnothing}_{X}\chi\in F_{n}\\}\subseteq F^{\prime\prime}$ and $\\{{\sf B}^{T}_{Y}\tau\to\tau\;|\;Y\subseteq V,\tau\in F_{n}\\}\subseteq F^{\prime\prime}$. Both of these statements are true by equation (31), part $F\subseteq F^{\prime\prime}$ of statement (33), and because $F(w)=F_{n}$. Statement $T=\mathcal{T}_{w_{b}}$ follows from Definition 5 and equation (34). Finally, note that $w\sim_{X}w_{b}$ for each $b\in\mathcal{B}$ by Definition 4 and equation (34). $\boxtimes\hskip 5.69054pt$

To continue the proof of the lemma, recall that set $\mathcal{B}$ has been
assumed to have larger cardinality than set $\mathcal{A}$. Thus, because
$C\subseteq\mathcal{A}$,

$|\\{pr_{2}(s(a))\;|\;a\in
C\\}|\leq|C|\leq|\mathcal{A}|<|\mathcal{B}|=|\\{Cone(w_{b})\;|\;b\in\mathcal{B}\\}|.$

Note that sets $\\{Cone(w_{b})\;|\;b\in\mathcal{B}\\}$ are pairwise disjoint
by Lemma 24. Hence, by Lemma 26, there must exist at least one element
$\beta\in\mathcal{B}$ such that

$\\{pr_{2}(s(a))\;|\;a\in C\\}\cap Cone(w_{\beta})=\varnothing.$ (35)

Let

$w^{\prime}=w_{\beta}.$ (36)

Choose an arbitrary element $\beta^{\prime}\in\mathcal{B}$ and define state
$v$ as follows, see Figure 5,

$v=T_{0},F_{0},X_{1},b_{1},\dots,T_{n-1},F_{n-1},X_{n},b_{n},T_{n},F_{n},\varnothing,\beta^{\prime},T,G^{\prime\prime}.$
(37)

###### Claim 4

$v\in W$.

  * Proof of Claim. By Definition 3 and the assumption $w\in W$ of the lemma, it suffices to show that $\\{\sigma\;|\;{\sf B}^{\varnothing}_{\varnothing}\sigma\in F_{n}\\}\cup\\{{\sf B}^{T}_{Z}\eta\to\eta\;|\;\eta\in\Phi,Z\subseteq V\\}\subseteq G^{\prime\prime}$. The latter is true by equation (32), part $G\subseteq G^{\prime\prime}$ of statement (33), and because $F(w)=F_{n}$. $\boxtimes\hskip 5.69054pt$

Figure 5: Towards the proof of Lemma 8.

Recall that we started the proof of the lemma by fixing a state $w\in W$ and
an action profile $s\in\Delta^{C}$ of coalition $C$. Define complete action
profile $\delta\in\Delta^{\mathcal{A}}$ as follows:

$\delta(a)=\begin{cases}s(a),&\mbox{if }a\in C,\\\
(\top,w),&\mbox{otherwise}.\end{cases}$ (38)

Note

$s=_{C}\delta.$ (39)

###### Claim 5

$(w^{\prime},\delta,v)\in M$.

  * Proof of Claim. Consider any formula

$[D]^{Q}_{Y}\psi\in F(w^{\prime})$ (40)

such that

$\forall a\in D\,(pr_{1}(\delta(a))=\psi),$ (41) $\forall a\in
D\,(w^{\prime}\sim_{Y}pr_{2}(\delta(a))),$ (42)
$Q\subseteq\mathcal{T}_{w^{\prime}},$ (43)

and

$Q\subseteq\mathcal{T}_{v}.$ (44)

By Definition 7, it suffices to show that $\psi\in F(v)$. Indeed, first, note
that

$Q\subseteq\mathcal{T}_{w^{\prime}}=\mathcal{T}_{w_{\beta}}=T$ (45)

by statement (43), equation (36), and Claim 3. Next, we consider the following
three cases separately:

Case I: $D=\varnothing$. Assumption (40) implies that
$[\varnothing]^{Q}_{Y}\psi\in F(w_{\beta})$ by equation (36). Hence,
$F(w_{\beta})\vdash[\varnothing]^{T}_{Y}\psi$ by statement (45) and the
Monotonicity axiom. Thus, $\neg[\varnothing]^{T}_{Y}\psi\notin F(w_{\beta})$
because set $F(w_{\beta})$ is consistent. Hence,
$\neg[\varnothing]^{T}_{Y}\psi\notin F^{\prime\prime}$ by equation (34). Then,
$\neg[\varnothing]^{T}_{Y}\psi\notin F^{\prime}$ by part $F^{\prime}\subseteq
F^{\prime\prime}$ of statement (33). Thus, $\psi\in G^{\prime}$ by the
assumption that the pair $(F^{\prime},G^{\prime})$ is in complete $T$-harmony
and Definition 10. Hence, $\psi\in G^{\prime\prime}$ by part
$G^{\prime}\subseteq G^{\prime\prime}$ of statement (33). Therefore, $\psi\in
F(v)$ by equation (37).

Case II: there exists an actor $a\in D\setminus C$. Then, $\delta(a)=(\top,w)$
by equation (38). Hence, $pr_{1}(\delta(a))=\top$. Thus, $\psi=\top$ by
equation (41). Therefore, $\psi\in F(v)$ because $F(v)$ is a maximal
consistent set of formulae.

Case III: $\varnothing\neq D\subseteq C$. We further split this case into two
subcases:

> Subcase IIIa: $Y\subseteq X$. Note that $pr_{1}(s(a))=pr_{1}(\delta(a))$ for
> each actor $a\in D$ by equation (38) and the assumption $D\subseteq C$ of
> Case III. Thus, $pr_{1}(s(a))=\psi$ for each actor $a\in D$ by statement
> (41). Hence, $D\subseteq D_{\psi}$ by equation (29). Then, by assumption
> (40), the assumption $Y\subseteq X$ of the subcase, statement (45), the
> Monotonicity axiom, and the Modus Ponens inference rule,
>
> $F(w^{\prime})\vdash[D_{\psi}]^{T}_{X}\psi.$ (46)
>
> Thus, $F(w^{\prime})\vdash{\sf B}^{\varnothing}_{X}[D_{\psi}]^{T}_{X}\psi$
> by Lemma 18 and the Modus Ponens inference rule. Hence,
>
> ${\sf B}^{\varnothing}_{X}[D_{\psi}]^{T}_{X}\psi\in F(w^{\prime}),$ (47)
>
> because set $F(w^{\prime})$ is maximal. Note that $w\sim_{X}w_{\beta}$ by
> Claim 3. Then, $w\sim_{X}w^{\prime}$ by equation (36). Thus,
> $[D_{\psi}]^{T}_{X}\psi\in F(w)$ by statement (47) and Lemma 5. Hence,
> $\psi\in\Psi$ by equation (30). Then, $\psi\in G$ by equation (32). Thus,
> $\psi\in G^{\prime\prime}$ by equation (33). Therefore, $\psi\in F(v)$ by
> equation (37).
>
> Subcase IIIb: there is a data variable $y\in Y\setminus X$. The assumption
> $\varnothing\neq D$ of Case III implies that there is an actor $a\in D$.
> Then, by the assumption $D\subseteq C$ of Case III,
>
> $a\in C.$ (48)
>
> Also, the assumption $a\in D$ implies $w^{\prime}\sim_{y}pr_{2}(\delta(a))$
> by statement (42) and the assumption $y\in Y$ of Subcase IIIb. Thus,
> $w^{\prime}\sim_{y}pr_{2}(s(a))$ by equation (38) and statement (48). Hence,
> by equation (36),
>
> $w_{\beta}\sim_{y}pr_{2}(s(a)).$ (49)
>
> At the same time, $pr_{2}(s(a))\notin Cone(w_{\beta})$ by equation (35) and
> statement (48). Therefore, $y\in X$ by Lemma 25, statement (49), and
> equation (34), which contradicts the assumption $y\in Y\setminus X$ of
> Subcase IIIb.

This concludes the proof of the claim $(w^{\prime},\delta,v)\in M$.
$\boxtimes\hskip 5.69054pt$

Thus, towards the proof of the lemma, we constructed state $w^{\prime}\in W$
(equation (36) and Claim 3), state $v\in W$ (Claim 4) and a complete action
profile $\delta\in\Delta^{\mathcal{A}}$ such that $w\sim_{X}w^{\prime}$
(equations (34) and (36)), $s=_{C}\delta$ (equation (39)),
$T\subseteq\mathcal{T}_{w^{\prime}}$ (equation (36) and Claim 3),
$T\subseteq\mathcal{T}_{v}$ (equation (37)), and $(w^{\prime},\delta,v)\in M$
(Claim 5). To finish the proof of the lemma, note that $\neg\varphi\in
G\subseteq G^{\prime\prime}=F(v)$ by equation (32), equation (33), and
equation (37) respectively. $\boxtimes\hskip 5.69054pt$