CANONICITY IN POWER AND MODAL LOGICS OF FINITE ACHRONAL WIDTH

Abstract

We develop a method for showing that various modal logics that are valid in their countably generated canonical Kripke frames must also be valid in their uncountably generated ones. This is applied to many systems, including the logics of finite width, and a broader class of multimodal logics of ‘finite achronal width’ that are introduced here.

1 Introduction

There is a fundamental question about the model theory of propositional modal logics that has remained open since the early days of the subject. It was first raised by Fine in [8] and asks: if a logic is valid in its countably generated canonical Kripke frames, must it also be valid in its uncountably generated ones?

To elaborate this, note that the points of a canonical frame are maximally consistent sets of formulas. If the ambient language has $\kappa $ atoms/variables, there will be at least $2^{\kappa }$ such points. This ‘ $\kappa $ -generated’ frame carries a particular model that verifies all (and only) the theorems of the logic, but in some cases it may also carry models that falsify some theorems. If a logic is valid in the frame, i.e., verified by all models on the frame, we say it is canonical in power $\kappa $ , or $\kappa $ -canonical. A logic canonical in all powers will be called totally canonical.

It is known that a $\kappa $ -canonical logic is $\lambda $ -canonical for all $\lambda <\kappa $ , and that there exist logics that are canonical in all finite powers but not $\omega $ -canonical (see Section 2.9 for more information). Our fundamental question is: if a logic is $\omega $ -canonical, must it be canonical in all uncountable powers, and hence totally canonical?

To put it another way: because the collection of logics forms a set, rather than a proper class, it can be seen that there does exist some infinite cardinal $\kappa $ such that every $\kappa $ -canonical logic is totally canonical. Our question asks whether the least such $\kappa $ is $\omega $ , or something larger.

There have been some positive answers given for limited classes of logics. Fine [8] made the important discovery that a logic must be totally canonical if it is characterised by (i.e., sound and complete for validity in) a class of frames that is first-order definable. He applied this in [9] to subframe logics, those that are characterised by a class that is closed under subframes. It was shown that a subframe logic whose validating frames are transitive is totally canonical iff the class of these frames is first-order definable. Moreover that holds iff the logic is compact (alias strongly complete), which means that any consistent set of formulas is satisfiable in a model on a frame that validates the logic. Now any $\omega $ -canonical logic is compact, so it follows that any $\omega $ -canonical transitive subframe logic is totally canonical.

Zakharyaschev [25] generalised these results, showing that they hold for any logic characterised by a class of transitive frames that is closed under cofinal subframes, and that there are continuum many ( $2^{\aleph _0}$ ) such logics that are not subframe logics. Wolter [23] removed the transitivity restriction in Fine’s analysis. Wolter [22] also studied linear temporal logics, showing that they are totally canonical iff characterised by a first-order definable class, but that this condition is now stronger than compactness. The linear temporal logic of the real numbers is compact but not totally canonical. Nonetheless we show here that every $\omega $ -canonical linear temporal logic is totally canonical.

The present paper develops a technique for giving a positive answer to the fundamental question for various logics, by a kind of Löwenheim–Skolem argument that reduces a ‘big’ failure of canonicity to a countably generated one. We combine Kripke modelling with algebraic semantics, under which logics L correspond to varieties (equationally definable classes) $V_L$ of algebras. Corresponding to the canonical frame construction there is an operation assigning to any modal algebra ${\cal A}$ a frame ${\cal A}_+$ whose points are the ultrafilters of $ {\cal A}$ . The algebra ${\cal A}^{\sigma }$ of all subsets of ${\cal A}_+$ is the canonical extension of ${\cal A}$ . When ${\cal A}$ is the Lindenbaum algebra of L, relative to a language with $\kappa $ atoms, then ${\cal A}_+$ is isomorphic to the $\kappa $ -generated canonical frame of L, and L is $\kappa $ -canonical iff ${\cal A}^{\sigma }\in V_L$ . Moreover the Lindenbaum algebra is free in $V_L$ on $\kappa $ generators, and from this one can show that L is $\kappa $ -canonical iff ${\cal A}^{\sigma }\in V_L$ for every ${\cal A}\in V_L$ that is generated by a set of cardinality at most $\kappa $ . We find it convenient to work with this algebraic formulation of canonicity [11, sec. 3.5].

Let us say that a logic or variety is resolved if it is either totally canonical, or not $\omega $ -canonical (in which case it is not canonical in any infinite power). The fundamental question asks whether every logic is resolved. We illustrate our strategy for tackling this in Section 4, by applying it to logics that contain the axiom $\lozenge \lozenge p\to \Box \lozenge p$ , which we call 5 $_2$ (it is a weakening of the 5-axiom from the system S5). To explain the semantic meaning of 5 $_2$ we take a temporal view of the binary relation R of a frame and think of a set of the form $R(x)=\{z:Rxz\}$ as the future of point x. Then a frame validates 5 $_2$ iff for each x, all points in $R(x)$ have the same future, i.e., $R(y)=R(y')$ for all $y,y'\in R(x)$ .

We show that any logic containing $5_2$ is resolved, and that there is a continuum of such logics. These results are then substantially generalised by introducing a new family $\{U_n:n<\omega \}$ of axioms that generalise the ‘finite width’ axioms $\{I_n:n<\omega \}$ of Fine [7]. The relational condition for validity of $I_n$ is that no future set $R(x)$ contains an antichain with more than n points. Here an antichain is a set S such that $Ryz$ fails for all distinct $y,z\in S$ , i.e., no member of S is in the future of any other member. A finite width logic is one that includes $K4I_n$ , the smallest normal logic to contain the transitivity axiom 4 and the axiom $I_n$ , for some n.

$U_n$ is the formula

$$ \begin{align*}\bigvee_{i\leq n}\Box\big(\Box q_i\to\bigvee\nolimits_{j\leq n,\,j\neq i}\Box q_j\big), \end{align*} $$

which is derivable from 4 and $I_n$ . Its relational meaning is obtained by replacing antichains by the notion of an achronal set S, one for which $R(y)\not \subseteq R(z)$ for all distinct $y,z\in S$ , i.e., no two points of S have $\subseteq $ -comparable futures. The condition for validity of $U_n$ is that no set $R(x)$ contains an achronal set with more than n points. See Section 5.3 for more details.

This discussion has assumed we are dealing with a single modality $\lozenge $ and its dual $\Box $ . In fact we allow ourselves a multimodal language with a set ${\mathsf {M}}$ of diamond modalities $\lozenge ,\blacklozenge ,\dots $ having duals $\Box ,\blacksquare ,\dots $ , and take $U_n^{\mathsf {M}}$ to be the set of formulas

$$ \begin{align*}\bigvee_{i\leq n}\Box\big(\blacksquare q_i\to\bigvee\nolimits_{j\leq n,\,j\neq i}\blacksquare q_j\big) \end{align*} $$

for all $\lozenge ,\blacklozenge \in {\mathsf {M}}$ . We prove that any logic in this language that includes $U_n^{\mathsf {M}}$ is resolved.

In the monomodal case ${\mathsf {M}}=\{\lozenge \}$ , this result includes all the finite width logics, but it covers much more. We show that there is a continuum of logics that include $K4U_n$ and are included in $K4I_n$ , and a continuum that include $KU_{n+1}$ and are included in $KU_n$ , for each n (as well as other results in this vein).

Fine [7] showed that any logic containing one of the finite width logics $K4I_n$ is Kripke complete: it is complete for validity in its Kripke frames. This situation does not extend to the $KU_n$ ’s, or even the $K4U_n$ ’s, as we show by constructing an extension of $K4U_2$ that is Kripke incomplete.

1.1 Layout of paper

Section 2 recalls some relevant definitions and sets out canonicity in power. Section 3 develops a strategy for proving that certain modal logics (or varieties of BAOs) are resolved. Section 4 applies this strategy to logics extending $K5_2$ , and shows that such extensions are numerous.

We take a break from canonicity in Sections 5 and 6, which can be read largely independently of the rest of the paper. Motivated by the work on $K5_2$ , in Section 5 we introduce the modal logics $KU_n$ , for finite $n\geq 1$ , and compare them to some other logics. Extensions of the $KU_n$ are called logics of finite achronal width, and the remainder of the paper studies them. In Section 6 we show that some of them are Kripke incomplete. We return to canonicity in Section 7, where we apply the strategy to them, showing that they are all resolved.

2 Basic definitions

We start by recalling some standard modal and algebraic notions, and setting up some definitions and notation for later use.

2.1 General machinery used in the paper

We work in ZFC set theory and use standard set-theoretic material, including maps or functions, ordinals, and cardinals. A cardinal is an (initial) ordinal. We write the first infinite cardinal as both $\omega $ and $\aleph _0$ ; countable will mean of cardinality at most this cardinal. The cardinality of a set X is denoted by $|X|$ , and the power set of X by $\wp (X)$ . We write ${ \mathrm{dom}}(f)$ for the domain of a map f.

Definition 2.1. Let R be a binary relation on a set X (i.e., $R\subseteq X\times X$ ), and let $Y\subseteq X$ .

1. 1. We may write any of $xRy$ , $Rxy$ , $R(x,y)$ to denote that $(x,y)\in R$ . Later, we will use the same convention for first-order formulas.

2. 2. For $x\in X$ , we write $R(x)=\{y\in X:Rxy\}$ .

   Thinking of temporal logic, we may speak of $R(x)$ as the (R-)future of $x$ .

3. 3. We write $R[Y]=\{R(y):y\in Y\}$ .

4. 4. Y is said to be R-closed (in $X\!$ ) if $\bigcup R[Y]\subseteq Y$ . That is, if $y\in Y$ , $x\in X$ , and $Ryx$ , then $x\in Y$ .

5. 5. Y is said to be an R-antichain if $\neg Ryz$ for all distinct $y,z\in Y$ .

6. 6. The R-width of Y is the least cardinal $\kappa $ such that every R-antichain $Z\subseteq Y$ has cardinality $\leq \kappa $ .

2.2 Multimodal logic

We fix a nonempty set ${\mathsf {M}}$ of unary diamond-modalities, and a set ${\mathsf {Q}}=\{q_i:i<\omega \}$ of propositional atoms. Modal ${\mathsf {M}}$ -formulas, or simply modal formulas, are then defined as usual. Each atom in ${\mathsf {Q}}$ is a formula, as is $\top $ , and if $\varphi ,\psi $ are formulas, so are $\neg \varphi $ , $\varphi \vee \psi $ , and $\lozenge \varphi $ , for each $\lozenge \in {\mathsf {M}}$ .

We adopt standard conventions. We let $p,q,r,\ldots $ stand for arbitrary distinct atoms in ${\mathsf {Q}}$ . We let $\bot $ abbreviate $\neg \top $ ; $\varphi \wedge \psi $ abbreviate $\neg (\neg \varphi \vee \neg \psi )$ ; $\varphi \to \psi $ abbreviate $\neg \varphi \vee \psi $ ; $\varphi \leftrightarrow \psi $ abbreviate $(\varphi \to \psi )\wedge (\psi \to \varphi )$ ; and $\Box \varphi $ abbreviate $\neg \lozenge \neg \varphi $ , for each $\lozenge \in {\mathsf {M}}$ . We adopt the usual binding conventions, whereby $\neg ,\lozenge ,\wedge ,\vee ,\to ,\leftrightarrow $ (for each $\lozenge \in {\mathsf {M}}$ ) are in decreasing order of tightness.

A normal modal ${\mathsf {M}}$ -logic is a set of ${\mathsf {M}}$ -formulas containing all propositional tautologies, the axioms $\Box (p\to q)\to (\Box p\to \Box q)$ and $\lozenge p\leftrightarrow \neg \Box \neg p$ for each $\lozenge \in {\mathsf {M}}$ , ¹ and closed under the inference rules of modus ponens (from $\varphi $ and $\varphi \to \psi $ , infer $\psi $ ), generalisation (from $\varphi $ , infer $\Box \varphi $ ), and substitution (from $\varphi $ , infer any substitution instance of it—any formula obtained from $\varphi $ by replacing its atoms by arbitrary formulas).

2.3 Structures

We assume some familiarity with basic first-order model theory. For unfamiliar terms, see, e.g., [5, 13]. A signature is a set of non-logical symbols (function symbols, relation symbols, and constants) together with their types and arities. Others call it a similarity type, alphabet, or vocabulary. Equality is regarded as a logical symbol and is always available. We will be using various model-theoretic structures, some of which will be two-sorted. We take it as read that standard model-theoretic results apply to two-sorted structures. We identify (notationally) a structure ${\mathfrak M}$ with its domain ${ \mathrm{dom}}({\mathfrak M})$ . We write $S^{\mathfrak M}$ for the interpretation of a symbol or term S in ${\mathfrak M}$ . We write ${\bar a}\in {\mathfrak M}$ to indicate that ${\bar a}$ is a tuple of elements of the domain of ${\mathfrak M}$ . For a map f defined on ${\mathfrak M}$ , we write $f({\bar a})$ for the tuple obtained from ${\bar a}$ by applying f to its elements in order.

2.4 Kripke frames, models, semantics

Kripke frames are formulated as structures, as follows. We extend this slightly to cover Kripke models too.

Definition 2.2. Introduce a binary relation symbol $R_{\lozenge }$ for each $\lozenge \in {\mathsf {M}}$ . A (Kripke) frame is a structure for this signature. A subframe of a frame ${\cal F}$ is simply a substructure of ${\cal F}$ in the usual model-theoretic sense. An inner subframe of ${\cal F}$ is a subframe whose domain is $R_{\lozenge }^{\cal F}$ -closed in ${\cal F}$ (Definition 2.1) for every $\lozenge \in {\mathsf {M}}$ .

A valuation into a frame ${\cal F}$ is a map $g:{\mathsf {Q}}\to \wp ({\cal F})$ . (Recall that notationally we identify ${\cal F}$ with its domain.)

A (Kripke) model is a pair ${\cal M}=({\cal F},g)$ , where ${\cal F}$ is a frame and $g$ a valuation into it. The frame of ${\cal M}$ is ${\cal F}$ . We may regard ${\cal M}$ as a structure for the signature of frames by identifying it with ${\cal F}$ (for this purpose). So, for example, we write $t,u\in {\cal M}$ to mean that $t,u\in {\cal F}$ , and ${\cal M}\models R_{\lozenge } tu$ to mean that ${\cal F}\models R_{\lozenge } tu$ , for $\lozenge \in {\mathsf {M}}$ .

A submodel of ${\cal M}$ is a Kripke model of the form $({\cal F}',g')$ , where ${\cal F}'$ is a subframe of ${\cal F}$ and $g'$ is the valuation into it given by $g'(q)=g(q)\cap {\cal F}'$ , for each $q\in {\mathsf {Q}}$ . A submodel is fully determined by its domain.

We now recall the standard modal definitions of truth, validity, etc.

Definition 2.3. Let ${\cal M}=({\cal F},g)$ be a Kripke model. We define ${\cal M},w\models \varphi $ (in words, ‘ $\varphi $ is true in ${\cal M}$ at $w$ ’), for each $w\in {\cal F}$ and modal formula $\varphi $ , by induction as usual: ${\cal M},w\models \top $ ; ${\cal M},w\models q$ iff $w\in g(q)$ , for $q\in {\mathsf {Q}}$ ; ${\cal M},w\models \neg \varphi $ iff ${\cal M},w\not \models \varphi $ ; ${\cal M},w\models \varphi \vee \psi $ iff ${\cal M},w\models \varphi $ or ${\cal M},w\models \psi $ or both; and if $\lozenge \in {\mathsf {M}}$ , then ${\cal M},w\models \lozenge \varphi $ iff ${\cal M},u\models \varphi $ for some $u\in {\cal M}$ with ${\cal M}\models R_{\lozenge } wu$ .

We say that a modal formula $\varphi $ is satisfied in a Kripke model ${\cal M}$ if ${\cal M},w\models \varphi $ for some $w\in {\cal M}$ . We will say that ${\cal M}$ verifies $\varphi $ (written ${\cal M}\models \varphi $ ), if ${\cal M},w\models \varphi $ for every $w\in {\cal M}$ , and that ${\cal M}$ strongly verifies $\varphi $ if it verifies every substitution instance of $\varphi $ .

Let ${\cal F}$ be a Kripke frame, and let ${\cal K}$ be a class of frames. We say that $\varphi $ is satisfiable in ${\cal F}$ , if it is satisfied in some Kripke model with frame ${\cal F}$ ; valid at a point $w$ in ${\cal F}$ , if ${\cal M},w\models \varphi $ for every Kripke model ${\cal M}$ with frame ${\cal F}$ ; valid in ${\cal F}$ (written ${\cal F}\models \varphi $ ), if every model with frame ${\cal F}$ verifies $\varphi $ ; and valid in ${\cal K}$ (written ${\cal K}\models \varphi $ ), if $\varphi $ is valid in every frame in ${\cal K}$ . In the latter cases, we also say that ${\cal F}$ or ${\cal K}$ validates $\varphi $ .

We say that a set S of modal formulas is valid in ${\cal F}$ , and write ${\cal F}\models S$ , if each formula in S is valid in ${\cal F}$ . The other kinds of validity are extended to sets of formulas similarly.

The set of all formulas valid in ${\cal F}$ or ${\cal K}$ is a normal modal ${\mathsf {M}}$ -logic, called the logic of (or the logic determined by) ${\cal F}$ or ${\cal K}$ . Logics of this form are said to be Kripke complete.

2.5 Point-generated inner subframes

Definition 2.4. For an ordinal $\alpha $ , we put $^{\alpha } {\mathsf {M}}=\{s\mid s:\alpha \to {\mathsf {M}}\}$ , the set of functions from $\alpha $ into ${\mathsf {M}}$ , and $^{<\alpha }{\mathsf {M}}=\bigcup _{\beta <\alpha }{}^{\beta } {\mathsf {M}}$ . One can think of the elements of $^{<\omega }{\mathsf {M}}$ as the finite sequences of diamonds.

For an ordinal $\alpha $ , a map $s\in {}^{\alpha }{\mathsf {M}}$ , and $\lozenge \in {\mathsf {M}}$ , we write $s\hat \ \lozenge \in {}^{\alpha +1}{\mathsf {M}}$ for the map whose restriction to $\alpha $ is $s $ and whose value on $\alpha $ is $\lozenge $ . Thinking of $s $ as a sequence, $s\hat \ \lozenge $ is the same sequence with $\lozenge $ appended.

For each $s\in {}^{<\omega }{\mathsf {M}}$ , we define the first-order formula $R_s xy$ of the signature of frames, by induction on the ordinal ${ \mathrm{dom}}(s)$ :

• • $R_{\emptyset } xy$ is $x=y$ , where $\emptyset $ is the empty map in $^0{\mathsf {M}}$ .

• • $R_{s\hat \ \lozenge }xy$ is $\exists z(R_s xz\wedge R_{\lozenge } zy)$ .

Finally, let ${\cal F}$ be a frame and $w_0\in {\cal F}$ . The inner subframe of ${\cal F}$ generated by $w_0$ is the subframe ${\cal F}(w_0)$ of ${\cal F}$ with domain

$$\begin{align*}\{w\in{\cal F}:{\cal F}\models R_s w_0w\mbox{ for some }s\in{}^{<\omega}{\mathsf{M}} \}. \end{align*}$$

Taking $s=\emptyset $ here, we see that ${\cal F}(w_0)$ contains $w_0$ . It is the smallest inner subframe of ${\cal F}$ to do so.

2.6 ${\mathsf {M}}$ -BAOs and translations

It is now well known that modal logic can be ‘algebraised’ using boolean algebras with operators (BAOs). We will just give some definitions; for more information, see, e.g., [2, chap. 5]. We will pass fairly freely between modal logic and algebra.

An ${\mathsf {M}}$ -BAO is an algebra ${\cal A}$ with signature $\{+,-,0,1\}\cup {\mathsf {M}}$ , where the $\{+,-,0,1\}$ -reduct of ${\cal A}$ is a boolean algebra and each $\lozenge \in {\mathsf {M}}$ is a unary function symbol interpreted in ${\cal A}$ as a normal additive operator (that is, ${\cal A}\models \lozenge 0=0$ and ${\cal A}\models \lozenge (a+b)=\lozenge a+\lozenge b$ for each $a,b\in {\cal A}$ ). This is as per [2, definition 5.19]. The double use of $\lozenge $ for a modal operator and a function symbol should not cause problems in practice.

Standardly, each modal ${\mathsf {M}}$ -formula $\varphi $ can be translated to a term $\tau _{\varphi }$ of this signature (an ‘ ${\mathsf {M}}$ -BAO term’). Introduce pairwise distinct variables $v_i$ ( $i<\omega $ ). We let $\tau _{\top }=1$ , $\tau _{q_i}=v_i$ for $i<\omega $ , $\tau _{\neg \varphi }=\,-\tau _{\varphi }$ , $\tau _{\varphi \vee \psi }=\tau _{\varphi }+\tau _{\psi }$ , and $\tau _{\lozenge \varphi }=\lozenge \tau _{\varphi }$ , for $\lozenge \in {\mathsf {M}}$ . We can now say that an ${\mathsf {M}}$ -BAO ${\cal A}$ validates a modal formula $\varphi $ if ${\cal A}\models \forall \bar v(\tau _{\varphi }=1)$ , where $\bar v$ is a tuple enumerating the variables occurring in $\tau _{\varphi }$ . As usual, a class ${\cal C}$ of ${\mathsf {M}}$ -BAOs validates a modal formula $\varphi $ if every ${\cal A}\in {\cal C}$ does, and ${\cal C}$ validates a set of modal formulas if it validates every formula in the set.

A variety of ${\mathsf {M}}$ -BAOs is a class V of ${\mathsf {M}}$ -BAOs defined by a set of equations. The set $L_V$ of modal ${\mathsf {M}}$ -formulas validated by V is then a normal modal ${\mathsf {M}}$ -logic as defined in Section 2.2. If L is a normal modal ${\mathsf {M}}$ -logic, $V_L$ denotes the variety of all ${\mathsf {M}}$ -BAOs defined by the set $\{\tau _{\varphi }=1:\varphi \in L\}$ of equations. We have $V_{L_V}=V$ and $L_{V_L}=L$ . See, e.g., [2, sec. 5.2] for more.

Conversely, each ${\mathsf {M}}$ -BAO term $\tau $ written with the variables $v_i$ can be translated to a modal ${\mathsf {M}}$ -formula $\varphi _{\tau }$ . We let $\varphi _1=\top $ , $\varphi _0=\bot $ , $\varphi _{v_i}=q_i$ , $\varphi _{-\tau }=\neg \varphi _{\tau }$ , $\varphi _{\tau +\upsilon }=\varphi _{\tau }\vee \varphi _{\upsilon }$ , and $\varphi _{\lozenge \tau }=\lozenge \varphi _{\tau }$ for $\lozenge \in {\mathsf {M}}$ . We extend this translation to equations: given ${\mathsf {M}}$ -BAO terms $\tau ,\upsilon $ , we let $\varphi _{\tau =\upsilon }$ be the modal formula $\varphi _{\tau }\leftrightarrow \varphi _{\upsilon }$ .

2.7 Canonical extensions

For an ${\mathsf {M}}$ -BAO ${\cal A}$ , we can form, in the usual way:

• • Its canonical frame ${\cal A}_+$ , whose domain comprises the ultrafilters of ${\cal A}$ , and which is regarded as a frame in the sense of Definition 2.2, with interpretations given as usual by ${\cal A}_+\models R_{\lozenge }\mu \nu $ iff $a\in \nu \,{\Rightarrow }\, \lozenge a\in \mu $ for all $a\in {\cal A}$ , where $\mu ,\nu $ are any ultrafilters of ${\cal A}$ and $\lozenge \in {\mathsf {M}}$ .

• • Its canonical extension ${\cal A}^{\sigma }$ (which is also an ${\mathsf {M}}$ -BAO). It is also known as a ‘perfect extension’ or the ‘canonical embedding algebra’, and written $\mathfrak {Em}{\cal A}$ .

For details, see, e.g., [2, definition 5.40] or [14].

2.8 Sahlqvist formulas

Sahlqvist theory is now a basic and well-known part of modal logic, so we will be very brief: see, e.g., [2, sec. 3.6] or [4, sec. 10.3] for details. Sahlqvist formulas are modal ${\mathsf {M}}$ -formulas of a certain syntactic form, and they have some useful properties. Every Sahlqvist formula $\varphi $ has a first-order correspondent: an easily-computable first-order sentence $\chi _{\varphi }$ of the signature of frames (Definition 2.2), such that for an arbitrary frame ${\cal F}$ we have ${\cal F}\models \chi _{\varphi }$ iff $\varphi $ is valid in ${\cal F}$ . As an example, if $\lozenge \in {\mathsf {M}}$ and $q\in {\mathsf {Q}}$ then $\varphi =\lozenge \lozenge q\to \lozenge q$ is a Sahlqvist formula, and $\chi _{\varphi }$ is $\forall xyz(R_{\lozenge } xy\wedge R_{\lozenge } yz\to R_{\lozenge } xz)$ , saying that $R_{\lozenge }$ is transitive. Moreover, every Sahlqvist formula $\varphi $ is canonical: an ${\mathsf {M}}$ -BAO ${\cal A}$ validates $\varphi $ iff $\varphi $ is valid in the frame ${\cal A}_+$ (iff ${\cal A}_+\models \chi _{\varphi }$ , iff ${\cal A}^{\sigma }$ validates $\varphi $ ). The logic axiomatised by a set $\Phi $ of Sahlqvist formulas (i.e., the smallest normal ${\mathsf {M}}$ -modal logic containing $\Phi $ ) is the logic of the class of frames defined by $\{\chi _{\varphi }:\varphi \in \Phi \}$ , and hence is Kripke complete.

2.9 Canonicity in power

Definition 2.5. We say that a variety V of ${\mathsf {M}}$ -BAOs is canonical, or for emphasis, totally canonical, if ${\cal A}^{\sigma }\in V$ for every ${\cal A}\in V$ . For a cardinal $\kappa $ , we say that V is $\kappa $ -canonical if ${\cal A}^{\sigma }\in V$ for every ${\cal A}\in V$ that is ‘ $\kappa $ -generated’—that is, generated as an algebra by a subset of ${\cal A}$ of cardinality $\leq \kappa $ .

We say that V is resolved if it is either totally canonical, or not even $(|{\mathsf {M}}|+\omega )$ -canonical.

This definition of $\kappa $ -canonicity, or canonicity in the power $\kappa $ , is a slight variant of ones in [8, p. 30] and [12, sec. 6]. The connection of these notions to canonicity of modal logics is again well known [2, sec. 5.3]: V is canonical iff $L_V$ is canonical—i.e., every canonical frame of $L_V$ validates $L_V$ —and V is $\kappa $ -canonical iff every canonical frame of $L_V$ defined with $\leq \kappa $ atoms validates $L_V$ .

Let us consider resolvedness in the case ${\mathsf {M}}=\{\lozenge \}$ , where $|{\mathsf {M}}|+\omega =\omega $ . [12, theorem 6.1] gives an example of a variety of $\{\lozenge \}$ -BAOs that is finitely canonical (n-canonical for all finite n) but not $\omega $ -canonical. Nonetheless, as far as we are aware, all known $\omega $ -canonical varieties of $\{\lozenge \}$ -BAOs are totally canonical. No nonresolved varieties of $\{\lozenge \}$ -BAOs are known. Fine [8, p. 30] asked if there are any (his question was for modal logics and we have read it across for varieties). This is asking whether there is a dichotomy between totally canonical and non- $\omega $ -canonical varieties of $\{\lozenge \}$ -BAOs, with no other kinds existing.

Let us unpack this a little more. For arbitrary ${\mathsf {M}}$ now, let E be the set of all ${\mathsf {M}}$ -BAO equations, and let $\Xi =\wp (E)$ . Varieties are defined by members of $\Xi $ . A subset $\Sigma \subseteq \Xi $ therefore defines a particular kind of variety: a $\Sigma $ -variety is a variety of ${\mathsf {M}}$ -BAOs defined by a set of equations in $\Sigma $ . Since $\Sigma $ is a set, the ZFC axiom of replacement ensures that there exists a cardinal $\kappa $ such that every non-canonical $\Sigma $ -variety V contains a $\kappa $ -generated algebra ${\cal A}$ with ${\cal A}^{\sigma }\notin V$ . Hence, every $\kappa $ -canonical $\Sigma $ -variety is totally canonical. Let $\kappa _{\Sigma }$ be the least such $\kappa $ . Then $\Sigma \subseteq \Sigma '\subseteq \Xi $ implies $\kappa _{\Sigma }\leq \kappa _{\Sigma '}$ ; if every $\Sigma $ -variety is canonical then $\kappa _{\Sigma }=0$ ; and every $\Sigma $ -variety is resolved iff $\kappa _{\Sigma }\leq |{\mathsf {M}}|+\omega $ .

As far as we are aware, all known varieties of ${\mathsf {M}}$ -BAOs are resolved, and it is an open question whether every variety of ${\mathsf {M}}$ -BAOs is resolved — that is, $\kappa _{\Xi }\leq |{\mathsf {M}}|+\omega $ . In the absence of an answer, we can still try to identify large sets $\Sigma $ for which every $\Sigma $ -variety is resolved. That is what we will do in the current paper.

3 Strategy for canonicity

In this section (in Section 3.9 and Theorem 3.13 especially) we present a model-theoretic strategy for proving that a variety of ${\mathsf {M}}$ -BAOs is resolved. Along the way, we accumulate some other results (such as Corollaries 3.4 and 3.10) that will be useful later.

3.1 The variety V

We now fix a variety V of ${\mathsf {M}}$ -BAOs. Further conditions on V will be imposed later.

3.2 The two-sorted structure ${\mathfrak B}$

Next we fix a ‘big’ two-sorted structure

$$ \begin{align*}{\mathfrak B}=({\cal B},{\cal B}_+), \end{align*} $$

where ${\cal B}\in V$ . We say that ${\cal B}$ comprises the elements of ${\mathfrak B}$ of algebra sort, and ${\cal B}_+$ comprises the elements of point sort. Further conditions on ${\mathfrak B}$ will be imposed later. It may be confusing but has to be accepted that each ultrafilter of ${\cal B}$ is both a subset of ${\cal B}$ and an element of ${\cal B}_+$ .

The two-sorted signature ${\cal L}$ of ${\mathfrak B}$ comprises the following symbols with the following interpretations in ${\mathfrak B}$ :

1. 1. The algebra operations $+,-,0,1,\lozenge $ of ${\cal B}$ for each $\lozenge \in {\mathsf {M}}$ , all taking algebra elements to algebra elements. Their interpretation in ${\mathfrak B}$ is copied from ${\cal B}$ . As abbreviations, we write $x\cdot y=\,-({-}x+\,{-}y)$ and $\Box x=\,{-}\lozenge\, {-}x$ for each $\lozenge \in {\mathsf {M}}$ .

2. 2. A binary relation symbol ${\,{\mathrel {\underline {\in }}}\,}:{\cal B}\times {\cal B}_+$ , with ${\mathfrak B}\models b\,{\mathrel {\underline {\in }}}\, \mu $ iff b is a member of the ultrafilter $\mu $ .

3. 3. The binary relation symbols $R_{\lozenge }:{\cal B}_+\times {\cal B}_+$ (for each $\lozenge \in {\mathsf {M}}$ ) introduced for frames in Definition 2.2, with interpretations copied from the canonical frame ${\cal B}_+$ . So for each $\lozenge \in {\mathsf {M}}$ ,

   $$\begin{align*}{\mathfrak B}\models\forall xy(R_{\lozenge} xy\leftrightarrow\forall z(z\mathrel{\underline{\in}} y\to\lozenge z\mathrel{\underline{\in}} x)). \end{align*}$$

   Note that formulas of the signature of frames, such as $R_sxy$ ( $s\in {}^{<\omega }{\mathsf {M}}$ ) from Definition 2.4, are also ${\cal L}$ -formulas.

4. 4. Unary relation symbols $Q_i$ ( $i<\omega $ ) of point sort. They can be forgotten about until Section 3.9. For now, bear in mind that they are indeed in ${\cal L}$ and get interpretations in ${\cal L}$ -structures.

We leave the sorts of variables and structure elements to be determined by context.

3.3 Countable ${\mathsf {M}}$

From now on, we assume that ${\mathsf {M}}$ is countable. This is the most common case encountered in practice, although there are some exceptions, such as the signatures of some infinite-dimensional cylindric and polyadic algebras. For countable ${\mathsf {M}}$ , saying that a variety is resolved says that it is canonical iff it is $\omega $ -canonical.

We make this countability restriction purely for simplicity of exposition. Suitably formulated, our results readily generalise to uncountable ${\mathsf {M}}$ (see Section 7.4).

3.4 The structure ${\mathfrak A}\preceq {\mathfrak B}$

We fix a countable elementary substructure

$$\begin{align*}{\mathfrak A}=({\cal A},W)\preceq{\mathfrak B}. \end{align*}$$

Such a structure exists because ${\mathsf {M}}$ , and hence ${\cal L}$ , are countable (and this is the only time we use the countability of ${\mathsf {M}}$ ). We write ${\cal L}({\mathfrak A})$ for ${\cal L}$ expanded by a new constant $\underline {a}$ for each element a of ${\mathfrak A}$ . From now on, $\mathfrak {A,B}$ will denote the expansions of these respective structures to ${\cal L}({\mathfrak A})$ -structures in which each $\underline {a}$ names a. Note that these expansions continue to satisfy ${\mathfrak A}\preceq {\mathfrak B}$ .

Easily, ${\mathfrak A}\preceq {\mathfrak B}$ implies that ${\cal A}\preceq {\cal B}$ as algebras, so ${\cal A}$ is an ${\mathsf {M}}$ -BAO and ${\cal A}\in V$ (since V is an elementary class). Although ${ \mathrm{dom}}{\mathfrak A}\subseteq { \mathrm{dom}} {\mathfrak B}$ , for clarity we will sometimes use the inclusion map

$$\begin{align*}\iota:{\mathrm{dom}}{\mathfrak A}\to{\mathrm{dom}} {\mathfrak B}. \end{align*}$$

It is an ${\cal L}({\mathfrak A})$ -elementary embedding.

To save time, we will use the easy half of the Tarski–Vaught criterion (see [5, proposition 3.1.2] or [13, theorem 2.5.1]): since ${\mathfrak A}\preceq {\mathfrak B}$ , if $\varphi (x)$ is an ${\cal L}({\mathfrak A})$ -formula and ${\mathfrak B}\models \exists x\varphi (x)$ , then there is $a\in {\mathfrak A}$ with ${\mathfrak B}\models \varphi (a)$ .

3.5 The ${\cal L}'$ -expansions $\mathfrak {A',B'}$

Since ${\mathfrak A}$ and ${\mathfrak B}$ are elementarily equivalent ${\cal L}({\mathfrak A})$ -structures, by Frayne’s theorem [5, corollary 4.3.13] there exist an ultrapower ${\mathfrak A}^*$ and an ${\cal L}({\mathfrak A})$ -elementary embedding $\sigma :{\mathfrak B}\to {\mathfrak A}^*$ . (The ultrapower ${\mathfrak M}^*$ , using the same ultrafilter, is defined for every structure ${\mathfrak M}$ .) Let $\delta :{\mathfrak A}\to {\mathfrak A}^*$ be the diagonal embedding (called the ‘natural embedding’ in [5, p. 221]). Because each element of ${\mathfrak A}$ is named by a constant of ${\cal L}({\mathfrak A})$ , we have $\delta =\sigma \circ \iota $ (see Figure 1).

Fig. 1 The ${\cal L}({\mathfrak A})$ -elementary maps $\delta ,\iota ,\sigma $ . The diagram commutes.

Definition 3.1.

1. 1. Let ${\cal L}'$ denote the expansion of ${\cal L}({\mathfrak A})$ by a unary relation symbol $\underline {\mu }$ of algebra sort for each ultrafilter $\mu \in {\cal A}_+$ .

2. 2. Expand ${\mathfrak A}$ to an ${\cal L}'$ -structure ${\mathfrak A}'$ , by interpreting each $\underline {\mu }$ as $\mu $ . In other words, for each $a\in {\cal A}$ we put ${\mathfrak A}'\models \underline {\mu }(a)$ iff $a\in \mu $ .

3. 3. ${\mathfrak A}^{\prime *}$ denotes the $^*$ -ultrapower $({\mathfrak A}')^*$ of ${\mathfrak A}'$ . It is an ${\cal L}'$ -expansion of ${\mathfrak A}^*$ .

4. 4. Expand ${\mathfrak B}$ to an ${\cal L}'$ -structure ${\mathfrak B}'$ , by setting ${\mathfrak B}'\models \underline {\mu }(b)$ iff ${\mathfrak A}^{\prime *}\models \underline {\mu }(\sigma (b))$ , for each $b\in {\cal B}$ and $\mu \in {\cal A}_+$ .

Of course, $\delta :{\mathfrak A}'\to {\mathfrak A}^{\prime *}$ is still the diagonal embedding, so is ${\cal L}'$ -elementary. The maps $\iota :{\mathfrak A}'\to {\mathfrak B}'$ and $\sigma :{\mathfrak B}'\to {\mathfrak A}^{\prime *}$ are ${\cal L}'$ -embeddings, but as Example 3.8 shows, they are not always ${\cal L}'$ -elementary.

3.6 Simple formulas

Definition 3.2. An ${\cal L}'$ -formula is said to be simple if it is a boolean combination of ${\cal L}({\mathfrak A})$ -formulas and atomic ${\cal L}'$ -formulas of the form $\underline {\mu }(\tau )$ , where $\mu \in {\cal A}_+$ and $\tau $ is an ${\cal L}({\mathfrak A})$ -term (equivalently, an ${\cal L}'$ -term) of algebra sort.

The following is a weak (but still useful) preservation result.

Proposition 3.3.

1. 1. For each simple ${\cal L}'$ -formula $\theta ({\bar x})$ and each tuple ${\bar b}$ of elements of ${\mathfrak B}$ whose sorts match those of ${\bar x}$ , we have ${\mathfrak B}'\models \theta ({\bar b})$ iff ${\mathfrak A}^{\prime *}\models \theta (\sigma ({\bar b}))$ .

2. 2. For each simple ${\cal L}'$ -formula $\theta ({\bar x},{\bar y})$ , if ${\mathfrak A}'\models \exists {\bar x}\forall {\bar y}\theta $ then ${\mathfrak B}'\models \exists {\bar x}\forall {\bar y}\theta $ .

Proof. (1) is proved by induction on the structure of $\theta $ as a simple formula. If $\theta $ is an ${\cal L}({\mathfrak A})$ -formula, the result holds because $\sigma $ is ${\cal L}({\mathfrak A})$ -elementary. Suppose that $\theta =\underline {\mu }(\tau ({\bar x}))$ , where $\mu \in {\cal A}_+$ and $\tau ({\bar x})$ is an algebra-sorted ${\cal L}({\mathfrak A})$ -term. Let ${\bar b}\in {\mathfrak B}$ have sorts matching those of ${\bar x}$ , ² and write $b=\tau ^{{\mathfrak B}}({\bar b})\in {\cal B}$ . Then

$$\begin{align*}\begin{array}{r@{\ \ }cl@{\ \ }l} {\mathfrak B}'\models\theta({\bar b}) &\iff& {\mathfrak B}'\models\underline{\mu}(\tau({\bar b})) &\mbox{as }\theta=\underline{\mu}(\tau({\bar x})) \\ &\iff& {\mathfrak B}'\models\underline{\mu}(b) &\mbox{by definition of }b \\ &\iff& {\mathfrak A}^{\prime *}\models\underline{\mu}(\sigma(b)) &\mbox{by definition of the expansion }{\mathfrak B}' \\ &\iff& {\mathfrak A}^{\prime *}\models\underline{\mu}(\tau(\sigma({\bar b}))) &\mbox{as } \sigma \mbox{ is } {\cal L}({\mathfrak A})\mbox{-elementary, so } \sigma(b)=\tau^{{\mathfrak A}^*}(\sigma({\bar b})) \\ &\iff& {\mathfrak A}^{\prime *}\models\theta(\sigma({\bar b})) &\mbox{as }\theta=\underline{\mu}(\tau({\bar x})). \end{array} \end{align*}$$

The boolean cases are standard.

It is enough to prove (2) for ${\cal L}'$ -sentences of the form $\forall {\bar y}\theta $ , where $\theta ({\bar y})$ is simple. For, given this much, if ${\mathfrak A}'\models \exists {\bar x}\forall {\bar y}\theta ({\bar x},{\bar y})$ , then choose ${\bar a}\in {\mathfrak A}'$ with ${\mathfrak A}'\models \forall {\bar y}\theta ({\bar a},{\bar y})$ . Let $\underline {{\bar a}}$ be the tuple of constants in ${\cal L}({\mathfrak A})$ corresponding to ${\bar a}$ . Clearly, $\theta (\underline {{\bar a}},{\bar y})$ is also a simple ${\cal L}'$ -formula, and ${\mathfrak A}'\models \forall {\bar y}\theta (\underline {{\bar a}},{\bar y})$ . So by assumption, ${\mathfrak B}'\models \forall {\bar y}\theta (\underline {{\bar a}},{\bar y})$ . Then certainly, ${\mathfrak B}'\models \exists {\bar x}\forall {\bar y}\theta ({\bar x},{\bar y})$ .

So let $\theta ({\bar y})$ be simple and suppose that ${\mathfrak A}'\models \forall {\bar y}\theta $ . As $\delta :{\mathfrak A}'\to {\mathfrak A}^{\prime *}$ is ${\cal L}'$ -elementary, ${\mathfrak A}^{\prime *}\models \forall {\bar y}\theta $ as well. Let ${\bar b}\in {\mathfrak B}$ be arbitrary subject to matching the sorts of ${\bar y}$ . Since ${\mathfrak A}^{\prime *}\models \forall {\bar y}\theta $ , certainly ${\mathfrak A}^{\prime *}\models \theta (\sigma ({\bar b}))$ . Part 1 now gives us ${\mathfrak B}'\models \theta ({\bar b})$ . Since ${\bar b}$ was arbitrary, we obtain ${\mathfrak B}'\models \forall {\bar y}\theta $ as required.

Corollary 3.4. If $\theta ({\bar x})$ is a simple ${\cal L}'$ -formula, then ${\mathfrak A}'\models \forall {\bar x}\theta $ iff ${\mathfrak B}'\models \forall {\bar x}\theta $ .

Proof. ${\Rightarrow }$ is a special case of Proposition 3.3(2). For $\Leftarrow $ , if ${\mathfrak A}'\not \models \forall {\bar x}\theta $ then ${\mathfrak A}'\models \exists {\bar x}\neg \theta $ , and since $\neg \theta $ is also simple, the proposition yields ${\mathfrak B}'\models \exists {\bar x}\neg \theta $ . Hence, ${\mathfrak B}'\not \models \forall {\bar x}\theta $ .

3.7 Some applications

Corollary 3.4 will be used several times, beginning with the following:

Corollary 3.5. For each $\mu \in {\cal A}_+$ , the set $\underline {\mu }^{{\mathfrak B}'}=\{b\in {\mathfrak B}':{\mathfrak B}'\models \underline {\mu }(b)\}$ is an ultrafilter of ${\cal B}$ .

Proof. The conclusion says that ${\mathfrak B}'\models \forall xyz(\underline {\mu }(x)\wedge \underline {\mu }(y)\wedge z\geq x\cdot y\to \underline {\mu }(z))$ and ${\mathfrak B}'\models \forall x(\underline {\mu }(-x)\leftrightarrow \neg \underline {\mu }(x))$ . These are universally-quantified simple ${\cal L}'$ -sentences, and they hold in ${\mathfrak A}'$ since $\mu $ is an ultrafilter of ${\cal A}$ . By Corollary 3.4, they also hold in ${\mathfrak B}'$ .

So as well as $\underline {\mu }^{{\mathfrak B}'}\subseteq {\cal B}$ , we also have $\underline {\mu }^{{\mathfrak B}'}\in {\cal B}_+$ .

Definition 3.6. For $w\in W$ , let $\hat w=\{a\in {\cal A}:{\mathfrak A}\models a\,{\mathrel {\underline {\in }}}\, w\}$ . Let ${\widehat W}=\{\hat w:w\in W\}$ .

Since ${\mathfrak A}=({\cal A},W)\preceq {\mathfrak B}=({\cal B},{\cal B}_+)$ , we have $W\subseteq {\cal B}_+$ , so each $w\in W$ is an ultrafilter of ${\cal B}$ , and $w=\{b\in {{\cal B}}:{\mathfrak B}\models b\,{\mathrel {\underline {\in }}}\, w\}$ . However, taking ${\mathfrak A}$ in isolation, the elements of W are just ‘abstract points’. Unless ${\cal A}={\cal B}$ , elements of W are not subsets of ${\cal A}$ , and for $w\in W$ we do not have $w=\hat w$ . Nonetheless, we have the following.

Lemma 3.7. Each $\hat w$ (for $w\in W$ ) is an ultrafilter of ${\cal A}$ , and so ${\widehat W}\subseteq {\cal A}_+$ .

Proof. We have ${\mathfrak B}\models \forall xyzt(x\,{\mathrel {\underline {\in }}}\, t\wedge y\,{\mathrel {\underline {\in }}}\, t\wedge z\geq x\cdot y\to z\,{\mathrel {\underline {\in }}}\, t)$ and ${\mathfrak B}\models \forall xt({-}x\,{\mathrel {\underline {\in }}} t\leftrightarrow \neg (x\,{\mathrel {\underline {\in }}}\, t))$ . Because ${\mathfrak A}\preceq {\mathfrak B}$ , these ${\cal L}$ -sentences also hold in ${\mathfrak A}=({\cal A},W)$ .

In fact, $\hat w$ is the intersection with ${\cal A}$ of the ultrafilter $w$ of ${\cal B}$ , for each $w\in W$ . In general, the inclusion ${\widehat W}\subseteq {\cal A}_+$ is strict. For example, this happens when ${\cal A}_+$ is uncountable, since W and hence ${\widehat W}$ are countable.

Example 3.8. The converse implication in Proposition 3.3(2) can fail. For example, suppose that ${\cal A}_+$ is uncountable. So there is $\mu \in {\cal A}_+\setminus {\widehat W}$ . Consider the simple ${\cal L}'$ -formula

$$\begin{align*}\theta(x,y)\;{\buildrel \mathrm{def} \over =}\; y\mathrel{\underline{\in}} x\leftrightarrow\underline{\mu}(y). \end{align*}$$

By Corollary 3.5 we have $\underline {\mu }^{{\mathfrak B}'}\in {\cal B}_+$ , and evidently ${\mathfrak B}'\models \forall y(y\,{\mathrel {\underline {\in }}}\, \underline {\mu }^{{\mathfrak B}'}\leftrightarrow \underline {\mu }(y))$ . Hence, $\underline {\mu }^{{\mathfrak B}'}$ witnesses ${\mathfrak B}'\models \exists x \forall y\theta $ . But $\mu \notin {\widehat W}$ , so there is no $w\in W$ with ${\mathfrak A}'\models \forall y(y\,{\mathrel {\underline {\in }}}\, w\leftrightarrow \underline {\mu }(y))$ . Hence, ${\mathfrak A}'\not \models \exists x \forall y\theta $ .

So the elementarily-equivalent ${\cal L}'$ -structures ${\mathfrak A}'$ and ${\mathfrak A}^{\prime *}$ need not be elementarily equivalent to ${\mathfrak B}'$ , since they may disagree on the ${\cal L}'$ -sentence $\exists x\forall y\theta $ . It follows that the embeddings $\iota :{\mathfrak A}'\to {\mathfrak B}'$ and $\sigma :{\mathfrak B}'\to {\mathfrak A}^{\prime *}$ are not ${\cal L}'$ -elementary in general.

3.8 An embedding $f:{\cal A}_+\to {\cal B}_+$

Definition 3.9. Let $f:{\cal A}_+\to {\cal B}_+$ be given by: $f(\mu )=\underline {\mu }^{{\mathfrak B}'}$ , for each $\mu \in {\cal A}_+$ .

By Corollary 3.5, f is well defined. We plainly have

(1) $$ \begin{align} {\mathfrak B}'\models\forall x(\underline{\mu}(x)\leftrightarrow x\mathrel{\underline{\in}} f(\mu)) \end{align} $$

for each $\mu \in {\cal A}_+$ . A similar map was given by Surendonk [18] (see [19, 20] for more on this topic).

Corollary 3.10. The map $f$ is a frame embedding, and $f(\hat w)=w$ for each $w\in W$ .

If the expression ‘ $f(\hat w)=w$ ’ appears confusing, recall from the discussion after Definition 3.6 that $w$ and $\hat w$ are quite different objects and cannot be identified. While $\hat w$ is an ultrafilter of ${\cal A}$ , $w$ is ‘actually’ an ultrafilter of ${\cal B}$ , and so is $f(\hat w)$ .

Proof. First we check that f is injective. Let $\mu ,\nu \in {\cal A}_+$ and suppose that $f(\mu )= f(\nu )$ , so $\underline {\mu }^{{\mathfrak B}'}=\underline {\nu }^{{\mathfrak B}'}$ . So if $\theta $ is the ${\cal L}'$ -sentence $\forall x(\underline {\mu }(x)\leftrightarrow \underline {\nu }(x))$ , then ${\mathfrak B}'\models \theta $ . By Corollary 3.4 we have ${\mathfrak A}'\models \theta $ too, so $\mu =\nu $ .

Now let $\lozenge \in {\mathsf {M}}$ be given. Then for each $\mu ,\nu \in {\cal A}_+$ , we have ${\cal A}_+\models R_{\lozenge }\mu \nu $ iff ${\mathfrak A}'\models \forall x(\underline {\nu }(x)\to \underline {\mu }(\lozenge x))$ . By Corollary 3.4, this is iff ${\mathfrak B}'\models \forall x(\underline {\nu }(x)\to \underline {\mu }(\lozenge x))$ , iff ${\cal B}_+\models R_{\lozenge }(\underline {\mu }^{{\mathfrak B}'},\underline {\nu }^{{\mathfrak B}'})$ —that is, ${\cal B}_+\models R_{\lozenge }(f(\mu ),f(\nu ))$ . So f preserves each $R_{\lozenge }$ both ways.

Hence, f is an embedding (in the usual model-theoretic sense) from ${\cal A}_+$ to ${\cal B}_+$ .

Finally, let $w\in W$ be given. Let $\mu =\hat w\in {\cal A}_+$ . Plainly, ${\mathfrak A}'\models \forall x(\underline {\mu }(x)\leftrightarrow x\,{\mathrel {\underline {\in }}}\, \underline {w})$ . By Corollary 3.4, ${\mathfrak B}'\models \forall x(\underline {\mu }(x)\leftrightarrow x\,{\mathrel {\underline {\in }}}\,\underline {w})$ as well. By (1), we obtain ${\mathfrak B}\models \forall x(x\,{\mathrel {\underline {\in }}}\,\underline {w}\leftrightarrow x\,{\mathrel {\underline {\in }}}\, f(\mu ))$ . But it follows from the definition of ${\mathfrak B}=({\cal B},{\cal B}_+)$ that ${\mathfrak B}\models \forall yz(\forall x(x\,{\mathrel {\underline {\in }}}\, y\leftrightarrow x\,{\mathrel {\underline {\in }}}\, z)\to y=z)$ , so $w=f(\mu )=f(\hat w)$ .

We remark that f need not be a bounded morphism (V would be easily seen to be resolved if it were). For if it were, then $R_{\lozenge }^{{\cal B}_+}(w)\subseteq f({\cal A}_+)$ for every $\lozenge \in {\mathsf {M}}$ and $w\in W$ ; yet it can be that $|R_{\lozenge }^{{\cal B}_+}(w)|>|{\cal A}_+|$ . See [18, sec. 6] for details and related discussion.

Problem 3.11. Is $f$ elementary—or can it be made so by choosing the ultrapower ${\mathfrak A}^*$ appropriately?

A positive answer would imply that the canonical frames of all free V-algebras of infinite rank are elementarily equivalent. For discussion around this, see, e.g., [18] and [20, question 3.47].

3.9 A strategy for proving total canonicity

We will now describe a method, based on embeddings $f:{\cal A}_+\to {\cal B}_+$ as above, that will be used to show that certain varieties are resolved.

We assume that $\phi _0$ is a modal ${\mathsf {M}}$ -formula true at some point in ${\cal B}_+$ under the valuation $g:{\mathsf {Q}}\to \wp ({\cal B}_+)$ given by $g(q_i)=Q_i^{\mathfrak B}$ for each $i<\omega $ .

Recall that each modal ${\mathsf {M}}$ -formula $\psi $ has a standard translation: an ${\cal L}$ -formula $\psi ^x(x)$ for each point-sorted variable x. We define $\psi ^x$ by induction on $\psi $ as usual: $\top ^x=\top $ , $q_i^x=Q_i(x)$ for $i<\omega $ , $(\neg \psi )^x=\neg (\psi ^x)$ , $(\psi \vee \chi )^x=\psi ^x\vee \chi ^x$ , and $(\lozenge \psi )^x=\exists y(R_{\lozenge } xy\wedge \psi ^y)$ for each $\lozenge \in {\mathsf {M}}$ , where y is some point-sorted variable other than $ x$ . A standard induction on $\psi $ now shows that for each $t\in {\cal B}_+$ (and any x), we have

(2) $$ \begin{align} ({\cal B}_+,g),t\models\psi \iff {\mathfrak B}\models\psi^x(t). \end{align} $$

Since $\phi _0$ is satisfied in the Kripke model $({\cal B}_+,g)$ , we have ${\mathfrak B}\models \exists x\phi _0^x$ . By the Tarski–Vaught criterion (Section 3.4), there is $w_0\in W$ with ${\mathfrak B}\models \phi _0^x(w_0)$ , and so

(3) $$ \begin{align} ({\cal B}_+,g),w_0\models\phi_0. \end{align} $$

We fix such a $w_0$ . Let ${\cal F}={\cal A}_+(\widehat {w_0})$ be the inner subframe of ${\cal A}_+$ generated by $\widehat {w_0}$ (see Definitions 2.4 and 3.6), and let ${\cal M}$ be the submodel of $({\cal B}_+,g)$ with domain $f({\cal F})$ . By Corollary 3.10, $w_0=f(\widehat {w_0})\in f({\cal F})={\cal M}$ . See Figure 2 for a rough illustration.

Fig. 2 Schematic diagram of elements of the strategy.

Definition 3.12. We will say that the Truth Lemma holds in $V$ if the following always holds in these given circumstances:

For each $m\in {\cal M}$ and modal ${\mathsf {M}}$ -formula $\psi $ , we have ${\cal M},m\models \psi $ iff $({\cal B}_+,g),m\models \psi $ . In particular, ${\cal M},w_0\models \phi _0$ .

Theorem 3.13. If the Truth Lemma holds in V, then V is resolved.

Proof. Assume that V is not canonical. So there is ${\cal B}\in V$ with ${\cal B}^{\sigma }\notin V$ . Hence, some equation $\varepsilon $ valid in V is not valid in ${\cal B}^{\sigma }$ . Translate $\varepsilon $ to a modal formula $\varphi _{\varepsilon }$ as in Section 2.6. Then $\neg \varphi _{\varepsilon }$ is satisfiable in the frame ${\cal B}_+$ . Form ${\mathfrak B}$ from ${\cal B}$ , choosing the $Q_i^{\mathfrak B}$ so that the valuation g above will satisfy $\neg \varphi _{\varepsilon }$ in ${\cal B}_+$ , and then form ${\mathfrak A}$ , ${\cal A}$ , W, $w_0$ , ${\cal F}$ , ${\cal M}$ , etc., all as above, using $\phi _0=\neg \varphi _{\varepsilon }$ . By the Truth Lemma, ${\cal M},w_0\models \neg \varphi _{\varepsilon }$ .

Now the frame $f({\cal F})$ of ${\cal M}$ is isomorphic (via $f^{-1}$ ) to ${\cal F}$ . Hence, $\neg \varphi _{\varepsilon }$ is satisfiable in ${\cal F}$ . As ${\cal F}$ is an inner subframe of ${\cal A}_+$ , standard modal arguments (see, e.g., [2, theorem 3.14] or [4, corollary 2.9]) show that $\neg \varphi _{\varepsilon }$ is satisfiable in ${\cal A}_+$ , and it follows that ${\cal A}^{\sigma }\not \models \varepsilon $ and ${\cal A}^{\sigma }\notin V$ . Since ${\cal A}\in V$ is countable, we see that V is not $\omega $ -canonical. Hence, V is resolved.

For countable ${\mathsf {M}}$ , this result reduces the problem of showing that a variety is resolved to the problem of showing that the Truth Lemma holds in it.

The main challenge in establishing the Truth Lemma is the following. Suppose that $m\in {\cal M}$ and $({\cal B}_+,g),m\models \lozenge \psi $ , so there is $z\in {\cal B}_+$ with ${\mathfrak B}\models R_{\lozenge } mz$ and $({\cal B}_+,g),z\models \psi $ . We need to find such a z in ${\cal M}$ . It suffices to find one in W, and our whole strategy relies upon doing so. In favourable circumstances, we can do it using the Tarski–Vaught criterion from Section 3.4, even when $m\notin W$ . The proof of Proposition 4.2 illustrates the process.

4 Logics above ${K}5_2$

Application of the strategy of the last section (Section 3.9) will now be illustrated by showing that it can be successfully applied in the monomodal language (where ${\mathsf {M}}=\{\lozenge \}$ ) to all normal modal logics that include a logic we call $K5_2$ . To define this, for each $n<\omega $ let $\lozenge ^n$ denote a sequence of $\lozenge $ ’s of length n. Then the axiom $\lozenge ^n p\to \Box \lozenge p$ will be called $5_n$ . To describe its corresponding frame condition we introduce the notation $R_{\lozenge }{}^n$ for the relation $R_{\lozenge ^n}$ , i.e., the n-fold composition of $R_{\lozenge }$ with itself. A frame validates $5_n$ iff its relation satisfies

(4) $$ \begin{align} \text{for all } x,y,z, \ R_{\lozenge}{}xy \text{ and } R_{\lozenge}{}^{n}xz \text{ implies } R_{\lozenge} yz. \end{align} $$

$5_n$ is a Sahlqvist formula with first-order correspondent (4). This implies that if an algebra ${\cal B}$ validates $5_n$ , then its canonical frame ${\cal B}_+$ will satisfy (4) and so validate $5_n$ .

$5_0$ is the Brouwerian axiom $ p\to \Box \lozenge p$ , corresponding to symmetry of $R_{\lozenge }$ , which is the case $n=0$ of (4). $5_1$ is $\lozenge p\to \Box \lozenge p$ , whose equivalent form $\lozenge \Box p\to \Box p$ is commonly known as 5, due to its role in the definition of Lewis’s system S5.

4.1 Canonicity of extensions of $K5_2$

We now turn to $5_2$ .

Lemma 4.1. A frame validates $5_2$ iff for all $n<\omega $ it satisfies

(5) $$ \begin{align} \text{for all } x,y,z, \ R_{\lozenge}{}^nxy \text{ and } R_{\lozenge}{}^{n+1}xz \text{ implies } R_{\lozenge} yz. \end{align} $$

Proof. The case $n=1$ of (5) is the same as the case $n=2$ of (4), which is the condition for validity of $5_2$ . So it suffices to show that the case $n=1$ of (5) implies that (5) holds for all n.

So assume the $n=1$ case of (5). Then we prove (5) by induction on n. The base case $n=0$ asserts that if $x=y$ and $R_{\lozenge } xz$ then $R_{\lozenge } yz$ , which is true. Now assume inductively that (5) holds for n. Then if $R_{\lozenge }{}^{n+1}xy$ and $R_{\lozenge }{}^{n+2}xz$ , there are $y',z'$ such that $R_{\lozenge }{}^nxy'$ and $R_{\lozenge }{}y'y$ , and $R_{\lozenge }{}^{n+1}xz'$ and $R_{\lozenge }{}z'z$ . From $R_{\lozenge }{}^nxy'$ and $R_{\lozenge }{}^{n+1}xz'$ by the hypothesis on n we get $R_{\lozenge }{}y'z'$ . Thus we have $R_{\lozenge }{}y'y$ and $R_{\lozenge }{}^2y'z$ (since $R_{\lozenge }{}y'z'$ and $R_{\lozenge }{}z'z$ ), hence $R_{\lozenge }{}yz$ by the $n=1$ case. Thus (5) holds for $n+1$ .

Proposition 4.2. Let V be any variety of monomodal BAOs that validate $5_2$ . Then the Truth Lemma holds in V.

Proof. Suppose we have an algebra ${\cal B}\in V$ , a countable elementary substructure ${\mathfrak A}=({\cal A},W)$ of ${\mathfrak B}=({\cal B},{\cal B}_+)$ , an embedding $f:{\cal A}_+\to {\cal B}_+$ such that $f(\hat w)=w$ for every $w\in W$ (Corollary 3.10), and a valuation g on ${\cal B}_+$ ; with ${\cal M}$ being the submodel of $({\cal B}_+,g)$ with domain $f({\cal F})$ , where ${\cal F}$ is the inner subframe ${\cal A}_+(\widehat {w_0})$ of ${\cal A}_+$ generated by $\widehat {w_0}$ for some $w_0\in W$ . Then we have to show that for each $m\in {\cal M}$ and modal formula $\psi $ , we have ${\cal M},m\models \psi $ iff $({\cal B}_+,g),m\models \psi $ .

The proof is by induction on the formation of $\psi $ . The significant case is $\lozenge \psi $ , assuming inductively the result for $\psi $ . If ${\cal M},m\models \lozenge \psi $ , then there is some $z_0$ in ${\cal M}$ with $R_{\lozenge }^{{\cal M}} m z_0$ and ${\cal M},z_0\models \psi $ . But then $({\cal B}_+,g),z_0\models \psi $ by the induction hypothesis on $\psi $ , and $R_{\lozenge }^{{\mathfrak B}} m z_0$ as ${\cal M}$ is a submodel of ${\cal B}_+$ . This shows that $({\cal B}_+,g),m\models \lozenge \psi $ .

Conversely, suppose that $({\cal B}_+,g),m\models \lozenge \psi $ with $m\in {\cal M}$ . Then there is some $z_0\in {\cal B}_+$ with $R_{\lozenge }^{{\mathfrak B}} m z_0$ and $({\cal B}_+,g),z_0\models \psi $ . Hence ${\mathfrak B}\models \psi ^x(z_0)$ by (2). Since $m\in {\cal M}$ , we have $(R_{\lozenge }^{{\mathfrak B}})^n w_0 m$ for some $n\geq 0$ , hence $(R_{\lozenge }^{{\mathfrak B}})^{n+1}w_0 z_0$ . Therefore,

$$ \begin{align*} {\mathfrak B}\models \exists z_1\cdots\exists z_n\exists x(R_{\lozenge} \underline{w_0}z_1 \land R_{\lozenge} z_1z_2\land\cdots\land R_{\lozenge} z_nx\land\psi^x). \end{align*} $$

Now $w_0\in W$ , so $n+1$ applications of the Tarski–Vaught criterion to this last fact yield elements $w_1,\dots ,w_n,w\in W$ such that

$$ \begin{align*}{\mathfrak B}\models R_{\lozenge} w_0 w_1\land R_{\lozenge} w_1w_2\land\cdots\land R_{\lozenge} w_nw\land\psi^x(w). \end{align*} $$

So $(R_{\lozenge }^{{\mathfrak B}})^{n+1}w_0w$ . Now $W\not \subseteq {\cal M}$ in general. But as $f:{\cal A}_+\to {\cal B}_+$ is an embedding, and $\hat u\in {\cal A}_+$ and $f(\hat u)=u$ for each $u\in W$ , we see that $(R^{{\cal A}_+}_{\lozenge })^{n+1}\widehat {w_0}\hat w$ . Since ${\cal F}={\cal A}_+(\widehat {w_0})$ , we obtain $\hat w\in {\cal F}$ , and hence $w=f(\hat w)\in {\cal M}$ . By (2), $({\cal B}_+,g),w\models \psi $ . Hence ${\cal M},w\models \psi $ by the induction hypothesis. Also, we now have $(R_{\lozenge }^{{\mathfrak B}})^n w_0 m$ and $(R_{\lozenge }^{{\mathfrak B}})^{n+1} w_0 w$ , so (5) gives $R^{{\mathfrak B}}_{\lozenge } mw$ . This is because ${\cal B}\in V$ , so ${\cal B}$ validates $5_2$ , hence so does the frame ${\cal B}_+$ , and so Lemma 4.1 applies to ${\cal B}_+$ .

Since $R^{{\mathfrak B}}_{\lozenge } mw$ we get $R^{{\cal M}}_{\lozenge } mw$ as m and $w$ are in ${\cal M}$ . Together with ${\cal M},w\models \psi $ , this implies the desired ${\cal M},m\models \lozenge \psi $ , and completes the inductive case for $\lozenge $ .

$K5_n$ is the smallest normal logic to contain $5_n$ . $K5_2$ is a sublogic of $K5$ , as can be seen model-theoretically by deriving the case $n=2$ of (4) from its $n=1$ case. (A proof-theoretic demonstration is also straightforward.) It follows from the result just proved and Theorem 3.13 that:

Theorem 4.3. Every normal logic extending $K5_2$ that is $\omega $ -canonical is totally canonical.

4.2 Continuum-many logics between $K5_2$ and $K5$

Theorem 4.3 applies to all normal extensions of $K5$ . But whereas $K5$ has only countably many extensions [15], we will now show that $K5_2$ has continuum many. Indeed there are continuum many between $K5_2$ and $K5$ .

Fig. 3 The intransitive frame ${\cal D}_j$ validating $5_2$ .

The proof adapts a construction from [4, p. 162]. For each $j\in \omega $ , let ${\cal D}_j$ be the ‘diamond-shaped’ frame depicted in Figure 3. We take this as an intransitive irreflexive frame in which the only relations that hold are those given by the displayed arrows. Thus the relation $R_{\lozenge }$ of ${\cal D}_j$ is

$$ \begin{align*}\begin{array}{@{}r@{\ }l} \{ (j+1,j'),(j+1,j''), (j',j-1), (j'',j-1)\} \cup\{(i,i-1): j-1\geq i\geq 1\},&\mbox{if }j>0, \\[2pt] \{ (1,0'),(1,0'')\},&\mbox{if }j=0. \end{array} \end{align*} $$

By inspection, this relation satisfies (4) with $n=2$ , so ${\cal D}_j$ validates 5 $_2$ . (If we replaced $R_{\lozenge }$ by its transitive closure, $5_2$ would not be valid when $j>0$ .)

For each $i\in \omega $ , let $\alpha _i$ be the constant formula $\lozenge ^i\top \land \neg \lozenge ^{i+1}\top $ . In ${\cal D}_j$ , if $i<j$ or $i=j+1$ , then $\alpha _i$ holds at i and nowhere else. If $i>j+1$ , then $\alpha _i$ does not hold at any point. On the other hand, $\alpha _j$ holds at both $j'$ and $j''$ . Now let $\varphi _i$ be the formula

$$ \begin{align*}\Box(\alpha_i \to p) \lor \Box(\alpha_i \to \neg p). \end{align*} $$

If $i\ne j$ , then $\alpha _i$ is true at no more than one point in ${\cal D}_j$ , so ${\cal D}_j\models \varphi _i$ . But ${\cal D}_j\not \models \varphi _j$ , for making p true just at $j'$ gives a model on ${\cal D}_j$ at which $\alpha _j \to p$ is false at $j''$ and $\alpha _j \to \neg p$ is false at $j'$ , hence $\varphi _j$ is false at $j+1$ .

For each non-empty subset $I\subseteq \omega $ , let $L_I$ be the smallest normal modal logic containing $K5_2\cup \{\varphi _i:i\in I\}$ . Suppose that $I\ne J\subseteq \omega $ with, say, some $j\in J\setminus I$ . As $j\notin I$ we have ${\cal D}_j\models \varphi _i$ for all $i\in I$ . Since also ${\cal D}_j\models K5_2$ , the logic determined by ${\cal D}_j$ includes $K5_2\cup \{\varphi _i:i\in I\}$ , so it includes $L_I$ as the smallest such. Thus ${\cal D}_j\models L_I$ . But ${\cal D}_j\not \models \varphi _j$ , so then $\varphi _j\notin L_I$ . On the other hand $j\in J $ , so $\varphi _j\in L_J$ by definition. Hence $L_I\ne L_J$ . The case $I\setminus J\ne \emptyset $ is likewise.

Thus there are $2^{\aleph _0}$ logics $L_I$ , one for each subset I of $\omega $ , and they all include K5 $_2$ . But they are all included in $K5$ , because every formula $\varphi _i$ is a $K5$ -theorem. To show this, it is enough to show that $\varphi _i$ is valid in every point-generated $K5$ -frame, since these frames determine the logic. By an analysis originally due to Segerberg [17], each such frame either (i) is a single irreflexive point, or (ii) has the property that every point has a reflexive point in its future. In case (i), every formula of the form $\Box \psi $ is valid in the frame, hence the $\varphi _i$ ’s are. In case (ii), for any $i\in I$ the formula $\lozenge ^{i+1}\top $ is true at every point, hence $\alpha _i$ is false everywhere and so $\varphi _i$ again is valid.

5 The modal logics $KU_n^{\mathsf {M}}$

In the remainder of the paper, we will define a wider class of logics and extend the canonicity analysis for $K5_2$ to them.

The rough idea is this. Take ${\mathsf {M}}=\{\lozenge \}$ . By (4) for $n=2$ , a frame ${\cal F}$ validates $K5_2$ iff for each $x\in {\cal F}$ , all points in $R^{\cal F}_{\lozenge }(x)$ have the same future: $R^{\cal F}_{\lozenge }(y)=R^{\cal F}_{\lozenge }(y')$ for all $y,y'\in R^{\cal F}_{\lozenge }(x)$ . Extended to $(R^{\cal F}_{\lozenge })^n(x)$ by Lemma 4.1, this frame condition was used in the proof of Proposition 4.2 for the crucial deduction

$$ \begin{align*}(R_{\lozenge}^{{\mathfrak B}})^n w_0 m \wedge (R_{\lozenge}^{{\mathfrak B}})^{n} w_0 w_n \wedge R_{\lozenge}^{\mathfrak B} w_nw \;\;{\Rightarrow}\;\; R^{{\mathfrak B}}_{\lozenge} mw. \end{align*} $$

Lemma 4.1 ensures that $R^{\mathfrak B}_{\lozenge }(w_n)= R^{\mathfrak B}_{\lozenge }(m)$ , so the deduction goes through. But the deduction can be made assuming only that $R^{\mathfrak B}_{\lozenge }(w_n)\subseteq R^{\mathfrak B}_{\lozenge }(m)$ . For then, $w\in R^{\mathfrak B}_{\lozenge }(w_n)\subseteq R^{\mathfrak B}_{\lozenge }(m)$ , so $R^{{\mathfrak B}}_{\lozenge } mw$ as required.

This suggests weakening the $5_2$ frame condition to: any two points in any $R^{\cal F}_{\lozenge }(x)$ have $\subseteq $ -comparable futures. That is, $R^{\cal F}_{\lozenge }(y)\subseteq R^{\cal F}_{\lozenge }(y')$ or $R^{\cal F}_{\lozenge }(y')\subseteq R^{\cal F}_{\lozenge }(y)$ for all $y,y'\in R^{\cal F}_{\lozenge }(x)$ . This may seem to allow $R^{\mathfrak B}_{\lozenge }(w_n)\supseteq R^{\mathfrak B}_{\lozenge }(m)$ above, rather than the desired converse inclusion; we will solve this problem in Proposition 7.5. We then weaken it further by replacing ‘two’ by ‘ $n+1$ ’, for arbitrary $n>0$ . This is handled in the proof of Proposition 7.5 by adding a set K of parameters. We arrive at:

• • Given any $n+1$ points from any $R^{\cal F}_{\lozenge }(x)$ , two of them have $\subseteq $ -comparable futures.

Theorem 7.7 will extend Theorem 4.3 to this case, and for arbitrary ${\mathsf {M}}$ .

So we are led to consider sets and sequences of points in a Kripke frame whose futures are pairwise incomparable with respect to inclusion, forming a $\subseteq $ -antichain. Borrowing from the physics of spacetime, we call such sets and sequences achronal. We will define them formally below, and then introduce some modal logics called $KU^{\mathsf {M}}_n$ that limit the size of achronal sets, and so stand as weakenings of $K5_2$ to which the methods of Section 4.1 can still be applied.

We will then take a break from canonicity and spend the rest of this section, and all of the next, examining these logics. We return to canonicity in Section 7, where we prove resolvedness of all normal modal ${\mathsf {M}}$ -logics extending some $KU^{\mathsf {M}}_n$ . They will be called logics of finite achronal width.

5.1 Achronal sets and sequences

Definition 5.1. Let ${\cal F}$ be a frame and $\lozenge \in {\mathsf {M}}$ .

1. 1. A subset $S\subseteq {\cal F}$ is said to be $\lozenge $ -achronal if $R_{\lozenge }^{\cal F}(x)\not \subseteq R_{\lozenge }^{\cal F}(y)$ for each distinct $x,y\in S$ .

2. 2. Let $\alpha $ be an ordinal. A sequence $(y_i:i<\alpha )$ of points of ${\cal F}$ is said to be $\lozenge $ -achronal if $R_{\lozenge }^{\cal F}(y_i)\not \subseteq R_{\lozenge }^{\cal F}(y_j)$ for each distinct $i,j<\alpha $ .

3. 3. An achronal set (or sequence) is a $\lozenge $ -achronal set (or sequence, resp.) for some $\lozenge \in {\mathsf {M}}$ .

Sets with at most one element are $\lozenge $ -achronal. Subsets of $\lozenge $ -achronal sets are $\lozenge $ -achronal, and similarly for sequences. The following lemma is elementary but worth nailing down.

Lemma 5.2. Let ${\cal F}$ be a frame, $S\subseteq {\cal F}$ , $\lozenge \in {\mathsf {M}}$ , and $\kappa $ a cardinal. The following are equivalent:

1. 1. S has a $\lozenge $ -achronal subset of cardinality $\kappa $ .

2. 2. There exists a $\lozenge $ -achronal sequence $(y_i:i<\kappa )$ of elements of S.

3. 3. There is $Y\subseteq S$ such that $R^{\cal F}_{\lozenge }[Y]$ is an $\subseteq $ -antichain of cardinality $\kappa $ (see Definition 2.1).

4. 4. $R^{\cal F}_{\lozenge }[S]$ has $\subseteq $ -width at least $\kappa $ (see Definition 2.1).

Proof. For $1\,{\Rightarrow }\,2$ , if $Y\subseteq S$ is $\lozenge $ -achronal and of cardinality $\kappa $ , let $(y_i:i<\kappa )$ enumerate Y without repetitions. This is a $\lozenge $ -achronal sequence in S.

For $2\,{\Rightarrow }\,3$ , let $(y_i:i<\kappa )$ be a $\lozenge $ -achronal sequence in S. Then $Y=\{y_i:i<\kappa \}$ satisfies 3.

$3\,{\Rightarrow }\,4$ is trivial. For $4\,{\Rightarrow }\,1$ , assume 4. So there is an $\subseteq $ -antichain $\boldsymbol {A}\subseteq R^{\cal F}_{\lozenge }[S]$ of cardinality $\kappa $ . For each $Z\in \boldsymbol {A}$ , pick a point $y_Z\in S$ with $R^{\cal F}_{\lozenge }(y_Z)=Z$ . Then $\{y_Z:Z\in \boldsymbol {A}\}\subseteq S$ is achronal and of cardinality $\kappa $ .

The condition ‘there is $Y\subseteq S$ of cardinality $\kappa $ such that $R^{\cal F}_{\lozenge }[Y]$ is an $\subseteq $ -antichain’ clearly follows from condition 3 in the lemma, but is strictly weaker, as we may have $|R^{\cal F}_{\lozenge }[Y]|<\kappa $ . As an informal example, let ${\cal F}=(\omega ,R)$ , where $R=\emptyset $ . Here, ${\cal F}$ has no achronal subset with more than one element, but $R[\omega ]=\{\emptyset \}$ is trivially an $\subseteq $ -antichain.

5.2 The logic $KU_n^{\mathsf {M}}$

Definition 5.3. Let $0<n<\omega $ . We write $KU_n^{\mathsf {M}}$ for the smallest normal modal ${\mathsf {M}}$ -logic containing the following set $U^{\mathsf {M}}_n$ of axioms:

$$\begin{align*}U_n^{\mathsf{M}}=\Big\{ \bigvee_{i\leq n}\Box\big(\blacksquare q_i\to\bigvee_{j\leq n,\,j\neq i}\blacksquare q_j\big) \;:\; \lozenge,\blacklozenge\in{\mathsf{M}} \Big\}. \end{align*}$$

For avoidance of doubt, $i$ and $j$ here denote ordinals in $\{0,\ldots ,n\}$ .

A normal modal ${\mathsf {M}}$ -logic is said to be of finite achronal width if it contains $U^{\mathsf {M}}_n$ for some $n$ with $0<n<\omega $ .

5.3 First-order correspondents of the $U_n^{\mathsf {M}}$

The $U_n^{\mathsf {M}}$ axiom shown above is equivalent to $(\bigwedge _{i}\lozenge (\blacksquare q_i\wedge \neg \bigvee _{j\neq i}\blacksquare q_j))\to \bot $ , a Sahlqvist formula according to [2, definition 3.51]. Its first-order correspondent [2, theorem 3.54] is

$$\begin{align*}\forall xy_0\ldots y_n\bigvee_{i\leq n} \big[ R_{\lozenge} xy_i\to\bigvee_{j\leq n,\,j\neq i}\forall z(R_{\blacklozenge} y_iz\to R_{\blacklozenge} y_jz)\big]. \end{align*}$$

The part following the $\forall xy_0\ldots y_n$ is the disjunction of the formulas $\neg R_{\lozenge } xy_i$ , for each $i\leq n$ , and $\forall z(R_{\blacklozenge } y_iz\to R_{\blacklozenge } y_jz)$ , for each distinct $i,j\leq n$ . Reordering these to put the $\neg R_{\lozenge } xy_i$ first, we see that the whole correspondent is logically equivalent to

(6) $$ \begin{align} \forall xy_0\ldots y_n \Big( \Big( \bigwedge_{i\leq n}R_{\lozenge} xy_i \Big) \to \bigvee_{i,j\leq n,\>i\neq j} \forall z(R_{\blacklozenge} y_iz\to R_{\blacklozenge} y_jz) \Big). \end{align} $$

This is the form that we will use. A frame validates $U_n^{\mathsf {M}}$ iff (6) holds in the frame for every $\lozenge ,\blacklozenge \in {\mathsf {M}}$ .

Informally, (6) says that for any $R_{\lozenge }$ -successors ${y_0,\ldots {},y_{n}}$ of some given world, we have $R_{\blacklozenge }(y_i)\subseteq R_{\blacklozenge }(y_j)$ for some distinct $i,j\leq n$ . That is, the sequence $(y_i:i\leq n)$ is not $\blacklozenge $ -achronal. So by Lemma 5.2, (6) is equivalent to each of:

• • Every $\blacklozenge $ -achronal set contained in some $R_{\lozenge }(x)$ has at most n elements.

• • For each x, the $\subseteq $ -width of $R_{\blacklozenge }[R_{\lozenge }(x)]$ is at most n.

Consequently, $U_n^{\mathsf {M}}$ is valid in precisely those frames ${\cal F}$ such that for each $x\in {\cal F}$ and $\lozenge \in {\mathsf {M}}$ , every achronal subset of $R^{\cal F}_{\lozenge }(x)$ has at most n elements.

5.4 Alternative formulation

The axiom shown in Definition 5.3 can be reformulated more in the style of [7] and [24], as

$$\begin{align*}\Big(\bigwedge_{i\leq n}\lozenge (p_i\wedge\blacksquare q_i)\Big) \to\bigvee_{i,j\leq n,\,i\neq j}\lozenge(p_i\wedge\blacksquare q_j), \end{align*}$$

where ${p_0,\ldots {},p_{n}},{q_0,\ldots {},q_{n}}\in {\mathsf {Q}}$ are pairwise distinct atoms. This form is also Sahlqvist, with first-order correspondent (6). So while the two forms are not equivalent formulas, they lie in the same normal modal ${\mathsf {M}}$ -logics. As axioms, they are interchangeable. We give the alternative form in case it is more appealing.

5.5 $U_1^{\mathsf {M}}$

To gain some familiarity with the $U_n^{\mathsf {M}}$ , let us quickly discuss the simplest case, when $M=\{\lozenge \}$ and $n=1$ . Then $U_1^{\mathsf {M}}=\{\Box (\Box q_0\to \Box q_1)\vee \Box (\Box q_1\to \Box q_0)\}$ . This is not a new axiom. For example, Van Benthem [1, lemma 3.2] used $\Box (\Box p\to \Box q)\vee \Box (\Box q\to \Box p)$ as part of a Kripke-incompleteness proof, and stated an equivalent form of the correspondent (6) for it. We will say a little more about this in Section 6.

Plainly, every frame ${\cal F}$ such that

(7) $$ \begin{align} (R^{\cal F}_{\lozenge}[{\cal F}],\subseteq) \mbox{ is a chain---i.e.},\ R^{\cal F}_{\lozenge}(x)\subseteq R^{\cal F}_{\lozenge}(y) \mbox{ or } R^{\cal F}_{\lozenge}(y)\subseteq R^{\cal F}_{\lozenge}(x) \mbox{ for every } x,y\in{\cal F} \end{align} $$

has no achronal subset with more than one element, so satisfies (6) for $n=1$ and validates $U_1^{\mathsf {M}}$ . Indeed, it validates $U^{\mathsf {M}}_n$ for all $n\geq 1$ .

This provides a source of simple examples. Any frame forming a transitive chain, such as $(\omega ,<)$ , satisfies (7), but other frames do too. For example, the irreflexive transitive frame ${\cal G}_j$ shown in Figure 5 below satisfies (7) and validates $U_1^{\mathsf {M}}$ , but has an infinite R-antichain.

5.6 Comparing the $U_n^{\mathsf {M}}$ with each other

Let $K^{\mathsf {M}}$ denote the smallest normal modal ${\mathsf {M}}$ -logic. Plainly, (6) for n implies (6) for $n+1$ , and it follows that $KU_1^{\mathsf {M}}\supseteq KU_2^{\mathsf {M}}\supseteq \cdots \supseteq K^{\mathsf {M}}$ .

We show that the inclusions are strict. For any set X, let ${\cal F}_X$ be the ‘lawn rake-like’ frame with domain $\{a\}\cup X$ , for some point $a\notin X$ , and with

(8) $$ \begin{align} R_{\lozenge}^{{\cal F}_X}= R=\{(a,x),(x,x):x\in X\} \quad\mbox{for each }\lozenge\in{\mathsf{M}}. \end{align} $$

The achronal subsets of ${\cal F}_X$ are $\{a\}$ and the subsets of X. These all have size at most $|X|$ , if $X\neq \emptyset $ . So for $0<n<\omega $ , the frame ${\cal F}_{n+1}$ validates $U^{\mathsf {M}}_{n+1}$ . But ${\cal F}_{n+1}$ does not validate $U^{\mathsf {M}}_n$ , since $n+1$ is an achronal set with $>n$ elements contained in $R(a)$ . So the inclusion $KU_n^{\mathsf {M}}\supset KU_{n+1}^{\mathsf {M}}$ is strict. We will show more in Section 5.9.3.

Given any modal ${\mathsf {M}}$ -formula $\varphi \notin K^{\mathsf {M}}$ , filtrating the canonical model for $K^{\mathsf {M}}$ provides a finite Kripke model ${\cal M}$ satisfying $\neg \varphi $ . Let $|{\cal M}|=n$ , say. Then evidently, the frame of ${\cal M}$ validates $U_n^{\mathsf {M}}$ . Hence, $\varphi \notin KU_n^{\mathsf {M}}$ . We deduce that $\bigcap _{0<n<\omega }KU_n^{\mathsf {M}}=K^{\mathsf {M}}$ .

Of course there are many normal ${\mathsf {M}}$ -logics (containing $K^{\mathsf {M}}$ but) not containing any $KU_n^{\mathsf {M}}$ . For instance, the logic of the lawn-rake frame ${\cal F}_{\omega }$ does not contain any $KU^{\mathsf {M}}_n$ , since $\omega $ is an infinite achronal subset of ${\cal F}_{\omega }$ .

5.7 Comparing the $U_n^{\mathsf {M}}$ with other logics

Let us take a look at the monomodal case, where ${\mathsf {M}}=\{\lozenge \}$ . We will write $U^{\{\lozenge \}}_n$ as simply $U_n$ , and $R_{\lozenge }$ as just R. For suitable n, the logic $KU_n$ weakens some known logics.

1. 1. $KU_1\subset K5_2\subset K5$ , where $K5_2$ and $K5$ are as described in Section 4.

   As we said at the start of Section 5, the correspondent of $5_2$ (see (4) and (5)) says that all successors of a given world have the same R-future, and this implies (6) with $n=1$ . So every frame that validates $5_2$ also validates $U_1$ .

   Since $K5_2$ is Sahlqvist axiomatised, it is Kripke complete [2, theorem 4.42]. So for each modal formula $\varphi $ , if $\varphi \notin K5_2$ then $\neg \varphi $ is satisfied in some Kripke model whose frame validates $5_2$ . By the above, this frame also validates $U_1$ , and consequently $\varphi \notin KU_1$ . We deduce that $KU_1\subseteq K5_2$ as stated. The inclusion $K5_2\subseteq K5$ was indicated in Section 4.1.

   The frame $(\omega ,<)$ validates $U_1$ , as we saw in Section 5.5, but any two distinct points in it have different futures, so it does not validate $5_2$ . Hence, the inclusion $KU_1\subset K5_2$ is strict. We saw in Section 4.2 that the inclusion $K5_2\subset K5$ is (very) strict.

2. 2. $KU_n\subset K4I_n$ for every n, where the latter is as in [7] and is the smallest normal modal logic containing the Sahlqvist axioms

   (9) $$ \begin{align} \begin{array}{rcll} 4&=&\lozenge\lozenge p\to\lozenge p &\mbox{(transitivity),} \\ I_n&=&(\bigwedge_{i\leq n}\lozenge q_i)\to\bigvee_{i,j\leq n,\,i\neq j}\lozenge(q_i\wedge(q_j\vee\lozenge q_j)). \end{array} \end{align} $$

   The first-order correspondent of $I_n$ says that no $R(x)$ contains an R-antichain with $>n$ points. Given this and transitivity, if ${y_0,\ldots {},y_{n}}\in R(x)$ , there are $i\neq j$ with $y_i=y_j$ or $Ry_iy_j$ , and hence (by transitivity) with $R(y_j)\subseteq R(y_i)$ . So (6) holds for n, and hence, every frame validating $4I_n$ also validates $U_n$ . Again, $K4I_n$ is Sahlqvist and so Kripke complete, and it follows that $KU_n\subseteq K4I_n$ .

   

   Fig. 4 The logics $KU_n$ , $K4I_n$ , $K5_2$ , and $K5$ (monomodal case).

   The inclusion $KU_n\subset K4I_n$ is proper for each n, since frames such as $ (\omega ,\{(i,i+1):i<\omega \}) $ validate $U_n$ but not even $K4$ . We will see transitive examples in Section 5.9.1.

3. 3. The lawn-rake frame ${\cal F}_{n+1}$ from Section 5.6 validates $K4I_{n+1}$ , since it is transitive and its only subset $\{a\}\cup (n+1)$ with $>n+1$ points is not an R-antichain—see (8). But as we said, it does not validate $U_{n}$ . Hence, $KU_n\not \subseteq K4I_{n+1}$ .

4. 4. Rather trivially, $K4\not \subseteq K5$ , since the frame $(\{0,1,2\},\{(0,1)\}\cup \{1,2\}^2)$ validates $K5$ but is not transitive. Also, $K5_2\not \subseteq K4I_1$ , since $(\omega ,<)$ validates $K4I_1$ but (as we saw in item 1) not $5_2$ .

The situation is therefore as shown in Figure 4. No inclusions can be added that do not already follow from the ones shown by transitivity of inclusion.

1. 5. $U_n$ is somewhat related to Xu’s axiom $\mathsf {Wid}_n^*$ [24, p. 1178], whose correspondent says that for every x, every R-antichain with $>n$ points in $R(x)$ contains distinct points $y,y'$ with the same proper future—that is, $\forall z(R^{\bullet } yz \leftrightarrow R^{\bullet } y'z)$ , where $R^{\bullet } yz$ abbreviates $R yz\wedge \neg R zy$ . This clearly bears some similarity to (6), but the two are independent even with transitivity. The lawn-rake frame ${\cal F}_{\omega }$ from Section 5.6 is transitive and validates all $K4\mathsf {Wid}_n^*$ , but no $U_n$ . Now let $K4U_n$ be the smallest normal modal logic containing $U_n$ and the transitivity axiom 4. The transitive frame $(W,R)$ , where $W=\{a\}\cup (\omega \times 2)$ , $a\notin \omega \times 2$ , and $R=\{(a,(i,k)),((i,k),(j,1)):j\leq i<\omega ,\; k<2\}$ , validates $K4U_1$ (by virtue of (7)), and so all $K4U_n$ , but no $\mathsf {Wid}_n^*$ , since no two points in the R-antichain $\omega \times \{0\}$ have the same proper successors.

5.8 $S4U_n=S4I_n$

There is another connection between $U_n$ and $I_n$ . For a binary relation R on a set W, let be the relation on W defined by iff $R(y)\subseteq R(x)$ . It is an exercise to verify that (i) an R-achronal set (defined in the obvious way) is the same thing as an -antichain; (ii) is reflexive and transitive; (iii) iff R is reflexive; (iv) iff R is transitive. By (ii)–(iv), we get (v) .

However, (vi) is not monotonic with respect to inclusion, even on transitive relations. For suppose $|W|\geq 2$ and $R=\{(x,x):x\in W\}$ (identity). Then $\emptyset $ and R are transitive and $\emptyset \subseteq R$ . But R is also reflexive, so by (iii) and (iv), . So .

Fig. 5 Irreflexive transitive frame ${\cal G}_j$ for Sections 5.9.1 and 5.9.2.

Lastly, and getting to the point, (vii) if ${\cal F}=(W,R)$ is rooted ³ and transitive, and , then ${\cal F}$ validates $U_n$ iff validates $I_n$ , for each $0<n<\omega $ .

It follows from (iii), (iv), and (vii) that $S4U_n=S4I_n$ , where these are the smallest normal modal logics containing 4, the reflexivity axiom $ p\to \lozenge p$ , and $U_n$ (respectively,  $I_n$ ).

5.9 Continuum-many logics in intervals in Figure 4

Here we remain in the monomodal case: ${\mathsf {M}}=\{\lozenge \}$ . We still write $U^{\{\lozenge \}}_n$ as $U_n$ and $R_{\lozenge }$ as R.

We saw in Section 4.2 that there are continuum-many normal modal logics between $K5_2$ and $K5$ . We will now briefly indicate that the same holds for many of the other intervals in Figure 4.

5.9.1 Continuum-many logics between $K4U_n$ and $K4I_n$

Fix n with $0<n<\omega $ . Then there are continuum-many normal monomodal logics between $K4U_n$ and $K4I_n$ .

The proof is similar to the one in Section 4.2. For each $j<\omega $ we define the irreflexive transitive frame ${\cal G}_j=(j+1\cup \{a_l:l<\omega \},R_j)$ , where the $a_l$ are pairwise distinct and not in $j+1$ , and

$$\begin{align*}R_j = \{(k,m):k<m\leq j\} \cup \{(0,a_l),\,(a_l,m) \;:\; l<\omega,\;1\leq m\leq j\}. \end{align*}$$

See Figure 5.

From (7) in Section 5.5, we see that $U_1$ , and hence $U_n$ , are valid in each ${\cal G}_j$ . Let ${\cal I}_n$ be the class of frames that validate $K4I_n$ , and for each $J\subseteq \omega $ , let $L_J$ be the (normal monomodal) logic of the class ${\cal C}_J={\cal I}_n\cup \{{\cal G}_j:j\in J\}$ of frames. For each $i<\omega $ , let $\alpha _i=\lozenge ^i\top \wedge \neg \lozenge ^{i+1}\top $ as in Section 4.2, and

$$\begin{align*}\psi_i= I_n\vee\Box(\alpha_i\to p)\vee\Box(\alpha_i\to\neg p), \end{align*}$$

where $I_n$ is as in (9) and p is an atom not occurring in $I_n$ . It can be verified that:

1. 1. $K4U_n\subseteq L_J\subseteq K4I_n$ (because $K4U_n$ is valid in ${\cal C}_J$ , and ${\cal I}_n\subseteq {\cal C}_J$ ).

2. 2. $\psi _i$ is valid in ${\cal I}_n$ for each $i<\omega $ (because its disjunct $I_n$ is valid in ${\cal I}_n$ ).

3. 3. $I_n$ is not valid at 0 in any ${\cal G}_j$ (because of the infinite $R_j$ -antichain $\{a_l:l<\omega \}$ ).

4. 4. $\psi _i$ is valid in ${\cal G}_j$ iff $i\neq j$ , for each $i,j<\omega $ (proved as in Section 4.2, using point 3).

5. 5. Hence, $\psi _i\in L_J$ iff $i\notin J$ , for each $i<\omega $ and $J\subseteq \omega $ .

So if $I,J\subseteq \omega $ and $i\in I\setminus J$ , then $\psi _i\in L_J\setminus L_I$ . We conclude that the $L_J$ ( $J\subseteq \omega $ ) are pairwise distinct.

5.9.2 Continuum-many logics between $KU_1$ and $K5_2$

There are also continuum-many normal modal logics lying between $KU_1$ and $K5_2$ . Let ${\cal K}$ be the class of frames validating $K5_2$ , and for $J\subseteq \omega \setminus \{0\}$ , let $L_J$ be the logic of the class ${\cal K}\cup \{{\cal G}_j:j\in J\}$ , where the ${\cal G}_j$ are as in Figure 5 again. For $j\geq 1$ , the points $a_0,1\in R_j(0)$ have different futures, so ${\cal G}_j\not \models 5_2$ and ${\cal G}_j\notin {\cal K}$ . However, ${\cal G}_0\in {\cal K}$ , so we exclude $0$ from J.

Using $\xi _i=5_2\vee \Box (\alpha _i\to p)\vee \Box (\alpha _i\to \neg p)$ this time, it can be checked that $KU_1\subseteq L_J\subseteq K5_2$ and that the $L_J$ are pairwise distinct.

5.9.3 Continuum-many logics between $KU_{n+1}$ and $KU_n$

Finally, for each ${0<n<\omega }$ , there are continuum-many normal modal logics between $KU_{n+1}$ and $KU_n$ . For $J\subseteq \omega $ , let $L_J$ be the logic of ${\cal U}_n\cup \{{\cal E}_j^n:j\in J\}$ , where ${\cal U}_n$ is the class of frames validating $U_n$ , and ${\cal E}_j^n$ is the transitive frame shown in Figure 6. This frame validates $U_{n+1}$ . What may not be clear from the figure is that ${r_0,\ldots {},r_{n}}$ are reflexive, the only reflexive points in the frame. They therefore form an $(n+1)$ -point achronal set, and so ${\cal E}_j^n$ does not validate $U_n$ at $j+1$ .

Fig. 6 Transitive frame ${\cal E}_j^n$ for Section 5.9.3; the circled nodes are reflexive.

The proof of distinctness of the $L_J$ this time uses $\zeta _i=U_n\vee \Box (\alpha _i\to p)\vee \Box (\alpha _i\to \neg p)$ , noting that $\alpha _i$ is never true at ${r_0,\ldots {},r_{n}}$ since these points are reflexive. Again, $KU_{n+1}\subseteq L_J\subseteq KU_n$ , and the $L_J$ are pairwise distinct. We leave details to the reader.

6 Kripke incompleteness

Here we consider Kripke completeness (or as it turns out, the lack of it) of finite-achronal-width logics (i.e., normal extensions of some $KU_n^{\mathsf {M}}$ ). Our starting point is the result of Fine [7] that all finite-width logics (those extending some $K4I_n$ ) are Kripke complete. We might ask whether the same holds for finite-achronal-width logics.

First, Fine’s result does not extend to multimodal logics. For ${\mathsf {M}}=\{\lozenge ,\blacklozenge \}$ , the normal temporal logic given by Thomason [21] (see also [2, theorem 4.49], [4, exercise 6.23], and [10, pp. 55–56]), extended by $I_1$ for both diamonds, is not Kripke complete and indeed is not valid in any Kripke frame. Since this logic contains $U_1^{\mathsf {M}}$ , not all normal extensions of even the bimodal $K4U_1^{\{\lozenge ,\blacklozenge \}}$ are Kripke complete.

So we will restrict our attention to the monomodal case, where ${\mathsf {M}}=\{\lozenge \}$ . As usual, we write $U^{\{\lozenge \}}_n$ simply as $U_n$ . In this case, we can at least say that all normal extensions of each $S4U_n$ are Kripke complete, by the result of [7] and since $S4U_n=S4I_n\supseteq K4I_n$ (see Section 5.8).

This can fail for smaller logics. Van Benthem [1] showed that the smallest normal logic containing the axioms $T=p\to \lozenge p$ , $M=\Box \lozenge p\to \lozenge \Box p$ , $Q=\lozenge p\wedge \Box (p\to \Box p)\to p$ , and $U_1$ is Kripke incomplete. See also [2, exercise 4.4.4]. In fact, using work of Blok [3], it can be shown that $KTU_1$ has continuum-many Kripke-incomplete normal extensions.

6.1 Extensions of $K4U_2$

These latter extensions do not contain the transitivity axiom 4. What about extensions that do? As we will see, the general Kripke completeness of logics containing any $K4I_n$ does not extend to those containing any $K4U_n$ . We now show that there is a Kripke-incomplete normal extension of $K4U_2$ . The proof builds on Fine's construction in [6] of an incomplete logic containing S4, which we transfer to an extension of K4.

The means of doing this is a formula translation $\phi \mapsto \phi {{}^{\circ }}$ that is defined inductively by putting $\phi {{}^{\circ }}=\phi $ if $\phi $ is an atom or constant, letting the translation commute with the Boolean connectives, i.e., $(\neg \phi ){{}^{\circ }}= \neg (\phi {{}^{\circ }})$ etc., and putting $(\lozenge \phi ){{}^{\circ }}=\phi {{}^{\circ }}\lor \lozenge (\phi {{}^{\circ }})$ . Then $(\Box \phi ){{}^{\circ }}=\phi {{}^{\circ }}\land \Box (\phi {{}^{\circ }})$ . Introducing the abbreviations $\lozenge {{}^{\circ }}\phi $ for $\phi \lor \lozenge \phi $ , and $\Box {{}^{\circ }}\phi $ for $\phi \land \Box \phi $ , we have $(\lozenge \phi ){{}^{\circ }}=\lozenge {{}^{\circ }}(\phi {{}^{\circ }})$ and $(\Box \phi ){{}^{\circ }}=\Box {{}^{\circ }}(\phi {{}^{\circ }})$ .

For any frame ${\cal F}=(W,R)$ , let ${\cal F}{{}^{\circ }}=(W,R{{}^{\circ }})$ , where $R{{}^{\circ }}=R\cup \{(x,x):x\in W\}$ , the ‘reflexive closure’ of R. If ${\cal M}=({\cal F},V)$ is any model on ${\cal F}$ , let ${\cal M}{{}^{\circ }}=({\cal F}{{}^{\circ }},V)$ . The definition of $R{{}^{\circ }}$ ensures that

(10) $$ \begin{align} \begin{aligned} {\cal M},x\models \lozenge{{}^{\circ}}\phi &\text{\ iff } \exists y(xR{{}^{\circ}} y \text{ and } {\cal M},y\models\phi), \text{and} \\ {\cal M},x\models \Box{{}^{\circ}}\phi &\text{\ iff } \forall y(xR{{}^{\circ}} y \text{ implies } {\cal M},y\models\phi). \end{aligned} \end{align} $$

Lemma 6.1.

1. (1) For any formula $\phi $ and any $x $ in W, ${\cal M}{{}^{\circ }},x\models \phi $ iff ${\cal M},x\models \phi {{}^{\circ }}$ .

2. (2) ${\cal M}{{}^{\circ }}\models \phi $ iff ${\cal M}\models \phi {{}^{\circ }}$ .

3. (3) ${\cal F}{{}^{\circ }}\models \phi $ iff ${\cal F}\models \phi {{}^{\circ }}$ .

Proof.

1. (1) By induction on formation of formulas. The crucial case is that of a formula $\lozenge \phi $ under the hypothesis that the result holds for $\phi $ . Then ${\cal M}{{}^{\circ }},x\models \lozenge \phi $ iff there is some y with $xR{{}^{\circ }} y$ and ${\cal M}{{}^{\circ }},y\models \phi $ , which by the hypothesis holds iff there is some y with $xR{{}^{\circ }} y$ and ${\cal M},y\models \phi {{}^{\circ }}$ . The latter is equivalent by (10) to ${\cal M},x\models \lozenge {{}^{\circ }}(\phi {{}^{\circ }})$ , i.e., to ${\cal M},x\models (\lozenge \phi ){{}^{\circ }}$ .

2. (2) Follows from (1).

3. (3) Let ${\cal F}{{}^{\circ }}\models \phi $ . Then for any model ${\cal M}$ on ${\cal F}$ we have ${\cal M}{{}^{\circ }}\models \phi $ , hence ${\cal M}\models \phi {{}^{\circ }}$ by (2). This shows ${\cal F}\models \phi {{}^{\circ }}$ . Conversely, assume ${\cal F}\models \phi {{}^{\circ }}$ . Let ${\cal M}'=({\cal F}{{}^{\circ }},V)$ be any model on ${\cal F}{{}^{\circ }}$ . Put ${\cal M}=({\cal F},V)$ . Then ${\cal M}\models \phi {{}^{\circ }}$ , so ${\cal M}{{}^{\circ }} \models \phi $ by (2). But ${\cal M}{{}^{\circ }}={\cal M}'$ , so this shows that $\phi $ is verified by every model on ${\cal F}{{}^{\circ }}$ . $\Box $

Fine defines certain formulas $E,G,H$ and specifies L to be the smallest normal extension of S4 to contain G and H. He shows that

(11) $$ \begin{align} \text{any frame that validates } L \text{ also validates } \neg E, \end{align} $$

and then shows that $\neg E$ is not in L.

Lemma 6.2. Let $L'$ be any normal extension of $K4$ that contains $G{{}^{\circ }}$ and $H{{}^{\circ }}$ . Any frame that validates $L'$ also validates $\neg E{{}^{\circ }}$ .

Proof. Let ${\cal F}\models L'$ . We show that ${\cal F}{{}^{\circ }}\models L$ . First, ${\cal F}$ is transitive as it validates 4, so ${\cal F}{{}^{\circ }}$ is an S4-frame. Also ${\cal F} \models G{{}^{\circ }} \land H{{}^{\circ }}$ , hence ${\cal F}{{}^{\circ }} \models G\land H$ by Lemma 6.1(3). Thus the logic determined by ${\cal F}{{}^{\circ }}$ includes L, i.e., ${\cal F}{{}^{\circ }}\models L$ .

It follows by the result (11) that ${\cal F}{{}^{\circ }}\models \neg E$ . Hence by Lemma 6.1(3), ${\cal F}\models \neg E{{}^{\circ }}$ .

Fine's proof in [6] that $\neg E$ is not in L involves constructing a model that falsifies $\neg E$ but verifies all substitution instances of the axioms of L, hence verifies L. The frame of this model can be depicted as in Figure 7 (cf. [4, figure 6.5]).

Fig. 7 An irreflexive transitive frame validating $U_2$ but not $U_1$ .

The labelling gives a four-colouring, partitioning the nodes into a-points, b-points, etc. The frame relation is depicted by the arrows. Note that the a-points form an infinite antichain, and the d-points form an infinite ascending R-chain, the only one in the frame other than subsequences of the d-points. The frame is point-generated by $d_0$ .

[6] took the relation to be the reflexive transitive relation generated by the displayed arrows. It is a partial ordering. Here we do not need the relation to be reflexive. For the rest of this section, let ${\cal F}=(W,R)$ be the irreflexive transitive version of this frame. Then Fine’s frame is ${\cal F}{{}^{\circ }}$ . The relation R, which is asymmetric, can be specified by listing all the future sets:

$$ \begin{align*} &R(b_0)=R(c_0)=\emptyset, \\ &R(b_1)=\{b_0\},\enspace R(c_1)=\{c_0\}, \\ &R(b_{m+2})=\{b_0,\dots, b_{m+1}, c_0,\dots,c_m\}, \\ &R(c_{m+2})=\{b_0,\dots, b_{m}, c_0,\dots,c_{m+1}\}, \\ &R(a_{m})=\{b_0,\dots, b_{m+1}, c_0,\dots,c_{m+1}\}, \\ &R(d_{m})=\{d_n:m<n\}\cup\bigcup\{R{{}^{\circ}}(a_n):m\leq n\}. \end{align*} $$

${\cal F}$ fails to validate $U_1$ in infinitely many ways. For instance, it contains the pair $(b_1,c_1)$ which is achronal as their futures $\{b_0\}$ and $\{c_0\}$ are $\subseteq $ -incomparable. Similarly, every pair $(b_{m+1},c_{m+1})$ is achronal.

On the other hand ${\cal F}$ validates $U_2$ , since it has no triple of points that is achronal. To see why, note that the sequence $(R(b_m):m<\omega )$ of future sets of b-points increases monotonically under $\subseteq $ as m increases, so any two such sets are comparable. Likewise the $R(c_m)$ ’s are increasing, and so are the $R(a_m)$ ’s, while the $R(d_m)$ ’s are decreasing. So any two points of the same colour have comparable futures, hence cannot both belong to an achronal triple.

Also, a d-point cannot belong to any achronal triple, as the future of any a, b, or c point consists entirely of b and c points, while the future of any d point includes all of the b and c points. Hence the future of any d point is comparable to that of any other point.

That leaves the only possibility for an achronal triple being that it consists of one point of each of the colours $a,b,c$ . However $R(a_m)\supseteq R(b_{m+2})\supseteq R(b_{m+1})\supseteq \cdots \supseteq R(b_{0})$ , while $R(a_m)\subseteq R(b_{m+k})$ for all $k\geq 3$ . Hence the future of any a point is comparable to that of any b point (and similarly of any c point). So this possibility is ruled out, and no achronal triple exists.

In [6], a model $({\cal F}{{}^{\circ }},V)$ is defined that satisfies E at $d_0$ . Let ${\cal M}=({\cal F},V)$ be the model on ${\cal F}$ with the same valuation, so that $({\cal F}{{}^{\circ }},V)$ is ${\cal M}{{}^{\circ }}$ , and ${\cal M}{{}^{\circ }}\not \models \neg E$ . To prove that ${\cal M}{{}^{\circ }}$ verifies L it was shown that ${\cal F}{{}^{\circ }}\models G$ , and that ${\cal M}{{}^{\circ }}$ strongly verifies H, i.e., it verifies every substitution instance of H. Thus all axioms of L are strongly verified by ${\cal M}{{}^{\circ }}$ . But the rules of inference preserve strong verification, so ${\cal M}{{}^{\circ }}$ (strongly) verifies L.

By Lemma 6.1, from ${\cal M}{{}^{\circ }}\not \models \neg E$ we get ${\cal M}\not \models \neg E{{}^{\circ }}$ , and from ${\cal F}{{}^{\circ }}\models G$ we get ${\cal F}\models G{{}^{\circ }}$ . We also have ${\cal F}\models U_2$ . If we can show that  ${\cal M}$ strongly verifies $H{{}^{\circ }}$ , then putting $L' = K4U_2G{{}^{\circ }} H{{}^{\circ }}$ we get ${\cal M}\models L'$ , so $\neg E{{}^{\circ }}\notin L'$ . Hence by Lemma 6.2, $L'$ is a Kripke incomplete extension of $K4U_2$ .

So far we have not needed to know what $E,G,H$ are, given the results about them in [6]. But Lemma 6.1 does not appear to give access to a proof that ${\cal M}$ strongly verifies $H{{}^{\circ }}$ , since a substitution instance of $H{{}^{\circ }}$ need not be of the form $\phi {{}^{\circ }}$ where $\phi $ is a substitution instance of H. So we must revisit the proof in [6] that ${\cal M}{{}^{\circ }}$ strongly verifies H and adapt it to show that ${\cal M}$ strongly verifies $H{{}^{\circ }}$ . The formula H is

$$ \begin{align*}\neg(s\land\Box(s\to\lozenge(\neg s\land t\land\lozenge(\neg s\land\neg t\land\lozenge s)))), \end{align*} $$

where s and t are atoms, so $H{{}^{\circ }}$ is

$$ \begin{align*}\neg(s\land\Box{{}^{\circ}}(s\to\lozenge{{}^{\circ}}(\neg s\land t\land\lozenge{{}^{\circ}}(\neg s\land\neg t\land\lozenge{{}^{\circ}} s)))). \end{align*} $$

To show that this is strongly verified by our model ${\cal M}$ , suppose otherwise for the sake of contradiction. Then there are formulas $\phi $ and $\psi $ and some $w\in W$ with

$$ \begin{align*}{\cal M},w \models \phi\land\Box{{}^{\circ}}(\phi\to\lozenge{{}^{\circ}}(\neg \phi\land \psi\land\lozenge{{}^{\circ}}(\neg \phi\land\neg \psi\land\lozenge{{}^{\circ}} \phi))). \end{align*} $$

Hence in ${\cal M}$ there are points $x,y,z$ with $wR{{}^{\circ }} xR{{}^{\circ }} yR{{}^{\circ }} z$ , such that $w\models \phi $ , $x\models \neg \phi \land \psi $ , $y\models \neg \phi \land \neg \psi $ and $z\models \phi $ . Then $w\ne x\ne y\ne z$ , so $wRxRyR z$ . Since $z\models \phi $ , we can use $H{{}^{\circ }}$ again to repeat the argument to obtain further points $zRx'Ry'Rz'\models \phi $ and so on ad infinitum, generating an infinite ascending R-chain from w. This means we must have $w=d_m$ for some m, with the chain consisting of d-points, and the formulas $\phi $ , $\neg \phi \land \psi $ , $\neg \phi \land \neg \psi $ being true cofinally along the chain.

The rest of the argument to a contradiction is as in [6]. We repeat the details. Let $\Box \chi _1,\dots , \Box \chi _k$ be all the formulas from which $\phi $ and $\psi $ can be constructed by Boolean connectives. Since the $R(d_i)$ ’s are decreasing, if $d_i\models \Box \chi _l$ , then $d_j\models \Box \chi _l$ for all $j>i$ . Hence there exists some $n\geq m$ such that the truth values of $\Box \chi _1,\dots ,\Box \chi _k$ are fixed from $d_n$ on, i.e., $d_i\models \Box \chi _l$ iff $d_n\models \Box \chi _l$ , for all $i\geq n$ and $l\leq k$ .

We have not yet had to say anything about the valuation V. In fact there are two atoms $p_0$ and $p_1$ with $V(p_0)=\{d_{i}:i\ \text {is even}\}$ and $V(p_1)=\{d_{i}:i \ \text {is odd}\}$ , while no other atoms are true at any d-point. So if $i,j\geq n$ have the same parity (even/odd), then $d_i$ and $d_j$ agree on the truth values of all atoms and the formulas $\Box \chi _1,\dots \Box \chi _k$ , so they agree on $\phi $ and $\psi $ and all their Boolean combinations.

But there exist three d-points beyond $d_n$ at which the formulas $\phi $ , $\neg \phi \land \psi $ , and $\neg \phi \land \neg \psi $ successively are true. Then at least two of these points must have the same parity of index, hence must agree on the truth-values of the formulas, which is impossible. That is the contradiction confirming that ${\cal M}$ strongly verifies $H{{}^{\circ }}$ , finishing the proof that $K4U_2G{{}^{\circ }} H{{}^{\circ }}$ is Kripke incomplete.

The following is not settled by this argument:

Problem 6.3. Are all normal monomodal logics extending $K4U_1$ Kripke complete?

Conclusion

On the one hand then, compared with Fine’s $K4I_n$ , the logics $KU_n$ are rather weak (or small). They do not contain the transitivity axiom 4, there are continuum-many normal modal logics between $K4U_n$ and $K4I_n$ , and some normal extensions of $KTU_1 $ and of $K4U_2$ are Kripke incomplete. This is good news inasmuch as it indicates that Theorem 7.7 covers a wide range of logics. On the other hand, the frame conditions imposed by the $U_n$ are substantial, as it is easy to find frames such as the lawn-rake frame ${\cal F}_{\omega }$ that do not validate any $KU_n$ .

7 Canonicity for logics above $KU_n^{\mathsf {M}}$

We are going to prove (in Theorem 7.7) that all $\omega $ -canonical normal modal ${\mathsf {M}}$ -logics of finite achronal width (see Definition 5.3) are totally canonical. By the inclusions shown in Figure 4, this holds for normal extensions of $K5_2$ , $K5$ , and $K4I_n$ as well. In terms of varieties, we will prove that every variety that validates some $U_n$ is resolved. The proof extends the one in Section 4.1.

7.1 Infinite achronal sets in subsets of frames

We start by extending Lemma 4.1 to this setting. For any n, validity of the axioms $U_n^{\mathsf {M}}$ in a frame ${\cal F}$ guarantees that no set $R^{\cal F}_{\lozenge }(x)$ (for $x\in {\cal F}$ and $\lozenge \in {\mathsf {M}}$ ) has an infinite achronal subset. But does this extend to sets of the form $R_s(x)=\{y\in {\cal F}:{\cal F}\models R_sxy\}$ for arbitrary $s\in {}^{<\omega }{\mathsf {M}}$ ? (See Definition 2.4 for $R_s$ .)

Example 7.1. There do exist frames ${\cal F}$ (monomodal ones, with ${\mathsf {M}}=\{\lozenge \}$ ) in which no $R^{\cal F}_{\lozenge }(x)$ (for any $x\in {\cal F}$ ) has an infinite achronal subset but $R_s(x)=\{y\in {\cal F}:{\cal F}\models R_sxy\}$ does, for some $x\in {\cal F}$ , where $s=(\emptyset \hat \ \lozenge )\hat \ \lozenge $ is the sequence of two $\lozenge $ s.

Let ${\cal F}=(\{a\}\cup (\omega \times 2),R)$ , where $a\notin \omega \times 2$ and $R=\{(a,(i,0)),((i,0),(j,1)), ((i,1),(i,1)):j\leq i<\omega \}$ . Then $R(a)=\omega \times \{0\}$ , which does not contain even a two-element achronal set, since $\{R((i,0)):i<\omega \}$ forms a chain under inclusion. And $R(x)$ is finite for all $x\in {\cal F}\setminus \{a\}$ , so certainly has no infinite achronal subsets. But $R_s(a)=\omega \times \{1\}$ is infinite and achronal, since if $i<j<\omega $ then $R((i,1))=\{(i,1)\}$ and $R((j,1))=\{(j,1)\}$ are $\subseteq $ -incomparable.

Inspired by Lemma 4.1, we show in the next lemma that this cannot happen for frames validating some $U_n^{\mathsf {M}}$ . It will be used in Proposition 7.5. A more effective version could be proved using Ramsey numbers.

Lemma 7.2. Let $0<n<\omega $ and let ${\cal F}$ be a frame validating $U^{\mathsf {M}}_n$ . Let $s\in {}^{<\omega }{\mathsf {M}}$ and $x\in {\cal F}$ , and write $R_s(x)$ for the set $\{y\in {\cal F}:{\cal F}\models R_sxy\}$ . Then every achronal subset of $R_s(x)$ is finite.

Proof. In the proof, we write $R^{\cal F}_{\lozenge }(y)$ as just $R_{\lozenge }(y)$ , for $y\in {\cal F}$ and $\lozenge \in {\mathsf {M}}$ . The proof is by induction on the finite ordinal ${ \mathrm{dom}}(s)$ . For $s=\emptyset $ , the lemma holds trivially, since $R_{\emptyset }(x)=\{x\}$ is itself finite. Assume inductively that the lemma holds for $s\in {}^{<\omega }{\mathsf {M}}$ (for all $x\in {\cal F}$ ), and let $\lozenge \in {\mathsf {M}}$ be given. We prove that every achronal subset of $R_{s\hat \ \lozenge }(x)$ is finite.

By Lemma 5.2, it is enough to show the following. Let $y_0,y_1,\ldots \in R_{s\hat \ \lozenge }(x)$ , and let $\blacklozenge \in {\mathsf {M}}$ be given. Then $R_{\blacklozenge }(y_i)\subseteq R_{\blacklozenge }(y_j)$ for some distinct $i,j<\omega $ .

Choose $z_0,z_1,\ldots \in R_{s}(x)$ such that $y_i\in R_{\lozenge }(z_i)$ for each $i<\omega $ . By Ramsey’s theorem [16], there is infinite $K=\{k_0,k_1,\ldots \}\subseteq \omega $ , where $k_0<k_1<\cdots $ , such that:

1. 1. $R_{\lozenge }(z_k)\subseteq R_{\lozenge }(z_l)$ for each $k<l$ in K, or

2. 2. $R_{\lozenge }(z_k)\supset R_{\lozenge }(z_l)$ for each $k<l$ in K, or

3. 3. $R_{\lozenge }(z_k)\not \subseteq R_{\lozenge }(z_l)\not \subseteq R_{\lozenge }(z_k)$ for each $k<l$ in K.

The last option is impossible, since if it held, $(z_{k_i}:i<\omega )$ would be an infinite achronal sequence in $R_s(x)$ , which by Lemma 5.2 would contradict the inductive hypothesis for s. If option 1 holds, then $y_{k_0},\ldots ,y_{k_n}\in R_{\lozenge }(z_{k_n})$ . If option 2 holds, then $y_{k_0},\ldots ,y_{k_n}\in R_{\lozenge }(z_{k_0})$ . Either way, $y_{k_0},\ldots ,y_{k_n}\in R_{\lozenge }(t)$ for some $t\in {\cal F}$ . Since $U_n^{\mathsf {M}}$ is valid in ${\cal F}$ at t, by (6) in Section 5.3 there must be distinct $i,j\leq n$ with $R_{\blacklozenge }(y_{k_i})\subseteq R_{\blacklozenge }(y_{k_j})$ , as required. This completes the induction and proves the lemma.

7.2 Underlying

We now return to the variety V of Section 3.1. From now on, we assume that the logic of V is of finite achronal width—that is, above some $KU_n^{\mathsf {M}}$ . Explicitly, for some integer $n\geq 1$ , the translations $\tau _{\varphi }$ (given in Section 2.6) of the axioms $\varphi \in U_n^{\mathsf {M}}$ to ${\mathsf {M}}$ -BAO terms have value 1 in every algebra in V under all assignments to their variables. In terms of Section 2.6, we could just say that V validates some $KU^{\mathsf {M}}_n$ .

We will show in Theorem 7.7 that V is resolved. We make free use of material in Sections 2 and 3.

Definition 7.3. For $\lozenge \in {\mathsf {M}}$ , we let stand for the ${\cal L}$ -formula $\forall z(R_{\lozenge } yz\to R_{\lozenge } xz)$ .

This recalls in Section 5.8. For $t,u\in {\cal B}_+$ , we have iff $R_{\lozenge }^{{\cal B}_+}(u)\subseteq R_{\lozenge }^{{\cal B}_+}(t)$ : the $\lozenge $ -future of u in the frame ${\cal B}_+$ is contained in that of t. Then a subset of ${\cal B}_+$ is $\lozenge $ -achronal iff it is an antichain with respect to .

Definition 7.4.

1. 1. Let $S,T\subseteq {\cal B}_+$ . We say that $T$ underlies $S$ if for each $s\in S$ and $\lozenge \in {\mathsf {M}}$ , there is $t\in T$ with . This is a kind of density or cofinality property.

2. 2. As is standard, a subset $D\subseteq {\mathfrak B}$ is said to be ${\cal L}({\mathfrak A})$ -definable if $D=\{d\in {\mathfrak B}:{\mathfrak B}\models \gamma (d)\}$ for some ${\cal L}({\mathfrak A})$ -formula $\gamma (x)$ .

The following is the key technical proposition in the proof. It will be used in Lemma 7.6. The embedding $f:{\cal A}_+\to {\cal B}_+$ is as in Definition 3.9.

Proposition 7.5. Let ${\cal F}$ be an inner subframe of ${\cal A}_+$ generated by an element of ${\widehat W}$ , and let D be an ${\cal L}({\mathfrak A})$ -definable subset of ${\cal B}_+$ . Then $W\cap D$ underlies $f({\cal F})\cap D$ .

Proof. Choose $w_0\in W$ such that ${\cal F}={\cal A}_+(\widehat {w_0})$ . Let $D=\{d\in {\cal B}_+:{\mathfrak B}\models \gamma (d)\}\subseteq {\cal B}_+$ , where $\gamma (x)$ is some arbitrary ${\cal L}({\mathfrak A})$ -formula with x of point sort. Let $\mu \in {\cal F}$ with $f(\mu )\in D$ , and let $\lozenge \in {\mathsf {M}}$ . We show that there is $w\in W\cap D$ with .

Clearly, if $f(\mu )\in W$ then we can take $w=f(\mu )$ . So we can suppose that

(12) $$ \begin{align} f(\mu)\in D\setminus W. \end{align} $$

There is no loss of generality if we replace D by a ‘nicer’ ${\cal L}({\mathfrak A})$ -definable subset E of D still containing $f(\mu )$ . We will take advantage of this. First, by definition of ${\cal F}$ (Definition 2.4), we can choose $s\in {}^{<\omega }{\mathsf {M}}$ with

(13) $$ \begin{align} {\cal A}_+\models R_s (\widehat{w_0},\mu). \end{align} $$

Moving from ${\cal A}_+$ to ${\mathfrak B}$ , let

(14) $$ \begin{align} D'=\{d\in D: {\mathfrak B}\models R_s {w_0}d\}. \end{align} $$

Now let $K\subseteq W\cap D'$ be maximal such that $K\cup \{f(\mu )\}$ is $\lozenge $ -achronal in the frame ${\cal B}_+$ . Such a K exists by Zorn’s lemma; it may be empty. Since ${\cal B}\in V$ and the axioms in $U^{\mathsf {M}}_n$ are Sahlqvist, it follows that ${\cal B}_+$ validates $U^{\mathsf {M}}_n$ , so by (14) and Lemma 7.2, there are no infinite achronal subsets of $D'$ . Hence, K is finite. So if we let

(15) $$ \begin{align} E=\{x\in D'\setminus K: K\cup\{x\} \mbox{ is } \lozenge\mbox{-achronal in } \ {{\cal B}}_+ \}, \end{align} $$

then E is ${\cal L}({\mathfrak A})$ -definable, by the ${\cal L}({\mathfrak A})$ -formula

(We do not need to add a disjunct $x=\underline {k}$ at the end here.)

By (15) and (14), $E\subseteq D'\subseteq D$ . Also, ${\mathfrak B}\models R_s(w_0,f(\mu ))$ by (13) and Corollary 3.10; so by (12) and (14), $f(\mu )\in D'$ . By (12) again, $f(\mu )\notin W\supseteq K$ . So by (15) and the definition of K,

(16) $$ \begin{align} f(\mu)\in E. \end{align} $$

We now proceed to find $w\in W\cap E$ with —that is, $R^{\mathfrak B}_{\lozenge }(w)\subseteq R^{\mathfrak B}_{\lozenge }(f(\mu ))$ . Assume for contradiction that $(\dagger )$ there is no such $w$ .

Claim 1. for every $w\in W\cap E$ .

Proof of claim

Let $w\in W\cap E$ . Then $w\notin K$ by (15), so $K\subset K\cup \{w\}\subseteq W\cap D'$ . The maximality of K now implies that $K\cup \{w,f(\mu )\}$ is not $\lozenge $ -achronal in ${\cal B}_+$ . That is, it is not an -antichain in ${\mathfrak B}$ . Since $K\cup \{w\}$ and $K\cup \{f(\mu )\}$ are clearly $\lozenge $ -achronal, so are such antichains, we must have or . Our assumption $(\dagger )$ rules out the second of these, so indeed, . Since $w$ was arbitrary, this proves the claim.

We now extend this to the whole of E.

Claim 2. for every $e\in E$ .

Proof of claim

First, it is an exercise in canonical frames to show that for every $t,u\in {\cal B}_+$ ,

(17)

Now fix any $w\in W\cap E$ . Claim 1 says that . So by (17), we have ${\mathfrak B}\models \forall x(\lozenge x\,{\mathrel {\underline {\in }}}\, f(\mu )\to \lozenge x\,{\mathrel {\underline {\in }}}\, w)$ . By definition of f (see (1) in Section 3.8), this says that

$$ \begin{align*} {\mathfrak B}'\models\forall x(\underline{\mu}(\lozenge x)\to \lozenge x\mathrel{\underline{\in}}\underline{w}). \end{align*} $$

This is a universally-quantified simple formula, so by Corollary 3.4, ${\mathfrak A}'\models \forall x(\underline {\mu }(\lozenge x)\to \lozenge x\,{\mathrel {\underline {\in }}}\,\underline {w})$ as well. Now this holds for all $w\in W\cap E={\mathfrak A}\cap E$ . And since ${\mathfrak A}\preceq {\mathfrak B}$ , for $w\in W$ we have $w\in E$ iff ${\mathfrak B}\models \varepsilon (w)$ , iff ${\mathfrak A}\models \varepsilon (w)$ . So all in all,

$$ \begin{align*} {\mathfrak A}'\models\forall xy(\underbrace{\varepsilon(y)\wedge\underline{\mu}(\lozenge x)\to \lozenge x\mathrel{\underline{\in}} y}_{\theta}). \end{align*} $$

Here, $\theta $ is a simple ${\cal L}'$ -formula. So by Corollary 3.4 again, ${\mathfrak B}'\models \forall xy(\varepsilon (y)\wedge \underline {\mu }(\lozenge x)\to \lozenge x\,{\mathrel {\underline {\in }}}\, y)$ —this is a key step in the proof. By (1) again, ${\mathfrak B}\models \forall xy(\varepsilon (y)\wedge \lozenge x\,{\mathrel {\underline {\in }}}\, f(\mu )\to \lozenge x\,{\mathrel {\underline {\in }}}\, y)$ , so by (17),

(18)

Finally, take any $e\in E$ . Then ${\mathfrak B}\models \varepsilon (e)$ , so (18) yields , proving the claim.

We said in (16) that $f(\mu )\in E$ , and combined with Claim 2 or (18), this gives

(19)

Thus, $f(\mu )$ witnesses . By the Tarski–Vaught criterion (Section 3.4), there is $w\in W$ with

(20)

Now, taking $y=f(\mu )$ in (20), and recalling from (19) that ${\mathfrak B}\models \varepsilon (f(\mu ))$ , we get . Since (20) implies $w\in W\cap E$ , this contradicts our assumption $(\dagger )$ that there is no such $w$ , and proves the proposition.

7.3 Canonicity

We now prove that the Truth Lemma of Definition 3.12 holds in V. Define g, ${\cal F}$ , ${\cal M}$ as in Section 3.9. Recall the standard translation $\psi ^x$ from Section 3.9. Recalling (2) from that section, for each ${\mathsf {M}}$ -formula $\psi $ and $t\in {\cal B}_+$ we have

(21) $$ \begin{align} ({\cal B}_+,g),t\models\psi \iff {\mathfrak B}\models\psi^x(t). \end{align} $$

Lemma 7.6. (Truth Lemma)

For each $m\in {\cal M}$ and modal ${\mathsf {M}}$ -formula $\psi $ , we have ${\cal M},m\models \psi $ iff $({\cal B}_+,g),m\models \psi $ .

Proof. By induction on $\psi $ . The main case is of course $\lozenge \psi $ (where $\lozenge \in {\mathsf {M}}$ ). Assume the lemma inductively for $\psi $ . It is easy to check (as in the proof of Proposition 4.2) that if ${\cal M},m\models \lozenge \psi $ then $({\cal B}_+,g),m\models \lozenge \psi $ as well. Conversely, suppose that $({\cal B}_+,g),m\models \lozenge \psi $ . We will show that ${\cal M},m\models \lozenge \psi $ .

Let $D\subseteq {\cal B}_+$ be the set defined in ${\mathfrak B} $ by $(\lozenge \psi )^x$ . By (21), $m\in {\cal M}\cap D$ . By Proposition 7.5, $W\cap D$ underlies ${\cal M}\cap D$ , so there is $w\in W\cap D$ with —that is,

(22) $$ \begin{align} R_{\lozenge}^{\mathfrak B}(w)\subseteq R_{\lozenge}^{\mathfrak B}(m). \end{align} $$

Since $w\in D$ , we have ${\mathfrak B}\models (\lozenge \psi )^x(w)$ , which is to say that ${\mathfrak B}\models \exists y(R_{\lozenge }\underline wy\wedge \psi ^y)$ . So by the Tarski–Vaught criterion, there is $w'\in W$ with

(23) $$ \begin{align} {\mathfrak B} \models R_{\lozenge} ww'\wedge\psi^y(w'). \end{align} $$

So by (21),

(24) $$ \begin{align} ({\cal B}_+,g),w'\models\psi. \end{align} $$

By (23) and (22), $w'\in R_{\lozenge }^{\mathfrak B}(w)\subseteq R_{\lozenge }^{\mathfrak B}(m)$ , so

(25) $$ \begin{align} {\mathfrak B}\models R_{\lozenge} mw'. \end{align} $$

It follows that $w'\in {\cal M}$ . To see this, choose $\mu \in {\cal F}$ with $m=f(\mu )\strut $ . By Corollary 3.10, $f:{\cal A}_+\to {\cal B}_+$ is a frame embedding and $w'=f(\widehat {w'})$ . So by (25), ${\cal A}_+\models R_{\lozenge } \mu \widehat {w'}\strut $ . By definition, ${\cal F}$ is $R^{{\cal A}_+}_{\lozenge }$ -closed in ${\cal A}_+$ , and since $\mu \in {\cal F}$ , we get $\widehat {w'}\in {\cal F}$ and so $w'\in {\cal M}$ .

This means that we can apply the inductive hypothesis to (24), giving ${\cal M},w'\models \psi $ . Also, ${\cal M}$ is a submodel of $({\cal B}_+,g)$ , so (25) gives ${\cal M}\models R_{\lozenge } mw'$ . We conclude that ${\cal M},m\models \lozenge \psi $ , completing the induction.

Theorem 7.7. Assume that the logic of V is of finite achronal width—above $KU_n^{\mathsf {M}}$ , for some $0<n<\omega $ . Then V is resolved.

Proof. Immediate from Lemma 7.6 and Theorem 3.13.

7.4 Final remarks

Theorem 7.7 expresses a dichotomy: every variety of ${\mathsf {M}}$ -BAOs (or normal modal logic) of finite achronal width is either totally canonical or not even $\omega $ -canonical. It would be rather unsatisfactory if all examples fell on the same side of the line. But while $KU^{\mathsf {M}}_1,KU^{\mathsf {M}}_2,\ldots $ themselves are canonical, not all monomodal logics extending even $K4I_1$ are canonical. An example is S4.3Grz, the smallest monomodal logic containing $p\to \lozenge p$ , the axioms 4 and $I_1$ from (9), and $\mathrm {Grz}=\Box (\Box (p\to \Box p)\to p)\to p$ —see [7, p. 38].

Temporal logics and other logics with ‘converse diamonds’ are covered by Theorem 7.7. To get that $\lozenge ,\blacklozenge \in {\mathsf {M}}$ are mutually converse in all canonical frames of algebras in V, we simply require that V validate the Sahlqvist axioms $p\to \blacksquare \lozenge p$ and $p\to \Box \blacklozenge p$ , regarded as ${\mathsf {M}}$ -equations as usual. For ${\mathsf {M}}=\{\lozenge ,\blacklozenge \}$ , any normal modal ${\mathsf {M}}$ -logic containing these axioms, axiom 4 for $\lozenge $ from (9), and linearity axioms $I_1$ for $\lozenge ,\blacklozenge $ , also contains $U_1^{\mathsf {M}}$ and is a linear temporal logic covered by Theorem 7.7.

From Section 3.3 onwards, we took ${\mathsf {M}}$ to be countable. This assumption was made only for presentational simplicity. It had little to no effect on Sections 4–6, where ${\mathsf {M}}$ was usually a singleton $\{\lozenge \}$ anyway. But we could allow ${\mathsf {M}}$ to have uncountable cardinality $\kappa $ throughout the paper. The only change required to the proofs is that the elementary substructure ${\mathfrak A}\preceq {\mathfrak B}$ in Section 3.4 be taken of cardinality $\leq \kappa $ , rather than countable. The meaning of Theorem 7.7 becomes: if the logic of V is of finite achronal width and V is $\kappa $ -canonical then it is totally canonical. However, the theorem is formulated using resolvedness and is true as stated for all ${\mathsf {M}}$ of any cardinality.

8 Conclusion

We have shown that every variety of ${\mathsf {M}}$ -BAOs validating $K5_2$ , or $KU_n$ for some finite $n\geq 1$ , is resolved. Though we have made some progress on special cases, Fine’s problem from [8] in its full generality remains open and we still do not know whether every variety of ${\mathsf {M}}$ -BAOs is resolved. We also have no answer to Problems 3.11 and 6.3, as well as the following:

Problem 8.1. For finite $n\geq 1$ , are all normal monomodal extensions of the logic $K4\mathsf {Wid}_n^*$ defined by Xu in [24] resolved? (We discussed this logic in Section 5.7(5).)

Problem 8.2. Is every canonical normal multimodal logic of finite achronal width the logic of an elementary class of frames?

We have taken each $\lozenge \in {\mathsf {M}}$ to be a unary modal operator. It may be worth investigating whether the methods of this paper extend to polyadic modal signatures.