1. Introduction
The axiom schema
-
(K)
$\square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi )$
is part and parcel of any introduction to modal logic. Together with classical propositional logic (henceforth
$\textbf {CL}$
) and the rule of necessitation (if
$\vdash \varphi $
, then
$\vdash \square \varphi $
), (K) characterizes the minimal normal modal logic
$\textbf {K}$
that is sound and complete with respect to the class of all relational models (often referred to as Kripke-models). For that reason, (K) is often called the normality schema.Footnote
1
Much less familiar is the logic
$\textbf {EK}$
, which is the weakest modal logic that contains
$\textbf {CL}$
, axiom (K), and is closed under the rule of replacement of equivalents:
-
(RE) If
$\vdash \varphi \leftrightarrow \psi $
, then
$\vdash \square \varphi \rightarrow \square \psi $
.
Thus defined,
$\textbf {EK}$
falls in the broader class of classical modal logics [Reference Chellas3], which have a semantics in terms of neighbourhood models.Footnote
2
In this paper we will be concerned with both
$\textbf {EK}$
and its stronger kin
$\textbf {ECK}$
, which is obtained by adding the aggregation axiom (C) to
$\textbf {EK}$
:
-
(C)
$(\square \varphi \wedge \square \psi ) \rightarrow \square (\varphi \wedge \psi )$
.
While they seem obvious candidates for logical investigation alongside other classical modal logics,
$\textbf {EK}$
and
$\textbf {ECK}$
have so far been widely neglected. This might be due to a perceived lack of applications—after all, why would we want a logic that validates (K) and yet is not normal? So, why bother with such strange logics?
For one thing, the framework of classical modal logics is a generalization of the framework of normal modal logics. Exploring how weaker systems involving the most salient scheme characterizing the latter class of logics blends with the weakest systems of the former class of logics surely is a sensible enterprise. Indeed, in [Reference Chellas and Segerberg4] it was shown that
$ {\mathbf {EK}}$
is a prominent member of the class of prenormal modal logic, which forms a natural stepping stone to Lewis’ famous logic
$ {\mathbf {S1}}$
.Footnote
3
Secondly, that a framework for logics has proved fruitful rationalizes the more systematic study of such a framework, independently of particular and perhaps unforeseen future applications. Thirdly, there are apparent applications, a recent one being McNamara’s [Reference McNamara7] in the context of classical modal logics for agency where he argues for the cogency of (K). So we think the default question is not “why bother?,” but “why has there been so little bother?”Footnote
4
A different reason for not exploring completeness for these logics might be that they do not really present us with any novel technical insights or complications beyond those familiar from completeness proofs of other classical modal logics. The latter idea seems to be confirmed by the following exercise, mentioned quite in passing, in Chellas’ classical textbook on modal logic [Reference Chellas3, p. 261]:
9.33. Prove determination theorems for some classical systems containing the schema (K), in particular, for the systems
$\textbf {EK}$
and
$\textbf {ECK}$
.
By determination theorems, Chellas refers to the combination of soundness and weak completeness: a formula is derivable in the axiomatic system if and only if it is true in every model of the intended class of models [Reference Chellas3, p. 60]. In fact, weak completeness for
$\textbf {EK}$
and
$\textbf {ECK}$
can easily be proven, using a method for the construction of finite models first introduced by Lewis [Reference Lewis6], cf. [Reference Pacuit8, Section 2.4.1.1]. By Lewis’ proof, all classical modal logics characterized by a finite set of non-iterative axioms are weakly complete and decidable.
$\textbf {EK}$
and
$\textbf {ECK}$
are just two instances within this very broad class of non-iterative modal logics.
However, Chellas’ method for proving completeness throughout [Reference Chellas3]—as explained early on in the book and put into practice in the chapter that contains this exercise—does a lot more. It establishes neighbourhood canonicity: there is a neighbourhood model M such that (i) M is based on a frame that validates the logic in question; (ii) the domain of M is the set of all maximal consistent sets of formulas given that logic; and (iii) M satisfies the truth lemma. In this context, we say that M is characteristic (for the logic in question).Footnote
5
Taking (ii) and (iii) together, we obtain that every consistent set of formulas is satisfied at some state in M. This in turn implies strong completeness: if some formula
$\varphi $
is a semantic consequence of a (possibly infinite) set of formulas
$\Gamma $
, then
$\varphi $
is derivable from
$\Gamma $
in the logic. It is apparent that Exercise 9.33 is to be completed in the same manner as completeness proofs already given, thus establishing the existence of a characteristic model for
$ {\mathbf {EK}}$
and
$ {\mathbf {ECK}}$
.Footnote
6
However, doing so turns out to be far from trivial.
Surendonk [Reference Surendonk10] generalized Lewis’ result, establishing neighbourhood canonicity for all non-iterative classical modal logics.Footnote
7
Surendonk’s proof is quite elegant but circuitous. More precisely, Surendonk proceeds via the well-known algebraic semantics of these logics, embedding this semantics into first order logic and relying on the compactness of first order logic. Surendonk’s proof is also non-constructive: while it is shown that there must be some characteristic model for each logic in a very broad class, including
$ {\mathbf {EK}}$
and
$ {\mathbf {ECK}}$
, we are not given any procedure for constructing such a model, given a suitable axiomatization of the logic in question. In particular, for
$ {\mathbf {EK}}$
and
$ {\mathbf {ECK}}$
we are left in the dark as to what exactly the neighbourhood function of this model might look like and how the construction could generalize to iterative logics.Footnote
8
In the present paper, we provide a direct, constructive proof of neighbourhood canonicity for
$ {\mathbf {EK}}$
,
$ {\mathbf {ECK}}$
and four related logics, obtained by adding well-known axioms to
$ {\mathbf {EK}}$
and
$ {\mathbf {ECK}}$
. In addition, we give constructive proofs of a relativized form of neighbourhood canonicity (that still suffices to obtain strong completeness) for the extensions of each of these logics with a global modality.Footnote
9
The latter result takes us beyond Surendonk’s results, since the global modality is of the type
$ {\mathbf {S5}}$
, hence iterative. Our proofs are constructive in the sense that we explicitly define the characteristic models in question. They are direct in the sense that we only rely on basic set theoretic properties, without making any detour through first order logic.
The characteristic models we construct are moreover, in a straightforward sense, minimal. That is, the models are obtained by taking the smallest canonical neighbourhood models and closing their neighbourhood sets under the frame conditions that correspond to (K), respectively (K) and (C). Given this, the main difficulty consists in checking that the truth lemma is preserved by such closure. To this end, we first investigate an alternative, more perspicuous definition of the minimal characteristic models, giving us a better grip on their properties.
Our paper is set up as follows. We first introduce basic notation and terminology and explain our contribution in exact terms (Section 2). In Section 3, we focus on the logic
$ {\mathbf {EK}}$
, showing how the minimal characteristic model for it can be circumscribed in a way that allows us to establish the truth lemma for it and prove closure under the relevant frame conditions. Section 4 does essentially the same job for
$\textbf {ECK}$
, though the latter turns out to be a much harder nut to crack. We conclude the paper by pointing out how these two proofs generalize to the aforementioned extensions of both logics.
2. Preliminary definitions
2.1. Formal language, semantics, and logics
The basic modal language
$\mathfrak {L}$
is obtained by closing the language of classical propositional logic (based on a countable set
$\mathfrak {P}$
of propositional variables and the connectives
$\neg ,\vee ,\wedge ,\rightarrow ,\leftrightarrow $
) under a unary modal operator
$\square $
. We take
$\neg $
and
$\vee $
as primitive; the other classical connectives are defined from them in the usual way. We use
$\varphi ,\psi ,\ldots $
as metavariables for members of
$\mathfrak {L}$
and
$\Gamma ,\Delta ,\ldots $
as metavariables for subsets of
$\mathfrak {L}$
.
Neighbourhood models (henceforth: models) are structures of the type
$M =\langle W,N,V\rangle $
where W is a non-empty set of worlds (the domain of M),
$N: W\rightarrow \wp (\wp (W))$
is a neighbourhood function mapping each world w to its neighbourhood
$N(w)$
, and
$V: \mathfrak {P}\rightarrow \wp (W)$
is a valuation function mapping each propositional variable to a subset of W. Frames are just models with the valuation function stripped off, i.e. couples of the type
$\langle W,N\rangle $
. When the domain W of a model or frame is clear from the context and where
$X\subseteq W$
, we use
$\overline {X}$
to refer to the complement of X relative to W, i.e.,
$\overline {X} = W\setminus X$
. Truth at a world w in a model M is given by the usual semantic clauses for the propositional variables and connectives and the following clause for
$\square $
:
$$ \begin{align*}M,w\models \square\varphi \mbox{ iff } \|\varphi\|^M\in N(w),\end{align*} $$
where
$\|\varphi \|^M = \{w^{\prime }\in W\mid M,w^{\prime }\models \varphi \}$
denotes the truth set of
$\varphi $
in M.
We say that
$\varphi $
is valid on a frame
$\langle W,N\rangle $
if and only for every model M based on this frame and for every
$w\in W$
,
$M,w\models \varphi $
. Likewise, an axiom schema is valid on a frame iff every instance of the schema is valid on that frame.
In what follows and unless specified otherwise, we use
$\mathbf {L}$
as a metavariable for any classical modal logic, i.e., any logic that includes the minimal classical modal logic
$\textbf {E}$
. We assume that
$\mathbf {L}$
is specified in terms of a set of axioms on top of classical logic and (RE). We say that
$F = \langle W,N\rangle $
is an L-frame if it validates all
$\mathbf {L}$
-axioms; M is an
$\mathbf {L}$
-model if it is based on an
$\mathbf {L}$
-frame.
2.2. The logics
$ {\mathbf {EK}}$
and
$ {\mathbf {ECK}}$
Recall that
$ {\mathbf {EK}}$
is obtained by adding (RE) and (K) to propositional classical logic (cf. Section 1). The logic
$ {\mathbf {ECK}}$
is obtained by adding (C) to
$ {\mathbf {EK}}$
. It can be easily verified that a frame
$F = \langle W,N\rangle $
validates these axioms if and only if it satisfies the following conditions, respectively:
-
(k) if
$X\in N(w)$
and
$\overline {X} \cup Y \in N(w)$
, then
$Y\in N(w)$
. -
(c) if
$X\in N(w)$
and
$Y\in N(w)$
, then
$X\cap Y\in N(w)$
.
In what follows we will freely switch between these two frame conditions and frame validity (of the corresponding axioms), relying on the well-known correspondence between both.
2.3. Neighbourhood canonicity and (minimal) characteristic models
For any given
$\mathbf {L}$
, let
$W_{\mathbf {L}}$
be the set of all maximal
$\textbf {L}$
-consistent subsets of
$\mathfrak {L}$
. For all formulas
$\varphi $
, let
$|\varphi |_{\mathbf {L}} = \{w\in W_{\mathbf {L}} \mid \varphi \in w\}$
be the proof set of
$\varphi $
in
$\mathbf {L}$
. Let
$V_{\mathbf {L}}(p) = |p|_{\mathbf {L}}$
for all propositional variables p. We say that
$M = \langle W,N,V\rangle $
is a characteristic
$\mathbf {L}$
-model (equivalently, M is characteristic for
$\mathbf {L}$
) if and only if (i) M is an
$\mathbf {L}$
-model (hence,
$\langle W,N\rangle $
validates all instances of
$\mathbf {L}$
); (ii)
$W = W_{\mathbf {L}}$
; and (iii) M satisfies the truth lemma, i.e., for all
$w\in W_{\mathbf {L}}$
and
$\varphi \in \mathfrak {L}$
,
$$ \begin{align*}M,w\models \varphi \mbox{ iff } \varphi\in w.\end{align*} $$
Note that (i) and (iii) together imply that
$V = V_{\mathbf {L}}$
. We say that
$\mathbf {L}$
satisfies neighbourhood canonicity iff there is a characteristic
$\mathbf {L}$
-model.
A brief aside on terminology is in place. First, we use “neighbourhood canonicity” in the same sense as Surendonk [Reference Surendonk9, Reference Surendonk10] and in contrast to the standard notion of canonicity from the study of normal modal logics.Footnote
10
Recall that, in the context of normal modal logics, every logic comes with a unique canonical model. More precisely, in that setting, the canonical model for
$\mathbf {L}$
is the relational model
$\langle W,R,V\rangle $
that satisfies (ii) and (iii) and where
$R = \{(w,v)\in W\times W\mid \forall \varphi : \square \varphi \in w \Rightarrow \varphi \in v\}$
. A normal modal logic is canonical (satisfies canonicity) if its canonical model is based on a frame that validates that logic; as a matter of fact, not all normal modal logics are canonical in this sense [Reference Blackburn, de Rijke and Venema2, Chapter 4]. In contrast, in the setting of classical (non-normal) modal logics, it is common to speak of canonical models in plural, cf. [Reference Chellas3, Definition 9.3]. Here, a canonical model is any model that satisfies conditions (ii) and (iii). Characteristic models—a term we adopt here in the absence of a standard one—hence form a (strict) subclass of canonical models.Footnote
11
While it is fairly simple to define canonical models for any given classical modal logic
$\mathbf {L}$
, obtaining characteristic
$\mathbf {L}$
-models is not always so easy. To understand the first half of this claim, let
$$ \begin{align*}N^0_{\mathbf{L}}(w) =_{\textsf{df}} \{|\varphi|_{\mathbf{L}}\mid \square\varphi\in w\} .\end{align*} $$
The model
$M^0_{\mathbf {L}} = \langle W_{\mathbf {L}}, N^0_{\mathbf {L}}, V_{\mathbf {L}}\rangle $
is the basic (canonical) model for
$\mathbf {L}$
. Intuitively,
$M^0_{\mathbf {L}}$
is the simplest
$ {\mathbf {E}}$
-model that serves as a witness for every
$\mathbf {L}$
-consistent set of formulas. This follows from the following two lemmas:
Lemma 1. For every
$w\in W_{\mathbf {L}}$
and
$\varphi \in \mathfrak {L}$
:
$|\varphi |_{\mathbf {L}} \in N^0_{\mathbf {L}}(w)$
iff
$\square \varphi \in w$
.
Proof. Right to left is immediate in view of the construction. So suppose
$X\in N^0_{\mathbf {L}}(w)$
and
$X=|\varphi |_{ {\mathbf { L}}}$
. By the definition of
$N^0_{\mathbf {L}}$
, there is some
$\psi $
such that
$X= |\psi |_{ {\mathbf { L}}}$
and
$\square \psi \in w$
. Hence
$|\psi |_{\mathbf {L}} =|\varphi |_{\mathbf {L}}$
and hence
$\vdash \psi \leftrightarrow \varphi $
. By (RE),
$\square \varphi \in w$
.□
Lemma 2 (Truth Lemma)
For all
$w\in W_{\mathbf {L}}$
and all
$\varphi $
,
$M^0_{\mathbf {L}},w \models \varphi $
iff
$\varphi \in w$
. Hence, for all
$\varphi $
,
$\|\varphi \|^{M^0_{\mathbf {L}}} = |\varphi |_{\mathbf {L}}$
.
Proof. By a routine induction on the complexity of
$\varphi $
. The base case (
$\varphi \in \mathfrak {P}$
) and the classical connectives are safely left to the reader. For
$\varphi = \square \psi $
we have:
$M^0_{\mathbf {L}},w\models \varphi $
iff [by the semantic clause for
$\square $
]
$\|\psi \|^{M^0_{\mathbf {L}}} \in N^0_{\mathbf {L}}(w)$
iff [by the induction hypothesis]
$|\psi |_{\mathbf {L}} \in N^0_{\mathbf {L}}(w)$
iff [by Lemma 1]
$\square \psi \in w$
iff
$\varphi \in w$
.□
Whether
$M^0_{\mathbf {L}}$
is also an
$\mathbf {L}$
-model and hence a characteristic
$\mathbf {L}$
-model, depends on specific properties of
$\mathbf {L}$
. For a number of classical modal logics this is indeed the case, for others it is not.Footnote
12
$\textbf {EK}$
and
$\textbf {ECK}$
belong to the second category. In particular, we can easily show that
$N^0_{ {\mathbf {EK}}}$
does not satisfy frame condition (k), using a variant of an example from [Reference Pacuit8, Observation 2.40]:
Example 1. Consider any maximally consistent set
$w\in W_{ {\mathbf {EK}}}$
that contains
$\square p$
and
$\square (\neg p\vee q)$
. By the definition of
$N^0_{ {\mathbf {EK}}}$
,
$|p|_{ {\mathbf {EK}}}, |\neg p\vee q|_{ {\mathbf {EK}}}\in N^0_{ {\mathbf { EK}}}(w)$
. Note that the set of all subsets of
$|\neg p|_{ {\mathbf {EK}}}$
is uncountable.Footnote
13
So, since the formal language is countable, we can fix a
$Z\subset |\neg p|_{ {\mathbf {EK}}}$
such that (
$\star $
) for no
$\varphi $
,
$Z = |\varphi |_{ {\mathbf {EK}}}$
. Let
$X = |p|_{ {\mathbf {EK}}}$
and
$Y = Z\cup |p\wedge q|_{ {\mathbf {EK}}}$
. Note that
$\overline {X}\cup Y = |\neg p|_{ {\mathbf { EK}}}\cup Z\cup |p\wedge q|_{ {\mathbf {EK}}} = |\neg p\vee q|_{ {\mathbf {EK}}}$
. Hence,
$X, \overline {X}\cup Y\in N^0_{ {\mathbf { EK}}}(w)$
. Assume now that
$Y\in N^0_{ {\mathbf {EK}}}(w)$
. Then there must be some
$\psi $
such that
$\square \psi \in w$
and
$Y = |\psi |_{ {\mathbf {EK}}}$
. Since
$Z\cap |p\wedge q|_{ {\mathbf {EK}}} = \emptyset $
, it follows that
$Z = |\psi \wedge \neg p|_{ {\mathbf {EK}}}$
, contradicting (
$\star $
). Hence,
$Y\not \in N^0_{ {\mathbf {EK}}}(w)$
and hence
$N^0_{ {\mathbf {EK}}}(w)$
does not satisfy (k).
The same example can also be used to show that
$M^0_{ {\mathbf {ECK}}}$
is not an
$ {\mathbf {ECK}}$
-model. So more is needed to obtain a characteristic
$ {\mathbf {EK}}$
-model, resp. a characteristic
$ {\mathbf {ECK}}$
-model.
Our fix to this problem is in a sense straightforward: we close all the neighbourhood sets
$N^0_{\mathbf {L}}$
under (k). Accordingly, the minimal characteristic
$\textbf {EK}$
-model is
$M_{ {\mathbf {EK}}} = \langle W_{ {\mathbf {EK}}}, N_{ {\mathbf { EK}}}, V_{ {\mathbf {EK}}}\rangle $
, where for all
$w\in W_{ {\mathbf {EK}}}$
,
$N_{ {\mathbf {EK}}}(w)$
is the smallest set
$Q\subseteq \wp (W_{ {\mathbf {EK}}})$
such that
$N^0_{ {\mathbf {EK}}}\subseteq Q$
and Q satisfies (k). Likewise, the minimal characteristic
$ {\mathbf {ECK}}$
-model is
$M_{ {\mathbf {ECK}}} = \langle W_{ {\mathbf {ECK}}}, N_{ {\mathbf {ECK}}}, V_{ {\mathbf {ECK}}}\rangle $
, where for all
$w\in W_{ {\mathbf {ECK}}}$
,
$N_{ {\mathbf {ECK}}}(w)$
is the smallest set
$Q\subseteq \wp (W_{ {\mathbf {ECK}}})$
such that
$N^0_{ {\mathbf {ECK}}}\subseteq Q$
and Q satisfies (c) and (k).
Clearly these constructions satisfy items (i) and (ii) in our definition of a characteristic
$\mathbf {L}$
-model. The difficulty now consists in proving the truth lemma for
$M_{ {\mathbf {EK}}}$
, respectively
$M_{ {\mathbf {ECK}}}$
. In other words, we need to prove that, when closing the neighbourhood sets under (k), respectively (c) and (k), we are not making any new formulas of the form
$\square \varphi $
true. This is the key problem; we solve it for
$\textbf {EK}$
in Section 3 and for
$ {\mathbf {ECK}}$
in Section 4.
3. Circumscribing the minimal
$\textbf {EK}$
-model
We are going to show that the minimal
$ {\mathbf {EK}}$
-model can be circumscribed in a way that facilitates proving the truth lemma and condition (k) for this model. In order to present our proof in its most general form—and to make it amenable to variations such as those in Section 5—we first introduce a new notion. Say an arbitrary model
$M = \langle W,N,V\rangle $
is
$\textbf {L}$
-fähig if and only if the following two conditions hold:
-
(F1) For all
$\mathbf {L}$
-axioms
$\varphi $
, for all
$w\in W$
:
$M,w\models \varphi $
. -
(F2) For all
$w\in W$
, for all
$X\in N(w)$
: there is a
$\varphi $
such that
$X = \|\varphi \|^{M}$
.
Condition (F1) basically says that M must be a model for
$\mathbf {L}$
. Condition (F2) states that all the neighbourhoods for every given world w in the domain of M are expressible in M. Note that the basic canonical model for
$ {\mathbf {EK}}$
is
$\textbf {EK}$
-fähig, in view of Lemma 2 and the definition of
$N^0_{\mathbf {L}}$
respectively.
In what follows, we show that whenever some
$ {\mathbf {E}}$
-model is
$\textbf {EK}$
-fähig, we can transform it into an equivalent
$ {\mathbf {EK}}$
-model. Thus, in particular, we can transform the basic canonical model for
$ {\mathbf {EK}}$
into an equivalent
$ {\mathbf {EK}}$
-model. We will then also show that the resulting model is a characteristic
$ {\mathbf {EK}}$
-model (Theorem 1) and that it is in fact the minimal characteristic
$ {\mathbf {EK}}$
-model (Theorem 2).
Fix an
$ {\mathbf {E}}$
-model
$M^0 = \langle W,N^0,V\rangle $
that is
$ {\mathbf {EK}}$
-fähig. Let
$M^1 = \langle W,N^1,V\rangle $
, where
$$ \begin{align} N^1 (w) = N^0(w) \cup \{Y\subseteq W\mid \exists X_1,\ldots,X_n \in N^0(w): \overline{X_1}\cup\ldots\cup\overline{X_n}\cup Y\in N^0(w)\}. \end{align} $$
We show that
$M^1$
is pointwise equivalent to
$M^0$
(Lemma 3) and that
$M^1$
is an
$\textbf {EK}$
-model (Lemma 4).
Lemma 3 (Truth Preservation)
For all
$w\in W$
, for all
$\varphi $
,
$M^0,w\models \varphi $
iff
$M^1,w\models \varphi $
.
Proof. By an induction on the complexity of
$\varphi $
. We only need to consider the case for
$\varphi = \square \psi $
. (
$\Rightarrow $
) Suppose
$M^0,w\models \varphi $
. Then
$\|\psi \|^{M^0} \in N^0(w)$
. By the definition of
$N^1$
,
$\|\psi \|^{M^0}\in N^1(w)$
. By the induction hypothesis,
$\|\psi \|^{M^0} = \|\psi \|^{M^1}$
and so
$\|\psi \|^{M^1}\in N^1(w)$
. Hence,
$M^1,w\models \square \psi $
.
(
$\Leftarrow $
) Suppose
$M^1,w\models \varphi $
. So
$\|\psi \|^{M^1}\in N^1(w)$
and hence by the induction hypothesis,
$\|\psi \|^{M^0}\in N^1(w)$
. Assume now that
$\|\psi \|^{M^0}\not \in N^0(w)$
. Then there are
$X_1,\ldots , X_n$
such that
$X_1, \ldots , X_n, \overline {X_1}\cup \cdots \cup \overline {X_n}\cup \|\psi \|^{M^0}\in N^0(w)$
. By (F2), there are
$\chi _1, \ldots , \chi _n$
such that each
$X_i = \|\chi _i\|^{M^0}$
and
$M^0,w\models \square \chi _1, \ldots , M^0,w\models \square \chi _n, M^0,w\models \square (\neg \chi _1\vee \cdots \vee \neg \chi _n\vee \psi )$
. By (F1) we obtain:
-
$M^0,w\models \square (\neg \chi _2\vee \cdots \vee \neg \chi _n\vee \psi ).$
-
$M^0,w\models \square (\neg \chi _3\vee \cdots \vee \neg \chi _n\vee \psi ).$
-
$\vdots $
-
$M^0,w\models \square \psi .$
Hence,
$\|\psi \|^{M^0} \in N^0(w)$
—a contradiction. So
$\|\psi \|^{M^0} \in N^0(w)$
and thus
$M^0,w\models \varphi $
.□
Lemma 4 (Closure)
$M^1$
satisfies (k). That is, if
$X, \overline {X }\cup Y \in N^1(w)$
, then
$Y \in N^1(w)$
.
Proof. Suppose there are
$w\in W$
and
$X ,Y $
such that
$X , \overline {X }\cup Y \in N^1(w)$
. So there are
$n,m\in \mathbb {N}$
and
$Z_1, \ldots , Z_n$
,
$T_1,\ldots , T_m$
, and
$V_1$
,
$V_2$
such that each of the following hold:
-
(i)
$Z_1 \in N^0(w),\ldots , Z_n\in N^0(w).$
-
(ii)
$V_1 = \overline {Z_1}\cup \cdots \cup \overline {Z_n}\cup X \in N^0(w).$
-
(iii)
$T_1 \in N^0(w),\ldots ,T_m\in N^0(w).$
-
(iv)
$V_2 = \overline {T_1}\cup \cdots \cup \overline {T_m}\cup \overline {X }\cup Y \in N^0(w).$
Note that n or m or both may be
$0$
; our argument below covers each of these border cases. The general outline of the argument goes as follows. We construct a set
$X^*$
from the sets
$V_1$
,
$V_2$
, and
$Z_1, \ldots , Z_n$
by boolean operations. This
$X^*$
serves as a “shortcut” for X in the derivation of Y. That is, we first prove that
$X^*\in N^0(w)$
. Next, we show that
$V_2 = \overline {T_1}\cup \cdots \cup \overline {T_m}\cup \overline {X^* }\cup Y$
(cf. equation 7 below). Once there, we can directly use
$X^*$
instead of X, in the derivation of Y.
By (F2), each of the sets
$Z_1, \ldots , Z_n,V_1,T_1,\ldots ,T_m,V_2$
corresponds to the truth set of some formula in
$M^0$
(and by Lemma 3, also in
$M^1$
). For the sake of readability, we omit the superscript
$M^0$
in writing down these truth sets. For each
$Z_i$
, let
$\chi _i$
be such that
$Z_i = \|\chi _i\|$
and let for each
$T_j$
,
$\tau _j$
be such that
$T_j = \|\tau _j\|$
. Moreover, let
$V_1 = \|\theta _1\|$
and let
$V_2 = \|\theta _2\|$
. Finally, let
$\varepsilon = \neg \theta _2 \vee (\theta _1 \wedge \chi _1 \wedge \cdots \wedge \chi _n)$
and
$X ^* = \overline {V_2} \cup (V_1 \cap Z_1 \cap \cdots \cap Z_n)$
. Note that, if
$n=0$
, then
$\epsilon = \neg \theta _2\vee \theta _1$
and
$X ^* = \overline {V_2} \vee V_1$
. By well-known properties of the classical connectives,
$$ \begin{align} X^* = \|\varepsilon\|.\end{align} $$
Note that
$\overline {V_2} = T_1\cap \cdots \cap T_m \cap X \cap \overline {Y }$
and hence,
$\overline {V_2} \subseteq X $
. Also, since
$V_1 = \overline {Z_1}\cup \cdots \cup \overline {Z_n}\cup X $
,
$V_1 \cap Z_1 \cap \cdots \cap Z_n \subseteq X $
. Taken together, this implies that
$$ \begin{align} X^* \subseteq X. \end{align} $$
We now prove that
$$ \begin{align} V_1 = \overline{Z_1}\cup \cdots\cup \overline{Z_n}\cup X ^*. \end{align} $$
(
$\subseteq $
) Suppose that
$x\in V_1$
. Hence,
$x\in V_1 \cap Z_1 \cap \cdots \cap Z_n$
or
$x\in \overline {Z_1}\cup \cdots \cup \overline {Z_n}$
. Hence,
$x\in \overline {Z_1}\cup \cdots \cup \overline {Z_n} \cup X ^*$
. (
$\supseteq $
) Immediate in view of (3) and since
$V_1 = \overline {Z_1}\cup \cdots \cup \overline {Z_n}\cup X $
.
By (4), (2), and the fact that each
$Z_i = \|\chi _i\|$
,
$$ \begin{align} V_1 = \|\neg\chi_1 \vee\cdots\vee\neg\chi_n \vee\varepsilon\|. \end{align} $$
By (5) and Lemma 1, and since
$V_1 \in N^0(w)$
,
$M^0,w\models \square (\neg \chi _1 \vee \cdots \vee \neg \chi _n \vee \varepsilon )$
. Also, in view of the preceding,
$M^0,w\models \square \chi _1, \ldots , \square \chi _n$
. So by (F1), we can apply the K-axiom n times (cf. the proof of Lemma 3) to derive that
$M^0,w\models \square \varepsilon $
and hence, by (2) and Lemma 1 again,
$$ \begin{align} X ^* \in N^0(w).\end{align} $$
Finally, we prove that
$$ \begin{align} V_2 = \overline{T_1}\cup \cdots\cup\overline{T_m}\cup \overline{X ^*}\cup Y. \end{align} $$
(
$\subseteq $
) By (3),
$\overline {X }\subseteq \overline {X ^*}$
. Hence,
$V_2 = \overline {T_1}\cup \cdots \cup \overline {T_m}\cup \overline {X }\cup Y \subseteq \overline {T_1}\cup \cdots \cup \overline {T_m}\cup \overline {X ^*}\cup Y $
.
(
$\supseteq $
) Note that
$\overline {X ^*} = V_2 \cap (\overline {V_1} \cup \overline {Z_1} \cup \cdots \cup \overline {Z_n}) \subseteq V_2$
. Hence,
$\overline {T_1}\cup \cdots \cup \overline {T_m}\cup \overline {X ^*}\cup Y \subseteq \overline {T_1}\cup \cdots \cup \overline {T_m}\cup V_2\cup Y = V_2$
.
By (7) and (iv),
$$ \begin{align} \overline{T_1}\cup \cdots\cup\overline{T_m}\cup \overline{X ^*}\cup Y \in N^0(w). \end{align} $$
By (6), (8), and (iii), our definition of
$N^1$
guarantees that
$Y \in N^1(w)$
.□
For what follows, recall that
$M^0_{ {\mathbf {EK}}}$
is the basic canonical model for
$ {\mathbf {EK}}$
. Let
$M^1_{ {\mathbf { EK}}}$
be obtained from
$M^0_{ {\mathbf {EK}}}$
, by extending
$N^0_{ {\mathbf {EK}}}$
according to Equation 1. We have:
Theorem 1.
$M^1_{ {\mathbf {EK}}}$
is a characteristic model for
$ {\mathbf {EK}}$
.
Proof. Note that
$M^0_{ {\mathbf {EK}}}$
is
$\textbf {EK}$
-fähig by Lemma 2 and in view of the definition of
$N^0_{\mathbf {L}}$
. By Lemma 4,
$M^1_{ {\mathbf {EK}}}$
is an
$\textbf {EK}$
-model. Consider now an
$\textbf {EK}$
-consistent set
$\Gamma $
. Let
$\Delta $
be a maximal
$ {\mathbf {EK}}$
-consistent extension of
$\Gamma $
. By Lemma 2,
$M^0_{ {\mathbf {EK}}},\Delta \models \psi $
for every
$\psi \in \Gamma $
. By Lemma 3,
$M^1_{ {\mathbf { EK}}},\Delta \models \psi $
for every
$\psi \in \Gamma $
.□
Recall that the minimal characteristic
$ {\mathbf {EK}}$
-model is
$M_{ {\mathbf {EK}}} = \langle W_{ {\mathbf { EK}}},N_{ {\mathbf {EK}}},V_{ {\mathbf {EK}}}\rangle $
, where
$N_{ {\mathbf {EK}}}(w)$
denotes the closure of
$N^0_{ {\mathbf {EK}}}(w)$
under (k). We now prove that
$M_{ {\mathbf {EK}}} = M^1_{ {\mathbf {EK}}} $
.
Lemma 5. For all
$w\in W_{ {\mathbf {EK}}}$
,
$N^1_{ {\mathbf {EK}}}(w) = N_{ {\mathbf {EK}}}(w)$
.
Proof. Note first that
$N^1_{ {\mathbf {EK}}}(w) \subseteq N_{ {\mathbf {EK}}}(w)$
. That is, suppose that
$X\in N^1_{ {\mathbf {EK}}}(w)$
. Then there are
$Y_1, \ldots , Y_n \subseteq W_{ {\mathbf {EK}}}$
such that
$Y_1, \ldots , Y_n, \overline {Y_1}\cup \cdots \cup \overline {Y_n} \cup X\in N^0_{ {\mathbf {EK}}}(w)$
. Applying (k) n times, we obtain:
-
$\overline {Y_2}\cup \cdots \cup \overline {Y_n} \cup X\in N_{ {\mathbf {EK}}}(w).$
-
$\overline {Y_3}\cup \cdots \cup \overline {Y_n} \cup X\in N_{ {\mathbf {EK}}}(w).$
-
$\vdots $
-
$X\in N_{ {\mathbf {EK}}}(w).$
By Lemma 4 and since
$N^0_{ {\mathbf {EK}}}(w) \subseteq N^1_{ {\mathbf {EK}}}(w)$
, it holds that
$N_{ {\mathbf { EK}}}(w)\subseteq N^1_{ {\mathbf {EK}}}(w)$
. Hence,
$N^1_{ {\mathbf {EK}}}(w) = N_{ {\mathbf {EK}}}(w)$
.□
Lemma 5 immediately gives us:
Theorem 2.
$M^1_{ {\mathbf {EK}}}$
is the minimal characteristic
$ {\mathbf {EK}}$
-model.
4. Circumscribing the minimal
$\textbf {ECK}$
-model
Let us now turn to the logic
$ {\mathbf {ECK}}$
. To present our circumscription technique for this logic in the most general way, we again start from an arbitrary model
$M^0 = \langle W,N^0,V\rangle $
that is
$\textbf {ECK}$
-fähig and we prove that it can be transformed into a pointwise equivalent
$ {\mathbf {ECK}}$
-model. After that, we return to the specific case of the basic canonical model for
$ {\mathbf {ECK}}$
.
At first sight, the axiom (C) makes life easier for us. First, using the axiom (C), it can be shown by standard means that
$N^0$
obeys (c):
Observation 1. For all
$w\in W$
: if
$X_1,\ldots , X_n\in N^0(w)$
then
$X_1\cap \cdots \cap X_n\in N^0(w)$
.
Relying on this property, we can show that a single application of condition (k) to each
$N^0(w)$
gives us the same neighbourhoods as our more intricate characterization given by equation (1):
Lemma 6. For all
$w\in W_{}$
and all
$Y\subseteq W_{}$
, the following claims are equivalent:
-
(i) There is an
$X\in N^0(w)$
such that
$\overline {X}\cup Y \in N^0(w)$
. -
(ii) There are
$X_1, \ldots , X_n\in N^0(w)$
such that
$\overline {X_1}\cup \cdots \cup \overline {X_n}\cup Y \in N^0(w)$
.
Proof. The implication from (i) to (ii) is obvious. So suppose (ii) holds. Let
$X = X_1\cap \cdots \cap X_n$
. Then
$X\in N^0(w)$
by Observation 1 and
$\overline {X} = \overline {X_1}\cup \cdots \cup \overline {X_n}$
. Hence,
$\overline {X}\cup Y\in N^0(w)$
.□
So, we could simply define our target model as
$M^1_{} = \langle W_{}, N^1,V_{}\rangle $
, where for all
$w\in W_{}$
,
$$ \begin{align} N^1(w) =_{\textsf{df}} N^0(w) \cup \{Y\subseteq W_{}\mid \exists X\in N^0(w):\overline{X}\cup Y\in N^0(w)\}.\end{align} $$
By Lemma 6, and reasoning in entirely the same way as we did in the previous section, one can show that
$M^1_{}$
satisfies condition (k). Unfortunately, we now encounter difficulties in showing that condition (c) is satisfied for this new model. So, rather than working with
$M^1_{}$
, we further enrich the neighbourhoods
$N^1(w)$
, by closing them under intersection:
$$ \begin{align} N^2(w) =_{\textsf{df}} \{X_1\cap \cdots\cap X_n\mid X_1,\ldots, X_n\in N^1(w)\}. \end{align} $$
Obviously, (c) is satisfied for
$N^2$
. We now prove that the model
$M^2_{} = \langle W_{}, N^2,V_{}\rangle $
is equivalent to
$M^0_{}$
(Lemma 8) and satisfies (k) (Lemma 9). Let us start with a basic observation.
Lemma 7. For all
$w\in W_{}$
:
$X\in N^2(w)$
iff one of the following three conditions obtains
-
1.
$X\in N^0(w)$
. -
2. there are
$Z_1,\ldots , Z_n, Z\in N^0(w)$
and
$Y_1,\ldots ,Y_n \subseteq W_{}$
such that
$\overline {Z_1}\cup Y_1,\ldots , \overline {Z_n}\cup Y_n \in N^0(w)$
and
$X = Y_1\cap \cdots \cap Y_n\cap Z$
. -
3. there are
$Z_1,\ldots , Z_n\in N^0(w)$
and
$Y_1,\ldots ,Y_n \subseteq W_{}$
such that
$\overline {Z_1}\cup Y_1,\ldots , \overline {Z_n}\cup Y_n \in N^0(w)$
and
$X = Y_1\cap \cdots \cap Y_n$
.
Proof. (
$\Leftarrow $
) Obviously, (1.) implies that
$X\in N^2(w)$
, since
$N^0(w)\subseteq N^1(w) \subseteq N^2(w)$
. To see why also (2.) and (3.) imply that
$X\in N^2(w)$
, note that both (2.) and (3.) imply that
$Y_1,\ldots , Y_n\in N^1(w)$
. The rest is immediate in view of the definition of
$N^2$
.
(
$\Rightarrow $
) Suppose that
$X\in N^2(w)$
. Let
$Y_1,\ldots ,Y_m\in N^1(w)$
be such that
$X=Y_1\cap \cdots \cap Y_m$
. Without loss of generality, suppose
$n\in \{0,\ldots , m\}$
is such that
$Y_1,\ldots , Y_n \in N^1(w) \setminus N^0(w)$
and
$Y_{n+1},\ldots , Y_m\in N^0(w)$
. Case 1:
$n=0$
. Then by Observation 1,
$X\in N^0(w)$
and hence (1.) holds. Case 2:
$0 < n <m$
. Let
$Z = Y_{n+1}\cap \cdots \cap Y_m$
. By Observation 1,
$Z\in N^0(w)$
. Hence, (2.) holds. Case 3:
$n=m$
. Then (3.) holds.□
Lemma 8 (Truth Preservation)
For all
$\varphi $
and all
$w\in W_{}$
,
$M^0_{},w\models \varphi $
iff
$M^2_{},w\models \varphi $
.
Proof. As usual, we prove this by an induction on the complexity of
$\varphi $
. We need only care about the case
$\varphi =\square \psi $
, and for that case, left to right is trivial in view of the fact that
$N^0(w)\subseteq N^2(w)$
. For right to left, suppose that
$M^2_{},w\models \square \psi $
. Assume for contradiction that
$M^0_{},w\not \models \square \psi $
and hence
$\|\psi \|^{M^0}_{} \not \in N^0(w)$
.
By Lemma 7, there are only two cases to consider, viz. items (2.) and (3.) of that lemma for
$X = \|\psi \|^{M^0}_{}$
. We will show that (2.) leads to a contradiction; the reasoning for (3.) is completely analogous but simpler—one just has to omit Z in what follows.
So suppose there are
$Z_1,\ldots , Z_n,Z\in N^0(w)$
and
$Y_1,\ldots , Y_n$
such that
$\overline {Z_1}\cup Y_1, \ldots , \overline {Z_n}\cup Y_n\in N^0(w)$
and
$Y_1 \cap \cdots \cap Y_n\cap Z = \|\psi \|^{M^0}_{}$
. In the remainder of this proof, let i range over
$\{1,\ldots ,n\}$
. Let
$Y = Y_1\cap \cdots \cap Y_n$
, so that
$X = Y\cap Z$
.
For all i, let
$\overline {Z_i}\cup Y_i = V_i$
. Note that since they are all members of
$N^0(w)$
, all the
$Z_i$
and all the
$V_i$
are the truth set of some formula in
$M^0$
. Let, for all i,
$\xi _i$
be such that
$V_i=\|\xi _i\|^{M^0}_{}$
and
$\tau _i$
be such that
$Z_i=\|\tau _i\|^{M^0}_{}$
. For all i, let
$Y^*_i = (V_i \cap Z_i) \cup (X \cap \overline {Z_i})$
. Note that for all i,
$Y^*_i = \|(\xi _i \wedge \tau _i) \vee (\psi \wedge \neg \tau _i)\|^{M^0}_{}$
. We henceforth abbreviate
$(\xi _i \wedge \tau _i) \vee (\psi \wedge \neg \tau _i)$
by
$\theta _i$
. The following can be easily verified for all i:
$$ \begin{align} Y^*_i \subseteq Y_i. \end{align} $$
$$ \begin{align} (V_i \setminus \overline{Z_i}) \subseteq Y^*_i. \end{align} $$
By (11) and (12), for all
$i\in \{1,\ldots ,n\}$
:
$$ \begin{align} V_i = \overline{Z_i}\cup Y^*_i. \end{align} $$
By (13),
$V_i = \|\neg \tau _i\vee \theta _i\|^{M^0}$
. Note that, for all such i,
$M^0,w \models \square (\neg \tau _i \vee \theta _i )$
. Since also
$M^0,w\models \square \tau _i \in w$
and by (F1), we can apply axiom (K) to derive that
$M^0,w\models \square \theta _i $
for all i. Consequently,
$Y^*_1,\ldots , Y^*_n\in N^0(w)$
. By Observation 1,
$$ \begin{align} Y^*_1 \cap \cdots\cap Y^*_n\cap Z\in N^0(w).\end{align} $$
We now prove that
$$ \begin{align} Y^*_1 \cap \cdots \cap Y^*_n\cap Z = Y \cap Z. \end{align} $$
(
$\subseteq $
) Immediate by (11) and since
$Y=Y_1\cap \cdots \cap Y_n$
. (
$\supseteq $
) Suppose that
$x\in Y\cap Z$
. So
$x\in Y_1\cap \cdots \cap Y_n$
and
$x\in Z$
. Let
$i\in \{1,\ldots ,n\}$
. So
$x\in Y_i$
. Case 1:
$x\in Z_i$
. Then
$x\in Z_i \cap Y_i$
. Since
$V_i = \overline {Z_i}\cup Y_i$
, it follows that
$x\in V_i \cap Z_i$
and hence
$x\in Y^*_i$
. Case 2:
$x\not \in Z_i$
. Then
$x\in Y\cap Z \cap \overline {Z_i}$
, so
$x\in X\cap \overline {Z_i}$
and hence
$x\in Y^*_i$
.
By (14) and (15),
$Y\cap Z\in N^0(w)$
. Hence,
$X\in N^0(w)$
, contradicting our original supposition.□
Lemma 9 (Closure)
For all
$w\in W$
: if
$X, \overline {X}\cup Y\in N^2(w)$
, then
$Y\in N^2(w)$
.
Proof. Suppose the antecedent holds. Then, relying on Lemma 7, we need to distinguish six cases, depending on whether (1.), (2.), or (3.) of that observation holds for X and for
$\overline {X}\cup Y$
. We will focus on the most complicated of these cases, i.e., (2.) holds for both X and
$\overline {X}\cup Y$
. The proofs for the other cases are simplifications of the proof we give below.
So suppose that there are
$Z_1,\ldots , Z_n, Z, Y_1, \ldots , Y_n, Z^{\prime }_1,\ldots , Z^{\prime }_m,Z^{\prime },Y^{\prime }_1,\ldots ,Y^{\prime }_m$
such that each of the following hold:
-
(i)
$Z_1,\ldots , Z_n,Z\in N^0(w)$
. -
(ii)
$\overline {Z_1}\cup Y_1, \ldots , \overline {Z_n}\cup Y_n \in N^0(w)$
. -
(iii)
$Y_1\cap \cdots \cap Y_n\cap Z = X$
. -
(iv)
$Z^{\prime }_1,\ldots , Z^{\prime }_m,Z^{\prime }\in N^0(w)$
. -
(v)
$\overline {Z^{\prime }_1}\cup Y^{\prime }_1, \ldots , \overline {Z^{\prime }_m}\cup Y^{\prime }_m \in N^0(w)$
. -
(vi)
$Y^{\prime }_1\cap \cdots \cap Y^{\prime }_m\cap Z^{\prime } = \overline {X}\cup Y$
.
In the remainder of this proof, let i range over
$\{1,\ldots ,n\}$
and j over
$\{1,\ldots ,m\}$
. Our argument follows the main overall strategy that we used to prove Lemma 4, but it is more complicated in the details. In the first part of the proof, we define several “shortcuts”
$X^*_{i,j}$
(one for each
$(i,j) \in \{1,\ldots , n\}\times \{1,\ldots ,m\}$
) and show that these are in
$N^0(w)$
. Next, for every given j, we use the sets
$X^*_{i,j}$
to derive another “shortcut”
$Y^*_j \in N^1(w)$
. In the third and last part of the proof, we show that the intersection of all the
$Y^*_j$
and
$Z^{\prime }$
equals Y, and hence
$Y\in N^2(w)$
.
Part 1. Let
$V_i = \overline {Z_i}\cup Y_i$
and let
$V^{\prime }_j = \overline {Z^{\prime }_j}\cup Y^{\prime }_j$
. Note that
$$ \begin{align} V^{\prime}_j =\overline{Z^{\prime}_j}\cup (Y^{\prime}_1\cap \cdots\cap Y^{\prime}_m\cap Z^{\prime}) \cup \left(Y^{\prime}_j\cap \left(\bigcup_{1\leq k\leq m, k\neq j} \overline{Y^{\prime}_k} \cup \overline{Z^{\prime}}\right)\right).\end{align} $$
and hence, by (vi),
$$ \begin{align} V^{\prime}_j =\overline{Z^{\prime}_j}\cup \overline{X}\cup Y \cup \left(Y^{\prime}_j\cap \left(\bigcup_{1\leq k\leq m, k\neq j} \overline{Y^{\prime}_k} \cup \overline{Z^{\prime}}\right)\right).\end{align} $$
By (iii),
$$ \begin{align} V^{\prime}_j =\overline{Z^{\prime}_j}\cup \overline{Y_1} \cup\cdots\cup \overline{Y_n}\cup \overline{Z} \cup Y \cup \left(Y^{\prime}_j\cap \left(\bigcup_{1\leq k\leq m, k\neq j} \overline{Y^{\prime}_k} \cup \overline{Z^{\prime}}\right)\right).\end{align} $$
By (18), for all
$i,j$
:
$$ \begin{align}\overline{V^{\prime}_j} \subseteq Y_i. \end{align} $$
For all
$i,j$
, let
$X^*_{i,j} = \overline {V^{\prime }_j}\cup (V_i \cap Z_i)$
. Since
$(V_i\cap Z_i)\subseteq Y_i$
and by (19), for all
$i,j$
, each of the following hold:
$$ \begin{align} X^*_{i,j}\subseteq Y_i. \end{align} $$
$$ \begin{align} V_i\cap Z_i \subseteq X^*_{i,j}.\end{align} $$
$$ \begin{align} V_i = \overline{Z_i}\cup X^*_{i,j}. \end{align} $$
Note that each
$X^*_{i,j}$
is the truth set of some
$\tau _i$
in
$M^0$
, since it is a boolean combination of
$V^{\prime }_j$
,
$V_i$
, and
$Z_i$
, each of which are in
$N^0(w)$
, and since by (F2), every member of
$N^0(w)$
is itself a truth set of a formula in
$M^0$
. Hence, by condition (F1) and axiom (K), and since each
$Z_i\in N^0(w)$
, we can infer that for all
$i,j$
:
$$ \begin{align} X^*_{i,j}\in N^0(w).\end{align} $$
Part 2. We now reason again about the
$V^{\prime }_j$
. First, for all
$i,j$
:
$$ \begin{align} \overline{X^*_{i,j}} \subseteq V^{\prime}_j.\end{align} $$
By (20),
$$ \begin{align} \overline{Y_i}\subseteq \overline{X^*_{i,j}}.\end{align} $$
From the latter two observations and in view of (18), we can infer:
$$ \begin{align} V^{\prime}_j = \overline{Z^{\prime}_j}\cup \overline{X^*_{1,j}}\cup \cdots\cup \overline{X^*_{n,j}} \cup \overline{Z} \cup Y \cup \left(Y^{\prime}_j \cap \left(\bigcup_{1\leq k\leq m, k\neq j} \overline{Y^{\prime}_k} \cup \overline{Z^{\prime}}\right)\right).\end{align} $$
By (23), since
$Z^{\prime }_j\in N^0(w)$
and
$Z\in N^0(w)$
, and by Lemma 6, we can infer that for all j,
$$ \begin{align}Y \cup \left(Y^{\prime}_j \cap \left(\bigcup_{1\leq k\leq m, k\neq j} \overline{Y^{\prime}_k} \cup \overline{Z^{\prime}}\right)\right) \in N^1(w).\end{align} $$
Let, for all j,
$Y^*_j = Y \cup (Y^{\prime }_j \cap (\bigcup _{1\leq k\leq m, k\neq j} \overline {Y^{\prime }_k} \cup \overline {Z^{\prime }})) $
.
Part 3. By the definition of
$N^2(w)$
and since
$Z^{\prime }\in N^0(w)$
,
$$ \begin{align} \bigcap_{1\leq j\leq m} Y^*_j \cap Z^{\prime} \in N^2(w).\end{align} $$
We can rewrite the latter set as follows:
-
$\bigcap _{1\leq j\leq m} Y^*_j\cap Z^{\prime }$
-
$= \bigcap _{1\leq j\leq m} (Y \cup (Y^{\prime }_j \cap (\bigcup _{1\leq k\leq m, k\neq j} \overline {Y^{\prime }_k} \cup \overline {Z^{\prime }})))\cap Z^{\prime } $
-
$= (Y\cup (Y^{\prime }_1\cap \cdots \cap Y^{\prime }_m\cap \overline {Z^{\prime }})) \cap Z^{\prime }$
-
$= (Y\cap Z^{\prime }) \cup (Y^{\prime }_1\cap \cdots \cap Y^{\prime }_m\cap \overline {Z^{\prime }} \cap Z^{\prime })$
-
$=Y\cap Z^{\prime }$
.
Hence,
$Y\cap Z^{\prime }\in N^2(w)$
. Since
$Y^{\prime }_1\cap \cdots \cap Y^{\prime }_m\cap Z^{\prime } = \overline {X}\cup Y$
,
$Y\subseteq Z^{\prime }$
. Hence,
$Y\cap Z^{\prime } = Y$
. So we obtain that
$Y \in N^2(w)$
.□
Recall that
$M^0_{ {\mathbf {ECK}}} = \langle W_{ {\mathbf {ECK}}},N^0_{ {\mathbf {ECK}}},V_{ {\mathbf {ECK}}}\rangle $
is the basic canonical model for
$ {\mathbf {ECK}}$
. It is easily observed that
$M^0_{ {\mathbf {ECK}}}$
is
$ {\mathbf { ECK}}$
-fähig. Let
$M^2_{ {\mathbf {ECK}}}$
be defined from
$M^0_{ {\mathbf {ECK}}}$
, in accordance with equations (9) and (10). This gives us:
Theorem 3.
$M^2_{ {\mathbf {ECK}}}$
is a characteristic model for
$ {\mathbf {ECK}}$
.
Theorem 4.
$M^2_{ {\mathbf {ECK}}}$
is the minimal
$ {\mathbf {ECK}}$
-model.
Proof. Fix an arbitrary
$w\in W$
. It suffices to show that
$N^2_{ {\mathbf {ECK}}}(w)$
is the smallest set Q such that (i)
$N^0_{ {\mathbf {ECK}}}(w)\subseteq Q$
and (ii) Q is closed under (k) and (c). In view of the preceding, it can easily verified that both (i) and (ii) hold for
$N^2_{ {\mathbf {ECK}}}(w)$
. Consider now an arbitrary
$Z\in N^2_{ {\mathbf {ECK}}}(w)$
and fix an Q that satisfies both (i) and (ii). By the definition of
$N^2_{ {\mathbf {ECK}}}(w)$
, there must be
$X_1, Y_1, \ldots , X_n,Y_n$
such that
$X_1, \ldots , X_n, \overline {X_1}\cup Y_1, \ldots , \overline {X_n}\cup Y_n\in N^0_{ {\mathbf {ECK}}}(w)$
, and
$Y_1\cap \cdots \cap Y_n = Z$
. Since Q satisfies (i),
$X_1, \ldots , X_n, \overline {X_1}\cup Y_1, \ldots , \overline {X_n}\cup Y_n\in Q$
. Since Q is closed under (k),
$Y_1,\ldots , Y_n\in M$
and hence, since Q satisfies (c), also
$Z\in Q$
. So
$N^2_{ {\mathbf {ECK}}}(w) \subseteq Q$
, and hence
$N^2_{ {\mathbf {ECK}}}(w)$
is the smallest set that satisfies (i) and (ii).□
5. More logics
We finish this paper by pointing out how our results generalize to some extensions of
$\textbf {EK}$
and
$\textbf {ECK}$
. We first consider four stronger logics (Section 5.1); after that, we consider conservative extensions of the resulting class of six logics with a global modality (Section 5.2).
5.1. Stronger logics
We focus here on the frame conditions specified in Table 1 and the corresponding axioms. We follow Chellas’ naming conventions, thus e.g., the logic obtained by adding (P) to
$ {\mathbf {EK}}$
(
$ {\mathbf {ECK}}$
) is
$ {\mathbf {EKP}}$
(
$ {\mathbf {ECKP}}$
). As will become clear, the insights from the two previous sections can be used to obtain characteristic models for all the logics from Table 1.
Some familiar axioms and frame conditions for classical modal logics, and the logics obtained by adding them to
$\textbf {EK}$
, resp.
$\textbf {ECK}$
.
Adding (M) to
$\textbf {EK}$
turns (C) into a derivable rule:
Theorem 5. (C) is derivable in
$\textbf {EKM}$
.
Proof. Suppose
$\square \varphi $
and
$\square \psi $
. By (M) and the first premise, we get
$\square (\varphi \vee \neg \psi )$
and hence by (RE),
$\square ((\varphi \wedge \psi ) \vee \neg \psi )$
. By the latter and the second premise, using (K), we get
$\square (\varphi \wedge \psi )$
.□
Conversely, it can easily be checked that (K) is derivable in
$ {\mathbf {ECM}}$
. As a corollary,
$ {\mathbf {EKM}} = {\mathbf { ECKM}} = {\mathbf {ECM}}$
, where
$ {\mathbf {ECM}}$
is the weakest regular modal logic in Chellas’ terminology. Neighbourhood canonicity for the latter is meanwhile a folklore result in the study of classical modal logics, cf. [Reference Chellas3, Chapter 9, Section 3]. This leaves us with (P) and (T).
We start by mapping out the logical relations between the four logics thus obtained, and
$\textbf {EK}$
and
$\textbf {ECK}$
. First, in the context of
$ {\mathbf {EK}}$
, (T) obviously implies (P). Hence, it suffices to prove that (C) is not derivable in
$ {\mathbf {EKT}}$
, in order to show that it also not derivable in
$ {\mathbf {EK}}$
or in
$ {\mathbf {EKP}}$
. So let
$W = \{w,v,u,s\}$
,
$N(w) = \{\{w,v\},\{w,u\}\}$
, and
$N(x) = \emptyset $
for
$x\in \{v,u,s\}$
. Let
$V(p) = \{w,v\}$
and
$V(q) = \{w,u\}$
. The model
$M = \langle W,N,V\rangle $
obviously satisfies (t). To see why it also satisfies (k), note that whenever
$X \in N(w)$
, then
$\overline {X}$
contains s and hence there is no Y such that
$\overline {X}\cup Y\in N(w)$
. So the model will validate all instances of (T) and (K). However, it invalidates
$(\square p\wedge \square q)\rightarrow \square (p\wedge q)$
, which is an instance of (C).
(P) is not derivable in
$ {\mathbf {ECK}}$
. To see why, consider
$M = \langle W,N,V\rangle $
with
$W = \{w\}$
,
$N(w) = \emptyset $
. Then
$M,w\models \square \bot $
, but M satisfies both (k) and (c) and hence it validates all instances of (K) and (C). In view of the preceding this means that also (T) is not derivable in
$ {\mathbf {ECK}}$
or in
$ {\mathbf {EK}}$
.
Finally, (T) is not derivable in
$ {\mathbf {ECKP}}$
. To see why, let
$M = \langle W,N,V\rangle $
, where
$W = \{w,w^{\prime }\}$
,
$N(w) = \{\{w^{\prime }\}\}$
,
$N(w^{\prime }) = \{\{w\}\}$
, and
$V(p) = \{w\}$
. Then
$M,w\models \square \neg p\wedge p$
and hence (T) is violated at
$M,w$
. However, M satisfies (k), (c), and (p). As a corollary, (T) is also not derivable in
$ {\mathbf {EKP}}$
.
Taking these observations together, we obtain exactly the relations depicted in Figure 1. Here, an arrow from one logic to another indicates that the former is strictly stronger than the latter; obviously this relation is transitive. Whenever there is no (chain of) arrow(s) between two logics, they are incomparable. Consequently, each of the six logics in the picture are distinct.
Relations between the six logics that are center stage in this paper, from weakest (bottom left) to strongest (top right).
Let us now go turn to the construction of characteristic models. We start with the easiest case, i.e. the axiom (P). Canonicity for
$\textbf {EKP}$
and
$\textbf {ECKP}$
follows immediately by the same arguments as those given for their (P)-less counterparts. It suffices to use the constructions from Sections 3 and 4, but this time including the axiom (P) in the underlying logic used to construct the maximal consistent sets. By maximal consistency, each of these sets will contain
$\neg \square \bot $
and hence the truth lemma ensures that (p) is satisfied by the minimal models for these logics. Note that, by the same token, one can show that any definable frame condition—i.e., any frame condition that is characterized by a formula
$\varphi \in \mathfrak {L}$
—can be axiomatized by adding the
$\varphi $
in question to either
$ {\mathbf {EK}}$
or
$ {\mathbf { ECK}}$
. Well-known examples are:
$\emptyset \in N(w)$
(characterized by
$\square \bot $
) and
$W\not \in N(w)$
(characterized by
$\neg \square \top $
).
Finally, we turn to (T). For the logics
$\textbf {EKT}$
and
$\textbf {ECKT}$
one can again use the constructions from the two preceding sections, relying on the following theorem:
Theorem 6. Each of the following hold:
Proof.
Ad 1. Suppose that
$X\in N^1(w)$
. Case 1:
$X\in N^0(w)$
. By (F1),
$M^0,w\models \square \psi \in w$
for some
$\psi $
with
$X = \|\psi \|^{M^0}$
. By the axiom (T),
$M^0,w\models \psi $
and hence
$w\in X$
. Case 2: there are
$Y_1,\ldots ,Y_n\in N^0(w)$
such that
$S = \overline {Y_1}\cup \cdots \cup \overline {Y_n}\cup X\in N^0(w)$
. Since
$M^0$
is
$ {\mathbf {EKT}}$
-fähig, we can let each
$Y_i = \|\psi _i\|^{M^0}$
and let
$S = \|\varphi \|^{M^0}$
. Then, by the construction,
$M^0,w\models \square \psi _1$
,
$\ldots $
,
$M^0,w\models \square \psi _n$
, and
$M^0,w\models \square \varphi $
. By the axiom (T),
$M^0,w\models \psi _1$
,
$\ldots $
,
$M^0,w\models \psi _n$
, and
$M^0,w\models \varphi $
. Hence,
$w\in S\cap (Y_1\cap \cdots \cap Y_n)$
and hence
$w\in X$
.
Ad 2. Similar to item 1 but simpler; note that it suffices to prove that
$N^1$
satisfies condition (t); from that it follows immediately that also
$N^2$
satisfies (t).□
5.2. Adding a global modality
For various applications, it is useful to enrich the modal language with a global modality
$[\forall ]$
, cf. [Reference Goranko and Passy5]. Semantically, the enriched language is interpreted by adding the following clause: where
$M = \langle W,N,V\rangle $
,
$$ \begin{align*}M,w\models [\forall]\varphi \mbox{ iff for all } w^{\prime}\in W: M,w^{\prime}\models \varphi.\end{align*} $$
In what follows, we will use
$ {\mathbf {L}}_{\forall }$
to refer to the extension of
$\mathbf {L}$
with
$[\forall ]$
, where
$\mathbf {L}$
is any of the six logics from Figure 1.
Taken by itself,
$[\forall ]$
is a normal modal operator of type
$ {\mathbf {S5}}$
. When added to either of the six logics that were previously considered, it satisfies the following additional axiom, sometimes called “replacement of global equivalents”:
-
(RGE)
$[\forall ](\varphi \leftrightarrow \psi ) \rightarrow (\square \varphi \leftrightarrow \square \psi ).$
This axiom states that, whenever
$\varphi $
and
$\psi $
are true at exactly the same worlds in a given model, then
$\square \varphi $
and
$\square \psi $
are equivalent in that model. We now show that by adding (RGE) and all
$ {\mathbf {S5}}$
-properties for
$[\forall ]$
(including necessitation) to any logic
$\mathbf {L}$
from the previous sections, we get a strongly complete axiomatization for
$ {\mathbf {L}}_{\forall }$
. In fact, we prove that the logic in question satisfies a relativized type of neighbourhood canonicity. In what follows, we hold
$\mathbf {L}$
fixed; the reader should keep in mind that many notions (e.g., maximal consistency, model, etc.) are defined relative to this logic.
Note that in the presence of
$[\forall ]$
, neighbourhood canonicity fails: there cannot be a single model that serves as a witness for every maximal
$ {\mathbf {L}}_{\forall }$
-consistent set. For instance, while
$[\forall ]p$
is obviously a consistent formula—and hence a member of such a maximal consistent set—it excludes certain other maximal consistent sets that e.g. contain
$\neg [\forall ]p$
.
We can however construct relativized characteristic models, i.e. the construction is relativized to a given maximal
$ {\mathbf {L}}_{\forall }$
-consistent set
$\Gamma $
.Footnote
14
For any such
$\Gamma $
, we let
$W_\Gamma $
denote the set of all maximal consistent sets
$\Delta $
such that
$\{[\forall ]\varphi \mid [\forall ]\varphi \in \Delta \} = \{[\forall ]\varphi \mid [\forall ]\varphi \in \Gamma \}$
. In other words,
$W_\Gamma $
is the set of all maximal
$ {\mathbf { L}}_{\forall }$
-consistent sets that are “possible” in light of the
$[\forall ]$
-formulas that are a member of
$\Gamma $
. These are, intuitively, all and only those worlds that we should have if we want to construct a model in which all the members of
$\Gamma $
hold at some world.
Much like before, we define
$$ \begin{align*}N^0_\Gamma(w) = \{\{w^{\prime}\in W_\Gamma \mid \varphi\in w^{\prime}\}\mid \square\varphi\in w\} .\end{align*} $$
$$ \begin{align*}V_\Gamma(\varphi) = \{w\in W_\Gamma \mid \varphi\in w\} \mbox{ for all } \varphi\in\mathfrak{P} .\end{align*} $$
With these ingredients, we obtain the basic canonical model for
$ {\mathbf {L}}_{\forall }$
and
$\Gamma $
, i.e.,
$M^0_\Gamma = \langle W_\Gamma ,N^0_\Gamma ,V_\Gamma \rangle $
. Adapting our previous notation, one may let
$|\varphi |_{\Gamma } = \{w\in W_\Gamma \mid \varphi \in w\}$
. The truth lemma for
$M^0_\Gamma $
then states that, for all
$\varphi $
in the extended language,
$|\varphi |_{\Gamma } = \|\varphi \|^{M^0_\Gamma }$
. This lemma can be shown by a standard inductive proof, relying on the
$ {\mathbf {S5}}$
-properties of the global modality for formulas of the form
$[\forall ]\varphi $
and relying on (RGE) for
$\square $
.
From there, we can apply the exact same strategy as we did for
$\mathbf {L}$
. That is, it suffices to note that the basic canonical model for
$ {\mathbf {L}}_{\forall }$
and
$\Gamma $
is
$ {\mathbf {L}}_{\forall }$
-fähig. So, depending on whether (C) is or is not valid in
$ {\mathbf {L}}_{\forall }$
, we can use the circumscription technique from Sections 3 or 4 to obtain a pointwise equivalent
$ {\mathbf {L}}_{\forall }$
-model for
$\Gamma $
, and thus a relativized characteristic model for
$ {\mathbf {L}}_{\forall }$
and
$\Gamma $
.
This concludes our overview of relatively straightforward generalizations, building on the construction of characteristic models from the two previous sections. We leave the investigation of other axioms and frame conditions—notably, the iterative axioms (B), (4), and (5) for
$\square $
, that are the lead actors in epistemic and doxastic modal logics—for future work.
Acknowledgements
We are indebted to Olivier Roy, Thomas Agøtnes, Brian Chellas, Steven Kuhn, David Makinson, Roy Benton, and an anonymous reviewer for their incisive comments on and discussions of previous versions of this paper. Frederik Van De Putte’s research was funded by a Marie Skłodowska-Curie Fellowship (grant agreement ID: 795329), by a grant from the Research Foundation Flanders (FWO-Vlaanderen), no. 12Q1918N, and by a grant from the Dutch Research Council (NWO), no. VI.Vidi.191.105. The authors’ joint work on this paper was facilitated by the German-Polish PIOTR project (grant no. RO 4548/4-1, funded by the DFG and the NCN).
