# Knowledge-wh and False Belief Sensitivity:
A Logical Study (An Extended Abstract)

Yuanzhe Yang Department of Philosophy and Religious Studies
Peking University
Beijing, China<EMAIL_ADDRESS>
###### Abstract

In epistemic logic, a way to deal with knowledge-wh is to interpret them as a
kind of mention-some knowledge (MS-knowledge). But philosophers and linguists
have challenged both the sufficiency and necessity of such an account: some
argue that knowledge-wh has, in addition to MS-knowledge, also a sensitivity
to false belief (FS); others argue that knowledge-wh might only imply mention-
some true belief (MS-true belief). In this paper, we offer a logical study for
all these different accounts. We apply the technique of bundled operators, and
introduce four different bundled operators -
$[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi:=\exists x(\mathsf{[B]}\phi\wedge\phi)$,
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi:=\exists
x(\mathsf{[B]}\phi\wedge\phi)\wedge\forall x(\mathsf{[B]}\phi\to\phi)$,
$[\mathsf{K}^{\mathtt{MS}}]^{x}\phi:=\exists x\mathsf{[K]}\phi$ and
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi:=\exists
x\mathsf{[K]}\phi\wedge\forall x(\mathsf{[B]}\phi\to\phi)$ -, which
characterize the notions of MS-true belief, MS-true belief with FS, MS-
knowledge and MS-knowledge with FS respectively. We axiomatize the four logics
which take the above operators (as well as $\mathsf{[K]}$) as primitive
modalities on the class of $S4.2$-constant-domain models, and compare the
patterns of reasoning in the obtained logics, in order to show how the four
accounts of knowledge-wh differ from each other, as well as what they have in
common.

##  1 Introduction

In standard epistemic logic, for the most time, we deal with _propositional
knowledge_ (or knowledge-_that_): that is, an agent knows _that_ $\phi$, where
$\phi$ is a certain proposition. However, this clearly does not exhaust our
daily use of the notion of “knowledge”. Besides knowledge-that, we also
frequently talk about various kinds of _knowledge-wh_ : for example, I know
_how_ to ride a bike, I know _who_ proved the incompleteness theorems, I know
_when_ a certain meeting is held, I know _where_ to buy a certain book, I know
_what_ is the password of my computer, I know _why_ a certain event happens,
etc.

Thus, besides standard propositional knowledge, knowledge-wh also seems to be
an interesting subject for epistemic logic to study. There are already a
number of logical studies of various kinds of knowledge-wh (e.g. know whether
in [4], know why in [25], know how in [20],[5], [12], [13] and [23], just to
name a few), and a more general framework for logics of knowledge-wh is also
proposed in [21]. In this paper, following [21], we will also focus mainly on
the general logical structures shared by various kinds of knowledge-wh.

As suggested in [21] (following the philosophical stance of the so-called
“intellectualism” initiated in [18]), in many cases, knowledge-wh can be
interpreted as a kind of _mention-some knowledge_ (MS-knowledge for short):
for example, I know how to prove a theorem, iff _there exists_ some proof such
that I know that this proof is a proof for the theorem; I know where to buy
newspapers, iff _there exists_ some place where I know I can buy newspapers,
etc. Then, in such cases, it seems that the logical structure of knowledge-wh
can be formally captured by the first-order modal formula $\exists
x\mathsf{[K]}\phi(x)$.111 However, as it is also noted in [21], in some other
situations, it seems more natural to interpret knowledge-wh in terms of
mention-_all_ , rather than mention-_some_ , knowledge. For example, when I
say “I know who came to the meeting yesterday”, it may mean that I know _all_
the people who came to that meeting, which should probably be formalized as,
for example, $\forall x(\phi(x)\to\mathsf{[K]}\phi(x))$ or $\forall
x(\mathsf{[K]}\phi(x)\vee\mathsf{[K]}\neg\phi(x))$. We will not deal with the
mention-all reading of knowledge-wh in this paper, since the behavior of
mention-all knowledge is rather different from mention-some knowledge, and it
thus seems better to study it independently elsewhere. In fact, axiomatization
of mention-all knowledge in terms of $\forall
x(\mathsf{[K]}\phi(x)\vee\mathsf{[K]}\neg\phi(x))$ has been studied in [26],
an unpublished undergraduate thesis.

However, while it is quite clear that in many situations, knowledge-wh does
involve some kind of mention-some structure, it is not as clear whether MS-
knowledge really is the right account for knowledge-wh in these situations. In
fact, both the sufficiency and necessity of such an account are challenged.

For example, as it is argued in [6], [15], [8] and [24], knowledge-wh may not
only involve mention-some knowledge, but also involve _false belief
sensitivity_ (FS for short). Let’s consider the following scenario, adapted
from one offered in [6], to illustrate this point.

###### Example 1.1

There are two stores, Newstopia and Paperworld. Newstopia sells newspapers,
while Paperworld sells only stationery. Now, Alice _knows_ that Newstopia
sells newspapers, but also _believes_ erroneously that Paperworld sells
newspapers.

In such a scenario, it is natural to judge that that Alice does not know where
to buy newspapers (psychological experiments conducted in [15] also show that
such an intuition is shared by many people): even though she has a MS-
knowledge concerning where to buy newspapers, it seems that her false belief
that Paperworld sells newspapers would corrupt her knowledge-where.

Hence, maybe knowledge-wh should be sensitive to false belief: that is, even
under an MS-reading, maybe MS-knowledge should not be characterized by
$\exists x\mathsf{[K]}\phi(x)$ alone, but should rather be characterized by
$\exists x\mathsf{[K]}\phi(x)\wedge\forall x(\mathsf{[B]}\phi(x)\to\phi(x))$.

On the other hand, the necessity of the MS-knowledge account is also doubted.
For example, as it is argued in [2], it seems that knowledge-wh is subject to
a kind of _epistemic luck_ which is not consistent with propositional
knowledge. Let’s consider the following scenario, adapted from one offered in
[2], to illustrate this point.

###### Example 1.2

Suppose that Bob believes that $w$ is a way to change light bulbs, and $w$ is
indeed a reliable way to do so. His belief is obtained by reading an
instruction in a book. However, unknown to him, all other contents in the book
are erroneous, and it is merely due to a very rare print error that the
instruction he read is correct.

In this case, Bob’s true belief that $w$ is a way to change light bulbs is too
lucky to be counted as his _knowledge_ ; but nevertheless, it still seems
natural to judge that Bob knows how to change light bulbs.

Then, it seems that sometimes a mention-some true belief (MS-true belief for
short), i.e. $\exists x(\mathsf{[B]}\phi(x)\wedge\phi(x))$, is enough for
knowledge-wh. (In philosophical discussions, such a stance is sometimes called
“revisionary intellectualism”, which is first proposed in [3], in contrast to
intellectualism.)

Of course, none of the arguments presented above is decisive. But they do
reveal an enormous complexity in the question concerning the nature of
knowledge-wh. Hitherto, no consensus concerning this question is reached in
philosophical discussions, and nor will we offer a determinate answer here. On
the contrary, in this paper, we will study _all_ the accounts mentioned above
in a formal way.

In order to do so, we apply the technique of “bundled operators”222 For a
detailed introduction of such an idea, see [21] and [22]. . The general idea
is that we pack a complex first-order modal formula (e.g. $\exists
x\mathsf{[K]}\phi(x)\wedge\forall x(\mathsf{[B]}\phi(x)\to\phi(x))$) into the
semantics of a single operator, and study the logic which takes such an
“bundled operator” as primitive modality. By working in such languages with
limited expressivity, we can focus on the behavior of the epistemic notion in
which we are really interested, without being distracted by irrelevant notions
which can also be expressed in a stronger language. Moreover, with the help of
bundled operators, we can study the complex notions in a compact manner.

In this paper, then, we will study the following four different bundled
operators:333 The bundled operator $[\mathsf{K}^{\mathtt{MS}}]^{x}$ is first
introduced in [21] (the notation used there is $\Box^{x}$, though); later,
further study concerning its decidability and complexity is presented in [14],
and axiomatization in [19]. The result presented in this paper concerning this
operator (namely, the axiomatization on $S4.2$), however, is new. On the other
hand, $[\mathsf{tB}^{\mathtt{MS}}]$,
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]$ and
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]$ are all novel bundled operators
that have not yet been studied in literature.

$[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi(x)$ | $:=$ | $\exists x(\mathsf{[B]}\phi(x)\wedge\phi(x))$
---|---|---
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi(x)$ | $:=$ | $\exists x(\mathsf{[B]}\phi(x)\wedge\phi(x))\wedge\forall x(\mathsf{[B]}\phi(x)\to\phi(x))$
$[\mathsf{K}^{\mathtt{MS}}]^{x}\phi(x)$ | $:=$ | $\exists x\mathsf{[K]}\phi(x)$
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi(x)$ | $:=$ |  $\exists x\mathsf{[K]}\phi(x)\wedge\forall x(\mathsf{[B]}\phi(x)\to\phi(x))$.

We will axiomatize the logics which take these operators plus an operator for
propositional knowledge as primitive modalities on the class of $S4.2$-models,
a class of models which characterizes knowledge, belief and their interactions
in a reasonable way. Completeness results will also be presented. Moreover, we
will compare the obtained logics, in order to show the differences and
commonalities in the ways we reason about knowledge-wh, propositional
knowledge and belief, which are logically implied by the different accounts of
knowledge-wh.

##  2 First-order $S4.2$-models

First, we introduce the models we use to characterize knowledge and belief on
the semantic level.

Since first-order quantifiers are involved in the notions of MS-knowledge, MS-
true belief and FS, we will use _first-order Kripke models_ as the semantic
basis. We fix a set of predicates $\mathcal{P}$. A first-order Kripke model,
then, is defined as follow:444 In this paper, we will not introduce function
symbols and constants to our language. Hence, we will also not consider
functions and constants in the following definition.

###### Definition 2.1

A _first-order Kripke model_ is a $4$-tuple $\mathcal{M}=(W,D,R,\rho)$, where

  * •

$W\neq\emptyset$ is the set of epistemically possible worlds of the model;

  * •

$D\neq\emptyset$ is the domain of the model;

  * •

$R\subseteq W^{2}$ is the accessibility relation among the possible worlds,
which characterizes epistemic indistinguishability;

  * •

$\rho:\mathcal{P}\times W\to\wp(D^{<\omega})$ assigns each $n$-ary predicate
an $n$-ary relation on each possible world.

(We may abbreviate the term “first-order Kripke model” simply as “model” in
the following discussions.)

Note that such a model can be interpreted rather freely on the conceptual
level, so that it can characterize various kinds of knowledge-wh. For example,
if we want to characterize the knowledge-how of an agent, then the elements in
$D$ can be interpreted as different methods or devices available for the agent
in question, and a predicate $P\in\mathcal{P}$ can be interpreted as a certain
goal, while $a\in\rho(P,w)$ reads “at the epistemically possible world $w$,
$a$ is a way to achieve $P$”. Similarly, if we want to characterize knowledge-
where, then the elements in $D$ can be interpreted as different locations
accessible for the agent, while predicates in $\mathcal{P}$ are interpreted as
properties of these locations. Of course, in a similar fashion, different
models can also be used to characterize knowledge-who, knowledge-when or
knowledge-what.

Also note that we only consider _constant-domain_ models here: all possible
worlds in a model share the same domain. This is mainly in order to avoid
technical and conceptual complexities, and we believe this is indeed a
reasonable (though inevitably idealized) assumption.

Of course, since we use first-order Kripke models to characterize the
epistemic states of an agent, the Kripkean part of such models should also
possess certain frame properties.

It is a popular choice to use $S5$-models to characterize an agent’s
knowledge, but we will not use such models in this paper. This is mainly
because we need to deal with both knowledge and belief, as well as the
interactions between them (moreover, in our discussion, the notion of belief
should be interpreted in a rather strong sense, so we would prefer interaction
principles like $\mathsf{[B]}\phi\to\mathsf{[B]}\mathsf{[K]}\phi$ to hold),
and we must also allow the possibility for false belief, in order for the
notion of FS to make any sense at all. This, however, seems to be a difficult
task when knowledge is characterized by $S5$-models.

Hence, we will use _$S4.2$ -models_ instead - that is, models which are
reflexive, transitive and strongly convergent.555 Here, we use the notion of
_strong_ convergence to define $S4.2$-models; but elsewhere, when defining
$S4.2$-models, the notion of _weak_ convergence might be used instead (A frame
$(W,R)$ is _weakly_ convergent, iff for all $w,v,v^{\prime}\in W$ s.t. $wRv$
and $wRv^{\prime}$, there is some $u\in W$ s.t. $vRu$ and $v^{\prime}Ru$).
Standard modal logic cannot distinguish these two kinds of models (as noted in
[17]), but some of the languages studied in this paper are strong enough to
distinguish them. We choose the stronger notion of convergence here, because
it seems more favorable both technically and conceptually. This is also in
accordance with Stalnaker’s note in [17].  The formal definition is as follow:

###### Definition 2.2

A frame $(W,R)$ is _strongly convergent_ , iff for all $w\in W$, there is some
$u\in W$ s.t. for all $v\in W$, if $wRv$, then $vRu$.

A model based on a reflexive, transitive and strongly convergent frame is
called an $S4.2$-model.

We find such models attractive, because the class of $S4.2$-models validates
the logic of knowledge $\mathbf{S4.2}$, in which belief can be reasonably
_defined_ in terms of knowledge by the definition
$\mathsf{[B]}\phi:=\langle\mathsf{K}\rangle\mathsf{[K]}\phi$ (as explained in
[10], the underlying idea is that, if one knows that she does not know
something, then she would not believe it; and if she does not believe
something, then she would know by introspection that she does not know it).
Moreover, the logic for the belief defined in this way is $\mathbf{KD45}$, and
we also have many intuitive interaction principles between knowledge and
belief (e.g. $\mathsf{[K]}\phi\to\mathsf{[B]}\phi$,
$\mathsf{[B]}\phi\to\mathsf{[K]}\mathsf{[B]}\phi$,
$\neg\mathsf{[B]}\phi\to\mathsf{[K]}\neg\mathsf{[B]}\phi$,
$\mathsf{[B]}\phi\to\mathsf{[B]}\mathsf{[K]}\phi$). (It is Lenzen who first
proposed $\mathbf{S4.2}$ as a logic for knowledge in [10] and [11], from a
syntatic perspective. Later, Stalnaker also studied $\mathbf{S4.2}$ from a
more semantic perspective in [17].)

Moreover, as it is noted by Stalnaker in [17], in an $S4.2$-frame $(W,R)$, we
can define the following relation $R_{\mathsf{B}}$, which corresponds to the
notion of belief defined in terms of knowledge:

###### Definition 2.3

Given a frame $(W,R)$, $R_{\mathsf{B}}\subseteq W^{2}$ is the relation which
satisfies that for all $w,u\in W$, $wR_{\mathsf{B}}u$ iff for all $v\in W$
s.t. $wRv$, $vRu$.

It is not hard to check that if $(W,R)$ is an $S4.2$-frame, then
$(W,R_{\mathsf{B}})$ is $KD45$. Moreover, after we formally introduce the
languages and their semantics, it will be easy to check that $R_{\mathsf{B}}$
corresponds to $\mathsf{[B]}$ in exactly the way $R$ corresponds to
$\mathsf{[K]}$.

##  3 Languages and semantics

Now, we introduce the languages for the bundled operators, as well as their
exact semantics.

We first fix a set of variables $\mathbf{X}$. Then, for any
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
the corresponding language $\mathcal{L}([\mathsf{K}_{\mathtt{wh}}])$ (and also
$\mathcal{L}_{\approx}([\mathsf{K}_{\mathtt{wh}}])$) is defined as follow:

###### Definition 3.1

$\mathcal{L}([\mathsf{K}_{\mathtt{wh}}])$-formulas are defined recursively as
follow:

$\phi::=P(y_{1},...,y_{n})\mid\neg\phi\mid\phi\wedge\phi\mid\mathsf{[K]}\phi\mid[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$

where $P\in\mathcal{P}$, $n\geq 0$ and $x,y_{1},...,y_{n}\in\mathbf{X}$.

$\neg\mathsf{[K]}\neg\phi$ is denoted as $\langle\mathsf{K}\rangle\phi$;
$\mathsf{[B]}\phi$ is an abbreviation for
$\langle\mathsf{K}\rangle\mathsf{[K]}\phi$.

$\vee$, $\to$ and $\leftrightarrow$ are defined in the usual way.

Moreover, let $\mathcal{L}_{\approx}([\mathsf{K}_{\mathtt{wh}}])$ be the
language obtained by further adding an identity relation $\approx$ to
$\mathcal{L}([\mathsf{K}_{\mathtt{wh}}])$.666 In the following discussions, we
will be working in the language $\mathcal{L}([\mathsf{K}_{\mathtt{wh}}])$ when
we do not specifically mention the language in which we are working. We will
make it clear whenever we switch our working language to
$\mathcal{L}_{\approx}([\mathsf{K}_{\mathtt{wh}}])$.

Corresponding to our definition of the bundled operators, we define the
semantics for the above languages recursively as follow:

###### Definition 3.2

Given a model $\mathcal{M}=(W,D,R,\rho)$, a $w\in W$ and an assignment
$\sigma$ from $\mathbf{X}$ to $D$:

$\mathcal{M},w,\sigma\vDash P(x_{1},...,x_{n})$ | $\iff$ | $(\sigma(x_{1}),...,\sigma(x_{n}))\in\rho(P,w)$
---|---|---
$\mathcal{M},w,\sigma\vDash x\approx y$ | $\iff$ | $\sigma(x)=\sigma(y)$
$\mathcal{M},w,\sigma\vDash\neg\phi$ | $\iff$ | $\mathcal{M},w,\sigma\not\vDash\phi$
$\mathcal{M},w,\sigma\vDash\phi\wedge\psi$ | $\iff$ |  $\mathcal{M},w,\sigma\vDash\phi$ and $\mathcal{M},w,\sigma\vDash\phi$
$\mathcal{M},w,\sigma\vDash\mathsf{[K]}\phi$ | $\iff$ |  For all $v\in W$, if $wRv$, then $\mathcal{M},v,\sigma\vDash\phi$
$\mathcal{M},w,\sigma\vDash[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ | $\iff$ |  There is some $a\in D$, s.t. $\mathcal{M},w,\sigma[x\mapsto a]\vDash\mathsf{[B]}\phi\wedge\phi$
$\mathcal{M},w,\sigma\vDash[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ | $\iff$ |  (i) There is some $a\in D$, s.t. $\mathcal{M},w,\sigma[x\mapsto a]\vDash\mathsf{[B]}\phi\wedge\phi$
(ii) For all $b\in D$, $\mathcal{M},w,\sigma[x\mapsto
b]\vDash\mathsf{[B]}\phi\to\phi$
$\mathcal{M},w,\sigma\vDash[\mathsf{K}^{\mathtt{MS}}]^{x}\phi$ | $\iff$ |  There is some $a\in D$, s.t. $\mathcal{M},w,\sigma[x\mapsto a]\vDash\mathsf{[K]}\phi$
$\mathcal{M},w,\sigma\vDash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ | $\iff$ |  (i) There is some $a\in D$, s.t. $\mathcal{M},w,\sigma[x\mapsto a]\vDash\mathsf{[K]}\phi$
(ii) For all $b\in D$, $\mathcal{M},w,\sigma[x\mapsto
b]\vDash\mathsf{[B]}\phi\to\phi$

where $\sigma[x\mapsto a]$ is the assignment which maps $x$ to $a$, and agrees
with $\sigma$ on any other point.

Note that we need not introduce an independent operator for belief, since
$\mathsf{[B]}\phi$ is already defined by
$\langle\mathsf{K}\rangle\mathsf{[K]}\phi$ in the languages given above. It is
also not hard to check that on $S4.2$-models, the semantics for
$\mathsf{[B]}\phi$ defined this way is indeed the following one:

$\mathcal{M},w,\sigma\vDash\mathsf{[B]}\phi\iff$ For all $v\in W$, if
$wR_{\mathsf{B}}v$, then $\mathcal{M},v,\sigma\vDash\phi$
---

##  4 The logics

Then, we introduce the four logics, corresponding to our four accounts of
knowledge-wh respectively. Their axiomatizations are all obtained in a similar
fashion: generally speaking, we start from a standard $\mathbf{S4.2}$ system
for $\mathsf{[K]}$, and then add axioms and rules to describe the behaviors of
the bundled operators.

Below is a list of schemas of axioms and rules that will be used to offer the
axiomatizations (in which the operator $[\mathsf{K}_{\mathtt{wh}}]$ should be
substituted by $[\mathsf{tB}^{\mathtt{MS}}]$,
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]$, $[\mathsf{K}^{\mathtt{MS}}]$ or
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]$ in the corresponding logics):777
Note that when we use the notation $\phi[y/x]$ to denote the formula obtained
by replacing every free occurrences of $x$ in $\phi$ with $y$, we also
implicitly assume that $y$ is _admissible_ for $x$ in $\phi$: that is, $y$
does not appear in the scope of any operator of the form
$[\mathsf{K}_{\mathtt{wh}}]^{y}$ in $\phi$.

Axioms
---
$\mathtt{TBtoK_{wh}}$ | $(\mathsf{[B]}\phi\wedge\phi)[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$ | $\mathtt{KtoK_{wh}}$ | $\mathsf{[K]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
$\mathtt{K_{wh}toFS}$ | $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to(\mathsf{[B]}\phi\to\phi)[y/x]$ | $\mathtt{BtoBK_{wh}}$ | $\mathsf{[B]}\phi[y/x]\to\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
Rules
$\mathtt{K_{wh}toTB}$ | $\displaystyle{\frac{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg(\mathsf{[B]}\phi\wedge\phi))\cdots)}{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg[\mathsf{K}_{\mathtt{wh}}]^{x}\phi)\cdots)}}$
$\mathtt{K_{wh}toK}$ | $\displaystyle{\frac{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg\mathsf{[K]}\phi)\cdots)}{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg[\mathsf{K}_{\mathtt{wh}}]^{x}\phi)\cdots)}}$
$\mathtt{FS\&BtoK_{wh}}$ | $\displaystyle{\frac{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi\to\phi))\cdots)}{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi))\cdots)}}\quad$
$\mathtt{FS\&KtoK_{wh}}$ | $\displaystyle{\frac{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi\to\phi))\cdots)}{\vdash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[K]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi))\cdots)}}$
(In all the rules above, $n$ can be any natural number, and we require that
$x\notin\bigcup_{i\leq n}FV(\psi_{i})$)

By using rules like $\mathtt{K_{wh}toTB}$ or $\mathtt{FS\&KtoK_{wh}}$, we have
sacrificed some intuitiveness for technical reasons, but the underlying idea
is straightforward: for example, $\mathtt{K_{wh}toTB}$ essentially says
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\exists x(\mathsf{[B]}\phi\wedge\phi)$,
and $\mathtt{FS\&KtoK_{wh}}$ says $\forall
x(\mathsf{[B]}\phi\to\phi)\wedge\mathsf{[K]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$,
in languages where the existential and universal quantifiers are not
available.

With the help of the above axioms and rules, then, we can give the following
four logics:

$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}$ | $\mathbf{S4.2}^{\mathsf{[K]}}\oplus\\{\mathtt{TBtoK_{wh}},\mathtt{K_{wh}toTB}\\}$
---|---
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}$ | $\mathbf{S4.2}^{\mathsf{[K]}}\oplus\\{\mathtt{K_{wh}toFS},\mathtt{BtoBK_{wh}},\mathtt{K_{wh}toTB},\mathtt{FS\&BtoK_{wh}}\\}$
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}$ | $\mathbf{S4.2}^{\mathsf{[K]}}\oplus\\{\mathtt{KtoK_{wh}},\mathtt{K_{wh}toK}\\}$
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ | $\mathbf{S4.2}^{\mathsf{[K]}}\oplus\\{\mathtt{K_{wh}toFS},\mathtt{BtoBK_{wh}},\mathtt{K_{wh}toK},\mathtt{FS\&KtoK_{wh}}\\}$

Moreover, for any
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
when we work in the language
$\mathcal{L}_{\approx}([\mathsf{K}_{\mathtt{wh}}])$, let
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}_{\mathtt{wh}}]}$ be the logic defined as
follows:

$\mathbf{S4.2}_{\approx}^{[\mathsf{K}_{\mathtt{wh}}]}$ | $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}\oplus\\{x\approx x,\;x\approx y\to(\phi[x/z]\to\phi[y/z]),\;x\not\approx y\to\mathsf{[K]}(x\not\approx y)\\}$
---|---

Note that all the logics given here are non-normal, since they are all non-
aggregative: that is,
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\wedge[\mathsf{K}_{\mathtt{wh}}]^{x}\psi\to[\mathsf{K}_{\mathtt{wh}}]^{x}(\phi\wedge\psi)$
is not an inner theorem of $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ (or
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}_{\mathtt{wh}}]}$) for any
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],\\\
[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$ (in
fact, in all these logics,
$[\mathsf{K}_{\mathtt{wh}}]^{x}Px\wedge[\mathsf{K}_{\mathtt{wh}}]^{x}\neg Px$
is consistent). Moreover, some of the logics are even non-monotone, as we will
see below.

Then, we show the completeness theorem for these logics.

Since we are now dealing with bundled operators with more complex structures,
the strategy to prove completeness theorems for the case of
$[\mathsf{K}^{\mathtt{MS}}]$ in [21] and [19] cannot be directly applied here
(moreover, axiomatization of the logic of $[\mathsf{K}^{\mathtt{MS}}]$ on
$S4.2$ has also not yet been studied). Hence, we will develop a new strategy
to prove completeness theorems for all the above logics in a uniform way.

###### Theorem 4.1

$\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ (as well as
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}_{\mathtt{wh}}]}$) is sound and strongly
complete w.r.t. the class of $S4.2$-constant-domain models, where
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.

######  Proof 4.2.

We only sketch the general idea of the proof here. A detailed proof for the
case of $\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ can be
found in the appendix.

Generally, we use maximal consistent sets (MCS) of formulas which also contain
certain witness formulas to construct the canonical model. The main difficulty
is to ensure at the same time that (i) every MCS in the model contains all the
witness formulas we need, (ii) every formula of the form
$\langle\mathsf{K}\rangle\phi$ in an MCS has some accessible MCS containing
$\phi$ as its witness, and (iii) the canonical model is an $S4.2$-constant-
domain model.

In order to construct such a model, we use a step-by-step method. We start
from a consistent set $\Gamma_{0}$, and extend consistent sets to MCS, add new
formula sets as witnesses for formulas of the form
$\langle\mathsf{K}\rangle\phi$, and add witness formulas to formula sets
during the same process. The key is to ensure, at each step of the
construction, that every formula set except $\Gamma_{0}$ is _finite_ , and all
the information contained in a set is recorded in its predecessor with a
formula of the form $\langle\mathsf{K}\rangle\phi$. This ensures that we can
always add witness formulas to formula sets using rules like
$\mathtt{K_{wh}toTB}$ and $\mathtt{FS\&KtoK_{wh}}$.

Then, after countably many steps, we obtain a model which satisfies both (i)
and (ii), and is also an $S4$-constant-domain model. Finally, we add another
set of MCSs to the model to make it strongly convergent, so that we can obtain
an $S4.2$-model.

######  Remark 4.3.

The above logics also have some interesting technical aspects.

For example, it is shown in [14] that the language
$\mathcal{L}([\mathsf{K}^{\mathtt{MS}}])$ cannot distinguish constant-domain
and increasing-domain models in general. However, when we confine the models
to $S4.2$-ones, $\mathcal{L}([\mathsf{K}^{\mathtt{MS}}])$ _can_ distinguish
constant-domain and increasing-domain models, and consequently,
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}$ is not sound w.r.t. the class of
$S4.2$-increasing-domain models (e.g.
$\langle\mathsf{K}\rangle[\mathsf{K}^{\mathtt{MS}}]^{x}\phi\to[\mathsf{K}^{\mathtt{MS}}]^{x}\langle\mathsf{K}\rangle\phi$
is an inner theorem of $\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}$, but is
not valid on $S4.2$-increasing-domain models). In fact, for all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],\
\\\ [\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
$\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ is not sound w.r.t.
$S4.2$-increasing-domain models.

Another interesting fact is that
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}$ and
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ are able to
distinguish $S4.2$-models (defined in terms of _strong_ convergence) and
models which are reflexive, transitive but only weakly convergent. The axiom
$\mathtt{BtoBK_{wh}}:\mathsf{[B]}\phi[y/x]\to\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
does the trick. When $[\mathsf{K}_{\mathtt{wh}}]=[\mathsf{tB}^{\mathtt{MS}}]$
or $[\mathsf{K}^{\mathtt{MS}}]$, on the other hand, we also have
$\mathsf{[B]}\phi[y/x]\to\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$ as an
inner theorem of $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$, but in this
case, the formula does not have the power to distinguish strong and weak
convergence, and consequently, $\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}$
and $\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}$ are also sound w.r.t. the
class of reflexive, transitive and weakly convergent models.

##  5 Comparisons

Now, we have the formal ground to compare the different accounts of knowledge-
wh.

###  5.1 Differences

An interesting difference among the different accounts of knowledge-wh
concerns the ways these accounts interact with propositional knowledge.

For example, consider _positive introspection_. Since we take $\mathbf{S4.2}$
to be the underlying logic for propositional knowledge, which is stronger than
$\mathbf{S4}$, it is clear that propositional knowledge satisfies positive
introspection: $\mathsf{[K]}\phi\to\mathsf{[K]}\mathsf{[K]}\phi$ is an inner
theorem of $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ for any
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.
However, does knowledge-wh also have positive introspection? To put it more
formally, is
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
an inner theorem of $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$? The answer
is as follow:

######  Proposition 5.1.

$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}\vdash[\mathsf{K}^{\mathtt{MS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}]^{x}\phi$,
but
$\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}\not\vdash[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
when
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.

The underlying reason for the failure of positive introspection in
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}$,
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}$ and
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ is similar.
Essentially, this is because these accounts may involve true beliefs (the MS-
true belief in $[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ or
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$, or a true belief required
by the FS condition in $[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ or
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$), but positive
introspection requires _knowledge_ rather than mere true belief, while the
latter in general does not imply the former in an $\mathbf{S4.2}$ system.

The following proposition helps us make this point clear on the formal level.
Note that in the formulation of (a part of) the following proposition, we will
also need the identity relation $\approx$ and the logic
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}_{\mathtt{wh}}]}$ which involves the
axioms for $\approx$.

######  Proposition 5.2.

We have the following identities between logics:

$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}\oplus[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ | $=$ | $\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}\oplus\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi$
---|---|---
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ | $=$ | $\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi$
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ | $=$ | $\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus x\not\approx y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$

In other words, under our $\mathbf{S4.2}$ setting for propositional knowledge,
requiring $[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ and
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ to satisfy positive
introspection is in effect the same as requiring true belief to imply
knowledge. The case for $[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$, on
the other hand, is a bit more complex: when
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ satisfies positive
introspection, either true belief implies knowledge, or there is at most one
element in the domain (in which case the notion of FS is clearly trivialized).

A similar phenomenon also appears in the case of the formula
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[K]}\phi$.
Intuitively, the formula says that knowledge-wh offers the agent a way to
obtain propositional knowledge: for example, if we interpret
$[\mathsf{K}_{\mathtt{wh}}]$ in terms of knowledge-how, then the formula says
that if an agent knows how to achieve $\phi$, then she also knows how to make
herself know that $\phi$. In fact, Proposition 5.1 and 5.2 still hold after we
substitute every occurrences of
$\mathsf{[K]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$ in these propositions with
$[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[K]}\phi$, since
$[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[K]}\phi\leftrightarrow\mathsf{[K]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
is in fact an inner theorem in $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$
for all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.

A more interesting difference among the different accounts of knowledge-wh
concerns the _monotonicity_ of knowledge-wh. We say our notion of knowledge-wh
is _monotone_ if the following rule is admissible in the corresponding logic:

$\mathtt{MONO}\quad\displaystyle{\frac{\vdash\phi\to\psi}{\vdash[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to[\mathsf{K}_{\mathtt{wh}}]^{x}\psi}}$

The rule says that if $\psi$ follows logically from $\phi$, then if an agent
has knowledge-wh of $\phi$, then she automatically also has knowledge-wh of
$\psi$.

Note that in order for this to hold, we need to assume that the agent we
consider is logically omniscient; and we have indeed assumed so in our
underlying logic for propositional logic, $\mathbf{S4.2}^{\mathsf{[K]}}$.
However, even such a logically omniscient agent still may _not_ have a
monotone notion of knowledge-wh, when FS is involved in our account of
knowledge-wh.

The propositions below show how FS influences the monotonicity of knowledge-
wh. (Note that we need the identity relation $\approx$ to formulate
Proposition 5.4.)

######  Proposition 5.3.

$\mathtt{MONO}$ is admissible in $\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}]}$
and $\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}]}$, but inadmissible in
$\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}$ and
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$.

######  Proposition 5.4.

The following equivalences holds:

$\mathbf{S4.2}_{\approx}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus\mathtt{MONO}$ | $=$ | $\mathbf{S4.2}_{\approx}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus x\not\approx y\to(\mathsf{[B]}\phi\to\phi)$
---|---|---
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus\mathtt{MONO}$ | $=$ | $\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus x\not\approx y\to(\mathsf{[B]}\phi\to\phi)$

As we can see, FS corrupts the monotonicity of knowledge-wh. In fact, as it is
shown in Proposition 5.4, if we force
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ and
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ to be monotone, then either
the agent can have no false belief at all, or there is only one element in the
domain of the model which characterizes her knowledge and belief - in both
cases, the notion of FS is completely trivialized. In this sense, we may say
that FS is incompatible with the monotonicity of knowledge-wh in quite an
essential way: in order to retain the monotonicity of knowledge-wh, we have to
give up FS completely.

###  5.2 Commonalities

As we have seen, different accounts of knowledge-wh behave rather differently
when interacting with propositional knowledge. However, when interacting with
_belief_ , their behaviors are much more similar.

For example, the following proposition shows some inner theorems shared by all
the logics presented above:888 Note that (iii) in the proposition below is in
fact an _axiom_ in $\mathbf{S4.2}^{[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]}$
and $\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$.

######  Proposition 5.5.

For all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
the following are $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$-theorems:

(i) | $\mathsf{[B]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[B]}\phi$ | (ii) | $\neg\mathsf{[B]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\neg\mathsf{[B]}\phi$
---|---|---|---
(iii) | $\mathsf{[B]}\phi[y/x]\to\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$ | (iv) | $\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\vee\mathsf{[B]}\neg[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$

If we interpret $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$ in terms of knowledge-
how, then (i) and (ii) say that if an agent believes / does not believe that
some certain $y$ is a way to achieve $\phi$, then she knows how to make
herself believe / not believe that $\phi$; (iii) says that if the agent
believes that some $y$ is a way to achieve $\phi$, then she also believes that
she knows how to achieve $\phi$; and (iv) says that an agent is “confident”
concerning her own epistemic state: for any $\phi$, she either believes that
she knows how to $\phi$, or believes that she does not knows how to $\phi$.
Note that in $\mathbf{S4.2}^{\mathsf{[K]}}$, we also have the interaction
principles $\mathsf{[B]}\phi\to\mathsf{[K]}\mathsf{[B]}\phi$,
$\neg\mathsf{[B]}\phi\to\mathsf{[K]}\neg\mathsf{[B]}\phi$ and
$\mathsf{[B]}\phi\to\mathsf{[B]}\mathsf{[K]}\phi$ and
$\mathsf{[B]}\mathsf{[K]}\phi\vee\mathsf{[B]}\neg\mathsf{[K]}\phi$ between
propositional knowledge and belief; hence, we may say that when interacting
with propositional belief (rather than knowledge), our accounts of knowledge-
wh show more aspects that resemble propositional knowledge.

Also note that from (i) and (iii), we can deduce the following two formulas,
respectively:

(v) | $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[B]}\phi$ | (vi) | $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
---|---|---|---

As we can see, though
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to[\mathsf{K}_{\mathtt{wh}}]^{x}\mathsf{[K]}\phi$
and
$[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
cannot be deduced in $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ when
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
when the operator $\mathsf{[K]}$ is relaxed to $\mathsf{[B]}$, we obtain (v)
and (vi), which are inner theorems of
$\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}$ for all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.

Another interesting commonality shared by all our logics (which also has to do
with the interaction between knowledge-wh and belief) concerns what logic of
knowledge-wh our agent believes.

In section 5.1, we have already shown some complexities in the reasoning about
knowledge-wh: for example, concerning positive introspection and monotonicity,
different accounts yield different behaviors of knowledge-wh. These
complexities, however, only appear when _we_ reason about the knowledge-wh of
an agent from an external perspective; when _the agent herself_ reasons about
her own knowledge-wh from within, all such complexities evaporate.

To put this point more rigidly, we introduce the following notion:

######  Definition 5.6.

For any logic $\mathbf{L}$, let
$\mathbf{L}_{\mathsf{B}}=\\{\phi\mid\mathsf{[B]}\phi\in\mathbf{L}\\}$.

Intuitively, for a logic $\mathbf{L}$, $\mathbf{L}_{\mathsf{B}}$ collects all
the formulas which $\mathbf{L}$ says that an agent believes. In this sense, if
$\mathbf{L}$ characterizes the epistemic states of an agent, then
$\mathbf{L}_{\mathsf{B}}$ characterizes the epistemic logic believed by this
agent.

Then, with the help of this new notation, we can formulate the following
theorem:

######  Proposition 5.7.

For all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$,
$\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}_{\mathsf{B}}$ can be axiomatized
by the following system:

$\mathbf{S5}^{\mathsf{[K]}}$ |  All axioms and rules of an $\mathbf{S5}$ system for $\mathsf{[K]}$
---|---
$\mathtt{KtoK_{wh}}$ | $\mathsf{[K]}\phi[y/x]\to[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
$\mathtt{K_{wh}toK}^{0}$ | $\displaystyle{\frac{\vdash\mathsf{[K]}\phi\to\psi}{\vdash\mathsf{[K]}^{x}\phi\to\psi}}$ (where $x\notin FV(\psi)$)

It is also not hard to check that this system is equivalent to the system
$\mathsf{SMLMSK}$ presented in [21], a system in the language
$\mathcal{L}([\mathsf{K}^{\mathtt{MS}}])$ which is sound and strongly complete
w.r.t. the class of $S5$-models.

Hence, conceptually, the above theorem says that no matter which account of
knowledge-wh we choose, it makes no difference for our agent: the agent always
believes that her knowledge-wh behaves in exactly the same way as MS-
knowledge, and the logic for the underlying propositional knowledge is as
strong as $\mathbf{S5}$. In such a logic, of course knowledge-wh is monotone
and satisfies positive introspection; moreover, it even satisfies _negative
introspection_ :
$\neg[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\to\mathsf{[K]}\neg[\mathsf{K}_{\mathtt{wh}}]^{x}\phi$
is in $\mathbf{S4.2}^{[\mathsf{K}_{\mathtt{wh}}]}_{\mathsf{B}}$ for all
$[\mathsf{K}_{\mathtt{wh}}]\in\\{[\mathsf{tB}^{\mathtt{MS}}],[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}],[\mathsf{K}^{\mathtt{MS}}],[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]\\}$.
On the other hand, all the subtle differences among the different accounts of
knowledge-wh, generated from the gap between mere true belief and knowledge,
as well as the peculiar behavior of the FS condition, are all invisible for
the agent in question.

##  6 Conclusion

In this paper, we studied four bundled operators:
$[\mathsf{tB}^{\mathtt{MS}}]$, $[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]$,
$[\mathsf{K}^{\mathtt{MS}}]$ and $[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]$,
which correspond to the four different accounts of knowledge-wh. We
axiomatized the logics which take them (as well as $\mathsf{[K]}$) as
primitive modalities on the class of $S4.2$-constant-domain models, and
compared the ways we reason about knowledge-wh in different logics.

There many potential future works that can be done based on our work.

For example, we can further study the four bundled operators introduced in
this paper. We have only studied their behavior on $S4.2$-models, which
characterize knowledge and belief in a highly idealized way; our study of the
obtained logics is also far from complete. Hence, it seems interesting to
study the logics obtained in this paper in greater detail, or to study the
behavior of the bundled operators on other reasonable models for knowledge and
belief (of course, we need not confine ourselves to Kripke models). This may
offer us a deeper understanding of the different accounts of knowledge-wh, and
may eventually help us decide which account is indeed the right one.

Moreover, the kind of step-by-step proof method applied in this paper can be
generalized to study other complex epistemic notion. For example, there are
cases where it is better to understand knowledge-wh in terms of mention-all
knowledge, and there are also various competing accounts of these kinds of
knowledge-wh, e.g. the _weakly exhaustive_ reading (first proposed in [9]),
the _strongly exhaustive_ reading (first proposed in [7]), and the
_intermediately exhaustive_ reading (first raised, but soon rejected, in [7],
and later proposed again in [16]), which can be formalized as $\forall
x(\phi(x)\to\mathsf{[K]}\phi(x))$, $\forall
x(\mathsf{[K]}\phi(x)\vee\mathsf{[K]}\neg\phi(x))$ and $\forall
x(\phi(x)\to\mathsf{[K]}\phi(x))\wedge\forall
x(\mathsf{[B]}\phi(x)\to\phi(x))$, respectively. Using the technique developed
in this paper, we can easily pack these complex notions into bundled
operators, and study their behavior.

Speaking on a more general level, the step-by-step method used in this paper
can at least be generalized to any logic equipped with a set of ordinary modal
operators $\\{\Box_{a}\\}_{a\in\tau}$ plus a set of bundled operators of the
form $\blacksquare^{x}\phi:=\exists x\alpha[\phi/p]\wedge\forall
x\beta[\phi/p]$, where $\alpha$ and $\beta$ are propositional modal formulas
containing only one propositional symbol $p$, boolean connectives and
operators in $\\{\Box_{a}\\}_{a\in\tau}$. Our trick works no matter how
complicated the structures of $\alpha$ and $\beta$ are, so a great deal of
complex first-order modal notions can be handled in this way.

## References

  * [1]
  * [2] J. Adam Carter & Duncan Pritchard (2015): _Knowledge-How and Epistemic Luck_.  Noûs 49(3), pp. 440–453, 10.1111/nous.12054.
  * [3] Yuri Cath (2015): _Revisionary Intellectualism and Gettier_.  Philosophical Studies 172(1), pp. 7–27, 10.1007/s11098-013-0263-y.
  * [4] Jie Fan, Yanjing Wang & Hans van Ditmarsch (2015): _Contingency and Knowing Whether_.  Rev. Symb. Log. 8(1), pp. 75–107, 10.1017/S1755020314000343.
  * [5] Raul Fervari, Andreas Herzig, Yanjun Li & Yanjing Wang (2017): _Strategically knowing how_.  In Carles Sierra, editor: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, ijcai.org, pp. 1031–1038, 10.24963/ijcai.2017/143.
  * [6] B. R. George (2013): _Knowing-’Wh’, Mention-Some Readings, and Non-Reducibility_.  Thought: A Journal of Philosophy 2(2), pp. 166–177, 10.1002/tht3.88.
  * [7] Jeroen Groenendijk & Martin Stokhof (1982): _Semantic analysis of ”wh”-complements_.  Linguistics and Philosophy, pp. 175–233, 10.1007/BF00351052.
  * [8] Keith Harris (2019): _Knowledge-How and False Belief_.  Synthese 198(2), pp. 1845–1861, 10.1007/s11229-019-02172-2.
  * [9] Lauri Karttunen (1977): _Syntax and Semantics of Questions_.  Linguistics and Philosophy 1(1), pp. 3–44, 10.1007/bf00351935.
  * [10] Wolfgang Lenzen (1978): _Recent Work in Epistemic Logic_.  Acta Philosophica Fennica 30, pp. 1–219.
  * [11] Wolfgang Lenzen (1979): _Epistemologische Betrachtungen zu [S4, S5]_.  Erkenntnis 14(1), pp. 33–56, 10.1007/BF00205012.
  * [12] Yanjun Li & Yanjing Wang (2017): _Achieving While Maintaining: - A Logic of Knowing How with Intermediate Constraints_.  In Sujata Ghosh & Sanjiva Prasad, editors: Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings, Lecture Notes in Computer Science 10119, Springer, pp. 154–167, 10.1007/978-3-662-54069-5_12.
  * [13] Pavel Naumov & Jia Tao (2018): _Together We Know How to Achieve: An Epistemic Logic of Know-How_.  Artificial Intelligence 262(C), pp. 279–300, 10.1016/j.artint.2018.06.007.
  * [14] Anantha Padmanabha, R. Ramanujam & Yanjing Wang (2018): _Bundled Fragments of First-Order Modal Logic: (Un)Decidability_.  In Sumit Ganguly & Paritosh K. Pandya, editors: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, LIPIcs 122, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 43:1–43:20, 10.4230/LIPIcs.FSTTCS.2018.43.
  * [15] Jonathan Phillips & B. R. George (2018): _Knowledge Wh and False Beliefs: Experimental Investigations_.  Journal of Semantics 35(3), pp. 467–494, 10.1093/semant/ffy004.
  * [16] Benjamin Spector (2005): _Exhaustive interpretations: What to say and what not to say_.  In: Unpublished paper presented at the LSA workshop on Context and Content.
  * [17] Robert Stalnaker (2006): _On Logics of Knowledge and Belief_.  Philosophical Studies 128(1), pp. 169–199, 10.1007/s11098-005-4062-y.
  * [18] Jason Stanley & Timothy Willlamson (2001): _Knowing How_.  Journal of Philosophy 98(8), pp. 411–444, 10.2307/2678403.
  * [19] Xun Wang (2021): _Completeness Theorems for $\exists\Box$-Fragment of First-Order Modal Logic_.  In Sujata Ghosh & Thomas Icard, editors: Logic, Rationality, and Interaction: 8th International Workshop, Lori 2021, Xi’an, China, October 16-18, 2021, Proceedings, Springer Verlag, pp. 246–258, 10.1007/978-3-030-88708-7_20.
  * [20] Yanjing Wang (2015): _A logic of knowing how_.  In: Logic, Rationality, and Interaction: 5th International Workshop, LORI 2015, Taipei, Taiwan, October 28-30, 2015. Proceedings 5, Springer, pp. 392–405, 10.1007/978-3-662-48561-3_32.
  * [21] Yanjing Wang (2017): _A New Modal Framework for Epistemic Logic_.  In Jérôme Lang, editor: Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2017, Liverpool, UK, 24-26 July 2017, EPTCS 251, pp. 515–534, 10.4204/EPTCS.251.38.
  * [22] Yanjing Wang (2018): _Beyond Knowing That: A New Generation of Epistemic Logics_.  In Hans van Ditmarsch & Gabriel Sandu, editors: Jaakko Hintikka on Knowledge and Game Theoretical Semantics, Springer, pp. 499–533, 10.1007/978-3-319-62864-6_21.
  * [23] Yanjing Wang (2018): _A logic of goal-directed knowing how_.  Synth. 195(10), pp. 4419–4439, 10.1007/s11229-016-1272-0.
  * [24] Yimei Xiang (2016): _Complete and true: A uniform analysis for mention some and mention all_.  In: Proceedings of Sinn und Bedeutung, 20, pp. 815–832.
  * [25] Chao Xu, Yanjing Wang & Thomas Studer (2021): _A logic of knowing why_.  Synthese 198(2), pp. 1259–1285, 10.1007/s11229-019-02104-0.
  * [26] Zhouhang Zhou (2018): _An epistemic logic of mention-all_.  Undergraduate thesis, Peking University.

## Acknowledgement

I owe the very idea of studying knowledge-wh with FS using bundled operators
to Yanjing Wang, and I would also like to thank him for his insightful advice
on this paper.

I would also like to thank Yimei Xiang for introducing works concerning MS-
knowledge and FS in linguistics to me, and Xun Wang for discussing matters
concerning the $\exists\Box$-bundled fragment with me. I should also thank
three anonymous reviewers from TARK 2023 for their helpful advice on the
writing of this paper, and for identifying the typos and grammar mistakes in
the paper.

Finally, I would like to thank the support of NSSF grant 19BZX135.

##  Appendix A Appendix

In the appendix, we show how to prove theorem 4.1, Proposition 5.2 and
Proposition 5.4.

First, we consider theorem 4.1. We only prove the case for
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$, since the other
cases can be proved in a similar way. Moreover, for most of the time, we will
be working in the language
$\mathcal{L}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, since our proof can
easily be generalized to the case of
$\mathcal{L}_{\approx}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$ with the
help of some slight modifications. We will demonstrate how to do so along the
proof.

First, we check that the soundness result holds.

######  Proposition A.1.

$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ is sound w.r.t. the
class of $S4.2$-constant-domain models.

######  Proof A.2.

We only prove that $\mathtt{BtoBK_{wh}}$ is valid on the class of
$S4.2$-constant-domain models, and $\mathtt{FS\&KtoK_{wh}}$ preserves validity
on such models.

For $\mathtt{BtoBK_{wh}}$:

Let $\mathcal{M}=(W,R,D,\rho)$ be a $S4.2$-model, let $w\in W$ be arbitrary,
and let $\sigma$ be an arbitrary assignment. Assume that
$\mathcal{M},w,\sigma\vDash\mathsf{[B]}\phi[y/x]$. Then, for all $v\in W$ s.t.
$wR_{\mathsf{B}}v$, $\mathcal{M},v,\sigma\vDash\phi[y/x]$.

Then, let $v\in W$ be arbitrary, and assume that $wR_{\mathsf{B}}v$.

We first show that $\mathcal{M},v,\sigma\vDash\mathsf{[K]}\phi[y/x]$. This is
clear, since for all $u\in W$ s.t. $vRu$, it is easy to check that
$wR_{\mathsf{B}}u$, and thus $\mathcal{M},u,\sigma\vDash\phi[y/x]$.

Then, we show that for all $a\in D$, $\mathcal{M},v,\sigma[x\mapsto
a]\vDash\mathsf{[B]}\phi\to\phi$. This is also clear: since
$(W,R_{\mathsf{B}})$ is $KD45$, $v$ is $R_{\mathsf{B}}$-reflexive.

Hence, it is easy to see that
$\mathcal{M},v,\sigma\vDash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$,
and thus
$\mathcal{M},w,\sigma\vDash\mathsf{[B]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$.

For $\mathtt{FS\&KtoK_{wh}}$:

Let $\mathcal{M}=(W,D,R,\rho)$ be an arbitrary $S4.2$-model, and assume that
$\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi\to\phi))\cdots)$
is valid on $\mathcal{M},w$, where $n$ is an arbitrary natural number; and let
$x$ be an variable s.t. $x\notin\bigcup_{i\leq n}FV(\psi_{i})$.

Then, let $\sigma$ be an arbitrary assignment, and suppose (towards a
contradiction) that
$\mathcal{M},w,\sigma\not\vDash\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[K]}\phi[y/x]\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi))\cdots)$.
Then, there is some $w_{0},w_{1},...,w_{n}\in W$, s.t. $w=w_{0}Rw_{1}R\cdots
Rw_{n}$, $\mathcal{M},w_{i},\sigma\vDash\psi_{i}$ for all $i\leq n$, and
$\mathcal{M},w_{n},\sigma\not\vDash\mathsf{[K]}\phi[y/x]\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$.
By the validity of
$\psi_{0}\to\mathsf{[K]}(\psi_{1}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi\to\phi))\cdots)$,
and since $x\notin\bigcup_{i\leq n}FV(\psi_{i})$, for all $a\in D$,
$\mathcal{M},w_{n},\sigma[x\mapsto a]\vDash\mathsf{[B]}\phi\to\phi$. But then,
since $\mathcal{M},w_{n},\sigma\vDash\mathsf{[K]}\phi[y/x]$,
$\mathcal{M},w_{n},\sigma[x\mapsto\sigma(y)]\vDash\mathsf{[K]}\phi$, and thus
it should follow that
$\mathcal{M},w_{n},\sigma\vDash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$,
causing a contradiction.

It is also not hard to check that
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ has the following
inner theorems, which will be used in our completeness proof.

$\mathtt{NBK_{wh}toBNK_{wh}}$ | $\langle\mathsf{B}\rangle[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[B]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$
---|---
$\mathtt{BK_{wh}toK_{wh}B}$ | $\mathsf{[B]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\mathsf{[B]}\phi$
$\mathtt{R}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ |  $[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\leftrightarrow[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}\phi[y/x]$ (where $y$ does not appear in $\phi$)

Now, we are ready to prove the completeness theorem.

As preparation, we first define the language
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, which is obtained
by adding countably many new variables to
$\mathcal{L}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$. We use
$\mathbf{X}^{+}$ to denote the set of variables of
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$.

Then, we use a step-by-step method to prove the completeness theorem. We first
define the notion of a _network_. Note that when constructing such networks,
the states will all be taken from a set of states $\\{w_{i}\mid
i\in\omega\\}$, which we fix in advance.

######  Definition A.3.

A _network_ is a triple $\mathcal{N}=(W,R,\nu)$, where

  * •

$\\{w_{0}\\}\subseteq W\subseteq\\{w_{i}\mid i\in\omega\\}$;

  * •

$R\subseteq W^{2}$, and $(W,R)$ forms a tree where $w_{0}$ is the root;

  * •

$\nu$ assigns each element in $W$ a set of
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$-formulas.

We also define the following two properties for the formula sets in a network:

######  Definition A.4.

($\mathtt{MS}$-property) An
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$-formula set
$\Delta$ has _$\mathtt{MS}$ -property_, iff for all
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$ and
$x\in\mathbf{X}^{+}$, if
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\in\Delta$, then there is
some $y\in\mathbf{X}^{+}$ s.t. $\mathsf{[K]}\phi[y/x]\in\Delta$.

######  Definition A.5.

($\mathtt{FS}$-property) An
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$-formula set
$\Delta$ has _$\mathtt{FS}$ -property_, iff for all
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$ and
$x,y\in\mathbf{X}^{+}$, if
$\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi,\mathsf{[K]}\phi[y/x]\in\Delta$,
then there is some $z\in\mathbf{X}^{+}$ s.t.
$(\mathsf{[B]}\phi\wedge\neg\phi)[z/x]\in\Delta$.

Then, we define the notion of coherence and saturation for networks:

######  Definition A.6.

A network $\mathcal{N}=(W,R,\nu)$ is _coherent_ , iff the following conditions
are satisfied:

  * (i)

$W$ is finite;

  * (ii)

For all $w\in W$, $\nu(w)$ is
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$-consistent; and for
all $w\in W\setminus\\{w_{0}\\}$, $\nu(w)$ is finite;

  * (iii)

For all $w,v\in W$ s.t. $wRv$, there is some $\psi$ s.t.
$\vdash\psi\leftrightarrow\bigwedge\nu(v)$ and
$\langle\mathsf{K}\rangle\psi\in\nu(w)$;

  * (iv)

There are countably many variables in $\mathbf{X}^{+}$ which do not appear in
$\nu(w)$ for any $w\in W$.

######  Definition A.7.

A network $\mathcal{N}=(W,R,\nu)$ is _saturated_ , iff for all $w\in W$ and
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, the
following holds:

  * (i)

$\nu(w)$ is a MCS of
$\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$-formulas;

  * (ii)

If $\mathsf{[K]}\phi\in\nu(w)$, then for all $v\in W$ s.t. $wRv$,
$\phi\in\nu(v)$;

  * (iii)

If $\langle\mathsf{K}\rangle\phi\in\nu(w)$, then there is some $v\in W$ s.t.
$wRv$ and $\phi\in\nu(v)$;

  * (iv)

$\nu(w)$ has the $\mathtt{MS}$-property;

  * (v)

$\nu(w)$ has the $\mathtt{FS}$-property.

Then, corresponding to the requirements of saturation, we also introduce the
following notion of _defects_ :

######  Definition A.8.

The possible kinds of _defects_ we may find on a state on a $w\in W$ in a
network $\mathcal{N}=(W,R,\nu)$ are as follow:

  * (d1)

$\phi\notin\nu(w)$ and $\neg\phi\notin\nu(w)$

  * (d2)

$\mathsf{[K]}\phi\in\nu(w)$, but there is some $v\in W$ s.t. $wRv$ and
$\phi\notin\nu(v)$

  * (d3)

$\langle\mathsf{K}\rangle\phi\in\nu(w)$, but there is no $v\in W$ s.t. $wRv$
and $\phi\in\nu(v)$

  * (d4)

$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\in\nu(w)$, but there is no
$y\in\mathbf{X}^{+}$ s.t. $\mathsf{[K]}\phi[y/x]\in\nu(w)$

  * (d5)

$\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi,\mathsf{[K]}\phi[y/x]\in\nu(w)$,
but there is no $z\in\mathbf{X}^{+}$ s.t.
$(\mathsf{[B]}\phi\wedge\neg\phi)[z/x]\in\nu(w)$

where $w\in\\{w_{i}\mid i\in\omega\\}$,
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$ and
$x\in\mathbf{X}^{+}$.

Then, we prove the _repair lemma_ , which shows how to repair defects in a
coherent network, while maintaining its coherence.

######  Lemma A.9.

(Repair lemma) For any coherent network $\mathcal{N}=(W,R,\nu)$ and any defect
$(d)$ of $\mathcal{N}$, then there is a coherent network
$\mathcal{N}^{\prime}=(W^{\prime},R^{\prime},\nu^{\prime})$ s.t. $W\subseteq
W^{\prime}$, $R\subseteq R^{\prime}$, $\nu(w)\subseteq\nu^{\prime}(w)$ for all
$w\in W$, and $\mathcal{N}^{\prime}$ does not has $(d)$.

######  Proof A.10.

Let $\mathcal{N}=(W,R,\nu)$ be a coherent network, and assume that
$\mathcal{N}$ has a defect $(d)$ for some $w_{m}\in W$ and
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$.

Since $(W,R)$ forms a tree where $w_{0}$ is the root, there is a unique path
$w_{0}=v_{0}Rv_{1}R\cdots Rv_{n}=w_{m}$ in $\mathcal{N}$ for some
$n\in\omega$. Then, since $\mathcal{N}$ is coherent, for all $1\leq i\leq n$,
let $\psi_{i}$ stand for the formula s.t.
$\vdash\psi_{i}\leftrightarrow\bigwedge\nu(v_{i})$ and
$\langle\mathsf{K}\rangle\psi_{i}\in\nu(v_{i-1})$. Then, it is easy to see
that

$\nu(v_{0})\vdash\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n-1}\wedge\langle\mathsf{K}\rangle\psi_{n})\cdots))$

We then consider five cases.

Case 1: $(d)$ is of the kind $(d1)$. That is, $\phi\notin\nu(v_{n})$ and
$\neg\phi\notin\nu(v_{n})$. Then, it is easy to check that

$\nu(v_{0})\vdash\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\phi)\cdots))\vee\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\neg\phi)\cdots))$

Then, at least one of the disjuncts is consistent with
$\nu(v_{0})=\nu(w_{0})$. We only consider the case where the former is
consistent with $\nu(w_{0})$, since the other case is similar. In this case,
let

$\displaystyle\nu^{\prime}=$ $\displaystyle\\{(w,\nu(w))\mid w\neq v_{i}\text{
for all }i\leq n\\}$ $\displaystyle\cup$
$\displaystyle\\{(v_{n},\nu(v_{n})\cup\\{\phi\\})\\}$ $\displaystyle\cup$
$\displaystyle\\{(v_{i},\nu(v_{i})\cup\\{\langle\mathsf{K}\rangle(\psi_{i+1}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\phi)\cdots)\\})\mid
i<n\\}$

and let $\mathcal{N}^{\prime}=\langle W,R,\nu^{\prime}\rangle$. It is then
easy to check that $\mathcal{N}^{\prime}$ is coherent, and does not have the
defect $(d)$.

Case 2: $(d)$ is of the kind $(d2)$. That is, $\mathsf{[K]}\phi\in\nu(v_{n})$,
but there is some $u\in W$ s.t. $v_{n}Ru$ and $\phi\notin\nu(u)$. Since
$\mathcal{N}$ is coherent, there is some $\psi_{u}$ s.t.
$\vdash\psi_{u}\leftrightarrow\bigwedge\nu(u)$ and
$\langle\mathsf{K}\rangle\psi_{u}\in\nu(v_{n})$. Hence, it is easy to check
that

$\nu(v_{0})\vdash\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\langle\mathsf{K}\rangle(\psi_{u}\wedge\phi))\cdots))$

Then, let

$\displaystyle\nu^{\prime}=$ $\displaystyle\\{(w,\nu(w))\mid w\neq v_{i}\text{
for all }i\leq n\\}$ $\displaystyle\cup$
$\displaystyle\\{(u,\nu(u)\cup\\{\phi\\})\\}$ $\displaystyle\cup$
$\displaystyle\\{(v_{i},\nu(v_{i})\cup\\{\langle\mathsf{K}\rangle(\psi_{i+1}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\phi)\cdots)\\})\mid
i\leq n\\}$

It is easy to check that $\mathcal{N}^{\prime}=(W,R,\nu^{\prime})$ is still
coherent, and does not have the defect $(d)$.

Case 3: $(d)$ is of the kind $(d3)$. That is,
$\langle\mathsf{K}\rangle\phi\in\nu(v_{n})$, but there is no $u\in W$ s.t.
$v_{n}Ru$ and $\phi\in\nu(u)$. Since $W$ is finite, there is some
$\\{w_{i}\mid i\in\omega\\}\setminus W\neq\emptyset$. Then, let $w_{k}$ be the
element in $\\{w_{i}\mid i\in\omega\\}\setminus W$ with the least index
number, and let $W^{\prime}=W\cup\\{w_{k}\\}$,
$R^{\prime}=R\cup\\{(v_{n},w_{k})\\}$, and
$\nu^{\prime}=\nu\cup\\{(w_{k},\\{\phi\\})\\}$. It is easy to check that
$\mathcal{N}=(W^{\prime},R^{\prime},\nu^{\prime})$ is coherent, but does not
have $(d)$.

Case 4: $(d)$ is of the kind $(d4)$. That is,
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\in\nu(v_{n})$, but there is
no $y\in\mathbf{X^{+}}$ s.t. $\mathsf{[K]}\phi[y/x]\in\nu(v_{n})$. Then, let
$y\in\mathbf{X^{+}}$ be a variable that does not appear in $\nu(w)$ for any
$w\in W$, and suppose (towards a contradiction) that

$\nu(v_{0})\vdash\mathsf{[K]}(\psi_{1}\to\mathsf{[K]}(\psi_{2}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg\mathsf{[K]}\phi[y/x])\cdots))$

Then, by $\mathtt{K_{wh}toK}$ (and
$\mathtt{R}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$), we have

$\nu(v_{0})\vdash\mathsf{[K]}(\psi_{1}\to\mathsf{[K]}(\psi_{2}\to\cdots\mathsf{[K]}(\psi_{n}\to\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi)\cdots))$

which contradicts the fact that $\nu(v_{0})=\nu(w_{0})$ is consistent. Hence,
$\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\mathsf{[K]}\phi[y/x])\cdots))$
is consistent with $\nu(v_{0})=\nu(w_{0})$. Hence, let

$\displaystyle\nu^{\prime}=$ $\displaystyle\\{(w,\nu(w))\mid w\neq v_{i}\text{
for all }i\leq n\\}$ $\displaystyle\cup$
$\displaystyle\\{(v_{n},\nu(v_{n})\cup\\{\mathsf{[K]}\phi[y/x]\\})\\}$
$\displaystyle\cup$
$\displaystyle\\{(v_{i},\nu(v_{i})\cup\\{\langle\mathsf{K}\rangle(\psi_{i+1}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge\mathsf{[K]}\phi[y/x])\cdots)\\})\mid
i<n\\}$

It is easy to check that $\mathcal{N}^{\prime}=(W,R,\nu)$ is still coherent,
and does not have the defect $(d)$.

Case 5: $(d)$ is of the kind $(d5)$. That is,
$\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\in\nu(v_{n})$ and
$\mathsf{[K]}\phi[y/x]\in\nu(v_{n})$, but there is no $z\in\mathbf{X^{+}}$
s.t. $(\mathsf{[B]}\phi\wedge\neg\phi)[z/x]\in\nu(v_{n})$. Then, let
$z\in\mathbf{X^{+}}$ be a variable that does not appear in $\nu(w)$ for any
$w\in W$, and suppose (towards a contradiction) that

$\nu(v_{0})\vdash\mathsf{[K]}(\psi_{1}\to\mathsf{[K]}(\psi_{2}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[B]}\phi[z/x]\to\phi[z/x]))\cdots))$

Then, by $\mathtt{FS\&KtoK_{wh}}$ (and
$\mathtt{R}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$), we have

$\nu(v_{0})\vdash\mathsf{[K]}(\psi_{1}\to\mathsf{[K]}(\psi_{2}\to\cdots\mathsf{[K]}(\psi_{n}\to(\mathsf{[K]}\phi[y/x]\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi))\cdots))$

which contradicts the fact that $\nu(v_{0})=\nu(w_{0})$ is consistent. Hence,
$\langle\mathsf{K}\rangle(\psi_{1}\wedge\langle\mathsf{K}\rangle(\psi_{2}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge(\mathsf{[B]}\phi\wedge\neg\phi)[z/x])\cdots))$
is consistent with $\nu(v_{0})=\nu(w_{0})$. Hence, let

$\displaystyle\nu^{\prime}=$ $\displaystyle\\{(w,\nu(w))\mid w\neq v_{i}\text{
for all }i\leq n\\}$ $\displaystyle\cup$
$\displaystyle\\{(v_{n},\nu(v_{n})\cup\\{(\mathsf{[B]}\phi\wedge\neg\phi)[z/x]\\})\\}$
$\displaystyle\cup$
$\displaystyle\\{(v_{i},\nu(v_{i})\cup\\{\langle\mathsf{K}\rangle(\psi_{i+1}\wedge\cdots\langle\mathsf{K}\rangle(\psi_{n}\wedge(\mathsf{[B]}\phi\wedge\neg\phi)[z/x])\cdots)\\})\mid
i<n\\}$

It is easy to check that $\mathcal{N}^{\prime}=(W,R,\nu)$ is still coherent,
and does not have the defect $(d)$.

Then, we can easily show that every coherent network can be extended into a
saturated network.

######  Lemma A.11.

For any coherent network $\mathcal{N}=(W,R,\nu)$, there exists a saturated
network $\mathcal{N}^{\prime}=(W^{\prime},R^{\prime},\nu^{\prime})$ s.t.
$W\subseteq W^{\prime}$, $R\subseteq R^{\prime}$ and
$\nu(w)\subseteq\nu^{\prime}(w)$ for all $w\in W$.

######  Proof A.12.

Let $\mathcal{N}=(W,R,\nu)$ be a coherent network.

It is not hard to see that there are only countably many possible defects.
Hence, we can enumerate them as $(d)_{1}$, $(d)_{2}$, $(d)_{3}$, …

Then, we define a countable sequence of networks
$\mathcal{N}_{i}=(W_{i},R_{i},\nu_{i})$ ($i\in\omega$) recursively as follow:

  * •

$\mathcal{N}_{0}=\mathcal{N}$;

  * •

Given a coherent network $\mathcal{N}_{k}$, let $(d)_{m}$ be the defect of
$\mathcal{N}_{k}$ with the least index number (note that according to our
definition of coherence, $\mathcal{N}_{k}$ necessarily has defects), and let
$\mathcal{N}_{k+1}=(W_{k+1},R_{k+1},\\\ \nu_{k+1})$ be a coherent network
which does not has $(d)_{m}$, and also satisfies that $W_{k}\subseteq
W_{k+1}$, $R_{k}\subseteq R_{k+1}$, $\nu_{k}(w)\subseteq\nu_{k+1}(w)$ for all
$w\in W_{k}$. The existence of such a network is guaranteed by lemma A.9.

Then, let $\mathcal{N}^{\prime}=(W^{\prime},R^{\prime},\nu^{\prime})$, where

  * •

$W^{\prime}=\bigcup_{i\in\omega}W_{i}$;

  * •

$R^{\prime}=\bigcup_{i\in\omega}R_{i}$;

  * •

For all $w\in W$, $\nu^{\prime}(w)=\bigcup_{i\geq k}\nu_{i}(w)$, where $k$ is
the least number s.t. $w\in W_{k}$.

It is not hard to see that $\mathcal{N}^{\prime}$ is a saturated network s.t.
$W_{0}\subseteq W$, $R_{0}\subseteq R$ and $\nu_{0}(w)\subseteq\nu(w)$ for all
$w\in W_{0}$.

Then, we show how to induce a canonical model from a saturated network.

######  Definition A.13.

Given a saturated network $\mathcal{N}=(W,R,\nu)$,
$\mathcal{M}^{c}_{\mathcal{N}}=(W_{\mathcal{N}}^{c},R_{\mathcal{N}}^{c},D_{\mathcal{N}}^{c},\rho_{\mathcal{N}}^{c})$
is the model induced from $\mathcal{N}$, where

  * •

$W_{\mathcal{N}}^{c}=\\{\nu(w)\mid w\in W\\}\cup FC$,
where $FC=\\{\Theta\mid\Theta\text{ is a MCS in
}\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]),\\{\phi\mid\mathsf{[B]}\phi\in\nu(w_{0})\\}\subseteq\Theta\\}$;999
$FC$ stands for _F_ inal _C_ luster. In fact, we can show that for all
$\Delta\in W^{c}$ and $\Theta\in FC$, $\Delta R^{c}\Theta$, which justifies
our naming.

  * •

$D_{\mathcal{N}}^{c}=\mathbf{X^{+}}$;

  * •

$R_{\mathcal{N}}^{c}$ satisfies that for all $\Delta,\Theta\in W^{c}$, $\Delta
R^{c}\Theta$ iff for all
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, if
$\mathsf{[K]}\phi\in\Delta$, then $\phi\in\Theta$;

  * •

$\rho_{\mathcal{N}}^{c}$ satisfies that for all $\Delta\in
W_{\mathcal{N}}^{c}$, $\bar{x}\in(D^{c}_{\mathcal{N}})^{<\omega}$ and
$P\in\mathcal{P}$, $\bar{x}\in\rho^{c}(P,\Delta)$ iff $P\bar{x}\in\Delta$.

We may drop the subscript $\mathcal{N}$ when the context is clear.

######  Remark A.14.

If we are working in the language
$\mathcal{L}_{\approx}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, then we let
$D^{c}_{\mathcal{N}}=\\{[x]\mid x\in\mathbf{X^{+}}\\}$, where
$[x]=\\{y\in\mathbf{X^{+}}\mid x\approx y\in\nu(w_{0})\\}$.

We then show that a model induced from a saturated network is indeed $S4.2$,
and also has all the properties we need.

######  Lemma A.15.

For any saturated network $\mathcal{N}$, $\mathcal{M}^{c}_{\mathcal{N}}$
satisfies the following:

  * (i)

$\mathcal{M}^{c}_{\mathcal{N}}$ is an $S4.2$-model;

  * (ii)

For all $\Delta\in W^{c}$ and $\langle\mathsf{K}\rangle\phi\in\Delta$, there
is some $\Delta^{\prime}\in W^{c}$ s.t. $\Delta R^{c}\Delta^{\prime}$ and
$\phi\in\Delta^{\prime}$;

  * (iii)

For all $\Delta\in W^{c}$, $\Delta$ has the $\mathtt{MS}$-property and the
$\mathtt{FS}$-property.

######  Proof A.16.

Let $\mathcal{M}^{c}_{\mathcal{N}}$ be an arbitrary model induced from a
saturated network $\mathcal{N}=(W,R,\nu)$.

For item (i): By the definition of $R^{c}$ and the canonicity of
$\mathtt{T}^{\mathsf{[K]}}$ and $\mathtt{4}^{\mathsf{[K]}}$, it is easy to see
that $\mathcal{M}^{c}_{\mathcal{N}}$ is reflexive and transitive.

We then show that $\mathcal{M}^{c}_{\mathcal{N}}$ is strongly convergent.

Clearly $FC\neq\emptyset$, since $\langle\mathsf{B}\rangle\top\in\nu(w_{0})$.

Then, we show that for all $\Delta\in W^{c}$ and $\Theta\in FC$, $\Delta
R^{c}\Theta$. Let $\Delta\in W^{c}$ and $\Theta\in FC$ be arbitrary. We
consider two cases:

Case 1: there is some $w\in W$ s.t. $\Delta=\nu(w)$. Let
$\mathsf{[K]}\phi\in\nu(w)$ be arbitrary. It is easy to see that
$\nu(w_{0})R^{c}\nu(w)$; hence,
$\langle\mathsf{K}\rangle\mathsf{[K]}\phi\in\nu(w_{0})$, i.e.
$\mathsf{[B]}\phi\in\nu(w_{0})$. Hence, by definition, $\phi\in\Theta$. Thus,
$\nu(w)R^{c}\Theta$.

Case 2: $\Delta\in FC$. Let $\mathsf{[K]}\phi\in\Delta$ be arbitrary. Then,
since $\Delta\in FC$, $\langle\mathsf{B}\rangle\mathsf{[K]}\phi\in\nu(w_{0})$,
i.e. $\mathsf{[K]}\langle\mathsf{K}\rangle\mathsf{[K]}\phi\in\nu(w_{0})$.
Then, by $\mathtt{T}^{\mathsf{[K]}}$,
$\langle\mathsf{K}\rangle\mathsf{[K]}\phi\in\nu(w_{0})$, i.e.
$\mathsf{[B]}\phi\in\nu(w_{0})$. Hence, $\phi\in\Theta$ and thus, $\Delta
R^{c}\Theta$.

Therefore, $\mathcal{M}_{\mathcal{N}}^{c}$ is strongly convergent.

For item (ii): Since $\mathcal{N}$ is saturated, we only need prove that for
all $\Theta\in FC$ and $\langle\mathsf{K}\rangle\phi\in\Theta$, there is some
$\Theta^{\prime}\in W^{c}$ s.t. $\Theta R^{c}\Theta^{\prime}$ and
$\phi\in\Theta^{\prime}$.

Let $\Theta\in FC$, $\langle\mathsf{K}\rangle\phi\in\Theta$ be arbitrary.
Then, since $\Theta\in FC$,
$\langle\mathsf{B}\rangle\langle\mathsf{K}\rangle\phi\in\nu(w_{0})$, i.e.
$\mathsf{[K]}\langle\mathsf{K}\rangle\langle\mathsf{K}\rangle\phi\in\nu(w_{0})$.
Hence, by $\mathtt{4}^{\mathsf{[K]}}$,
$\mathsf{[K]}\langle\mathsf{K}\rangle\phi\in\nu(w_{0})$, i.e.
$\langle\mathsf{B}\rangle\phi\in\nu(w_{0})$, and thus, there is some
$\Theta^{\prime}\in FC$ s.t. $\phi\in\Theta^{\prime}$. Then, as we have
already proved, $\Theta R^{c}\Theta^{\prime}$.

For item (iii): Again, since $\mathcal{N}$ is saturated, we only need to prove
that every $\Theta\in FC$ has the $\mathtt{MS}$-property and the
$\mathtt{FS}$-property.

Let $\Theta\in FC$ and $\phi\in\mathcal{L}^{+}([\mathsf{K}_{\mathtt{wh}}])$ be
arbitrary.

First, assume that $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\in\Theta$. Then,
$\langle\mathsf{B}\rangle[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\in\nu(w_{0})$, and
thus, by $\mathtt{NBK_{wh}toBNK_{wh}}$,
$\mathsf{[B]}\mathsf{[K]}^{x}\phi\in\nu(w_{0})$. Then, by
$\mathtt{BK_{wh}toK_{wh}B}$, $\mathsf{[K]}^{x}\mathsf{[B]}\phi\in\nu(w_{0})$.
Then, since $\mathcal{N}$ is saturated, $\nu(w_{0})$ has the
$\mathtt{MS}$-property, and thus there is some $y\in\mathbf{X^{+}}$ s.t.
$\mathsf{[K]}\mathsf{[B]}\phi[y/x]\in\nu(w_{0})$. Hence,
$\mathsf{[B]}\phi[y/x]\in\nu(w_{0})$, and thus
$\mathsf{[B]}\mathsf{[K]}\phi[y/x]\in\nu(w_{0})$. Hence,
$\mathsf{[K]}\phi[y/x]\in\Theta$.

Next, assume that $[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\in\Theta$. Then,
$\neg\mathsf{[B]}[\mathsf{K}_{\mathtt{wh}}]^{x}\phi\in\nu(w_{0})$, and thus
for all $y\in\mathbf{X}^{+}$, $\neg\mathsf{[B]}\phi[y/x]\in\nu(w_{0})$ by
$\mathtt{BtoBK_{wh}}$. Hence, for all $y\in\mathbf{X}^{+}$,
$\mathsf{[B]}\neg\mathsf{[B]}\phi[y/x]\in\nu(w_{0})$, and thus
$\mathsf{[B]}\phi[y/x]\notin\Theta$.

Then, it is routine to prove the truth lemma:

######  Lemma A.17.

For all $\mathcal{M}^{c}_{\mathcal{N}}$ induced from a saturated network
$\mathcal{N}$, for all $\Delta\in W^{c}$ and
$\phi\in\mathcal{L}^{+}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$,
$\mathcal{M}_{\mathcal{N}}^{c},\Delta,\sigma^{c}\vDash\phi\iff\phi\in\Delta$,
where $\sigma^{c}$ is the assignment s.t. $\sigma^{c}(x)=x$ for all
$x\in\mathbf{X}^{+}$.

######  Remark A.18.

If we are working in the language
$\mathcal{L}_{\approx}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$, then in the
formulation of the above lemma, we let $\sigma^{c}$ be the assignment s.t.
$\sigma^{c}(x)=[x]$ for all $x\in\mathbf{X}^{+}$.

Finally, notice that for any
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$-consistent set
$\Gamma$ of $\mathcal{L}([\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}])$-formulas
$\Gamma_{0}$, $(\\{w_{0}\\},\emptyset,\\{(w_{0},\Gamma_{0})\\})$ is a coherent
network. Hence, it can be extended into a saturated network
$\mathcal{N}^{\prime}$, from which we can induce a canonical model
$\mathcal{M}^{c}_{\mathcal{N}^{\prime}}$, such that
$\mathcal{M}^{c}_{\mathcal{N}^{\prime}},\nu^{\prime}(w_{0}),\sigma^{c}\vDash\Gamma_{0}$.

Hence, we have the following completeness theorem:

######  Theorem A.19.

$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$ (as well as
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$) is sound
and strongly complete w.r.t. the class of $S4.2$-constant-domain models.

Then, we consider Proposition 5.2. The cases for
$[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ and
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ are relatively easy, since
it is easy to see that $x\notin FV(\phi)$,
$[\mathsf{tB}^{\mathtt{MS}}]^{x}\phi$ and
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ are equivalent to
$\mathsf{[B]}\phi\wedge\phi$. Hence, we only prove the following proposition
here:

######  Proposition A.20.

The following equivalence holds:

$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$ | $=$ | $\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus x\not\approx y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$
---|---|---

######  Proof A.21.

We first show that $x\not\approx
y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$ can be deduced in
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$.
It is easy to check that $\vdash\phi\wedge x\not\approx
y\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{z}(x\approx z\to\phi[z/x])$,
where $z$ is a fresh variable. Then, by positive introspection,
$\vdash\phi\wedge x\not\approx
y\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{z}(x\approx
z\to\phi[z/x])$, and by $\mathtt{K_{wh}toFS}$, $\vdash\phi\wedge x\not\approx
y\to\mathsf{[K]}(\mathsf{[B]}(x\approx x\to\phi)\to(x\approx x\to\phi))$.
Hence, $\vdash\phi\wedge x\not\approx
y\to\mathsf{[K]}(\mathsf{[B]}\phi\to\phi)$, and thus $\vdash\phi\wedge
x\not\approx y\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$. Hence, $\vdash
x\not\approx y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$.

Then, we show that
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to\mathsf{[K]}[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi$
can be deduced in
$\mathbf{S4.2}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}_{\approx}\oplus
x\not\approx y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$.
Equivalently, we show that
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\mathsf{[K]}\phi$
can be deduced. Since $\vdash x\not\approx
y\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$ for some fresh $y$, by
$\mathtt{K_{wh}toK}$, we have
$\vdash[\mathsf{K}_{\mathtt{wh}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$. Then, we first show
that
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$.
On the one hand, it is easy to check that we have
$\vdash\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx y)\to
z\approx x$ (where $z$ is a fresh variable), and thus
$\vdash\mathsf{[K]}\phi[z/x]\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$. Hence,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$ by $\mathtt{K_{wh}toK}$ (and
$\mathtt{R}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$). On the other hand,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\wedge\phi\to\mathsf{[K]}\phi)$, and thus
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$ by $\mathtt{K_{wh}toFS}$. Hence,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to(\mathsf{[B]}\phi\to\mathsf{[K]}\phi)$.
Then, by $\mathtt{FS\&KtoK_{wh}}$ and $\mathtt{4}^{\mathsf{[K]}}$,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to(\mathsf{[K]}\phi\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\mathsf{[K]}\phi)$,
and thus
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\mathsf{[K]}\phi$
by $\mathtt{K_{wh}toK}$.

Finally, for Proposition 5.4, we only prove the case for
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]$, since the case for
$[\mathsf{tB}^{\mathtt{MS}}_{\mathtt{FS}}]$ is similar. That is, we prove the
following proposition:

######  Proposition A.22.

The following equivalence holds:

$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus\mathtt{MONO}$ | $=$ | $\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus x\not\approx y\to(\mathsf{[B]}\phi\to\phi)$
---|---|---

######  Proof A.23.

We first show that $x\not\approx y\to(\mathsf{[B]}\phi\to\phi)$ can be deduced
in
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus\mathtt{MONO}$.
Clearly $\vdash(x\approx y)\wedge(x\not\approx y)\to\phi$, i.e. $\vdash
x\approx y\to(x\not\approx y\to\phi)$. Then, by $\mathtt{MONO}$,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\approx
y)\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx y\to\phi)$. It
is also easy to check that
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\approx y)$. Hence,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx y\to\phi)$.
Then, by $\mathtt{K_{w}htoFS}$, $\vdash\mathsf{[B]}(x\approx
y\vee\phi)\to(x\not\approx y\to\phi)$. Hence, clearly
$\vdash\mathsf{[B]}\phi\to(x\not\approx y\to\phi)$, i.e. $\vdash x\not\approx
y\to(\mathsf{[B]}\phi\to\phi)$.

Then, we show that $\mathtt{MONO}$ is admissible in
$\mathbf{S4.2}_{\approx}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}\oplus
x\not\approx y\to(\mathsf{[B]}\phi\to\phi)$. Since we have $x\not\approx
y\to(\mathsf{[B]}\phi\to\phi)$ for some fresh $y$, by $\mathtt{K_{wh}toK}$,
$[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\phi\to\phi)$. Assume that $\vdash\phi\to\psi$. We first
prove that
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to(\mathsf{[B]}\psi\to\psi)$.
On the one hand,
$\vdash\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx y)\to
z\approx x$ (where $z$ is a fresh variable), and thus
$\vdash\mathsf{[K]}\phi[z/x]\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to\phi$. Then, since $\vdash\phi\to\psi$,
$\vdash\mathsf{[K]}\phi[z/x]\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to\psi$, and thus
$\vdash\mathsf{[K]}\phi[z/x]\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\psi\to\psi)$. Then, by $\mathtt{K_{wh}toK}$ and
$\mathtt{R}^{[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]}$
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge\neg[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\psi\to\psi)$. On the other hand, clearly
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{y}(x\not\approx
y)\to(\mathsf{[B]}\psi\to\psi)$. Hence,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to(\mathsf{[B]}\psi\to\psi)$.
And since $\vdash\phi\to\psi$, we also have
$\vdash\mathsf{[K]}\phi\to\mathsf{[K]}\psi$. Hence, by
$\mathtt{FS\&KtoK_{wh}}$,
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\wedge\mathsf{[K]}\phi\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\psi$,
and thus
$\vdash[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\phi\to[\mathsf{K}^{\mathtt{MS}}_{\mathtt{FS}}]^{x}\psi$
by $\mathtt{K_{wh}toK}$.