1 Introduction
In this article, we propose a logical system for reasoning about an agent’s abilities to tell apart groups of agents. Under the traditional Kripke approach to semantics of modal logics [Reference Kripke12], modal formulae are interpreted as properties of possible worlds. For example, we write
$w\Vdash \text {"Earth is round"}$
to express the fact that world w has the property of Earth being round. Prior [Reference Prior16] introduced the term “egocentric logic” for logical systems that capture properties of agents rather than possible worlds. Using his idea, we can write
$a \Vdash \text {"is sick"}$
to express the fact that agent a is sick. We can use usual Boolean connectives to construct more complicated formulae. For example, the statement
$$ \begin{align*}a \Vdash \text{"is a doctor"} \wedge \neg\,\text{"is sick"} \end{align*} $$
means that agent a is a doctor and is not sick. Seligman et al. [Reference Seligman, Liu and Girard18, Reference Seligman, Liu and Girard19] proposed a “for all friends” modality
$\mathsf {F}$
for egocentric setting. In their notations, the statement
$a \Vdash \mathsf {F}\text {"is sick"}$
means that all friends of agent a are sick and the statement
$$ \begin{align*}a \Vdash \text{"is sick"}\wedge\neg\mathsf{F}\neg\text{"is a doctor"} \end{align*} $$
means that agent a is sick and one of their friends is a doctor. Modality
$\mathsf {F}$
is also used in [Reference Christoff and Hansen2, Reference Christoff, Hansen and Proietti3]. Jiang and Naumov [Reference Jiang and Naumov11] introduced “likes those who” modality
$\mathsf {L}$
. For example, by
$a \Vdash \mathsf {L}\text {"is a doctor"}$
they denoted the sentence “agent a likes those who are doctors.” As usual, modalities can be nested. For example, statement
$a \Vdash \mathsf {L}\mathsf {L}\text {"is a doctor"}$
means that agent a likes those who like doctors.
Grove and Halpern [Reference Grove8–Reference Grove and Halpern10] suggested to consider the ternary satisfaction relation
$(a,w)\Vdash \varphi $
that means that, in world w, agent a has property
$\varphi $
. In philosophy of language, this approach is called 2D semantics [Reference Schroeter and Zalta17]. In such a setting, one can define knowledge modality
$\mathsf {K}$
. For example, the statement
$ (a,w)\Vdash \mathsf {K}\text {"is sick"} $
means that in world w the agent a knows that agent a is sick. This modality can be combined with modality
$\mathsf {F}$
to say that in world w agent a knows that one of their friends is sick:
$ (a,w)\Vdash \mathsf {K}\neg \mathsf {F}\neg \text {"is sick."} $
Epstein and Naumov [Reference Epstein and Naumov5] introduced modality
for “know who.” For example, the statement
means that in world w agent a knows at least one person who is a doctor. The statement
means that agent a knows who knows who is a doctor.
Knowing (at least one person) who is a doctor is different from the ability to tell apart doctors from non-doctors. This ability of an agent to tell apart (distinguish) agents who have property
$\varphi $
from those who do not have such a property is the subject of the current work. We write
$$ \begin{align*}(a,w)\Vdash \mathsf{A}\,\text{"is sick"} \end{align*} $$
to express that in world w agent a can tell apart (distinguish, classify) agents who are sick from those who are not sick. To connect with intuition, let us use the term “doctor” for the agents who can tell apart sick people from those who are not sick. Then, the statement
$$ \begin{align*}(a,w)\Vdash \mathsf{K}\mathsf{A}\,\text{"is sick"} \end{align*} $$
means that agent a knows that agent a themself is a doctor. The statement
$$ \begin{align*}(a,w)\Vdash \mathsf{A}\mathsf{A}\,\text{"is sick"} \end{align*} $$
means that agent a can tell apart doctors from non-doctors. Finally, the statement
$$ \begin{align*}(a,w)\Vdash \mathsf{A}\mathsf{K}\,\text{"is sick"} \end{align*} $$
means that agent a can tall apart agents who know about themselves that they are sick from those who don’t know that they are sick (whether they are actually sick or not). Such an agent a is probably a psychologist.
The contribution of this work is twofold. First, we propose a formal egocentric semantics for modality
$\mathsf {A}$
and a sound, complete, and decidable logical system that describes the interplay between modality
$\mathsf {A}$
and the knowledge modality
$\mathsf {K}$
. Second, we introduce and use a new, matrix-based, technique for proving completeness results for 2D semantics. Section 6 discusses this technique in detail.
The rest of this article is structured as follows. In the next section, we introduce the syntax and semantics of our formal system. Section 3 discusses related literature. In Section 4 we list the axioms of our system. The soundness of these axioms is shown in Section 5. Section 6 proves the completeness of our system using the newly proposed technique. Section 7 shows its decidability. We discuss possible extensions of our system in Section 8. Section 9 concludes.
2 Syntax and semantics
In this section, we present the syntax and the formal semantics of our logical system. The semantics is using epistemic models that we define below. Note that the only difference from the traditional S5 models is that propositional variables are interpreted as properties of pairs
$(a,w)$
, where a is an agent and w is a world. As a result, valuation function
$\pi $
maps each propositional variable to a set of such pairs. Informally,
$\pi (p)$
is the set of pairs for which property p is true. Throughout the article, we assume a fixed countable set of propositional variables.
Definition 2.1. A tuple
$(Ag,W,\{\sim _a\}_{a\in Ag},\pi )$
is an epistemic model if:
-
1.
$Ag$
is a set of “agents,” -
2. W is a set of all “worlds,”
-
3.
$\sim _a$
is an “indistinguishability” equivalence relation on W, -
4.
$\pi (p)\subseteq Ag\times W$
for each propositional variable p.
Figure 1 depicts an epistemic model capturing our introductory example. This model has three agents,
$a_1$
,
$a_2$
, and
$a_3$
, as well as four worlds,
$w_1$
,
$w_2$
,
$w_3$
, and
$w_4$
. Each indistinguishability relation is specified by listing its equivalence classes in the partition column. For example, agent
$a_1$
cannot distinguish world
$w_1$
from world
$w_2$
and they also cannot distinguish world
$w_3$
from world
$w_4$
. In this example, we assume that our language has a single propositional variable p, which means “is sick.” The set
$\pi (p)$
consists of all pairs
$(a,w)$
such that agent a is sick in world w. We visualize set
$\pi (p)$
on the left side of Figure 1. For example, propositional variable p in the first row, the first column of the table means that
$(a_1,w_1)\in \pi (p)$
.
Figure 1 An epistemic model. Informally, propositional variable p means “is sick.”
The language
$\Phi $
of our logical system is defined by the grammar:
$$ \begin{align*} \varphi:= p \;|\; \neg\varphi\;|\; \varphi\to\varphi \;|\;\mathsf{K}\varphi\;|\;\mathsf{A}\varphi, \end{align*} $$
where p is a propositional variable. We read
$\mathsf {K}\varphi $
as “knows about themself” and
$\mathsf {A}\varphi $
as “knows how to tell apart those who.” We assume that conjunction
$\wedge $
, disjunction
$\vee $
, biconditional
$\leftrightarrow $
, and false
$\bot $
are defined in the standard way. The semantics of our logical system is given in the definition below.
Definition 2.2. For any epistemic model
$(Ag,W,\{\sim _a\}_{a\in Ag},\pi )$
, any agent
$a\in Ag$
, any world
$w\in W$
, and any formula
$\varphi \in \Phi $
, the satisfaction relation
$(a,w)\Vdash \varphi $
is defined recursively as follows:
-
1.
$(a,w)\Vdash p$
if
$(a,w)\in \pi (p)$
. -
2.
$(a,w)\Vdash \neg \varphi $
if
$(a,w)\nVdash \varphi $
. -
3.
$(a,w)\Vdash \varphi \to \psi $
if
$(a,w)\nVdash \varphi $
or
$(a,w)\Vdash \psi $
. -
4.
$(a,w)\Vdash \mathsf {K}\varphi $
when for each world
$u\in W$
, if
$w\sim _a u$
, then
$(a,u)\Vdash \varphi $
. -
5.
$(a,w)\Vdash \mathsf {A}\varphi $
when for each agent
$b\in Ag$
and any worlds
$u,u'\in W$
, if
$w\sim _a u$
,
$w\sim _a u'$
, and
$(b,u)\Vdash \varphi $
, then
$(b,u')\Vdash \varphi $
.
Note that the meaning of the statement
$(a,w)\Vdash \mathsf {K}\varphi $
, as defined in item 4 above, is “in world w, agent a knows
$\varphi $
about themself.” It is the agent a who knows because the item is using the indistinguishability relation
$\sim _a$
. It is the agent a about whom the statement
$\varphi $
is known because, in that item, the statement
$(a,u)\Vdash \varphi $
refers to agent a.
The meaning of the statement
$(a,w)\Vdash \mathsf {A}\varphi $
is “in world w, agent a knows how to tell apart those for whom
$\varphi $
is true.” Indeed, item 5 above says that whether
$\varphi $
holds for an arbitrary agent b is consistent among all words indistinguishable by agent a. In our example, the statement
$(a,w)\Vdash \mathsf {A} p$
means that any agent b is either (i) sick in all worlds indistinguishable by agent a from world w or (ii) not sick in all worlds indistinguishable to agent a from world w.
Figure 2 shows examples of formulae that are true about different agents in different worlds of the epistemic model depicted in Figure 1. For instance, observe in Figure 1 that agent
$a_1$
cannot distinguish worlds
$w_1$
and
$w_2$
. At the same time, agent
$a_1$
is sick in both of these worlds. Thus, by item 4 of Definition 2.2, in both of these worlds, agent
$a_1$
knows that agent
$a_1$
is sick. We denote this by formula
$\mathsf {K} p$
in cells
$(a_1,w_1)$
and
$(a_1,w_2)$
of Figure 2. Agent
$a_1$
also cannot distinguish worlds
$w_3$
and
$w_4$
. They are sick in world
$w_3$
, but not
$w_4$
. Thus, in both of these worlds, agent
$a_1$
does not know that agent
$a_1$
is sick.
Figure 2 Examples of formulae satisfied in the epistemic model shown in Figure 1.
To illustrate modality
$\mathsf {A}$
, observe again that agent
$a_1$
cannot distinguish worlds
$w_1$
and
$w_2$
. Note that each of the agents in the model (
$a_1$
,
$a_2$
, and
$a_3$
) is sick in world
$w_1$
if and only if the same agent is sick in world
$w_2$
. Thus, in world
$w_1$
, agent
$a_1$
knows which of the agents is sick and which is not. In other words, agent
$a_1$
knows how to tell apart those who are sick from those who are not. Using the informal language from our introduction, agent
$a_1$
is a “doctor” in world
$w_1$
. In the formal language of our logical system,
$(a_1,w_1)\Vdash \mathsf {A} p$
.
Consider now agent
$a_2$
in the same world
$w_1$
. This agent cannot distinguish world
$w_1$
from world
$w_4$
. Additionally, agent
$a_1$
is sick in world
$w_1$
and is not sick in world
$w_4$
. Thus, in world
$w_1$
, agent
$a_2$
does not know if agent
$a_1$
is sick or not. Hence, in world
$w_1$
agent
$a_2$
is not a “doctor”:
$(a_2,w_1)\nVdash \mathsf {A} p$
.
Let us consider again world
$w_1$
where agent
$a_1$
cannot distinguish the current world from world
$w_2$
. As shown in Figure 2, for each agent in the model, the agent knows about themself that they are sick (formula
$\mathsf {K} p$
) in world
$w_1$
iff they know the same in world
$w_2$
. Thus, in world
$w_1$
, agent
$a_1$
knows how to tell apart the agents for whom
$\mathsf {K} p$
is true. Using our informal language from the introduction, agent
$a_1$
is a “psychologist” in world
$w_1$
. Formally, we write that
$(a_1,w_1)\Vdash \mathsf { A}\mathsf {K} p$
.
Finally, observe that, in our model, each agent a in each world w can tell psychologists apart:
$(a,w)\Vdash \mathsf {A}\mathsf {A}\mathsf {K} p$
. At the same, in our model, each agent in each world cannot tell doctors apart:
$(a,w)\nVdash \mathsf {A}\mathsf {A} p$
.
3 Related work
In this section, we discuss how else the notion “knowing how to tell apart” could be formalized and also how our modality fits into the larger fields of logics of know-wh.
3.1 Another formalization
We are not aware of any other existing attempts to formalize the notion of “knowing how to tell apart” as a modality, but, as is often the case with modalities, this notion can be expressed using quantifiers. More specifically, our language
$\Phi $
can be translated into the language of an epistemic modal logic with quantifiers over agents. An example of such a language is in our own work [Reference Naumov and Tao15], but it is not sufficiently rich. Namely, in [Reference Naumov and Tao15], we assume that propositional variables are statements about worlds. For the formalization to work, we need a language
$\mathcal {Q}$
that includes “agent predicates”
$P(x_1,\dots ,x_n)$
. The validity of such a predicate depends not only on the world we consider, but also on the values of agent variables
$x_1,\dots ,x_n$
.
Next, we describe a translation
$\tau _x$
from language
$\Phi $
into language
$\mathcal {Q}$
for each agent variable x. For any propositional variable p, the value
$\tau _x(p)$
is an agent predicate
$p(x)$
with a single agent variable x. In addition, let
$$ \begin{align*} \tau_x(\varphi\to\psi)&=\tau_x(\varphi)\to \tau_x(\psi),\\ \tau_x(\neg\varphi)&=\neg\tau_x(\varphi),\\ \tau_x(\mathsf{K}\varphi)&=\mathsf{K}_x\tau_x(\varphi),\\ \tau_x(\mathsf{A}\varphi)&=\forall y\, (\mathsf{K}_x\tau_y(\varphi) \vee \mathsf{K}_x\neg\tau_y(\varphi)). \end{align*} $$
We believe that under any reasonable semantics
$\Vdash _{\mathcal {Q}}$
of language
$\mathcal {Q}$
defined using epistemic models from Definition 2.1, for any world w of such a model and any formula
$\varphi \in \Phi $
,
$$ \begin{align*}(\sigma(x),w)\Vdash \varphi \text{ iff } w\Vdash_{\mathcal{Q}} \tau_x(\varphi) [\sigma], \end{align*} $$
where
$\sigma $
is any assignment of agents to agent variables.
3.2 Knowing-wh logics
Modality
$\mathsf {A}$
expresses a particular type of knowledge that an agent might have—knowledge of how to classify people into those who have a given property and those who do not. As such, it belongs to the growing class of know-wh [Reference Wang20] modalities: know how [Reference Fervari, Herzig, Li and Wang7, Reference Naumov and Tao14], know who [Reference Epstein and Naumov5], know why [Reference Xu, Wang and Studer21], and know value [Reference Baltag, Beklemishev, Demri and Maté1, Reference van Eijck, Gattinger and Wang4]. Among such modalities, the closest one to ours is probably the “know whether” modality
$\mathsf {Kw}$
proposed by Fan, Wang, and van Ditmarsch [Reference Fan, Wang and Van Ditmarsch6]. Note that in the traditional, non-egocentric setting, modality
$\mathsf {Kw}$
is definable through individual knowledge modality:
$\mathsf {Kw}_a\varphi \equiv \mathsf {K}_a\varphi \vee \mathsf {K}_a\neg \varphi $
. In the egocentric setting, the formula
$\mathsf {A}\varphi $
denotes the ability of an agent to tell apart those agents for whom
$\varphi $
is true from those for whom
$\varphi $
is false among all agents. At the same time, knowledge modality
$\mathsf {K}$
expresses knowledge of an agent about themself. It is clear that
$\mathsf {A}$
cannot be defined through
$\mathsf {K}$
. However, if a property
$\varphi $
is true for an agent, then the agent’s ability to decide
$\varphi $
about all agents implies their knowledge of the property about themself:
$\varphi \to (\mathsf {A}\varphi \to \mathsf {K}\varphi )$
. This formula is one of the axioms of our logical system that we introduce in the next section.
4 Axioms
In addition to tautologies in language
$\Phi $
, our logical system contains the following axioms:
-
1. Truth:
$\mathsf {K}\varphi \to \varphi $
. -
2. Distributivity:
$\mathsf {K}(\varphi \to \psi )\to (\mathsf {K}\varphi \to \mathsf {K}\psi )$
. -
3. Negative Introspection:
$\neg \mathsf {K}\varphi \to \mathsf {K}\neg \mathsf {K}\varphi $
. -
4. Introspection of Knowing All:
$\mathsf {A}\varphi \to \mathsf {K}\mathsf {A}\varphi $
. -
5. Self-Knowledge:
$\varphi \to (\mathsf {A}\varphi \to \mathsf {K}\varphi )$
. -
6. Negation:
$\mathsf {A}\varphi \to \mathsf {A}\neg \varphi $
. -
7. Conjunction:
$\mathsf {A}\varphi \wedge \mathsf {A}\psi \to \mathsf {A}(\varphi \wedge \psi )$
.
We say that formula
$\varphi \in \Phi $
is a theorem of our logical system and write
$\vdash \varphi $
if
$\varphi $
is derivable from the above axioms using the Modus Ponens, two forms of the Necessitation, and the Substitution inference rules:
$$ \begin{align*}\dfrac{\varphi, \varphi\to\psi}{\psi}\hspace{10mm} \dfrac{\varphi}{\mathsf{K}\varphi}\hspace{10mm} \dfrac{\varphi}{\mathsf{A}\varphi}\hspace{10mm} \dfrac{\varphi\leftrightarrow\psi}{\mathsf{A}\varphi\to\mathsf{A}\psi}. \end{align*} $$
We write
$X\vdash \varphi $
if a formula
$\varphi \in \Phi $
is derivable from the theorems of our logical system and an additional set of assumptions
$X\subseteq \Phi $
using only the Modus Ponens inference rule. It is easy to see that
$\varnothing \vdash \varphi $
iff
$\vdash \varphi $
. We say that set X is consistent if
$X\nvdash \bot $
.
The Truth, the Distributivity, and the Negative Introspection axioms are the standard axioms of epistemic logic S5. The Introspection of Knowing All axiom states that if an agent knows how to tell apart agents with a given property, then the agent knows that the agent has such an ability. The Self-Knowledge axiom states that if a statement
$\varphi $
is true about an agent and the agent knows how to tell apart the agents for whom
$\varphi $
is true, then the agent must know
$\varphi $
about themself. The Negation axiom states that if an agent knows how to tell apart those for whom
$\varphi $
is true, then it also knows how to tell apart those for whom
$\varphi $
is false. The Conjunction axiom states that if an agent knows separately how to tell apart agents who have each of the two properties, then the agent knows how to tell apart those who have both properties.
The next three lemmas capture well-known results in modal logic. To make the article self-contained, we reproduce their proofs in the Appendix.
Lemma 4.1 (deduction).
If
$X,\varphi \vdash \psi $
, then
$X\vdash \varphi \to \psi $
.
Lemma 4.2. If
$\varphi _1,\dots ,\varphi _n\vdash \psi $
, then
$\mathsf {K}\varphi _1,\dots ,\mathsf {K}\varphi _n\vdash \mathsf {K}\psi $
.
Lemma 4.3.
$\vdash \mathsf {K}\varphi \to \mathsf {K}\mathsf {K}\varphi $
.
Lemma 4.4.
$\vdash \neg \mathsf {A}\varphi \to \mathsf {K}\neg \mathsf {A}\varphi $
.
Proof By the Introspection of Knowing All axiom,
$\vdash \mathsf {A}\varphi \to \mathsf {K}\mathsf {A}\varphi $
. Thus,
$\vdash \neg \mathsf {K}\mathsf {A}\varphi \to \neg \mathsf {A}\varphi $
by the contrapositive. Hence,
$\vdash \mathsf {K}(\neg \mathsf {K}\mathsf {A}\varphi \to \neg \mathsf {A}\varphi )$
by the Necessitation inference rule. Then, by the Distributivity axiom and the Modus Ponens inference rule
$\vdash \mathsf {K}\neg \mathsf {K}\mathsf {A}\varphi \to \mathsf {K}\neg \mathsf {A}\varphi $
. Thus, by the Negative Introspection axiom and the laws of propositional reasoning, we have
$\vdash \neg \mathsf {K}\mathsf {A}\varphi \to \mathsf {K}\neg \mathsf {A}\varphi $
. Note that
$\neg \mathsf {A}\varphi \to \neg \mathsf {K}\mathsf {A}\varphi $
is the contrapositive of the Truth axiom. Therefore, by the laws of propositional reasoning,
$\vdash \neg \mathsf {A}\varphi \to \mathsf {K}\neg \mathsf {A}\varphi $
.
Lemma 4.5 (Lindenbaum).
Any consistent set of formulae can be extended to a maximal consistent set of formulae.
Proof The standard proof of Lindenbaum’s lemma [Reference Mendelson13, Proposition 2.14] applies.
5 Soundness
In this section, we prove the soundness of our logical system. The soundness of the Truth, the Distributivity, and the Negative Introspection axioms as well as of the Modus Ponens and the two forms of the Necessitation inference rules is straightforward. We prove the soundness of each of the remaining axioms and of the Substitution rule below.
Lemma 5.1. If
$(a,w)\Vdash \mathsf {A}\varphi $
, then
$(a,w)\Vdash \mathsf {K}\mathsf {A}\varphi $
.
Proof Consider any world
$u\in W$
such that
$$ \begin{align} w\sim_a u. \end{align} $$
By item 4 of Definition 2.2, it suffices to show that
$(a,u)\Vdash \mathsf {A}\varphi $
.
Next, consider any agent
$b\in Ag$
and any worlds
$u',u"\in W$
, such that
$u\sim _a u'$
,
$u\sim _a u"$
, and
$(b,u')\Vdash \varphi $
. By item 5 of Definition 2.2, it suffices to prove that
$(b,u")\Vdash \varphi $
. Indeed, statement (1) implies that
$w\sim _a u'$
,
$w\sim _a u"$
because
$\sim _a$
is an equivalence relation. Thus,
$(b,u")\Vdash \varphi $
by item 5 of Definition 2.2 and the assumption
$(a,w)\Vdash \mathsf {A}\varphi $
of the lemma.
Lemma 5.2. If
$(a,w)\Vdash \varphi $
and
$(a,w)\Vdash \mathsf {A}\varphi $
, then
$(a,w)\Vdash \mathsf {K}\varphi $
.
Proof Consider any world
$u\in W$
such that
$$ \begin{align} w\sim_a u. \end{align} $$
By item 4 of Definition 2.2, it suffices to show that
$(a,u)\Vdash \varphi $
.
Note
$w\sim _a w$
because
$\sim _a$
is an equivalence relation. Thus, the assumptions
$(a,w)\Vdash \mathsf {A}\varphi $
and
$(a,w)\Vdash \varphi $
of the lemma and statement (2) imply
$(a,u)\Vdash \varphi $
by item 5 of Definition 2.2.
Lemma 5.3. If
$(a,w)\Vdash \mathsf {A}\varphi $
, then
$(a,w)\Vdash \mathsf {A}\neg \varphi $
.
Proof Consider any agent
$b\in Ag$
and any worlds
$u,u'\in W$
such that
$$ \begin{align} w\sim_a u \;\;\text{ and }\;\; w\sim_a u'. \end{align} $$
By item 5 of Definition 2.2, it suffices to prove that if
$(b,u)\Vdash \neg \varphi $
, then
$(b,u')\Vdash \neg \varphi $
. Then, by item 2 of Definition 2.2 and the law of contraposition, it suffices to show that if
$(b,u')\Vdash \varphi $
, then
$(b,u)\Vdash \varphi $
. The last statement is true by the assumption
$(a,w)\Vdash \mathsf {A}\varphi $
of the lemma, statements (3), and item 5 of Definition 2.2.
Lemma 5.4. If
$(a,w)\Vdash \mathsf {A}\varphi $
and
$(a,w)\Vdash \mathsf {A}\psi $
, then
$(a,w)\Vdash \mathsf {A}(\varphi \wedge \psi )$
.
Proof Consider any agent
$b\in Ag$
and any worlds
$u,u'\in W$
such that
$$ \begin{align} w\sim_a u \;\;\text{ and }\;\; w\sim_a u' \end{align} $$
and
$$ \begin{align} (b,u)\Vdash \varphi \wedge \psi. \end{align} $$
By item 5 of Definition 2.2, it suffices to prove that if
$(b,u')\Vdash \varphi \wedge \psi $
.
The assumption (5) implies
$(b,u)\Vdash \varphi $
and
$(b,u)\Vdash \psi $
. Thus,
$(b,u')\Vdash \varphi $
and
$(b,u')\Vdash \psi $
by the assumptions
$(a,w)\Vdash \mathsf {A}\varphi $
and
$(a,w)\Vdash \mathsf {A}\psi $
of the lemma, statement (5), and item 5 of Definition 2.2. Then,
$(b,u')\Vdash \varphi \wedge \psi $
.
Lemma 5.5. If
$(a,w)\Vdash \varphi \leftrightarrow \psi $
for each agent a and each world w of each epistemic model, then
$(a,w)\Vdash \mathsf {A}\varphi \to \mathsf {A}\psi $
for each agent a and each world w of each epistemic model.
Proof Consider any agent a and any world w of an epistemic model such that
$(a,w)\Vdash \mathsf {A}\varphi $
. By item 3 of Definition 2.2, it suffices to prove that
$(a,w)\Vdash \mathsf {A}\psi $
.
By item 5 of Definition 2.2, the statement
$(a,w)\Vdash \mathsf {A}\varphi $
implies that for each agent
$b\in Ag$
and any worlds
$u,u'\in W$
, if
$w\sim _a u$
,
$w\sim _a u'$
, and
$(b,u)\Vdash \varphi $
, then
$(b,u')\Vdash \varphi $
. Then, by the assumption of the lemma, for each agent
$b\in Ag$
and any worlds
$u,u'\in W$
, if
$w\sim _a u$
,
$w\sim _a u'$
, and
$(b,u)\Vdash \psi $
, then
$(b,u')\Vdash \psi $
. Therefore,
$(a,w)\Vdash \mathsf {A}\psi $
again by item 5 of Definition 2.2.
6 Completeness
In this section, we prove the completeness of our logical system using a canonical model construction. Usually, in modal logic, the canonical model construction defines possible worlds as maximal consistent sets. In such proofs, the truth lemma states that a formula belongs to a maximal consistent set if and only if it is satisfied at the world defined by this set. In our egocentric semantics, a formula is satisfied not at a world, but at an agent–world pair. Thus, to use the traditional approach, we must learn how to “split” a maximal consistent set into an agent and a world. How easy such a split is depends on if we require each agent to be present in each world.
In [Reference Epstein and Naumov5], the split is done by an introduction of a tree-like structure on maximal consistent sets. Then, two equivalence relations are defined on the nodes of the tree: “agent”-equivalent and “world”-equivalent. The equivalence classes of these two relations are defined to be the agents and the worlds of the model, respectively. It is then shown that each world and each agent might share at most one node of the tree. If a world and an agent are disjoint, then the agent is assumed not to be present in the world. Otherwise, the formulae in the shared node (maximal consistent set) are the formulae true about the given agent in the given world. This construction relies on the fact that not all agents are required to be present in all worlds. To the best of our knowledge, the only other work that does such a split is [Reference Grove and Halpern10], in which the authors go even further by stipulating that “each agent exists in just one world” [Reference Grove and Halpern10, Appendix D].
We think that the semantics of modality
$\mathsf {A}$
is the most natural in the setting where all agents are present in all worlds. After all, what does it mean to decide if
$\varphi $
is true about an agent which might not even exist? To guarantee that all agents are present in all worlds, in this article, we devise a matrix-based technique for constructing a canonical model.
The matrix technique is inspired by Figure 2. Note that the rows of this table represent agents and the columns represent possible worlds. The cells of the table contain sets of formulae. In our construction, we build matrices (tables) whose cells are maximal consistent sets of formulae. We interpret the rows of the matrix as agents and columns as worlds.
Instead of defining a matrix at once, we use a recursive procedure that starts with a single
$1\times 1$
matrix and adds to it either a single column or a row and a column at a time. In most cases, the final matrix is an infinite-sized matrix obtained in the limit of this recursive construction. We are not aware of a similar technique used in any other proof of completeness.
The rest of this section is structured as follows. In Section 6.1, we establish various properties of maximal consistent sets. These results are used in Section 6.2 to recursively construct a sequence of matrices. To finish the proof of completeness, in Section 6.3, we show how a matrix can be converted to a model of our logical system as specified in Definition 2.1.
6.1 Maximal consistent sets
In the standard proof of completeness for epistemic modal logic, worlds are maximal consistent sets of formulae. In such a construction, for each maximal consistent set (possible world) w and each formula
$\varphi $
such that
$\mathsf {K}\varphi \notin w$
, the proof of the completeness builds another maximal consistent set (possible word) u such that
$\neg \varphi \in u$
and worlds w and u are indistinguishable. In our work, we also have such a lemma, it’s Lemma 6.10. In conjunction with item 4 of Definition 2.2, this lemma is used in the proof of the “truth lemma,” Lemma 6.19. In addition to this, we also need another lemma that would work in a similar way for modality
$\mathsf { A}$
. Because item 5 of Definition 2.2 refers to two additional worlds, u and
$u'$
(not mentioning the agent b), the equivalent of Lemma 6.10 needs to construct two maximal consistent sets instead of one. We state this new lemma as Lemma 6.13 at the end of this section. Because the proof of Lemma 6.13 is long and non-trivial, we split it into a sequence of smaller lemmas that we present in this subsection.
Lemma 6.1. The set
$\{\neg \varphi \}\cup \{\psi \;|\; \mathsf {K}\psi \in X\}\cup \{\chi \;|\; \chi ,\mathsf {A}\chi \in X\}$
is consistent for any consistent set
$X\subseteq \Phi $
and any formula
$\varphi \in \Phi $
such that
$X\nvdash \mathsf {K}\varphi $
.
Proof Suppose the opposite. Then, there are formulae
$$ \begin{align} &\mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k\in X,\chi_1,\mathsf{A}\chi_1,\dots,\chi_\ell,\mathsf{A}\chi_\ell\in X \end{align} $$
such that
$$ \begin{align*}\psi_1,\dots,\psi_k,\chi_1,\dots,\chi_\ell\vdash \varphi.\end{align*} $$
Thus, by Lemma 4.2,
$$ \begin{align*}\mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\mathsf{K}\chi_1,\dots,\mathsf{K}\chi_\ell\vdash \mathsf{K}\varphi.\end{align*} $$
Hence, by the Self-Knowledge axiom applied
$\ell $
times,
$$ \begin{align*} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\chi_1,\mathsf{A}\chi_1,\dots,\chi_\ell,\mathsf{A}\chi_\ell\vdash \mathsf{K}\varphi. \end{align*} $$
Therefore,
$X\vdash \mathsf {K}\varphi $
by statement (6), which contradicts the assumption
$X\vdash \mathsf {K}\varphi $
of the lemma.
Definition 6.2. For any set of formulae
$X\subseteq \Phi $
and any formula
$\varphi \in \Phi $
, a (finite or infinite) sequence
$\psi _1,\psi _2,\dots $
is
$(X,\varphi )$
-regular if for each k,
$$ \begin{align*} X\nvdash \mathsf{A}(\varphi\wedge \psi_1\wedge\dots\wedge\psi_k). \end{align*} $$
Lemma 6.3. For any set of formulae
$X\subseteq \Phi $
, any formula
$\varphi \in \Phi $
such that
$X\nvdash \mathsf {A}\varphi $
, and any (finite or infinite) sequence
$\mathsf {A}\psi _1,\mathsf {A}\psi _2,\dots $
of formulae from set X, there is an
$(X,\varphi )$
-regular sequence
$\psi ^{\prime }_1,\psi ^{\prime }_2,\dots $
such that, for each
$i\ge 1$
, either
$\psi ^{\prime }_i\equiv \psi _i$
or
$\psi ^{\prime }_i\equiv \neg \psi _i$
.
Proof We prove the existence of such sequence
$\psi ^{\prime }_1,\psi ^{\prime }_2,\dots $
by constructing it recursively and simultaneously proving that statement
$$ \begin{align} X\nvdash \mathsf{A}(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k) \end{align} $$
holds after k-th step of the construction.
Base:
$k=0$
. Then, it suffices to prove that
$X\nvdash \mathsf {A}\varphi $
, which is true by an assumption of the lemma.
Step:
$k>0$
. Suppose that statement (7) holds and, at the same time,
$$ \begin{align*} &X\vdash \mathsf{A}(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1}) \;\;\mbox{ and }\\ &X\vdash \mathsf{A}(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1}). \end{align*} $$
Thus, by the Negation axiom and the Modus Ponens inference rule,
$$ \begin{align*} &X\vdash \mathsf{A}\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1}) \;\;\mbox{ and }\\ &X\vdash \mathsf{A}\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1}). \end{align*} $$
Hence, by the Conjunction axiom and propositional reasoning,
$$ \begin{align*} X\vdash \mathsf{A}(\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1})\wedge \neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1})). \end{align*} $$
Then, by the Negation axiom and the Modus Ponens inference rule,
$$ \begin{align} X\!\vdash\! \mathsf{A}\neg(\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1})\wedge \neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1})). \end{align} $$
At the same time, note that formula
$$ \begin{align*} \neg(\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1})\wedge &\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1})) \\ &\qquad\qquad\qquad \leftrightarrow \varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k \end{align*} $$
is a propositional tautology. Thus, by the Substitution inference rule,
$$ \begin{align*} X\vdash \mathsf{A}\neg(\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \psi_{k+1})\wedge &\neg(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k\wedge \neg\psi_{k+1})) \\ &\qquad\qquad\qquad\qquad\to \mathsf{A}(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k). \end{align*} $$
Hence, by statement (8) and the Modus Ponens inference rule,
$$ \begin{align*} X\vdash\mathsf{A}(\varphi\wedge \psi^{\prime}_1\wedge\dots\wedge\psi^{\prime}_k), \end{align*} $$
which contradicts our assumption that statement (7) holds.
Lemma 6.4. For any set of formulae
$X\subseteq \Phi $
, any formula
$\varphi \in \Phi $
, and any
$(X,\varphi )$
-regular sequence
$\psi _1,\psi _2,\dots $
, the set
$\{\varphi ,\psi _1,\psi _2,\dots \}$
is consistent.
Proof Suppose that the set
$\{\varphi ,\psi _1,\psi _2,\dots \}$
is inconsistent. Thus, there is
$n\ge 0$
such that
$\vdash \neg (\varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
. Then,
$\vdash \mathsf {A}\neg (\varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
by the Necessitation inference rule. Hence, by the Negation axiom and the Modus Ponens inference rule,
$$ \begin{align} \vdash \mathsf{A}\neg\neg(\varphi\wedge \psi_1\wedge \dots \wedge \psi_n). \end{align} $$
Note that
$\neg \neg (\varphi \wedge \psi _1\wedge \dots \wedge \psi _n) \leftrightarrow (\varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
is a propositional tautology. Thus,
$\vdash \mathsf {A}(\varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
by the Substitution inference rule, statement (9), and the Modus Ponens inference rule. Therefore, by Definition 6.2, the sequence
$\psi _1,\psi _2,\dots $
is not
$(X,\varphi )$
-regular, which contradicts an assumption of the lemma.
Lemma 6.5. For any set of formulae
$X\subseteq \Phi $
, any formula
$\varphi \in \Phi $
, and any
$(X,\varphi )$
-regular sequence
$\psi _1,\psi _2,\dots $
, if
$\mathsf { A}\psi _1,\dots , \mathsf {A}\psi _2,\dots \in X$
, then the set
$\{\neg \varphi ,\psi _1,\psi _2,\dots \}$
is consistent.
Proof Assume that the set
$\{\neg \varphi ,\psi _1,\psi _2,\dots \}$
is inconsistent. Thus, there is
$n\ge 0$
such that
$\vdash \neg (\neg \varphi \wedge \psi _1\wedge \cdots \wedge \psi _n)$
. Hence, by the Necessitation inference rule,
$\vdash \mathsf {A}\neg (\neg \varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
. Then,
$$ \begin{align} X\vdash \mathsf{A}(\psi_1\wedge \dots \wedge \psi_n\wedge\neg(\neg\varphi\wedge\psi_1\wedge\dots\wedge\psi_n)) \end{align} $$
by the assumption
$\mathsf {A}\psi _1,\dots , \mathsf {A}\psi _2,\dots \in X$
of the lemma, the Conjunction axiom, and propositional reasoning. Next, note that the formula
$$ \begin{align*}(\psi_1\wedge \dots \wedge \psi_n\wedge\neg(\neg\varphi\wedge\psi_1\wedge\dots\wedge\psi_n)) \leftrightarrow \varphi\wedge\psi_1\wedge \dots \wedge \psi_n \end{align*} $$
is a tautology. Thus, by the Substitution inference rule, statement (10), and the Modus Ponens inference rule,
$X\vdash \mathsf {A}(\varphi \wedge \psi _1\wedge \dots \wedge \psi _n)$
. Therefore, by Definition 6.2, the sequence
$\psi _1,\psi _2,\dots $
is not
$(X,\varphi )$
-regular, which contradicts an assumption of the lemma.
Lemma 6.6. For any maximal consistent set X and any formula
$\mathsf {A}\varphi \notin X$
, there are maximal consistent sets Y and Z such that:
-
1.
$\varphi \in Y$
,
$\neg \varphi \in Z$
. -
2.
$\psi \in Y$
iff
$\psi \in Z$
for any formula
$\mathsf {A}\psi \in X$
.
Proof The assumption of the article that the set of propositional variables is countable implies that set X is also countable. Let
$\mathsf { A}\psi _1,\mathsf {A}\psi _2,\dots $
be an enumeration of all formulae of the form
$\mathsf {A}\psi $
in set X. Then,
$X\vdash \mathsf {A}\neg \psi _i$
for each
$i\ge 1$
by the Negation axiom and the Modus Ponens inference rule. Hence, because X is a maximal consistent set,
$\mathsf { A}\neg \psi _i\in X$
for each
$i\ge 1$
. Also, recall that
$\mathsf {A}\psi _1,\mathsf {A}\psi _2,\dots $
is an enumeration of formulae from set X. Hence,
$$ \begin{align} \mathsf{A}\psi_i, \mathsf{A}\neg\psi_i\in X \;\;\;\;\;\text{for each } i\ge 1. \end{align} $$
The assumption
$\mathsf {A}\varphi \notin X$
of the lemma implies that
$X\nvdash \mathsf {A}\varphi $
because X is a maximal consistent set. Thus, by Lemma 6.3, there is an
$(X,\varphi )$
-regular sequence
$\psi ^{\prime }_1,\psi ^{\prime }_2,\dots $
such that, for each
$i\ge 1$
,
$$ \begin{align} \psi^{\prime}_i= \psi_i\text{ or }\psi^{\prime}_i= \neg\psi_i. \end{align} $$
Then, by statement (11),
$$ \begin{align} \mathsf{A}\psi^{\prime}_i\in X \text{ for each } i\ge 1. \end{align} $$
Consider the sets of formulae
$$ \begin{align} Y_0 &=\{\varphi, \psi^{\prime}_1, \psi^{\prime}_2, \dots\},\ \ \end{align} $$
$$ \begin{align} Z_0 &=\{\neg\varphi, \psi^{\prime}_1, \psi^{\prime}_2, \dots\}. \end{align} $$
Note that set
$Y_0$
is consistent by Lemma 6.4 because
$\psi ^{\prime }_1,\psi ^{\prime }_2,\dots $
is an
$(X,\varphi )$
-regular sequence. Set
$Z_0$
is consistent by Lemma 6.5, statement (13), and also because
$\psi ^{\prime }_1,\psi ^{\prime }_2,\dots $
is an
$(X,\varphi )$
-regular sequence. By Lemma 4.5, sets
$Y_0$
and
$Z_0$
can be extended to maximal consistent sets Y and Z. Note that
$\varphi \in Y_0\subseteq Y$
and
$\neg \varphi \in Z_0\subseteq Z$
by statements (14) and (15), respectively.
To finish the proof of the lemma, it suffices to show that
$\psi \in Y$
iff
$\psi \in Z$
for any formula
$\mathsf {A}\psi \in X$
. Consider an arbitrary formula
$\mathsf {A}\psi \in X$
. Because
$\mathsf {A}\psi _1,\mathsf {A}\psi _2,\dots $
is an enumeration of all formulae of the form
$\mathsf { A}\psi $
in set X, there must exist
${i_0\ge 1}$
such that
$\psi =\psi _{i_0}$
. By statement (12), either
$\psi ^{\prime }_{i_0}= \psi _{i_0}$
or
$\psi ^{\prime }_{i_0}=\neg \psi _{i_0}$
. In the first case,
$\psi =\psi _{i_0}=\psi ^{\prime }_{i_0}\in Y_0\subseteq Y$
and
$\psi =\psi _{i_0}=\psi ^{\prime }_{i_0}\in Z$
by statements (14) and (15), respectively. In the second case,
$\neg \psi =\neg\psi _{i_0}=\psi ^{\prime }_{i_0}\in Y_0\subseteq Y$
and
$\neg \psi =\neg\psi _{i_0}=\psi ^{\prime }_{i_0}\in Z_0\subseteq Z$
by statements (14) and (15), respectively. Hence,
$\psi \notin Y$
and
$\psi \notin Z$
because sets Y and Z are consistent.
6.2 Pseudo models
As discussed in the preamble to Section 6, we construct the canonical model by building a sequence of matrices of maximal consistent sets. Informally, the rows of the matrix represent the agents and the columns represent the worlds.
We assume that a matrix can have either finite or
$\omega $
-many rows and columns. We also assume that matrix rows and columns are numbered starting with
$0$
. Thus, for example, if a matrix has three rows and
$\omega $
columns, then its rows are numbered
$0$
,
$1$
, and
$2$
and its columns are numbered by
$0$
,
$1$
,
$2$
,
$\dots $
(not including
$\omega $
). In this case, we will also say that the matrix size is
$3\times \omega $
. Formally, a matrix of size
$m\times n$
is an arbitrary function defined on the Cartesian product of ordinals m and n. We say that a matrix of size
$m\times n$
is finite if ordinals m and n are finite.
Technically, the canonical model is constructed using not just matrices, but structures consisting of a matrix and row-specific equivalence relations on the columns of the matrix. We call such structures pseudo-models.
Definition 6.7. A pseudo model is a pair
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
, where:
-
1.
$(X_{ij})$
is a matrix of maximal consistent sets of formulae, -
2.
$\sim _i$
is an equivalence relation on the columns that satisfies the following conditions for each
$i_1,i_2,j_1,j_2$
:-
(a)
$\mathsf {K}\varphi \in X_{i_1j_1}$
iff
$\mathsf {K}\varphi \in X_{i_1j_2}$
, where
$j_1\sim _{i_1} j_2$
, -
(b)
$\varphi \in X_{i_2j_1}$
iff
$\varphi \in X_{i_2j_2}$
, where
$\mathsf {A}\varphi \in X_{i_1j_1}$
and
$j_1\sim _{i_1} j_2$
.
-
By the size of a pseudo model
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
we mean the size of the matrix
$(X_{ij})$
. We say that a pseudo model is finite if the matrix
$(X_{ij})$
is finite.
Definition 6.8. For any ordinals
$m,m',n,n'\le \omega $
and any two pseudo models
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
and
$\langle (X^{\prime }_{ij}),\{\sim ' _i\}_i\rangle $
of sizes
$m\times n$
and
$m'\times n'$
, respectively, let
$\langle (X_{ij}),\{\sim _i\}_i\rangle \sqsubseteq \langle (X^{\prime }_{ij}),\{\sim ' _i\}_i\rangle $
if:
-
1.
$m\le m'$
and
$n\le n'$
, -
2.
$X_{ij}=X^{\prime }_{ij}$
for each
$i< \min (m,m')$
and each
$j< \min (n,n')$
, -
3.
$j_1\sim _i j_2$
iff
$j_1\sim ^{\prime }_i j_2$
for each
$i<\min (m,m')$
and
$j_1,j_2< \min (n,n')$
,
The next three lemmas represent the base and the recursive cases of building the sequence of pseudo models discussed earlier. We start with the simplest of these lemmas that constructs the first element of the sequence.
Lemma 6.9. If
$Y\nvdash \varphi $
, then there is a finite pseudo model
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
such that
$Y\cup \{\neg \varphi \}\subseteq X_{00}$
.
Proof The set
$Y\cup \{\neg \varphi \}$
is consistent because
$Y\nvdash \varphi $
. By Lemma 4.5, it has a maximal consistent extension
$X_{00}$
. Let
$(X_{00})$
be the matrix of the size
$1\times 1$
whose only cell contains the maximal consistent set
$X_{00}$
and
$\sim _0$
be the equivalence relation
$\{(0,0)\}$
on the singleton set
$\{0\}$
. Then, the pair
$((X_{00}),\{\sim _0\})$
is a pseudo model by Definition 6.7.
The next lemma specifies one of two recursive steps in constructing the sequence of pseudo models. Recall from our earlier discussion that this lemma is an analogue of constructing a new maximal consistent set (world) in the traditional completeness proof.
Lemma 6.10. For any finite pseudo model
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
and any formula
$\varphi \in \Phi $
, if
$\mathsf {K}\varphi \notin X_{i_0j_0}$
for some
$i_0,j_0$
, then there is a finite pseudo model
$\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
such that:
-
1.
$\langle (X_{ij}),\{\sim _i\}_i\rangle \sqsubseteq \langle (X^{\prime }_{ij}),\{\sim ' _i\}_i\rangle $
, -
2.
$\neg \varphi \in X^{\prime }_{i_0j'}$
for some
$j'$
such that
$j_0\sim ^{\prime }_{i_0}j'$
.
Proof Consider the set of formulae
$$ \begin{align} Y=\{\neg\varphi\}\cup \{\psi\;|\; \mathsf{K}\psi\in X_{i_0j_0}\}\cup \{\chi\;|\; \chi,\mathsf{A}\chi\in X_{i_0j_0}\}. \end{align} $$
The assumption
$\mathsf {K}\varphi \notin X_{i_0,j_0}$
of the lemma implies that
$X_{i_0,j_0}\nvdash \mathsf {K}\varphi $
because
$X_{i_0,j_0}$
is a maximal consistent set of formula. Then, set Y is consistent by Lemma 6.1. Let
$Y'$
be the maximal consistent extension of set Y. Such an extension exists by Lemma 4.5.
Claim 6.11.
$\mathsf {K}\psi \in X_{i_0j_0}$
iff
$\mathsf {K}\psi \in Y'$
.
Proof of Claim
$(\Rightarrow )$
If
$\mathsf {K}\psi \in X_{i_0j_0}$
, then
$X_{i_0j_0}\vdash \mathsf {K}\mathsf {K}\psi $
by Lemma 4.3. Thus,
$\mathsf {K}\mathsf {K}\psi \in X_{i_0j_0}$
because
$X_{i_0j_0}$
is a maximal consistent set. Hence,
$\mathsf {K}\psi \in Y\subseteq Y'$
by equation (16) and the choice of
$Y'$
as an extension of Y.
$(\Leftarrow )$
Suppose that
$\mathsf {K}\psi \notin X_{i_0j_0}$
. Then,
$\neg \mathsf {K}\psi \in X_{i_0j_0}$
because X is a maximal consistent set of formulae. Thus,
$X_{i_0j_0}\vdash \mathsf {K}\neg \mathsf {K}\psi $
by the Negative Introspection axiom and the Modus Ponens inference rule. Hence,
$\mathsf {K}\neg \mathsf {K}\psi \in X_{i_0j_0}$
because
$X_{i_0j_0}$
is a maximal consistent set. Hence,
$\neg \mathsf {K}\psi \in Y\subseteq Y'$
by equation (16) and the choice of
$Y'$
as an extension of set Y. Therefore,
$\mathsf {K}\psi \notin Y'$
because set
$Y'$
is consistent.
Assume that the finite matrix
$(X_{ij})$
has the size
$m\times n$
. Define
$m\times (n+1)$
matrix
$$ \begin{align} (X^{\prime}_{ij})= \begin{pmatrix} X_{0,0} & \dots & X_{0,j_0} & \dots & X_{0,n-1} & X_{0,j_0}\\ \dots & \dots & \dots & \dots & \dots & \dots\\ X_{i_0-1,0} & \dots & X_{i_0-1,j_0} & \dots & X_{i_0-1,n-1} & X_{i_0-1,j_0}\\[2pt] X_{i_0,0} & \dots & X_{i_0,j_0} & \dots & X_{i_0,n-1} & Y'\\[2pt] X_{i_0+1,0} & \dots & X_{i_0+1,j_0} & \dots & X_{i_0+1,n-1} & X_{i_0+1,j_0}\\ \dots & \dots & \dots & \dots & \dots & \dots\\ X_{m-1,0} & \dots & X_{m-1,j_0} & \dots & X_{m-1,n-1} & X_{m-1,j_0} \end{pmatrix}. \end{align} $$
In addition, let the relation
$\sim ^{\prime }_{i_0}$
be the transitive, reflexive, and symmetric closure of the relation
$\sim _{i_0}\!\cup \,\{(j_0,n)\}$
on the set
$\{0,1,\dots ,n\}$
and, for
$i\neq i_0$
, relation
$\sim ^{\prime }_{i}$
be the reflexive closure of the relation
$\sim _{i}$
on the set
$\{0,1,\dots ,n\}$
.
Claim 6.12.
$\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
is a finite pseudo model.
Proof of Claim
It suffices to verify conditions 2(a) and 2(b) of Definition 6.7.
Condition 2(a). Consider any
$i,j_1,j_2$
such that
$j_1\sim ^{\prime }_i j_2$
. It suffices to show that
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{ij_2}$
for any formula
$\psi \in \Phi $
. Without loss of generality, assume that
$j_1\le j_2$
. We consider the following three cases separately:
Case 1:
$j_1\le j_2<n$
. Then,
$j_1\sim _i j_2$
by the assumption
$j_1\sim ^{\prime }_i j_2$
and the choice of the relation
$\sim ^{\prime }_i$
. Hence,
$\mathsf {K}\psi \in X_{ij_1}$
iff
$\mathsf {K}\psi \in X_{ij_2}$
by item 2(a) of Definition 6.7 and the assumption of the lemma that
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
is a pseudo model. Note also that
$X^{\prime }_{ij_1}=X_{ij_1}$
and
$X^{\prime }_{ij_2}=X_{ij_2}$
by equation (17) and the assumption
$j_1\le j_2<n$
of the case. Thus,
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{ij_2}$
.
Case 2:
$j_1=j_2=n$
. Then,
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{ij_2}$
.
Case 3:
$j_1<j_2=n$
. Then, by the choice of the relation
$\sim ^{\prime }_i$
, the assumption
$j_1\sim ^{\prime }_i j_2$
implies that
$j_1\sim _i j_0$
and
$$ \begin{align} i=i_0. \end{align} $$
Observe that
$\mathsf {K}\psi \in X_{i_0j_1}$
iff
$\mathsf {K}\psi \in X_{i_0j_0}$
by item 2(a) of Definition 6.7, the statement
$j_1\sim _i j_0$
and the assumption
$j_1<n$
of the case. Thus, it follows that
$\mathsf {K}\psi \in X^{\prime }_{i_0j_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{i_0j_0}$
by equation (17) and the assumption
$j_1<n$
. Hence,
$\mathsf {K}\psi \in X^{\prime }_{i_0j_1}$
iff
$\mathsf {K}\psi \in Y'$
by Claim 6.11. Then,
$\mathsf {K}\psi \in X^{\prime }_{i_0j_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{i_0j_2}$
by equation (17) and the assumption
$j_2=n$
of the case. Therefore,
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{ij_2}$
by equation (18).
Condition 2(b). Consider any
$i_1,i_2,j_1,j_2$
and any formula
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
such that
$j_1\sim ^{\prime }_{i_1} j_2$
. It suffices to show that
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
for any formula
$\psi \in \Phi $
. We consider the following four cases separately:
Case 1:
$j_1,j_2<n$
. Then, by equation (17), the assumption
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
implies that
$\mathsf { A}\psi \in X_{i_1j_1}$
. In addition, the assumption
$j_1\sim ^{\prime }_{i_1} j_2$
and the assumption
$j_1,j_2<n$
of the case imply that
$j_1\sim _{i_1} j_2$
. Thus,
$\psi \in X_{i_2j_1}$
iff
$\psi \in X_{i_2j_2}$
by item 2(b) of Definition 6.7. Hence,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
by equation (17) and the same assumption
$j_1,j_2<n$
of the case.
Case 2:
$j_1=j_2=n$
. Then,
$X^{\prime }_{i_2j_1}=X^{\prime }_{i_2j_2}$
. Hence,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
.
Case 3:
$j_1<j_2=n$
. Then, the assumption
$j_1\sim ^{\prime }_{i_1} j_2$
and the definition of the relation
$\sim '$
imply that
$$ \begin{align} i_0=i_1 \hspace{5mm}\text{and} \hspace{5mm} j_0\sim_{i_1} j_1. \end{align} $$
Also, the assumption
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
, by the assumption
$j_1<n$
of the case and equation (17), implies that
$$ \begin{align} \mathsf{A}\psi\in X_{i_1j_1}. \end{align} $$
We further divide this case into the following two subcases:
Subcase 3A:
$i_0=i_1=i_2$
. The statement
$\mathsf {A}\psi \in X_{i_1j_1}$
implies
$ X_{i_1j_1}\vdash \mathsf {K}\mathsf {A}\psi $
by the Introspection of Knowing All axiom. Thus,
$\mathsf {K}\mathsf {A}\psi \in X_{i_1j_1}$
because
$X_{i_1j_1}$
is a maximal consistent set. Hence,
$\mathsf {K}\mathsf {A}\psi \in X_{i_1j_0}$
by item 2(a) of Definition 6.7 and part
$j_0\sim _{i_1} j_1$
of statement (19). Then,
$X_{i_1j_0}\vdash \mathsf {A}\psi $
by the Truth axiom and the Modus Ponens inference rule. Thus, because
$X_{i_1j_0}$
is a maximal consistent set,
$$ \begin{align} \mathsf{A}\psi\in X_{i_1j_0}. \end{align} $$
Hence,
$\psi \in X_{i_1j_0}$
iff
$\psi \in X_{i_1j_1}$
by item 2(b) of Definition 6.7 and the part
$j_0\sim _{i_1} j_1$
of statement (19). Then,
$\psi \in X_{i_1j_0}$
iff
$\psi \in X^{\prime }_{i_1j_1}$
by the assumption
$j_1<n$
of the case and equation (17). Thus,
$\psi \in X_{i_1j_0}$
iff
$\psi \in X^{\prime }_{i_2j_1}$
by the assumption
$i_1=i_2$
of the subcase.
Recall that we are proving that
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
. Then, it suffices to show that
$\psi \in X_{i_1j_0}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
. Furthermore, due to the assumption
$i_1=i_2$
of the subcase, it is enough to prove that
$\psi \in X_{i_1j_0}$
iff
$\psi \in X^{\prime }_{i_1j_2}$
. Finally, due to equation (17), the assumption
$j_2=n$
of the case, and part
$i_0=i_1$
of statement (19), it suffices to show that
$\psi \in X_{i_1j_0}$
iff
$\psi \in Y'$
.
We show the two parts of this biconditional statement separately:
Assume
$\psi \in X_{i_1j_0}$
. Thus,
$\psi , \mathsf {A}\psi \in X_{i_1j_0}$
due to statement (21). Hence,
$\psi , \mathsf {A}\psi \in X_{i_0j_0}$
by part
$i_0=i_1$
of statement (19). Then,
$\psi \in Y\subseteq Y'$
by equation (16).
Next, suppose
$\psi \notin X_{i_1j_0}$
. Then,
$\neg \psi \in X_{i_1j_0}$
because
$X_{i_1j_0}$
is a maximal consistent set. At the same time,
$X_{i_1j_0}\vdash \mathsf {A}\neg \psi $
by statement (21), the Negation axiom, and the Modus Ponens inference rule. Hence,
$\mathsf { A}\neg \psi \in X_{i_1j_0}$
because
$X_{i_1j_0}$
is a maximal consistent set. Thus,
$\neg \psi , \mathsf {A}\neg \psi \in X_{i_1j_0}$
. Then,
$\neg \psi , \mathsf {A}\neg \psi \in X_{i_0j_0}$
by part
$i_0=i_1$
of statement (19). Hence,
$\neg \psi \in Y\subseteq Y'$
by equation (16).
Subcase 3B:
$i_0=i_1\neq i_2$
. By part 2(b) of Definition 6.7 and part
$j_0\sim _{i_1} j_1$
of statement (19), statement (20) implies that
$\psi \in X_{i_2j_1}$
iff
$\psi \in X_{i_2j_0}$
. Then,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X_{i_2j_0}$
by equation (17) and the assumption
$j_1<n$
of the case. Hence,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2n}$
by equation (17). Therefore,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
by the assumption
$j_2=n$
of the case.
Case 4:
$j_2<j_1=n$
. Then, the assumption
$j_1\sim ^{\prime }_{i_1} j_2$
and the definition of the relation
$\sim '$
imply that
$$ \begin{align} i_0=i_1 \hspace{5mm}\text{and} \hspace{5mm} j_0\sim_{i_0} j_2. \end{align} $$
Then,
$\mathsf {A}\psi \in X^{\prime }_{i_0j_1}$
by the assumption
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
. Hence,
$X^{\prime }_{i_0j_1}\vdash \mathsf {K}\mathsf {A}\psi $
by the Introspection of Knowing All axiom and the Modus Ponens inference rule. Thus,
$\mathsf {K}\mathsf {A}\psi \in X^{\prime }_{i_0j_1}$
because
$X^{\prime }_{i_0j_1}$
is a maximal consistent sets. Then,
$\mathsf {K}\mathsf {A}\psi \in X^{\prime }_{i_0n}$
by the assumption
$j_1=n$
of the case. Hence,
$\mathsf {K}\mathsf {A}\psi \in Y'$
by equation (17). Then,
$\mathsf {K}\mathsf {A}\psi \in X_{i_0j_0}$
by Claim 6.11. Thus,
$\mathsf {K}\mathsf {A}\psi \in X_{i_0j_2}$
by item 2(a) of Definition 6.7 and the part
$j_0\sim _{i_0} j_2$
of statement (22). Hence,
$\mathsf {K}\mathsf {A}\psi \in X_{i_1j_2}$
by the part
$i_0=i_1$
of statement (22). Then,
$X_{i_1j_2}\vdash \mathsf {A}\psi $
by the Truth axiom and the Modus Ponens inference rule. Thus, because
$X_{i_1j_2}$
is a maximal consistent set,
$$ \begin{align} \mathsf{A}\psi\in X_{i_1j_2}. \end{align} $$
From this point, the proof continues the same way as in Case 3, except that
$j_1$
plays the role of
$j_2$
and
$j_2$
plays the role of
$j_1$
. In addition, we use statements (22) and (23) instead of statements (19) and (20), respectively. This concludes the proof of the claim.
To finish the proof of the lemma, note that, by equation (17) and the definition of relation
$\sim '$
, we have
$\langle (X_{ij}),\{\sim_i\}_i\rangle\sqsubseteq \langle (X'_{ij}),\{\sim'_i\}_i\rangle $
. Also,
$\neg \psi \in Y\subseteq Y'=X^{\prime }_{i_0n}$
by equations (16) and (17).
Next is the last of the three lemmas capturing the recursive construction of a sequence of pseudo models. This lemma extends the sequence when formula
$\mathsf {A}\varphi $
does not belong to some maximal consistent set.
As usual in set theory, by
$X\,\triangle \,Y$
we denote the symmetric difference of sets X and Y. For example,
$\{1,2\}\,\triangle \,\{2,3\}=\{1,3\}$
.
Lemma 6.13. For any finite pseudo model
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
and any formula
$\varphi \in \Phi $
, if
$\mathsf {A}\varphi \notin X_{i_0j_0}$
for some
$i_0,j_0$
, then there is a finite pseudo model
$\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
such that:
-
1.
$\langle (X_{ij}),\{\sim _i\}_i\rangle \sqsubseteq \langle (X^{\prime }_{ij}),\{\sim ' _i\}_i\rangle $
, -
2. for some
$i_1,j_1$
such that
$j_0\sim _{i_0}j_1$
and
$\varphi \in X^{\prime }_{i_1j_0}\,\triangle \, X^{\prime }_{i_1j_1}$
.
Proof By Lemma 6.6, the assumption
$\mathsf {A}\varphi \notin X_{i_0j_0}$
implies that there are maximal consistent sets Y and Z such that
$$ \begin{align} &\varphi\in Y\hspace{3mm}\text{and}\hspace{3mm} \neg\varphi\in Z,\qquad\qquad\quad\qquad\qquad\qquad \end{align} $$
$$ \begin{align} &\psi\in Y\hspace{3mm}\text{iff}\hspace{3mm}\psi\in Z \hspace{3mm}\text{for any formula}\hspace{1mm} \mathsf{A}\psi\in X_{i_0j_0}. \end{align} $$
Assume that matrix
$(X_{ij})$
has the size
$m\times n$
. Define
$(m+1)\times (n+1)$
matrix
$$ \begin{align} (X^{\prime}_{ij})= \begin{pmatrix} X_{0,0} & \dots & X_{0,j_0} & \dots & X_{0,n-1} & X_{0,j_0}\\ \dots & \dots & \dots & \dots & \dots & \dots\\ X_{i_0-1,0} & \dots & X_{i_0-1,j_0} & \dots & X_{i_0-1,n-1} & X_{i_0-1,j_0}\\[2pt] X_{i_0,0} & \dots & X_{i_0,j_0} & \dots & X_{i_0,n-1} & X_{i_0,j_0}\\[2pt] X_{i_0+1,0} & \dots & X_{i_0+1,j_0} & \dots & X_{i_0+1,n-1} & X_{i_0+1,j_0}\\ \dots & \dots & \dots & \dots & \dots & \dots\\ X_{m-1,0} & \dots & X_{m-1,j_0} & \dots & X_{m-1,n-1} & X_{m-1,j_0}\\[2pt] Y & \dots & Y & \dots & Y & Z \end{pmatrix}. \end{align} $$
In addition, let the relation
$\sim ^{\prime }_{i_0}$
be the transitive, reflexive, and symmetric closure of the relation
$\sim _{i_0}\!\cup \, \{(j_0,n)\}$
on the set
$\{0,1,\dots ,n\}$
. Let
$\sim ^{\prime }_{m}$
be the reflexive closure of the empty relation. Finally for
$i\notin \{i_0,m\}$
, let the relation
$\sim ^{\prime }_{i}$
be the reflexive closure of the relation
$\sim _{i}$
on the set
$\{0,1,\dots ,n\}$
.
Observe that, for any formula
$\psi \in \Phi $
,
$$ \begin{align} \psi\in X_{i_0j_0}\hspace{2mm}\text{iff}\hspace{2mm}\psi\in X^{\prime}_{i_0n} \end{align} $$
because sets
$X_{i_0j_0}$
and
$X^{\prime }_{i_0n}$
are equal by equation (26).
Claim 6.14.
$\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
is a finite pseudo model.
Proof of Claim
It suffices to verify conditions 2(a) and 2(b) of Definition 6.7.
Condition 2(a). Consider any
$i,j_1,j_2$
such that
$j_1\sim ^{\prime }_i j_2$
. It suffices to show that
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf { K}\psi \in X^{\prime }_{ij_2}$
for any formula
$\psi \in \Phi $
.
If
$i=m$
, then the assumption
$j_1\sim ^{\prime }_i j_2$
implies that
$j_1=j_2$
by the definition of the relation
$\sim ^{\prime }_m$
. Hence,
$\mathsf {K}\psi \in X^{\prime }_{ij_1}$
iff
$\mathsf {K}\psi \in X^{\prime }_{ij_2}$
. If
$i<m$
, then the proof is the same as the proof of Condition 2(a) in Claim 6.12 except that instead of Claim 6.11 it uses statement (27).
Condition 2(b). Consider any
$i_1,i_2,j_1,j_2$
and any formula
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
such that
$j_1\sim ^{\prime }_{i_1} j_2$
. It suffices to show that
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
. We consider the following four cases separately:
Case 1:
$j_1,j_2<n$
. If
$i_2=m$
, then
$X^{\prime }_{i_2j_1} = Y=X^{\prime }_{i_2j_2}$
by equation (26). Hence,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
. If
$i_2<m$
, then the proof is the same as the proof in Case 1 of Condition 2(b) in Claim 6.12.
Case 2:
$j_1=j_2=n$
. Then,
$X^{\prime }_{i_2j_1}=X^{\prime }_{i_2j_2}$
. Hence,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
.
Case 3:
$j_1<j_2=n$
. Then, the assumption
$j_1\sim ^{\prime }_{i_1} j_2$
and the definition of the relation
$\sim '$
imply that
$$ \begin{align} i_0=i_1 \hspace{5mm}\text{and} \hspace{5mm} j_0\sim_{i_1} j_1. \end{align} $$
Also, the assumption
$\mathsf {A}\psi \in X^{\prime }_{i_1j_1}$
, by the assumption
$j_1<n$
of the case and equation (26), implies that
$$ \begin{align} \mathsf{A}\psi\in X_{i_1j_1}. \end{align} $$
We further divide this case into the following two subcases:
Subcase 3A:
$i_2 \neq m$
. Then,
$\psi \in X_{i_2j_1}$
iff
$\psi \in X_{i_2j_0}$
by item 2(b) of Definition 6.7 and statements (28) and (29). Hence, by equation (26), the assumption
$i_2\neq m$
of the subcase, and the assumption
$j_1<n$
of the case,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_n}$
. Thus,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
by the assumption
$j_2=n$
of the case.
Subcase 3B:
$i_2=m$
. Note that
$\mathsf {A}\psi \in X_{i_0j_1}$
by statement (29) and the part
$i_0=i_1$
of statement (28). Thus,
$X_{i_0j_1}\vdash \mathsf {K}\mathsf {A}\psi $
by the Introspection of Knowing All axiom and the Modus Ponens inference rule. Hence, because
$X_{i_0j_1}$
is a maximal consistent set,
$\mathsf {K}\mathsf {A}\psi \in X_{i_0j_1}$
. Then,
$\mathsf {K}\mathsf {A}\psi \in X_{i_0j_0}$
by part 2(a) of Definition 6.7 and both parts of statement (28). Hence,
$X_{i_0j_0}\vdash \mathsf {A}\psi $
by the Truth axiom and the Modus Ponens inference rule. Thus,
$\mathsf {A}\psi \in X_{i_0j_0}$
because
$X_{i_0j_0}$
is a maximal consistent set. Then,
$\psi \in Y$
iff
$\psi \in Z$
by statement (25). Therefore,
$\psi \in X^{\prime }_{i_2j_1}$
iff
$\psi \in X^{\prime }_{i_2j_2}$
by equation (26), the assumption
$i_2=m$
of the subcase, and the assumption
$j_1<j_2=n$
of the case.
Case 4:
$j_2<j_1=n$
. Similar to how we proved statements (22) and (23) in Case 4 of the proof of Claim 6.12, we can show that
$$ \begin{align} &i_0=i_1 \hspace{5mm}\text{and} \hspace{5mm} j_0\sim_{i_0} j_2, \end{align} $$
$$ \begin{align} &\mathsf{A}\psi\in X_{i_1j_1}.\qquad\qquad\qquad \end{align} $$
From this point, the proof continues the same way as in Case 3 of the current proof, except that
$j_1$
plays the role of
$j_2$
and
$j_2$
plays the role of
$j_1$
. In addition, we use statements (30) and (31) instead of statements (28) and (29), respectively. This concludes the proof of the claim.
To finish the proof of the lemma, note that item 1 of this lemma is true by the choice of the pseudo model
$\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
. To prove item 2, observe that
$\varphi \in Y\,\triangle \, Z$
by statement (24). Thus,
$\varphi \in X^{\prime }_{mj_0}\,\triangle \, X^{\prime }_{mn}$
by equation (26). Also, recall that
$j_0\sim ^{\prime }_{i_0}n$
by the definition of relation
$\sim '$
.
The previous lemma concludes the description of the three steps of the recursive construction of a sequence of pseudo models. The next definition captures the property of the pseudo model at which the construction terminates after a finite number of steps or, as we will see later, the property of the pseudo model obtained at the limit of the construction.
Definition 6.15. A pseudo model
$\langle (X_{ij}),\{\sim _i\}_i\rangle $
is closed when for any formula
$\varphi \in \Phi $
and any indices
$i_0,j_0$
,
-
1. if
$\neg \mathsf {K}\varphi \in X_{i_0j_0}$
, then there is an index
$j_1$
such that
$j_0\sim _{i_0}j_1$
and
$\neg \varphi \in X_{i_0j_1}$
, -
2. if
$\neg \mathsf {A}\varphi \in X_{i_0j_0}$
, then there are indices
$i_1,j_1$
such that
$j_0\sim _{i_0}j_1$
and
$\varphi \in X_{i_1j_0}\,\triangle \, X_{i_1j_1}$
.
For any sequence of pairs of sets
$(S_0,T_0),(S_1,T_1),(S_2,T_2),\dots $
, by union
$\bigcup _i(S_i,T_i)$
we mean the pair
$(\bigcup _i S_i,\bigcup _i T_i)$
. Recall that, formally, by a matrix of size
$m\times n$
we mean a function defined on the Cartesian product of ordinals m and n. Note that a family of equivalence relations
$\{\sim _i\}_i$
can also be viewed as a function that assigns a relation
$\sim _i$
to each index i. Hence, any pseudo model is a pair of functions. Thus, keeping in mind that functions (as all relations) are sets, for any sequence
$M_0,M_1,M_2,\dots $
of pseudo models, one can consider the union
$\bigcup _i M_i$
.
Lemma 6.16. For any infinite chain
$M_0\sqsubseteq M_1\sqsubseteq M_2\sqsubseteq \dots $
of pseudo models,
$\bigcup _i M_i$
is a pseudo model and
$M_i\sqsubseteq \bigcup _i M_i$
.
Lemma 6.17. For any finite pseudo model M there is a closed (possibly infinite) pseudo model
$M'$
such that
$M\sqsubseteq M'$
.
Proof Let
$(i_1,j_1,\sigma _1),\dots , (i_k,j_k,\sigma _k),\dots $
be any enumeration of all such triples that
$i_k$
and
$j_k$
are non-negative integers and
$\sigma _k$
is a formula of the form either
$\mathsf {K}\psi $
or
$\mathsf {A}\psi $
. Construct an infinite chain of pseudo models
$M_0\sqsubseteq M_1\sqsubseteq M_2\sqsubseteq \dots $
using the following infinite recursive procedure:
Base Case: Let
$M_0=M$
. Label all elements of the sequence
$(i_1,j_1,\sigma _1)$
, …,
$(i_k,j_k,\sigma _k),\dots $
as “unfulfilled.”
Recursive Step: Suppose that chain
$M_0\sqsubseteq M_1\sqsubseteq M_2\sqsubseteq M_{k-1}$
is constructed and some of the elements of the sequence
$(i_1,j_1,\sigma _1)$
, …,
$(i_k,j_k,\sigma _k),\dots $
are already labeled as “fulfilled.”
Do the following steps to construct pseudo model
$M_k$
:
-
1. Consider the smallest
$\ell $
such that model
$M_{k-1}$
contain cells
$(i_\ell ,j_\ell )$
, the element
$(i_\ell ,j_\ell ,\sigma _\ell )$
is labeled as “unfulfilled,” and
$\sigma _\ell \notin X_{i_\ell ,j_\ell }$
. If such
$\ell $
does not exist, define
$M_{k}=M_{k-1}$
and skip the next two steps. -
2. Use either Lemma 6.10 (when
$\sigma _\ell $
has the form
$\mathsf {K}\psi $
) or Lemma 6.13 (when formula
$\sigma _\ell $
has the form
$\mathsf {A}\psi $
) to extend the pseudo model
$M_{k-1}$
to a new pseudo model
$M_{k}$
. -
3. Label the element
$(i_\ell ,j_\ell ,\sigma _\ell )$
as “fulfilled.”
Let
$M'= \bigcup _i M_i$
. Note that
$M'$
is a pseudo model by Lemma 6.16. Pseudo model
$M'$
is closed by Definition 6.15.
6.3 Completeness: final steps
So far, we have discussed pseudo models of our logical system. We are now ready to describe how any closed pseudo model can be converted into a model as described in Definition 2.1.
Definition 6.18. For any pseudo model
$M=\langle (X_{ij}),\{\sim _i\}_i\rangle $
, where
$(X_{ij})$
is a (possibly infinite) matrix of size
$m\times n$
, let
$M^*$
be the epistemic model
$$ \begin{align*}(\{i\in \omega\;|\;i<m\}, \{j\in \omega\;|\;j<n\},\{\sim_i\}_i,\pi),\end{align*} $$
where
$\pi (p)$
is equal to the set
$\{(i,j)\;|\; i<m, j<n, p\in X_{ij}\}$
for each propositional variable p.
The next lemma connects a closed pseudo model M with the corresponding epistemic model
$M^*$
.
Lemma 6.19. For any closed pseudo model
$M=\langle (X_{ij}),\{\sim _i\}_i\rangle $
and any formula
$\varphi \in \Phi $
, if
$\Vdash $
is the satisfaction relation for the epistemic model
$M^*$
, then
$(i,j)\Vdash \varphi $
iff
$\varphi \in X_{ij}$
for all
$i,j$
.
Proof We prove the statement of the lemma by structural induction on the formula
$\varphi $
.
Suppose that formula
$\varphi $
is a propositional variable p. Then,
$(i,j)\Vdash p$
iff
$(i,j)\in \pi (p)$
by item 1 of Definition 2.2. At the same time,
$(i,j)\in \pi (p)$
iff
$p\in X_{ij}$
by Definition 6.18.
If formula
$\varphi $
is a negation or an implication, then the statement of the lemma follows from the induction hypothesis, Definition 2.2, and the assumption that
$X_{ij}$
is a maximal consistent set in the standard way.
Suppose that formula
$\varphi $
has the form
$\mathsf {K}\psi $
.
$(\Rightarrow ):$
Assume that
$\mathsf {K}\psi \notin X_{ij}$
. Thus,
$\neg \mathsf {K}\psi \in X_{ij}$
because
$X_{ij}$
is a maximal consistent set. Then, by the assumption of the lemma that model M is closed and item 1 of Definition 6.15, there exists an index
$j'$
such that
$j\sim _{i}j'$
and
$\neg \varphi \in X_{ij'}$
. Thus,
$\psi \notin X_{ij'}$
because the set
$X_{ij'}$
is consistent. Hence,
$(i,j')\nVdash \psi $
by the induction hypothesis. Therefore,
$(i,j)\nVdash \mathsf {K}\psi $
by item 4 of Definition 2.2 and the statement
$j\sim _{i}j'$
.
$(\Leftarrow ):$
Suppose that
$\mathsf {K}\psi \in X_{ij}$
. Consider any
$j'$
such that
$j\sim _i j'$
. By item 4 of Definition 2.2, it suffices to show that
$(i,j')\Vdash \psi $
. Indeed, the assumptions
$\mathsf {K}\psi \in X_{ij}$
and
$j\sim _i j'$
, by item 2(a) of Definition 6.7, imply that
$\mathsf {K}\psi \in X_{ij'}$
. Hence,
$X_{ij'}\vdash \psi $
by the Truth axiom and the Modus Ponens inference rule. Thus,
$\psi \in X_{ij'}$
because
$X_{ij'}$
is a maximal consistent set. Therefore, by the induction hypothesis,
$(i,j')\nVdash \psi $
.
Suppose that formula
$\varphi $
has the form
$\mathsf {A}\psi $
.
$(\Rightarrow ):$
The assumption
$\mathsf {A}\psi \notin X_{ij}$
implies
$\neg \mathsf {A}\psi \in X_{ij}$
because
$X_{ij}$
is a maximal consistent set. Hence, by the assumption of the lemma that pseudo model M is closed and item 2 of Definition 6.15, there is an agent
$i'$
and a world
$j'$
such that
$j\sim _i j'$
and
$\psi \in X_{i'j}\,\triangle \, X_{i'j'}$
. Thus, by the induction hypothesis, exactly one of the following statements is true:
$(i',j)\Vdash \psi $
or
$(i',j')\Vdash \psi $
. Then,
$(i,j)\nVdash \mathsf {A}\psi $
by the assumption
$j\sim _i j'$
and item 5 of Definition 2.2.
$(\Leftarrow ):$
Let
$\mathsf {A}\psi \in X_{ij}$
. Towards the proof of
$(i,j)\Vdash \mathsf {A}\psi $
, consider an arbitrary agent
$i'$
and arbitrary worlds
$j',j"$
such that
$j\sim _i j'$
,
$j\sim _i j"$
, and
$(i',j')\Vdash \psi $
. By item 5 of Definition 2.2, it suffices to show that
$(i',j")\Vdash \psi $
.
First, by the induction hypothesis, the assumption
$(i',j')\Vdash \psi $
implies
$\psi \in X_{i'j'}$
. Thus, by item 2(b) of Definition 6.7, the assumption
$\mathsf {A}\psi \in X_{ij}$
and the assumption
$j\sim _i j'$
imply that
$\psi \in X_{i'j}$
.
Second, again by item 2(b) of Definition 6.7, the assumption
$\mathsf {A}\psi \in X_{ij}$
and the assumption
$j\sim _i j"$
imply that
$\psi \in X_{i'j"}$
. Therefore,
$(i',j")\Vdash \psi $
by the induction hypothesis.
We are now ready to state and prove the strong completeness theorem for our logical system.
Theorem 6.20. For any set of formulae
$Y\subseteq \Phi $
and any formula
$\varphi \in \Phi $
, if
$Y\nvdash \varphi $
, then there is an agent a and a world w of an epistemic model such that
$(a,w)\Vdash \gamma $
for each
$\gamma \in Y$
and
$(a,w)\nVdash \varphi $
.
Proof By Lemma 6.9, there is a finite pseudo model
$M=\langle (X_{ij}),\{\sim _i\}_i\rangle $
such that
$Y\cup \{\neg \varphi \}\subseteq X_{00}$
. By Lemma 6.17, there is a closed pseudo model
$M'=\langle (X^{\prime }_{ij}),\{\sim ^{\prime }_i\}_i\rangle $
such that
$M\sqsubseteq M'$
. Note that
$X_{00}=X^{\prime }_{00}$
by item 2 of Definition 6.8. Hence,
$Y\cup \{\neg \varphi \}\subseteq X^{\prime }_{00}$
. Thus,
$\gamma \in X^{\prime }_{00}$
for each formula
$\gamma \in Y$
and, because set
$X^{\prime }_{00}$
is consistent,
$\varphi \notin X^{\prime }_{00}$
. Therefore,
$(0,0)\Vdash \gamma $
for each
$\gamma \in Y$
and
$(0,0)\nVdash \varphi $
in epistemic model
$M^*$
by Lemma 6.19.
7 Decidability
In this section, we prove the decidability of our logical system. The standard way to show decidability in modal logic is to prove completeness with respect to the class of finite models. This usually can be done using the filtration technique in one of two ways: on-the-fly filtration or post-filtration. The on-the-fly filtration restricts formulae in all maximal consistent sets to subformulae of a given formula. This technique is often more efficient, but it only proves completeness instead of strong completeness. Post-filtration is applied after strong completeness is shown. It consists of collapsing the infinite model into a finite one by merging “similar” possible worlds.
It appears that our matrix construction is too complex for either an on-the-fly filtration or a post-filtration to be feasible. Instead, we use a different approach suggested by an anonymous reviewer. We introduce neighborhood semantics for our logic which is very different and is much simpler than the one given in Definitions 2.1 and 2.2. Then, we use on-the-fly filtration to show the completeness of our logical system with respect to the class of finite neighborhood models. Note that, unlike our original semantics, the neighborhood semantics does not capture the intended meaning of modality
$\mathsf {A}$
as “know how to tell apart.” This semantics is only used to prove the decidability of our logical system. Because strong completeness is not required to prove decidability, the fact that we do not show strong completeness for the neighborhood semantics is not significant.
7.1 Neighborhood semantics
In this subsection, we define a new and simple semantics for our logical system. As described above, this semantics will be used later to prove the decidability of the system. By
$\mathcal {P}(X)$
we denote the power set of set X.
Definition 7.1. A neighborhood model is a tuple
$(W,\sim ,\{\mathcal {N}_w\}_{w\in W},\pi )$
, where:
-
1. W is a (possibly empty) set of worlds,
-
2.
$\sim $
is an equivalence relation on set W, -
3.
$\mathcal {N}_w\subseteq \mathcal {P}(W)$
is a family of “neighborhoods” of world
$w\in W$
such that:-
(a)
$W\in \mathcal {N}_w$
for each world
$w\in W$
, -
(b)
$X\cap Y\in \mathcal {N}_w$
for any world
$w\in W$
and any
$X,Y\in \mathcal {N}_w$
, -
(c)
$W\setminus X\in \mathcal {N}_w$
for any world
$w\in W$
and any
$X\in \mathcal {N}_w$
, -
(d)
$\mathcal {N}_w=\mathcal {N}_u$
for any worlds
$w,u\in W$
such that
$w\sim u$
, -
(e) if
$w\in X$
,
$X\in \mathcal {N}_{w}$
, and
$w\sim u$
, then
$u\in X$
,
-
-
4.
$\pi (p)\subseteq W$
for each propositional variable p.
Definition 7.2. For any formula
$\varphi \in \Phi $
and any world
$w\in W$
of a neighborhood model
$(W,\sim ,\{\mathcal {N}_w\}_{w\in W},\pi )$
, the satisfaction relation
$w\Vdash \varphi $
is defined as follows:
-
1.
$w\Vdash p$
if
$w\in \pi (p)$
. -
2.
$w\Vdash \neg \varphi $
if
$w\nVdash \varphi $
. -
3.
$w\Vdash \varphi \to \psi $
if either
$w\nVdash \varphi $
or
$w\Vdash \psi $
. -
4.
$w\Vdash \mathsf {K}\varphi $
if
$u\Vdash \varphi $
for each world
$u\in W$
such that
$u\sim w$
. -
5.
$w\Vdash \mathsf {A}\varphi $
if
$\{u\in W\;|\;u\Vdash \varphi \}\in \mathcal {N}_w$
.
The proof of the next theorem is straightforward.
Theorem 7.3 (Soundness).
If
$\vdash \varphi $
, then
$w\Vdash \varphi $
for each world
$w\in W$
of each neighborhood model
$(W,\sim ,\{\mathcal {N}_w\}_{w\in W},\pi )$
.
7.2 Capturing sets
In the next several subsections, we prove the completeness of our logical system with respect to neighborhood semantics. Towards this proof, in this subsection, we introduce the notion of capturing sets. This notion will be used in the next subsection to define the worlds of the canonical neighborhood model. Informally, a set of formulae Y captures a set of formulae X if set Y is at least as expressive as set X.
Definition 7.4. A set
$Y\subseteq \Phi $
captures a set
$X\subseteq \Phi $
, written as
$X\preceq Y$
, if for each formula
$\chi \in X$
, there is a formula
$\gamma \in Y$
such that
$\vdash \chi \leftrightarrow \gamma $
.
It is easy to see that
$\preceq $
is a reflexive and transitive relation on
$\mathcal {P}(\Phi )$
. More importantly, it has the following right upward monotonicity property:
Lemma 7.5. If
$X\preceq Y$
and
$Y\subseteq Z$
, then
$X\preceq Z$
.
Definition 7.6. For any set of formula X, let
$\widehat {X}$
be the set of all Boolean combinations of formulae from X.
Let us now consider arbitrary Boolean expressions built from a fixed finite set of propositional variables
$x_1,\dots ,x_n$
. Although there are infinitely many such expressions, there are only
$2^{2^n}$
Boolean functions that these expressions represent. Any two Boolean expressions that represent the same Boolean function must be provably equivalent in propositional logic due to the completeness theorem for propositional calculus. Thus, one can identify a “basis” of
$2^{2^n}$
Boolean expressions such that all Boolean expressions are propositionally equivalent to one of the expressions in the basis.
We will now apply the observation from the previous paragraph to an arbitrary finite set X of formulae in language
$\Phi $
. We can think of formulae in X as atomic propositions. Formulae in set
$\widehat {X}$
are arbitrary Boolean combinations of these atomic propositions. Thus, set
$\widehat {X}$
must contain a finite subset (basis) Y such that each formula in set
$\widehat {X}$
is provably equivalent to one of the formulae in Y. Note that “provably” here refers to provability from tautologies using the Modus Ponens inference rule only. However, such provability implies provability in our logical system. Thus, the following lemma holds.
Lemma 7.7. For any finite set X, there is a finite set Y such that
$\widehat {X}\preceq Y$
.
In other words, if set X is finite, then the (infinite!) set
$\widehat {X}$
can be captured by some finite set.
7.3 Canonical model
In this subsection, for any nonempty finite set
$\Gamma $
of formulae, we construct a finite canonical neighborhood model. The model is finite in the sense that the set of possible worlds is finite. This implies that all neighborhoods and all sets of neighborhoods are also finite.
By Lemma 7.7, there is a finite set
$\Gamma _1$
such that
$\widehat {\Gamma }\preceq \Gamma _1$
. By Lemma 7.5, we can assume that
$\Gamma \subseteq \Gamma _1$
. By Definition 7.4, for any formula
$\gamma \in \widehat {\Gamma }$
there is a formula
$\gamma ^*\in \Gamma _1$
such that
$$ \begin{align} \vdash \gamma \leftrightarrow\gamma^*. \end{align} $$
Throughout the rest of this section, we fix a specific function
$*:\widehat {\Gamma }\to \Gamma _1$
that satisfies statement (32). The next lemma follows from statement (32) and the Substitution inference rule.
Lemma 7.8.
$\vdash \mathsf {A}\gamma \leftrightarrow \mathsf {A}(\gamma ^*)$
for any formula
$\gamma \in \widehat {\Gamma }$
.
Definition 7.9.
$ \Gamma _2=\Gamma _1\cup \{\mathsf {A}\gamma ,\neg \mathsf {A}\gamma ,\mathsf {K}\gamma ,\neg \mathsf {K}\gamma , \neg \gamma \;|\;\gamma \in \Gamma _1\} $
.
Definition 7.10.
W is the set of maximal consistent subsets of set
$\Gamma _2$
.
Note that sets
$\Gamma _2$
and W are finite due to set
$\Gamma _1$
being finite.
Usually, in canonical models for epistemic logics, two worlds are called indistinguishable if they contain the same
$\mathsf {K}$
-formulae. If the indistinguishable worlds are maximal consistent sets of formulae, then the Introspection of Knowing All axiom and the Truth axiom would imply that these sets will also have the same
$\mathsf {A}$
-formulae. Indeed, if one world contains a formula
$\mathsf {A}\varphi $
, then, by the Introspection of Knowing All axiom, it also contains formula
$\mathsf {K}\mathsf {A}\varphi $
. Then, the other world contains a formula
$\mathsf { K}\mathsf {A}\varphi $
and, by the Truth axiom, it also contains the formula
$\mathsf {A}\varphi $
. However, because we are constructing a finite model, we define the worlds as maximal consistent subsets of
$\Gamma _2$
. As a result, formula
$\mathsf {K}\mathsf {A}\varphi $
, from the above argument, might not belong to a world even if formula
$\mathsf {A}\varphi $
does. To account for this, we add item 2 to the definition below.
Definition 7.11. For any worlds
$w,u\in W$
, let
$w\sim u$
when for each formula
$\gamma \in \Gamma _1$
,
-
1.
$\mathsf {K}\gamma \in w$
iff
$\mathsf {K}\gamma \in u$
, -
2.
$\mathsf {A}\gamma \in w$
iff
$\mathsf {A}\gamma \in u$
.
We now proceed to define the families of neighborhoods
$\mathcal {N}_w$
. We start by defining a neighborhood
$N(\gamma )\subseteq W$
for each formula
$\gamma \in \Gamma _1$
. After that, we specify to which of the families each neighborhood belongs to.
Definition 7.12.
$N(\gamma )=\{w\in W\;|\;\gamma \in w\}$
for any formula
$\gamma \in \Gamma _1$
.
Definition 7.13.
$\mathcal {N}_w=\{N(\gamma )\;|\;\gamma \in \Gamma _1, \mathsf {A}\gamma \in w\}$
.
Intuitively, the above definition is chosen to match Definition 7.12 and item 5 of Definition 7.2.
Definition 7.14.
$$ \begin{align*}\pi(p)= \begin{cases} N(p), & \mbox{if } p\in \Gamma,\\ \varnothing, & \mbox{otherwise}. \end{cases} \end{align*} $$
7.4 Properties of neighborhoods
In the previous subsection, we have defined the canonical neighborhood model. In the next subsection, we show that it satisfies properties 3(a)–(e) of Definition 7.1. Towards this goal, in this subsection, we establish three auxiliary properties of the neighborhoods.
Lemma 7.15.
$(\gamma \to \gamma )^*\in \Gamma _1$
and
$N((\gamma \to \gamma )^*)=W$
for any
$\gamma \in \Gamma $
.
Proof Note that
$\gamma \to \gamma \in \widehat {\Gamma }$
by Definition 7.6. Hence,
$(\gamma \to \gamma )^*\in \Gamma _1$
because function
$*$
maps set
$\widehat {\Gamma }$
into set
$\Gamma _1$
.
To prove the other part of the lemma, consider any world
$w\in W$
. It suffices to show that
$w\in N((\gamma \to \gamma )^*)$
. Indeed,
$\gamma \to \gamma $
is a tautology. Thus,
$\vdash (\gamma \to \gamma )^*$
due to statement (32). Thus,
$(\gamma \to \gamma )^*\in w$
because
$(\gamma \to \gamma )^*\in \Gamma _1\subseteq \Gamma _2$
and w is a maximal consistent subset of
$\Gamma _2$
. Therefore,
$w\in N((\gamma \to \gamma )^*)$
by Definition 7.12.
Lemma 7.16.
$N(\gamma _1)\cap N(\gamma _2) = N((\gamma _1\wedge \gamma _2)^*)$
for any formulae
$\gamma _1, \gamma _2\in \Gamma _1$
.
Proof Consider any world
$w\in W$
. It suffices to prove that the statements
$w\in N(\gamma _1)\cap N(\gamma _2)$
and
$w\in N((\gamma _1\wedge \gamma _2)^*)$
are equivalent.
By the definition of the intersection, the statement
$w\in N(\gamma _1)\cap N(\gamma _2)$
is equivalent to the conjunction of the statements
$$ \begin{align*}w\in N(\gamma_1) \mbox{ and } w\in N(\gamma_2). \end{align*} $$
By Definition 7.12, the conjunction of the above two statements is equivalent to the conjunction of the statements
$$ \begin{align*}\gamma_1\in w \mbox{ and } \gamma_2\in w. \end{align*} $$
Because
$\gamma _1,\gamma _2\in \Gamma _1\subseteq \Gamma _2$
and w is a maximal consistent subset of
$\Gamma _2$
, the conjunction of the above two formulae is equivalent to the conjunction of the statements
$$ \begin{align*}w\vdash \gamma_1 \mbox{ and } w\vdash \gamma_2. \end{align*} $$
By the laws of propositional logic, the conjunction of the two above statements is equivalent to
$$ \begin{align*}w\vdash \gamma_1\wedge \gamma_2. \end{align*} $$
Note that
$\gamma _1\wedge \gamma _2\in \widehat {\Gamma }$
because
$\gamma _1,\gamma _2\in \Gamma _1\subseteq \widehat {\Gamma }$
and set
$\widehat {\Gamma }$
is closed with respect to Boolean operations. Hence, by statement (32), the above formula is equivalent to
$$ \begin{align*}w \vdash (\gamma_1\wedge \gamma_2)^*. \end{align*} $$
Observe that
$(\gamma _1\wedge \gamma _2)^*\in \Gamma _1\subseteq \Gamma _2$
because function
$*$
maps set
$\widehat {\Gamma }$
to
$\Gamma _1$
. Since w is a maximal consistent subset of
$\Gamma _2$
, the above formula is equivalent to
$$ \begin{align*}(\gamma_1\wedge \gamma_2)^*\in w. \end{align*} $$
The last statement is equivalent to the statement
$w\in N((\gamma _1\wedge \gamma _2)^*)$
by Definition 7.12.
Lemma 7.17.
$W\setminus N(\gamma ) = N((\neg \gamma )^*)$
for any formula
$\gamma \in \Gamma _1$
.
Proof Consider any world
$w\in W$
. It suffices to show that
$w\notin N(\gamma )$
iff
$w\in N((\neg \gamma )^*)$
. By Definition 7.12, the statement
$w\notin N(\gamma )$
is equivalent to the statement
$$ \begin{align*}\gamma\notin w.\end{align*} $$
Note that
$\gamma \in \Gamma _1$
by the assumption of the lemma. Thus,
$\neg \gamma \in \Gamma _2$
by Definition 7.9. Then, because set w is a maximal consistent subset of
$\Gamma _2$
, the above statement is equivalent to
$$ \begin{align*}w\vdash \neg\gamma.\end{align*} $$
Observe that
$\gamma \in \Gamma _1$
also implies
$\gamma \in \Gamma _1\subseteq \widehat {\Gamma }$
. Then,
$\neg \gamma \in \widehat {\Gamma }$
due to set
$\widehat {\Gamma }$
being closed with respect to Boolean operations. Thus, by statement (32), the above statement is equivalent to
$$ \begin{align*}w\vdash (\neg\gamma)^*.\end{align*} $$
Note that
$(\neg \gamma )^*\in \Gamma _1\subseteq \Gamma _2$
because function
$*$
maps set
$\widehat {\Gamma }$
into set
$\gamma _2$
. Then, because set w is a maximal consistent subset of
$\Gamma _2$
, the above statement is equivalent to
$$ \begin{align*}(\neg\gamma)^* \in w.\end{align*} $$
The last statement is equivalent to
$w\in N((\neg \gamma )^*)$
by Definition 7.12.
Note that the proof above is somewhat convoluted because, for an arbitrary
$\gamma \in \Gamma _1$
, formula
$\neg \gamma $
belongs to sets
$\widehat {\Gamma }$
and
$\Gamma _2$
, but not necessarily to
$\Gamma _1$
.
7.5 Well-definedness of canonical model
In this subsection, we prove that the canonical model
$(W,\sim ,\{\mathcal {N}_w\}_{w\in W},\pi )$
is a neighborhood model as specified in Definition 7.1. For this, we verify items 3(a)–(e) of the definition.
Lemma 7.18.
$W\in \mathcal {N}_w$
for each world
$w\in W$
.
Proof Recall the assumption in the beginning of Section 7.3 that set
$\Gamma $
is nonempty. Let
$\gamma $
be any formula from
$\Gamma $
. Note that
$\gamma \to \gamma $
is a propositional tautology. Thus,
$\vdash \mathsf {A}(\gamma \to \gamma )$
by the Necessitation inference rule. Note that
$\gamma \to \gamma \in \widehat {\Gamma }$
. Hence, by Lemma 7.8 and propositional reasoning
$$ \begin{align} \vdash \mathsf{A}((\gamma\to\gamma)^*). \end{align} $$
Note that
$(\gamma \to \gamma )^*\in \Gamma _1$
by Lemma 7.15. Thus,
$\mathsf {A}((\gamma \to \gamma )^*)\in \Gamma _2$
by Definition 7.9. Then,
$\mathsf {A}((\gamma \to \gamma )^*)\in w$
by statement (33) and because w is a maximal consistent subset of
$\Gamma _2$
. Hence,
$N((\gamma \to \gamma )^*)\in \mathcal {N}_w$
by Definition 7.13 and the part
$(\gamma \to \gamma )^*\in \Gamma _1$
of Lemma 7.15. Therefore,
$w\in \mathcal {N}_w$
by the part
$N((\gamma \to \gamma )^*)=W$
of Lemma 7.15.
Lemma 7.19. For any formulae
$\gamma _1,\gamma _2\in \Gamma _1$
and any world
$w\in W$
, if
$N(\gamma _1),N(\gamma _2)\in \mathcal {N}_w$
, then
$N(\gamma _1)\cap N(\gamma _2)\in \mathcal {N}_w$
.
Proof The assumption
$N(\gamma _1),N(\gamma _2)\in \mathcal {N}_w$
implies
$\mathsf {A}\gamma _1, \mathsf {A}\gamma _2\in w$
by Definition 7.13. Thus,
$w\vdash \mathsf {A}(\gamma _1\wedge \gamma _2)$
by the Conjunction axiom and propositional reasoning. Note that
$\gamma _1\wedge \gamma _2\in \widehat {\Gamma }$
. Hence,
$w\vdash \mathsf {A}((\gamma _1\wedge \gamma _2)^*)$
by Lemma 7.8. Observe that
$\mathsf {A}((\gamma _1\wedge \gamma _2)^*)\in \Gamma _2$
by Definition 7.9 and because the range of function
$*$
is
$\Gamma _1$
. Then,
$\mathsf {A}((\gamma _1\wedge \gamma _2)^*)\in w$
because w is a maximal consistent subset of
$\Gamma _2$
. Thus,
$N((\gamma _1\wedge \gamma _2)^*)\in \mathcal {N}_w$
by Definition 7.13. Therefore,
$N(\gamma _1)\cap N(\gamma _2)\in \mathcal {N}_w$
by Lemma 7.16.
Lemma 7.20. For any
$\gamma \in \Gamma _1$
, if
$N(\gamma )\in \mathcal {N}_w$
, then
$W\setminus N(\gamma )\in \mathcal {N}_w$
.
Proof The assumption
$N(\gamma )\in \mathcal {N}_w$
implies
$\mathsf {A}\gamma \in w$
by Definition 7.13. Thus,
$w\vdash \mathsf {A}\neg \gamma $
by the Negation axiom and the Modus Ponens inference rule. Hence,
$w\vdash \mathsf {A}((\neg \gamma )^*)$
by Lemma 7.8 and propositional reasoning. Note that
$\mathsf {A}((\neg \gamma )^*)\in \Gamma _2$
by Definition 7.9 and because the range of function
$*$
is
$\Gamma _1$
. Then,
$\mathsf {A}((\neg \gamma )^*)\in w$
because w is a maximal consistent subset of
$\Gamma _2$
. Thus,
$N((\neg \gamma )^*)\in \mathcal {N}_w$
by Definition 7.13. Therefore,
$W\setminus N(\gamma )\in \mathcal {N}_w$
by Lemma 7.17.
Lemma 7.21. For any formula
$\gamma \in \Gamma _1$
, if
$N(\gamma )\in \mathcal {N}_w$
and
$w\sim u$
, then
$N(\gamma )\in \mathcal {N}_u$
.
Proof The assumption
$N(\gamma )\in \mathcal {N}_w$
implies that
$\mathsf {A}\gamma \in w$
by Definition 7.13. Thus,
$\mathsf {A}\gamma \in u$
by Definition 7.11 and the assumption
$w\sim u$
of the lemma. Therefore,
$N(\gamma )\in \mathcal {N}_u$
by Definition 7.13.
Lemma 7.22. For any formula
$\gamma \in \Gamma _1$
, if
$N(\gamma )\in \mathcal {N}_w$
,
$w\in N(\gamma )$
, and
$w\sim u$
, then
$u\in N(\gamma )$
.
Proof The assumptions
$N(\gamma )\in \mathcal {N}_w$
and
$w\in N(\gamma )$
imply
$\mathsf {A}\gamma \in w$
and
$\gamma \in w$
by Definitions 7.13 and 7.12, respectively. Then,
$w\vdash \mathsf {K}\gamma $
by the Self-Knowledge axiom and the Modus Ponens inference rule applied twice. Note that
$\mathsf { K}\gamma \in \Gamma _2$
by Definition 7.9. Hence,
$\mathsf {K}\gamma \in w$
because w is a maximal consistent subset of
$\Gamma _2$
. Thus,
$\mathsf {K}\gamma \in u$
by Definition 7.11 and the assumption
$w\sim u$
of the lemma. Then,
$u\vdash \gamma $
by the Truth axiom and the Modus Ponens inference rule. Hence
$\gamma \in u$
because
$\gamma \in \Gamma _1\subseteq \Gamma _2$
and w is a maximal consistent subset of
$\Gamma _2$
. Therefore,
$u\in N(\gamma )$
by Definition 7.12.
7.6 Truth lemma
In this subsection, we prove the truth lemma for the neighborhood semantics. It is stated and proven as Lemma 7.27 at the end of this subsection. We start with several lemmas used in the induction step of the proof of Lemma 7.27. In this section, we assume that the finite set
$\Gamma $
is closed with respect to subformulae.
Lemma 7.23. For any world
$w\in W$
and any formula
$\mathsf {K}\varphi \in \Gamma $
such that
$\mathsf {K}\varphi \notin w$
, there is a world
$u\in W$
such that
$w\sim u$
and
$\varphi \notin u$
.
Proof Consider the following set of formulae
$$ \begin{align} X=\{\neg\varphi\}&\cup\{\mathsf{K}\psi\;|\;\mathsf{K}\psi\in w\}\cup\{\neg\mathsf{K}\chi\;|\;\neg\mathsf{K}\chi\in w \} \end{align} $$
$$ \begin{align} &\cup\{\mathsf{A}\sigma\;|\;\mathsf{A}\sigma\in w \} \cup\{\neg\mathsf{A}\tau\;|\;\neg\mathsf{A}\tau\in w \}. \end{align} $$
Claim 7.24. Set X is consistent.
Proof of Claim
Suppose the opposite. Then, there are formulae
$$ \begin{align} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\neg\mathsf{K}\chi_1,\dots,\neg\mathsf{K}\chi_\ell, \mathsf{A}\sigma_1,\dots,\mathsf{A}\sigma_m,\neg\mathsf{A}\tau_1,\dots,\neg\mathsf{A}\tau_n\in w \end{align} $$
such that
$$ \begin{align*}\mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\neg\mathsf{K}\chi_1,\dots,\neg\mathsf{K}\chi_\ell, \mathsf{A}\sigma_1,\dots,\mathsf{A}\sigma_m,\neg\mathsf{A}\tau_1,\dots,\neg\mathsf{A}\tau_n \vdash\varphi. \end{align*} $$
Then, by Lemma 4.2,
$$ \begin{align*} \mathsf{K}\mathsf{K}\psi_1,\dots,\mathsf{K}\mathsf{K}\psi_k,\mathsf{K}\neg\mathsf{K}\chi_1,\dots,\mathsf{K}\neg\mathsf{K}\chi_\ell, &\mathsf{K}\mathsf{A}\sigma_1,\dots,\mathsf{K}\mathsf{A}\sigma_m,\\ &\quad \mathsf{K}\neg\mathsf{A}\tau_1,\dots,\mathsf{K}\neg\mathsf{A}\tau_n \vdash\mathsf{K}\varphi. \end{align*} $$
Thus, by Lemma 4.3 and the Modus Ponens rule applied k times,
$$ \begin{align*} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\mathsf{K}\neg\mathsf{K}\chi_1,\dots,\mathsf{K}\neg\mathsf{K}\chi_\ell, \mathsf{K}\mathsf{A}\sigma_1,\dots,&\mathsf{K}\mathsf{A}\sigma_m,\\ &\mathsf{K}\neg\mathsf{A}\tau_1,\dots,\mathsf{K}\neg\mathsf{A}\tau_n \vdash\mathsf{K}\varphi. \end{align*} $$
Hence, by the Negative Introspection axiom and the Modus Ponens inference rule applied
$\ell $
times,
$$ \begin{align*} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\neg\mathsf{K}\chi_1,\dots,\neg\mathsf{K}\chi_\ell, \mathsf{K}\mathsf{A}\sigma_1,\dots,&\mathsf{K}\mathsf{A}\sigma_m,\\ &\quad \mathsf{K}\neg\mathsf{A}\tau_1,\dots,\mathsf{K}\neg\mathsf{A}\tau_n \vdash\mathsf{K}\varphi. \end{align*} $$
Then, by the Introspection of Knowing All axiom and the Modus Ponens inference rule applied m times,
$$ \begin{align*} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\neg\mathsf{K}\chi_1,\dots,\neg\mathsf{K}\chi_\ell, \mathsf{A}\sigma_1,\dots,\mathsf{A}\sigma_m, \mathsf{K}\neg\mathsf{A}\tau_1,\dots,\mathsf{K}\neg\mathsf{A}\tau_n \vdash\mathsf{K}\varphi. \end{align*} $$
Thus, by Lemma 4.4 and the Modus Ponens inference rule applied n times,
$$ \begin{align*} \mathsf{K}\psi_1,\dots,\mathsf{K}\psi_k,\neg\mathsf{K}\chi_1,\dots,\neg\mathsf{K}\chi_\ell, \mathsf{A}\sigma_1,\dots,\mathsf{A}\sigma_m, \neg\mathsf{A}\tau_1,\dots,\neg\mathsf{A}\tau_n \vdash\mathsf{K}\varphi. \end{align*} $$
Hence,
$w\vdash \mathsf {K}\varphi $
by statement (36). Observe that
$\mathsf {K}\varphi \in \Gamma $
by the assumption of the lemma. Hence,
$\mathsf {K}\varphi \in \Gamma \subseteq \Gamma _1\subseteq \Gamma _2$
. Therefore,
$\mathsf {K}\varphi \in w$
because w is a maximal consistent subset of
$\Gamma _2$
, which contradicts the assumption of the lemma.
By Lemma 4.5, set X can be extended to a maximal consistent set
$X'$
. Let u be the set
$\Gamma _2\cap X'$
. Note that the assumption
$\mathsf {K}\varphi \in \Gamma $
implies
$\varphi \in \Gamma \subseteq \Gamma _1$
because set
$\Gamma $
is closed with respect to subformulae. Then,
$\neg \varphi \in \Gamma _2$
by Definition 7.9. Observe also that
$\neg \varphi \in X\subseteq X'$
. Thus,
$\neg \varphi \in \Gamma _2\cap X'=u$
. Hence,
$\varphi \notin u$
because u is a consistent set of formulae. To finish the proof of the lemma, we need to show
$w\sim u$
. To establish this, by Definition 7.11, it suffices to prove the following claim.
Claim 7.25. For each formula
$\gamma \in \Gamma _1$
,
-
1.
$\mathsf {K}\gamma \in w$
iff
$\mathsf {K}\gamma \in u$
, -
2.
$\mathsf {A}\gamma \in w$
iff
$\mathsf {A}\gamma \in u$
.
Proof of Claim
By Definition 7.9, the assumption
$\gamma \in \Gamma _1$
implies that
$\mathsf {K}\gamma ,\mathsf {A}\gamma ,\neg \mathsf { K}\gamma ,\neg \mathsf {A}\gamma \in \Gamma _2$
.
If
$\mathsf {K}\gamma \in w$
, then
$\mathsf {K}\gamma \in X\subseteq X'$
by statement (34). Thus,
$\mathsf {K}\gamma \in X'\cap \Gamma _2=u$
because
$\mathsf {K}\gamma \in \Gamma _2$
.
On the other hand, if
$\mathsf {K}\gamma \in u$
, then
$\neg \mathsf {K}\gamma \notin u$
because set u is consistent. Then,
$\neg \mathsf {K}\gamma \notin w$
by statement (34). Thus,
$\mathsf {K}\gamma \in w$
because w is a maximal consistent subset of
$\Gamma _2$
and
$\mathsf {K}\gamma ,\neg \mathsf {K}\gamma \in \Gamma _2$
.
The proof of the second part of the claim is similar.
This concludes the proof of the lemma.
Lemma 7.26. For any world
$w\in W$
and any formula
$\mathsf {A}\varphi \in \Gamma $
, if
$\mathsf {A}\varphi \notin w$
, then
$N(\varphi )\notin \mathcal {N}_w$
.
Proof Suppose
$N(\varphi )\in \mathcal {N}_w$
. Thus, by Definition 7.13, there exists a formula
$\gamma \in \Gamma _1$
such that
$$ \begin{align} \mathsf{A}\gamma\in w \end{align} $$
and
$$ \begin{align} N(\varphi)=N(\gamma). \end{align} $$
Note that
$\mathsf {A}\varphi \in \Gamma \subseteq \Gamma _1$
by the assumption of the lemma. Thus,
$\neg \mathsf {A}\varphi \in \Gamma _2$
by Definition 7.9. Then,
$\neg \mathsf {A}\varphi \in w$
because w is a maximal consistent subset of w. Hence,
$\nvdash \mathsf { A}\gamma \to \mathsf {A}\varphi $
by statement (37) and consistency of set w. Thus,
$\nvdash \gamma \leftrightarrow \varphi $
by the Substitution inference rule applied contrapositively. We consider the following two cases separately:
Case 1:
$\nvdash \gamma \to \varphi $
. Thus, the set
$\{\neg \varphi ,\gamma \}$
is consistent. By Lemma 4.5, it can be extended to a maximal consistent set u. Note that
$\gamma \in u$
and, because set u is consistent,
$\varphi \notin u$
. Also
$\varphi \in \Gamma \subseteq \Gamma _1$
because set
$\Gamma $
is closed with respect to subformulae and also
$\gamma \in \Gamma _1$
. Thus,
$u\notin N(\varphi )$
and
$u\in N(\gamma )$
by Definition 7.12, which contradicts to statement (38).
Case 2:
$\nvdash \varphi \to \gamma $
. The proof is similar to the previous case.
Lemma 7.27.
$\varphi \in w$
iff
$w\Vdash \varphi $
for each formula
$\varphi \in {\Gamma }$
.
Proof We prove the statement of the lemma by induction on the structural complexity of formula
$\varphi $
.
First, suppose that formula
$\varphi $
is a propositional variable p. Note that
$p\in \Gamma \subseteq \Gamma _1$
by the assumption of the lemma. Note that the statement
$p\in w$
is equivalent to the statement
$w\in N(p)$
by Definition 7.12. The statement
$w\in N(p)$
is equivalent to the statement
$w\in \pi (p)$
by Definition 7.14. Finally, the statement
$w\in \pi (p)$
is equivalent to the statement
$w\Vdash p$
by item 1 of Definition 7.2.
Next, assume that formula
$\varphi $
has the form
$\neg \psi $
. Note that
$\varphi \in \Gamma $
by the assumption of the lemma. Hence,
$\psi \in \Gamma \subseteq \Gamma _1$
because set
$\Gamma $
is closed with respect to subformulae. Then,
$$ \begin{align} \psi,\neg\psi\in \Gamma_2. \end{align} $$
$(\Rightarrow ):$
Let
$w\Vdash \neg \psi $
. Then,
$w\nVdash \psi $
by item 2 of Definition 7.2. Hence,
$\psi \notin w$
by the induction hypothesis. Therefore,
$\neg \psi \in w$
by statement (39) because w is a maximal consistent subset of
$\Gamma _2$
.
$(\Leftarrow ):$
Let
$\neg \psi \in w$
. Then,
$\psi \notin w$
because set w is consistent. Hence,
$w\nVdash \psi $
by the induction hypothesis. Therefore,
$w\Vdash \neg \psi $
by item 2 of Definition 7.2.
Assume that formula
$\varphi $
has the form
$\psi _1\to \psi _2$
. Thus,
$\psi _1,\psi _2\in \Gamma \subseteq \Gamma _1$
because set
$\Gamma $
is closed with respect to subformulae. Then,
$$ \begin{align} \psi_1,\psi_2,\neg\psi_1,\neg\psi_2\in\Gamma_2. \end{align} $$
$(\Rightarrow ):$
Let
$w\Vdash \psi _1\to \psi _2$
. Then, by item 3 of Definition 7.2, either
$w\nVdash \psi _1$
or
$w\Vdash \psi _2$
. We consider these two cases separately.
Case 1:
$w\nVdash \psi _1$
. Thus,
$\psi _1\notin w$
by the induction hypothesis. Then,
$\neg \psi _1\in w$
by statement (40) because w is a maximal consistent subset of
$\Gamma _2$
. Note that
$\neg \psi _1\to (\psi _1\to \psi _2)$
is a propositional tautology. Thus,
$w\vdash \psi _1\to \psi _2$
by the Modus Ponens inference rule. Therefore,
$\psi _1\to \psi _2\in w$
because w is a maximal consistent subset of
$\Gamma _2$
and
$\psi _1\to \psi _2=\varphi \in \Gamma \subseteq \Gamma _1\subseteq \Gamma _2$
by the assumption
$\varphi \in \Gamma $
of the lemma.
Case 2:
$w\Vdash \psi _2$
. Then,
$\psi _2\in w$
by the induction hypothesis. Note that
$\psi _2\to (\psi _1\to \psi _2)$
is a propositional tautology. Then,
$w\vdash \psi _1\to \psi _2$
by the Modus Ponens inference rule. Therefore, just like in the first case,
$\psi _1\to \psi _2\in w$
.
$(\Leftarrow ):$
Let
$\psi _1\to \psi _2\in w$
. Thus, by the Modus Ponens rule, if
$w\vdash \psi _1$
, then
$w\vdash \psi _2$
. In other words, either
$w\nvdash \psi _1$
or
$w\vdash \psi _2$
. Then, either
$\psi _1\notin w$
or
$w\vdash \psi _2$
. Hence, either
$\psi _1\notin w$
or
$\psi _2\in w$
by statement (40) because w is a maximal consistent subset of
$\Gamma _2$
. Thus,
$w\nVdash \psi _1$
or
$w\vdash \psi _2$
by the induction hypothesis. Therefore,
$w\Vdash \psi _1\to \psi _2$
by item 3 of Definition 7.2.
Suppose that formula
$\varphi $
has the form
$\mathsf {K}\psi $
.
$(\Rightarrow ):$
Assume that
$\mathsf {K}\psi \in w$
. Consider any world
$u\in W$
such that
$w\sim u$
. By item 4 of Definition 7.2, it suffices to show that
$u\Vdash \psi $
. Indeed, by Definition 7.11, the assumptions
$\mathsf {K}\psi \in w$
and
$w\sim u$
imply that
$\mathsf {K}\psi \in u$
. Hence
$u\vdash \psi $
by the Truth axiom and the Modus Ponens inference rule. Note that
$\psi \in \Gamma \subseteq \Gamma _1\subseteq \Gamma _2$
because
$\mathsf {K}\psi \in \Gamma $
and set
$\Gamma $
is closed with respect to subformulae. Thus,
$\psi \in u$
because u is a maximal consistent subset of
$\Gamma _2$
. Therefore,
$u\Vdash \psi $
by the induction hypothesis.
$(\Leftarrow ):$
Assume that
$\mathsf {K}\psi \notin w$
. Then, by Lemma 7.23, there is a world
$u\in W$
such that
$w\sim u$
and
$\psi \notin u$
. Thus,
$u\nVdash \psi $
by the induction hypothesis. Therefore,
$w\nVdash \mathsf {K}\psi $
by item 4 of Definition 7.2.
Suppose that formula
$\varphi $
has the form
$\mathsf {A}\psi $
. Note that
$\psi \in \Gamma \subseteq \Gamma _1$
because set
$\Gamma $
is closed with respect to subformulae and
$\varphi \in \Gamma $
by the assumption of the lemma.
$(\Rightarrow ):$
Assume that
$\mathsf {A}\psi \in w$
. Then,
$N(\psi )\in \mathcal {N}_w$
by Definition 7.13. Thus,
$\{u\in W\;|\;\psi \in u\}\in \mathcal {N}_w$
by Definition 7.12. Hence,
$\{u\in W\;|\;u\Vdash \psi \}\in \mathcal {N}_w$
by the induction hypothesis. Therefore,
$w\Vdash \mathsf {A}\psi $
by item 5 of Definition 7.2.
$(\Leftarrow ):$
Assume that
$\mathsf {A}\psi \notin w$
. Thus,
$N(\psi )\notin \mathcal {N}_w$
by Lemma 7.26. Then,
$\{u\in W\;|\;\psi \in u\}\notin \mathcal {N}_w$
by Definition 7.12. Hence,
$\{u\in W\;|\;u\Vdash \psi \}\notin \mathcal {N}_w$
by the induction hypothesis. Therefore,
$w\nVdash \mathsf {A}\psi $
by item 5 of Definition 7.2.
7.7 Completeness and decidability
In this subsection, we finish the proof of the completeness theorem for neighborhood semantics. We say that a neighborhood model
$(W,\sim ,\{\mathcal {N}_w\}_{w\in W},\pi )$
is finite if set W is finite. Note that this implies that the family
$\mathcal {N}_w$
is finite and all its elements are finite sets.
Theorem 7.28 (Neighborhood completeness).
If
$\nvdash \varphi $
, then
$w\nVdash \varphi $
for some world w of a finite neighborhood model.
Proof Let
$\Gamma $
be the finite set of all subformulae of formula
$\neg \varphi $
. Consider the canonical model defined in the previous subsection. Note that this model is finite because set
$\Gamma _2$
is also finite.
The assumption
$\nvdash \varphi $
implies that the set
$\{\neg \varphi \}$
is consistent. By Lemma 4.5 it can be extended to a maximal consistent set X. Let w be the set
$X\cap \Gamma _2$
. Note that
$\neg \varphi \in w$
because
$\neg \varphi \in X$
and
$\neg \varphi \in \Gamma \subseteq \Gamma _1\subseteq \Gamma _2$
. Thus,
$\varphi \notin w$
because set w is consistent. Therefore,
$w\nVdash \varphi $
by Lemma 7.27.
Theorem 7.29 (Decidability).
Set
$\{\varphi \in \Phi \;|\;\vdash \varphi \}$
is decidable.
Proof Consider an algorithm that takes a formula
$\varphi $
as an input and executes two processes in parallel. The first process enumerates all proofs in our logical system and checks if any of them is a proof of formula
$\varphi $
. The second process enumerates all finite neighborhood models and checks if formula
$\varphi $
is false in at least one world of this model. By Theorem 7.3, at most one of these processes will succeed on a given input
$\varphi $
. By Theorem 7.28, at least one process will succeed on a given input
$\varphi $
. If the first process succeeds, formula
$\varphi $
belongs to the set
$\{\varphi \in \Phi \;|\;\vdash \varphi \}$
. If the second process succeeds, it does not.
8 Future work
In this section, we discuss several possible extensions of our logical system.
8.1 Know one
Our “telling apart” modality
$\mathsf {A}\varphi $
captures the ability of an agent to identify all possible agents with a given property
$\varphi $
. One can also consider the “knowing one” modality:
$(a,w)\Vdash \mathsf {O}\varphi $
when there exists an agent
$b\in Ag$
such that
$(b,u)\Vdash \varphi $
for each world
$u\in W$
, where
$w\sim _a u$
.
Informally,
$(a,w)\Vdash \mathsf {O}\varphi $
means that in world w agent a knows at least one agent (the agent b) that has property
$\varphi $
. Here are some of the properties of the interplay between this new modality and the modality that we have studied in this article:
-
1.
$\mathsf {O}\varphi \wedge \mathsf {A}\psi \to \mathsf {O}(\varphi \wedge \psi )\vee \mathsf {O}(\varphi \wedge \neg \psi )$
, -
2.
$\mathsf {O}\varphi \to \mathsf {K}\mathsf {O}\varphi $
, -
3.
$\mathsf {K}\varphi \to \mathsf {O}\varphi $
.
Although the Necessitation rule for modality
$\mathsf {O}$
is not sound, the Monotonicity rule
$$ \begin{align*}\dfrac{\varphi\to\psi}{\mathsf{O}\varphi\to\mathsf{O}\psi} \end{align*} $$
is sound. An interesting possible question for future work could be to study the definability of modalities
$\mathsf {O}$
,
$\mathsf {A}$
, and
$\mathsf {K}$
through each other. If they are not definable through each other, then one can look for a complete axiomatization of the interplay between these modalities. We think that a variation of our matrix technique could be potentially useful for proving completeness in this new setting.
8.2 Conditional tell apart
Another possible extension of this work is to consider “conditional telling apart.” For example, although in a world w an agent a, a pediatrician, might not be able to tell sick people apart, the agent can tell sick children apart. We write this as
$$ \begin{align*}(a,w)\Vdash \mathsf{A}(\text{"is sick"}\,|\,\text{"is a child"}). \end{align*} $$
Formally, conditional telling apart modality
$\mathsf {A}(~|~)$
is defined as follows:
$(a,w)\Vdash \mathsf {A}(\varphi \,|\,\psi )$
when for each agent
$b\in Ag$
such that
$(b,w)\Vdash \psi $
and any worlds
$u,u'\in W$
, if
$w\sim _a u$
,
$w\sim _a u'$
, and
$(b,u)\Vdash \varphi $
, then
$(b,u')\Vdash \varphi $
.
Formula
$\mathsf {A}(\varphi \,|\,\top )$
is equivalent to
$\mathsf {A}\varphi $
. Here is an example of a property in the language of conditional telling apart:
$$ \begin{align*}\mathsf{A}(\varphi\,|\,\psi_1)\wedge \mathsf{A}(\varphi\,|\,\psi_2)\to \mathsf{A}(\varphi\,|\,\psi_1\vee \psi_2).\end{align*} $$
A complete axiomatization of all such properties is a possible direction for future research.
8.3 Non-rigid names
One might argue that the logical system proposed in this article is very restricted because it cannot explicitly refer to agents. Names can be introduced into our language through an additional modality
$@_n$
. This allows for a very general class of non-rigid names that could be agent-specific and world-specific. By agent-specific names, we mean names, such as
$ma$
(mother), whose meaning depends on the agent. For example, the statement
$(a,w)\Vdash @_{ma}\text {"is sick"}$
means that the mother of agent a is sick in worlds w. The statement
$(a,w)\Vdash @_{ma}@_{ma}\text {"is sick"}$
means that agent a’s grandma (on the mother’s side) is sick. One can write
$$ \begin{align*}(a,w)\Vdash@_{ma}\mathsf{A}\text{"is sick"} \end{align*} $$
to express that agent a’s mother knows how to tell sick people apart. At the same time, the statement
$$ \begin{align*}(a,w)\Vdash\mathsf{A}@_{ma}\text{"is sick"} \end{align*} $$
means that agent a knows how to tell apart those whose mother is sick. The names can be also world-specific. For example, in different worlds, the mother of agent a could be different. Such a setting could be used to model situations when the agent does not know who his mother is.
To give a formal semantics of the language with non-rigid names, one can extend each epistemic model
$(Ag,W,\{\sim _a\}_{a\in Ag},\pi )$
with an additional component
$\{e^w_a\}^{w\in W}_{a\in \mathcal {A}}$
. By
$e^w_a$
we denote an “extension function” that maps a name n into an agent
$e^w_a(n)$
whom agent a calls by name n in world w. Using extension functions, the semantics of modality
$@_n$
can be defined as follows:
$(a,w)\Vdash @_n\varphi $
when
$(e^w_a(n),w)\Vdash \varphi $
.
A complete axiomatization of the properties of modalities
$\mathsf {A}$
,
$\mathsf {O}$
, and
$\mathsf {A}(~|~)$
in the language with non-rigid names remains another interesting question for future work.
9 Conclusion
The contribution of this paper is twofold. First, we proposed a sound, complete, and decidable modal logic of “knowing how to tell apart” in the egocentric setting. Second, we propose a new matrix-based technique for proving completeness results for 2D semantics. We hope that this technique could be potentially extended to other logical systems, such as those that we listed in the future work section.
Acknowledgment
We would like to thank an anonymous reviewer for the idea to prove decidability using neighborhood semantics and for the suggestion on how to improve the proof of Lemma 6.17.
Appendix A Proofs of auxiliary lemmas
To keep the work self-contained, in this appendix, we give the proofs of three standard results used in our article.
Lemma 4.1. If
$X,\varphi \vdash \psi $
, then
$X\vdash \varphi \to \psi $
.
Proof Suppose that sequence
$\psi _1,\dots ,\psi _n$
is a proof from set
$X\cup \{\varphi \}$
and the theorems of our logical system that uses the Modus Ponens inference rule only. In other words, for each
$k\le n$
, either
-
1.
$\vdash \psi _k$
, or -
2.
$\psi _k\in X$
, or -
3.
$\psi _k$
is equal to
$\varphi $
, or -
4. there are
$i,j<k$
such that formula
$\psi _j$
is equal to
$\psi _i\to \psi _k$
.
It suffices to show that
$X\vdash \varphi \to \psi _k$
for each
$k\le n$
. We prove this by induction on k by considering the four cases above separately.
Case I:
$\vdash \psi _k$
. Note that
$\psi _k\to (\varphi \to \psi _k)$
is a propositional tautology and, thus, is an axiom of our logical system. Hence,
$\vdash \varphi \to \psi _k$
by the Modus Ponens inference rule. Therefore,
$X\vdash \varphi \to \psi _k$
.
Case II:
$\psi _k\in X$
. Then,
$X\vdash \psi _k$
.
Case III: Formula
$\psi _k$
is equal to
$\varphi $
. Thus,
$\varphi \to \psi _k$
is a propositional tautology. Hence,
$X\vdash \varphi \to \psi _k$
.
Case IV: Formula
$\psi _j$
is equal to
$\psi _i\to \psi _k$
for some
$i,j<k$
. Thus, by the induction hypothesis,
$X\vdash \varphi \to \psi _i$
and
$X\vdash \varphi \to (\psi _i\to \psi _k)$
. Note that formula
$$ \begin{align*} (\varphi\to\psi_i)\to((\varphi\to(\psi_i\to\psi_k))\to(\varphi\to\psi_k)) \end{align*} $$
is a propositional tautology. Therefore,
$X\vdash \varphi \to \psi _k$
by applying the Modus Ponens inference rule twice.
Lemma 4.2. If
$\varphi _1,\dots ,\varphi _n\vdash \psi $
, then
$\mathsf {K}\varphi _1,\dots ,\mathsf { K}\varphi _n\vdash \mathsf {K}\psi $
.
Proof By Lemma 4.1 applied n times, the assumption
$\varphi _1,\dots ,\varphi _n\vdash \psi $
implies that
$$ \begin{align*}\vdash\varphi_1\to(\varphi_2\to\dots(\varphi_n\to\psi)\dots). \end{align*} $$
Thus, by the Necessitation inference rule,
$$ \begin{align*}\vdash\mathsf{K}(\varphi_1\to(\varphi_2\to\dots(\varphi_n\to\psi)\dots)). \end{align*} $$
Hence, by the Distributivity axiom and the Modus Ponens inference rule,
$$ \begin{align*}\vdash\mathsf{K}\varphi_1\to\mathsf{K}(\varphi_2\to\dots(\varphi_n\to\psi)\dots). \end{align*} $$
Then, again by the Modus Ponens rule,
$$ \begin{align*}\mathsf{K}\varphi_1\vdash\mathsf{K}(\varphi_2\to\dots(\varphi_n\to\psi)\dots). \end{align*} $$
Therefore,
$\mathsf {K}\varphi _1,\dots ,\mathsf {K}\varphi _n\vdash \mathsf {K}\psi $
by applying the previous steps
$(n-1)$
more times.
Lemma 4.3.
$\vdash \mathsf {K}\varphi \to \mathsf {K}\mathsf {K}\varphi $
.
Proof Note that formula
$\mathsf {K}\neg \mathsf {K}\varphi \to \neg \mathsf {K}\varphi $
is an instance of the Truth axiom. Thus, by contraposition,
$$ \begin{align} \vdash \mathsf{K}\varphi\to\neg\mathsf{K}\neg\mathsf{K}\varphi. \end{align} $$
Also,
$$ \begin{align} \neg\mathsf{K}\neg\mathsf{K}\varphi\to\mathsf{K}\neg\mathsf{K}\neg\mathsf{K}\varphi \end{align} $$
is an instance of the Negative Introspection axiom. Additionally, the formula
$$ \begin{align*} \neg\mathsf{K}\varphi\to\mathsf{K}\neg\mathsf{K}\varphi \end{align*} $$
is also an instance of the Negative Introspection axiom. Thus, by the law of contraposition,
$$ \begin{align*} \vdash \neg\mathsf{K}\neg\mathsf{K}\varphi\to \mathsf{K}\varphi. \end{align*} $$
Hence, by the Necessitation inference rule,
$$ \begin{align*} \vdash \mathsf{K}(\neg\mathsf{K}\neg\mathsf{K}\varphi\to \mathsf{K}\varphi). \end{align*} $$
Then, by the Distributivity axiom and the Modus Ponens inference rule,
$$ \begin{align} \vdash \mathsf{K}\neg\mathsf{K}\neg\mathsf{K}\varphi\to \mathsf{K}\mathsf{K}\varphi. \end{align} $$
Finally, by the laws of propositional reasoning, statements (41)–(43) imply the statement of the lemma.
Open access
