On the Blok-Esakia Theorem

Abstract

We discuss the celebrated Blok-Esakia theorem on the isomorphism between the lattices of extensions of intuitionistic propositional logic and the Grzegorczyk modal system. In particular, we present the original algebraic proof of this theorem found by Blok, and give a brief survey of generalisations of the Blok-Esakia theorem to extensions of intuitionistic logic with modal operators and coimplication.

In memory of Leo Esakia

5.1 Introduction

The Blok-Esakia theorem, which was proved independently by the Dutch logician Wim Blok [6] and the Georgian logician Leo Esakia [13] in 1976, is a jewel of non-classical mathematical logic. It can be regarded as a culmination of a long sequence of results, which started in the 1920–1930s with attempts to understand the logical aspects of Brouwer’s intuitionism by means of classical modal logic and involved such big names in mathematics and logic as K. Gödel, A.N. Kolmogorov, P.S. Novikov and A. Tarski. Arguably, it was this direction of research that attracted mathematical logicians to modal logic rather than the philosophical analysis of modalities by Lewis and Langford [43]. Moreover, it contributed to establishing close connections between logic, algebra and topology. (It may be of interest to note that Blok and Esakia were rather an algebraist and, respectively, a topologist who applied their results in logic.)

Blok’s and Esakia’s aims were to understand and describe the structure of the extremely complex lattices of modal and superintuitionistic (aka intermediate) logics—or, in algebraic terms, the lattices of varieties of topological Boolean and Heyting algebras.¹ Their theorem provided means for a comparative study of these lattices and gave a ‘superintuitionistic classification’ of the lattice of modal logics containing S4. Esakia [16] believed that one could give a complete description of the structure of all modal companions of an arbitrary superintuitionistic logic. In particular, he aimed to describe the structure of all modal companions of intuitionistic propositional logic Int, discovered that the McKinsey system S4.1 was one of them and that the Grzegorczyk [33] system Grz was the largest one. It is to be noted that the first to observe and investigate the close relationship between the lattices of extensions of Int and S4 were Dummett and Lemmon [11], who—in 1959—used the relational representations of topological Boolean and Heyting algebras that are known to us as Kripke frames. Maksimova and Rybakov [47] in 1974 laid a solid algebraic foundation to the area.

This chapter is a brief overview of results related to the Blok-Esakia theorem, which supplements the earlier survey [10]. In Sect. 5.2, we discuss the role and place of the Blok-Esakia theorem in the theory of modal and superintuitionistic logics. In Sect. 5.3, we give Blok’s original algebraic proof of this theorem, which has never been properly published. Section 5.4 surveys generalisations of the Blok-Esakia theorem to intuitionistic modal logics, and, in Sect. 5.5, we discuss its extension to intuitionistic logic with coimplication.

5.2 Modal Companions of Superintuitionistic Logics

According to the (informal) Brouwer-Heyting-Kolmogorov semantics of intuitionistic logic, a statement is true if it has a proof. Orlov [57] and Gödel [25] formalised this semantics by means of a modal logic where the formula $\Box \varphi$ stands for ‘$\varphi$ is provable.’ (Novikov [55] read $\Box \varphi$ as ‘$\varphi$ is establishable.’) Their modal logic contained classical propositional logic,² $\mathbf{Cl }$, three properly modal axioms

$$\begin{aligned} \Box (p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q), \qquad \Box p \rightarrow p, \qquad \Box p \rightarrow \Box \Box p, \end{aligned}$$

and the inference rules $\varphi /\Box \varphi$ (if we have derived $\varphi$, then $\varphi$ is provable), modus ponens and substitution. Gödel [25] observed that the resulting logic is equivalent to one of the systems in the Lewis and Langford [43] nomenclature, namely $\mathbf{S4 }$, and conjectured that propositional intuitionistic logic $\mathbf{Int }$, as axiomatised by Heyting [35], can be defined by taking

$$\begin{aligned} \varphi \in \mathbf{Int }\quad \text {iff} \quad T(\varphi ) \in \mathbf{S4 }, \end{aligned}$$

(5.1)

where $T(\varphi )$ is the modal formula obtained by prefixing $\Box$ to every subformula³ of the intuitionistic formula $\varphi$. This conjecture was proved by McKinsey and Tarski [49] in 1948; many other proofs of this fundamental result were given later by Maehara [44], Hacking [34], Schütte [67], Novikov [55], et al.

It has been known since Gödel’s [24] that there are infinitely many (more precisely, continuum-many [36]) logics between Int and Cl. Moreover, some of them are ‘constructive’ in the same way as Int, for instance, the Kleene realisability logic [38, 54, 65] or the Medvedev logic of finite problems [50]. The logics sitting between Int and Cl were called intermediate logics by Umezawa [72, 73]; in the 1960s, Kuznetsov suggested the name superintuitionistic logics (si-logics, for short) for all extensions of Int. We denote the class of si-logics by ExtInt. The class of normal (that is, closed under the necessitation rule $\varphi /\Box \varphi$) extensions of S4 will be denoted by NExtS4. Thus,

$$\begin{aligned} {\text {Ext}}\mathbf{Int }&= \{ \mathbf{Int }+ \varGamma \mid \varGamma \subseteq \fancyscript{L}_I \},\\ {\text {NExt}}\mathbf{S4 }&= \{ \mathbf{S4 }\, \oplus \, \varSigma \mid \varSigma \subseteq \fancyscript{L}_M \}, \end{aligned}$$

where $\fancyscript{L}_I$ is the set of propositional (intuitionistic) formulas, $\fancyscript{L}_M$ is the set of modal formulas, $+$ stands for ‘add the formulas in $\varGamma$ and take the closure under modus ponens and substitution,’ while $\oplus$ also requires the closure under necessitation.

Dummett and Lemmon [11] extended the translation $T$ to the whole class of si-logics. More precisely, with every si-logic $L = \mathbf{Int }+ \varGamma$ they associated the modal logic $\tau L = \mathbf{S4 }\oplus \{T(\varphi ) \mid \varphi \in \varGamma \}$ and showed that $L$ is embedded in $\tau L$ by $T$: for every $\varphi \in \fancyscript{L}_I$, we have

$$\begin{aligned} \varphi \in L \quad \text {iff} \quad T(\varphi ) \in \tau L. \end{aligned}$$

(5.2)

It turned out, in particular, that $\tau \mathbf{Cl }= \mathbf{S5 }$, $\tau \mathbf{KC } = \mathbf{S4.2 }$, $\tau \mathbf{LC } = \mathbf{S4.3 }$, where

$$\begin{aligned} \mathbf{Cl }&= \mathbf{Int }+ p \vee \lnot p,&\mathbf{S5 }&= \mathbf{S4 }\oplus p \rightarrow \Box \Diamond p,\\ \mathbf{KC }&= \mathbf{Int }+ \lnot p \vee \lnot \lnot p,&\mathbf{S4.2 }&= \mathbf{S4 }\oplus \Diamond \Box p \rightarrow \Box \Diamond p,\\ \mathbf{LC }&= \mathbf{Int }+ (p \rightarrow q) \vee (q\rightarrow p),&\mathbf{S4.3 }&= \mathbf{S4 }\oplus \Box (\Box p \rightarrow q) \vee \Box (\Box q \rightarrow p). \end{aligned}$$

One of the questions considered in [11] was to identify those properties of logics that were preserved under the map $\tau$.

Grzegorczyk [33] found a proper extension of S4 into which Int can also be embedded by $T$. His logic is known now as the Grzegorczyk logic

$$ \mathbf{Grz }= \mathbf{S4 }\ \oplus \ \Box ( \Box ( p \rightarrow \Box p) \rightarrow p) \rightarrow p. $$

Thus, we have, for every $\varphi \in \fancyscript{L}_I$:

$$\begin{aligned} \varphi \in \mathbf{Int }\quad \text {iff} \quad T(\varphi ) \in \mathbf{Grz }. \end{aligned}$$

(5.3)

In fact, according to the Blok-Esakia theorem, $\mathbf{Grz }$ is the largest extension of S4 into which Int is embeddable by $T$. Esakia [13] observed that Int was also embeddable into the McKinsey logic $\mathbf{S4.1 }= \mathbf{S4 }\oplus \Box \Diamond p \rightarrow \Diamond \Box p$.

A systematic study of the embeddings of si-logics into modal logics was launched by Maksimova and Rybakov [47], Blok [6] and Esakia [13, 15, 16]. Maksimova and Rybakov introduced two more maps:

$$ \rho :{\text {NExt}}\mathbf{S4 }\rightarrow {\text {Ext}}\mathbf{Int }\qquad \text {and} \qquad \sigma :{\text {Ext}}\mathbf{Int }\rightarrow {\text {NExt}}\mathbf{S4 }$$

where

• $\rho M = \{ \varphi \in \fancyscript{L}_I \mid T(\varphi ) \in M \}$, for every $M \in {\text {NExt}}\mathbf{S4 }$; Esakia called $\rho M$ the superintuitionistic fragment of $M$, and $M$ a modal companion of $\rho M$;

• $\sigma L = \tau L \oplus \mathbf{Grz }$, for every $L \in {\text {Ext}}\mathbf{Int }$ (Maksimova and Rybakov [47] used a somewhat different map, which was later shown to be equivalent to $\sigma$ by Blok and Esakia).

Thus, for example, $\rho \mathbf{Grz }= \rho \mathbf{S4.1 }= \mathbf{Int }$, $\tau \mathbf{Int }= \mathbf{S4 }$, and $\sigma \mathbf{Int }= \mathbf{Grz }$.

The results of Maksimova and Rybakov [47], Blok [6] and Esakia [13, 15, 16] on the relationship between ${\text {Ext}}\mathbf{Int }$ and ${\text {NExt}}\mathbf{S4 }$ can be summarised as follows:

• 1. The set of all modal companions of any si-logic $L$ forms the interval

  $$ \rho ^{-1}(L) = \{ M \in {\text {NExt}}\mathbf{S4 }\mid \tau L \subseteq M \subseteq \sigma L \}, $$

  with $\tau L$ being the smallest and $\sigma L$ the greatest modal companions of $L$ in $\text {NExt}\mathbf{S4 }$.⁴ Note that this interval always contains an infinite descending chain of logics; for some si-logics, it may contain continuum-many modal logics.

• 2. The map $\rho$ is a lattice homomorphism from ${\text {NExt}}\mathbf{S4 }$ onto ${\text {Ext}}\mathbf{Int }$, $\tau$ is a lattice isomorphism from ${\text {Ext}}\mathbf{Int }$ into ${\text {NExt}}\mathbf{S4 }$, and all the three maps $\rho$, $\tau$ and $\sigma$ preserve infinite sums and intersections of logics [47].

• 3. (The Blok-Esakia Theorem) The map $\sigma$ is a lattice isomorphism from ${\text {Ext}}\mathbf{Int }$ onto ${\text {NExt}}\mathbf{Grz }$.

• 4. Rybakov [66] also observed that, for any $L \in {\text {Ext}}\mathbf{Int }$, the lattice ${\text {Ext}}L$ is isomorphically embeddable into $\rho ^{-1} L$. It follows, for example, that there are a continuum of modal companions of $\mathbf{Int }$.

The emerging relationship between the lattices ${\text {Ext}}\mathbf{Int }$ and $\text {NExt}\mathbf{S4 }$ can be described semantically. Recall (see, e.g., [9, 27] for details and further references) that general frames for Int are structures of the form $\mathfrak F = (W,R,P)$, where $W$ is a non-empty set, $R$ a partial order on $W$ and $P$ is a collection of upward closed subsets of $W$ (with respect to $R$) that contains $\emptyset$ and is closed under $\cap$, $\cup$ and the operation $\rightarrow$ defined by taking

$$ X \rightarrow Y = \{ x\in W \mid \forall y \, (xRy \wedge y \in X \rightarrow y\in Y) \}. $$

If $P$ contains all upward closed subsets in $W$, then $\mathfrak F$ is called a Kripke frame and denoted by $\mathfrak F = (W,R)$. Every si-logic $L$ is characterised by the class ${\mathsf {Fr}}L$ of general frames validating $L$. General frames for S4 are triples of the form $\mathfrak F = (W,R,P)$, where $R$ a quasi-order on $W\ne \emptyset$ and $P\subseteq 2^W$ is a Boolean algebra of subsets of $W$ closed under the operation $\Box$ defined by taking

$$ \Box X = \{ x\in W \mid \forall y \, (xRy \rightarrow y\in X) \}. $$

General frames of the form $\mathfrak F = (W,R,2^W)$ are called Kripke frames and denoted by $\mathfrak F = (W,R)$. Every logic $M\in {\text {NExt}}\mathbf{S4 }$ is characterised by the class ${\mathsf {Fr}}M$ of general frames validating $M$. For example, a Kripke frame $\mathfrak F= (W,R)$ is in ${\mathsf {Fr}}\mathbf{Grz }$ iff $\mathfrak F$ does not contain an infinite ascending chain of the form $x_1Rx_2Rx_3 \dots$ with $x_i\ne x_{i+1}$, $i\ge 1$. We call such frames Noetherian. The smallest non-Noetherian frame contains two distinct points accessible from each other; we denote this frame by $\mathfrak C_2$.

Given a frame $\mathfrak F = (W,R,P)$ for $\mathbf{S4 }$ and a point $x \in W$, we denote by $C(x)$ the cluster generated by $x$ in $\mathfrak F$, that is, the set

$$ C(x) = \{ y\in W \mid xRy \text { and } yRx \}. $$

(Thus, the frame $\mathfrak C_2$ above is just a two-point cluster.) The skeleton of $\mathfrak F$ is the general frame $\rho \mathfrak F = (\rho W, \rho R, \rho P)$ for Int defined by taking $\rho X = \{C(x) \mid x\in X \}$, for $X \in P$, $C(x) \rho R C(y)$ iff $xRy$, and

$$ \rho P = \{\rho X \mid X\in P \text { and } X = \Box X \}. $$

Conversely, given a frame $\mathfrak F = (W,R,P)$ for Int, denote by $\sigma \mathfrak F$ the frame $(W,R,\sigma P)$ for S4, where $\sigma P$ is the Boolean closure of $P$ in $2^W$. Note that the operator $\sigma$ does not preserve Kripke frames as, for example, $\sigma (\omega ,\le )$ is not a Kripke frame. Another way of converting an intuitionistic frame $\mathfrak F = (W,R,P)$ into a modal one is by expanding its points into clusters. Given a cardinal $\kappa$, $0 <\kappa \le \omega$, define $\tau _\kappa \mathfrak F = (\kappa W, \kappa R, \kappa P)$ by replacing every $x \in W$ with a $\kappa$-cluster with the points $x_i$, for $i\in \kappa$, and taking $\kappa P$ to be the Boolean closure of $\{ X_I \mid I \subseteq \kappa \text { and } X\in \sigma P \}$, where $X_I = \{ x_i \mid i\in I \text { and } x\in X \}$ [79]. One can show that both $\rho \sigma \mathfrak F$ and $\rho \tau _\kappa \mathfrak F$ are isomorphic to $\mathfrak F$.

Given a class $\fancyscript{K}$ of frames, we set $\rho \fancyscript{K} = \{\rho \mathfrak F \mid \mathfrak F \in \fancyscript{K} \}$; a similar notation will be used for the operators $\sigma$ and $\tau _\kappa$. The logic determined by $\fancyscript{K}$ is denoted by ${\mathsf {Log}}\fancyscript{K}$ (it will always be clear from the context whether it is a si- or modal logic). Now, we have:

• ($\rho$) for any $M\in {\text {NExt}}\mathbf{S4 }$ and $\fancyscript{K}$, $M = {\mathsf {Log}}\fancyscript{K}$ iff $\rho M = {\mathsf {Log}}\rho \fancyscript{K}$,

• ($\tau$) for any $L\in {\text {Ext}}\mathbf{Int }$ and $\fancyscript{K}$, $L = {\mathsf {Log}}\fancyscript{K}$ iff $\tau L = {\mathsf {Log}}\{\tau _\kappa \fancyscript{K} \mid \kappa <\omega \}$,

• ($\sigma$) for any $L\in {\text {Ext}}\mathbf{Int }$ and $\fancyscript{K}$, $L = {\mathsf {Log}}\fancyscript{K}$ iff $\sigma L = {\mathsf {Log}}\sigma \fancyscript{K}$.

Thus, we can think of ${\text {NExt}}\mathbf{S4 }$ as a two-dimensional structure: in one dimension, we can change the skeleton of frames and thereby change the si-fragment $\rho M$ of a modal logic $M$; in the other, we can change the size of clusters in frames, which keeps the same si-fragment $\rho M$ but varies the logic between $\tau \rho M$ and $\sigma \rho M$.

A little bit different perspective can be obtained by employing the machinery of canonical formulas (see [4, 9, 80] for details and further references). For simplicity, let us imagine that all logics in ${\text {Ext}}\mathbf{Int }$ and ${\text {NExt}}\mathbf{S4 }$ are subframe logics, that is, their classes of frames are closed under taking (not necessarily generated) subframes. All such logics are Kripke complete [17, 78], so we can only deal with Kripke frames. Given a finite rooted quasi-order $\mathfrak F$, one can construct a modal formula, $\alpha (\mathfrak F)$, such that, for any frame $\mathfrak G$, we have $\mathfrak G \not \models \alpha (\mathfrak F)$ iff $\mathfrak F$ is a p-morphic image of a subframe of $\mathfrak G$; in this case we also say that $\mathfrak G$ is sub-reducible to $\mathfrak F$. A similar intuitionistic formula, $\beta (\mathfrak F)$, can be associated with any finite rooted partial order $\mathfrak F$. The formulas of the form $\alpha (\mathfrak F)$ and $\beta (\mathfrak F)$ are called subframe formulas. As shown in [17, 78], all subframe modal and si-logics can be axiomatised by the respective subframe formulas. (We note in passing that the subframe si-logics are precisely those logics in ${\text {Ext}}\mathbf{Int }$ that can be axiomatised by purely implicative formulas [78, 81].)

Given a si-logic $L = \mathbf{Int }+ \{\beta (\mathfrak F_i) \mid i\in I\}$, every logic $M \in \rho ^{-1} L$ can be represented in the form

$$\begin{aligned} M = \mathbf{S4 }\oplus \{\alpha (\mathfrak F_i) \mid i\in I\} \oplus \{\alpha (\mathfrak F_j) \mid j\in J\}, \end{aligned}$$

(5.4)

where every frame $\mathfrak F_j$, $j\in J$, contains a cluster with at least two points. The logic $\mathbf{S4 }\oplus \{\alpha (\mathfrak F_i) \mid i\in I\}$ is obviously $\tau L$, while $\sigma L = \tau L \oplus \alpha (\mathfrak C_2)$. The lattice $\rho ^{-1}\mathbf{Cl }$ of modal companions of classical logic $\mathbf{Cl }$ looks as follows:

$$ \tau \mathbf{Cl }= \mathbf{S5 } \subset \dots \subset \mathbf{S5 } \oplus \alpha (\mathfrak C_n) \subset \dots \subset \mathbf{S5 } \oplus \alpha (\mathfrak C_2) = {\mathsf {Log}}\{\mathfrak C_1\}, $$

where $\mathfrak C_n$ is a cluster with $n$ points. However, for other si-logics $L$, the lattice $\rho ^{-1} L$ may be very complex.

Every $M \in {\text {NExt}}\mathbf{S4 }$ can be represented as

$$\begin{aligned} M = M^* \oplus \tau \rho M, \quad \text {with} \quad M^* \subseteq \mathbf{Grz }. \end{aligned}$$

Muravitsky [53] called the logic $M^*$ a modal component of $M$ and observed that the modal components of $M$ form a dense sublattice of ${\text {NExt}}\mathbf{S4 }$ with $M \cap \mathbf{Grz }$ as its greatest element. The problem whether this sublattice always has a least element was left open in [53]. We only note here that a least element does exist if $M$ is a subframe logic.

The semantic characterisations given above can be used to investigate whether this or that property of logics is preserved under the maps $\rho$, $\tau$ and $\sigma$. For example, all the three maps preserve decidability, the finite model property and the disjunction property [47, 79]; Kripke completeness is preserved by $\rho$, $\tau$ but not by $\sigma$ [47, 68, 79]; interpolation is preserved only under $\rho$ [46]. (For more preservation results and further references consult [9, 10].)

In this chapter, we do not consider embeddings of Int and its extensions into the logic of formal provability (in Peano Arthmetic) GL, found by Boolos [7], Goldblatt [26] and Kuznetsov and Muravitskij [42]. A discussion of these results can be found in [10]; see also the chapters in this volume written by T. Litak and A. Muravitsky. Artemov [1] analyses the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic in the context of his logics of proofs LP closely related to S4. Relationships between first-order si- and modal logics are investigated in [23].

5.3 An Algebraic Proof of the Blok-Esakia Theorem

In this section, we give a sketch of the algebraic proof of the Blok-Esakia theorem that was found by Blok in his PhD thesis [6] but never published in a journal. (A proof using the machinery of canonical formulas was given in [9]; Jerabek [37] considered modal companions of si-logics from the point of view of inference rules and also gave a proof of the Blok-Esakia theorem.)

We remind the reader that si- and modal logics are determined by varieties of Heyting and, respectively, topological Boolean algebras. A Heyting algebra $\mathfrak {A}=(A,\wedge ,\vee ,\rightarrow ,\bot ,\top )$ extends a bounded distributive lattice $(A,\wedge ,\vee ,\bot ,\top )$ with a binary operator $a \rightarrow b$ for the relative pseudo-complement of $a$ with respect to $b$; that is, for all $c\in A$, we have $a \wedge c \le b$ iff $c \le a \rightarrow b$. The class of all Heyting algebras is a variety (equationally definable); we denote it by $H$. Subvarieties $V$ of $H$ are in 1–1 correspondence to si-logics: for any class $\fancyscript{V}$ of Heyting algebras, the set

$$ L (\fancyscript{V}) = \{ \varphi \in \fancyscript{L}_{I}\mid \forall \mathfrak {A}\in \fancyscript{V}\ \mathfrak {A}\models (\varphi =\top )\} $$

is a si-logic and, conversely, for every si-logic $L$,

$$ \fancyscript{V}(L) = \{ \mathfrak {A} \mid \forall \varphi \in L\ \mathfrak {A}\models (\varphi =\top )\} $$

is a variety of Heyting algebras. Moreover, $L(\fancyscript{V}(L))=L$ and $\fancyscript{V}(L(\fancyscript{V}))=\fancyscript{V}$ for any si-logic $L$ and any variety $\fancyscript{V}$ of Heyting algebras. These results can be proved directly or using duality between Heyting algebras and general frames for Int: for any such general frame $\mathfrak {F}= (W,R,P)$, the set $P$ with operations $\cap$, $\cup$, and $\rightarrow$ defined above forms a Heyting algebra denoted by $\mathfrak {F}^{+}$. Conversely, for every Heyting algebra $\mathfrak {A}$, one can construct a general frame $\mathfrak {A}_{+}=(W,R,P)$ whose domain $W$ consists of all prime filters $X$ in $\mathfrak {A}$ with $X R Y$ iff $X \subseteq Y$, and $V\in P$ iff there exists $a\in A$ with $V = \{ X\in W\mid a\in X\}$. Moreover, $\mathfrak {A}$ is isomorphic to $(\mathfrak {A}_{+})^{+}$.

A topological Boolean algebra, or an S4-algebra, $\mathfrak {A} = (A,\wedge ,\vee ,\lnot ,\bot ,\top ,\Box )$ extends a Boolean algebra $(A,\wedge ,\vee ,\lnot ,\bot ,\top )$ with a unary operator $\Box$ satisfying the following equations, for all $a,b\in A$:

$$ \Box \top = \top , \qquad \Box (a\wedge b) = \Box a \wedge \Box b, \qquad \Box a \le a, \qquad \Box a \le \Box \Box a. $$

The class of all S4-algebras is a variety; we denote it by $\fancyscript{V}(\mathbf{S4})$. Subvarieties $V$ of $\fancyscript{V}(\mathbf{S4 })$ are in 1–1 correspondence to normal extensions of S4: for any class $\fancyscript{V}$ of S4-algebras, the set

$$ L(\fancyscript{V})= \{ \varphi \in \fancyscript{L}_{M}\mid \forall \mathfrak {A}\in \fancyscript{V}\ \mathfrak {A}\models (\varphi =\top )\} $$

is a logic in NExtS4 and, conversely, for every logic $L \in {\text {NExt}}\mathbf{S4 }$,

$$ \fancyscript{V}(L) = \{ \mathfrak {A} \mid \forall \varphi \in L\ \mathfrak {A}\models (\varphi =\top )\} $$

is a variety of S4-algebras. Moreover, $L(\fancyscript{V}(L))=L$ and $\fancyscript{V}(L(\fancyscript{V}))=\fancyscript{V}$ for any $L\in {\text {NExt}}\mathbf{S4 }$ and any variety $\fancyscript{V}$ of S4-algebras. Similarly to the representation of Heyting algebras by frames for Int above, one can represent S4-algebras by general frames for S4. For any such general frame $\mathfrak {F}= (W,R,P)$ for S4, the set $P$ with the operations intersection, union, complement, and $\Box$ defined above forms an S4-algebra denoted by $\mathfrak {F}^{+}$. Conversely, for every S4-algebra $\mathfrak {A}$, one can construct a general frame $\mathfrak {A}_{+}=(W,R,P)$ whose domain $W$ consists of all ultrafilters $X$ in $\mathfrak {A}$ with $X R Y$ iff $\{a \mid \Box a\in X\} \subseteq Y$, and $V\in P$ iff there exists $a\in A$ with $V = \{ X\in W\mid a\in X\}$. And again, $\mathfrak {A}$ is isomorphic to $(\mathfrak {A}_{+})^{+}$.

We are in the position now to describe the relationship between si-logics and normal extensions of S4 at the level of Heyting and S4-algebras.

From S4 -algebras to Heyting algebras. For any S4-algebra $\mathfrak {A}= (A,\wedge ,\vee , \lnot ,\bot ,\top ,\Box )$, we define a Heyting algebra $\rho \mathfrak {A}$ by taking

$$ \rho \mathfrak {A} = (\rho A,\wedge ,\vee ,\rightarrow ,\bot ,\top ), $$

where $\rho A= \{\Box a \mid a\in A\}$ and $a\rightarrow b= \Box (\lnot a \vee b)$. Alternatively, one can obtain (an isomorphic copy of) $\rho \mathfrak {A}$ by applying the operation $\rho$ defined for general frames to $\mathfrak {A}_{+}$ and then taking the induced algebra; that is, $\rho \mathfrak {A}$ is isomorphic to $(\rho (\mathfrak {A}_{+}))^{+}$.

From Heyting algebras to S4 -algebras. Conversely, with every Heyting algebra $\mathfrak {A}$ one can associate an S4-algebra $\sigma \mathfrak {A}$ in the following way. First, given a bounded distributive lattice $\mathfrak {D}= (D,\wedge ,\vee ,\bot ,\top )$, we construct the free Boolean extension $\mathfrak {B}$ of $\mathfrak {D}$ with domain $B=\sigma D \supseteq D$, which is the (uniquely determined) Boolean algebra generated by $D$ such that, for any bounded lattice homomorphism $f: \mathfrak {D} \rightarrow \mathfrak {C}$ into a Boolean algebra $\mathfrak {C}$, there exists a unique Boolean homomorphism $h: \mathfrak {B} \rightarrow \mathfrak {C}$ with $h$ $D =f$. Now, given a Heyting algebra $\mathfrak {A}=(A, \wedge ,\vee ,\rightarrow , \bot ,\top )$, we obtain the S4-algebra $\sigma \mathfrak {A}$ by setting in the free Boolean extension of its underlying bounded distributive lattice

$$ \Box a= \bigwedge _{i=1}^{n}(a_{i} \rightarrow b_{i}), \quad \text {for}\; a= \bigwedge _{i=1}^{n}(\lnot a_{i} \vee b_{i}). $$

One can show that $\sigma \mathfrak {A}\in \fancyscript{V}(\mathbf{Grz })$ and that $\mathfrak {A}\models (\varphi =\top )$ iff $\sigma \mathfrak {A}\models (T(\varphi )=\top )$. $\sigma \mathfrak {A}$ can also be obtained by first forming $\mathfrak {A}_{+}=(W,R,P)$ and then taking the S4-algebra $(W,R,\sigma P)^{+}$ induced by $(W,R,\sigma P)$, where $\sigma P$ has been defined above.

Given classes $\fancyscript{K}$ and $\fancyscript{H}$ of S4- and Heyting algebras, respectively, we set

$$ \rho \fancyscript{K} = \{ \rho \mathfrak {A} \mid \mathfrak {A}\in \fancyscript{K}\} \quad \text {and} \quad \sigma \fancyscript{H} = \{ \sigma \mathfrak {A} \mid \mathfrak {A}\in \fancyscript{H}\}. $$

We denote by $\mathsf{H}\fancyscript{K}$, $\mathsf{S}\fancyscript{K}$, $\mathsf{P}\fancyscript{K}$, and $\mathsf{P}_\mathsf{U}\fancyscript{K}$ the classes of subalgebras, homomorphic images, products, and ultraproducts of algebras in $\fancyscript{K}$, respectively. Recall that a class $\fancyscript{K}$ of algebras (of the same signature) is a variety if, and only if, it is closed under subalgebras, homomorphic images, and products. Every first-order definable class (and, hence, every variety) is closed under ultraproducts. The following lemma can be proved by showing that $\rho \fancyscript{V}$ is closed under subalgebras, homomorphic images, and products [5, 6]:

Lemma 1

For any variety $\fancyscript{V}$ of S4-algebras, $\rho \fancyscript{V}$ is a variety of Heyting algebras.

For a variety $\fancyscript{V}$ of Heyting algebras, $\sigma \fancyscript{V}$ is not always a variety. We denote by $\sigma ^{*}\fancyscript{V}$ the variety of S4-algebras generated by $\sigma \fancyscript{V}$. The following result implies the Blok-Esakia Theorem:

Theorem 1

(i) For every variety $\fancyscript{V}$ of Heyting algebras, $\rho \sigma ^{*}\fancyscript{V}=\fancyscript{V}$.

(ii) For every variety $\fancyscript{V}$ of Grz-algebras, $\sigma ^{*}\rho \fancyscript{V}=\fancyscript{V}$.

For a detailed and instructive exposition of the main steps of the proof of Theorem 1, we refer the reader to [3]. Here we focus on (ii) and, in particular, the following technical lemma from Blok’s PhD thesis, which is the key to the algebraic proof of the Blok-Esakia theorem.

Lemma 2

Let $\mathfrak {A}\in \fancyscript{V}(\mathbf{Grz})$ be a countable algebra and let $\mathfrak {B}$ be a subalgebra of $\mathfrak {A}$ such that

• $\rho A \subseteq B$;

• there exists $c\in A$ such that $A$ is the Boolean closure of $B \cup \{c\}$ in $\mathfrak {A}$ $($denoted, slightly abusing notation, $\mathfrak {A}=[\mathfrak {B}\cup \{c\}]_{BA})$.

Then $\mathfrak {A}\in \mathsf{S}\mathsf{P}_\mathsf{U}\mathfrak {B}$.

Proof

(sketch). We follow the proof given in Blok’s PhD thesis [6]. Suppose that $B=\{b_i \mid i<\omega \}$ and let $U$ be a non-principal ultrafilter on $\omega$. We remind the reader of the definition of the ultraproduct $\prod _{i<\omega }\mathfrak {B}/U$. First, we define an equivalence relation $\sim _U$ by taking $g \sim _{U} g'$ iff $\{i< \omega \mid g(i)=g'(i)\} \in U$, for any $g,g'\in \prod _{i<\omega }B$, and set $[g]= \{ g' \mid g\sim _{U} g'\}$. The domain of $\prod _{i<\omega }\mathfrak {B}/U$ is $\{[g]\mid g\in \prod _{i<\omega }B\}$. For $b\in B$, let $\widehat{b}=(b,b,\dots )\in \prod _{i<\omega }B$. The map $f :\mathfrak {B} \rightarrow \prod _{i<\omega }\mathfrak {B}/U$ defined by taking $f(b)= [\widehat{b}]$ is an embedding of the S4-algebra $\mathfrak {B}$ into the S4-algebra $\prod _{i<\omega }\mathfrak {B}/U$. We show that $f$ extends to an embedding $\widehat{f}$ of the S4-algebra $\mathfrak {A}$ into the S4-algebra $\prod _{i<\omega }\mathfrak {B}/U$.

For $n\ge 0$, let

$$ C_{n}= \{ b_{i}\in B \mid b_{i}\le c,\ i \le n\}, \qquad c_{n} = \bigvee _{b\in C_{n}}b, \qquad \widehat{c} = ( c_{n} )_{n<\omega }. $$

First, using a Lemma on the existence of Boolean embeddings from [31, p. 84] one can show that $f$ can be extended to a Boolean embedding $\widehat{f} :\mathfrak {A}\rightarrow \prod _{i<\omega }\mathfrak {B}/U$ with $\widehat{f}(c)=[\widehat{c}]$. The next, and crucial, part of the proof is to show that $\widehat{f}$ commutes with the $\Box$-operator. Then $\mathfrak {A}\in \mathsf{S}\mathsf{P}_\mathsf{U}\mathfrak {B}$, as required. To show that $\widehat{f}$ commutes with $\Box$, let $a\in A$. Then

$$ a= (c \vee d_{1}) \wedge (\lnot c \vee d_{2}) \wedge d_{3}, $$

for some $d_{1},d_{2},d_{3}\in B$. It suffices to show that  

(a):

$\widehat{f}(\Box (c \vee d_{1})) = \Box \widehat{f}(c \vee d_{1})$,

(b):

$\widehat{f}(\Box (\lnot c \vee d_{2})) = \Box \widehat{f}(\lnot c \vee d_{2})$,

(c):

$\widehat{f}(\Box d_{3}) = \Box \widehat{f}d_{3}$,

  since then we shall have:

$$\begin{aligned} \widehat{f}(\Box a)&= \widehat{f}(\Box ((c \vee d_{1}) \wedge (\lnot c \vee d_{2}) \wedge d_{3}))\\&= \widehat{f}(\Box (c \vee d_{1}) \wedge \Box (\lnot c \vee d_{2}) \wedge \Box d_{3})\\&= \widehat{f}(\Box (c \vee d_{1})) \wedge \widehat{f}(\Box (\lnot c \vee d_{2})) \wedge \widehat{f}(\Box d_{3})\\&= \Box \widehat{f}(c \vee d_{1}) \wedge \Box \widehat{f}(\lnot c \vee d_{2}) \wedge \Box \widehat{f}d_{3}\\&= \Box \widehat{f}(a). \end{aligned}$$

Now, (c) follows from $d_{3}\in B$ and the condition that $f$ is a homomorphism. For (a), let $b=d_{1}$. We observe that

$$ \Box (c \vee b) = \Box ((\Box (c \vee b) \wedge \lnot b) \vee b) $$

because $\Box (c \vee b) \wedge \lnot b \le c$. We have $\Box (c \vee b) \wedge \lnot b\in B$ since $\Box (c \vee b)\in \rho A \subseteq B$ and $b\in B$. Hence $\Box (c \vee b) \wedge \lnot b = b_{n}$ for some $n< \omega$. We obtain $c_{n} \ge b_{n}$ and, for all $m\ge n$,

$$ \Box (c \vee b) = \Box ((\Box (c \vee b) \wedge \lnot b) \vee b) \le \Box (c_{m} \vee b) \le \Box (c \vee b). $$

Thus, $\Box (c\vee b)= \Box ( c_{m}\vee b)$ for all $m\ge n$. The equation $\widehat{f}(\Box (c \vee b)) = \Box \widehat{f}(c \vee b)$ follows.

To show (b), let $b=d_{2}$, $p= \Box (\lnot c \vee b)$, and $q= \Box ((c \wedge \lnot b) \vee p)$. We note that $q= \Box (\lnot (\lnot c \vee b) \vee \Box (\lnot c \vee b))$. We obtain $\lnot p \wedge q \le c \wedge \lnot b$. Since $\mathfrak {A}\in \fancyscript{V}(\mathbf{Grz})$, we obtain, for all $x$,

$$ \mathfrak {A}\models \Box (\lnot \Box (\lnot x \vee \Box x) \vee \Box x) = \Box x $$

and, therefore,

$$\begin{aligned} \Box (\lnot q \vee p)&= \Box (\lnot \Box (\lnot (\lnot c \vee b) \vee \Box (\lnot c \vee b)) \vee \Box (\lnot c \vee b))\\&= \Box (\lnot c \vee b). \end{aligned}$$

We have $\lnot p \wedge q \in B$ since $\rho A \subseteq B$, and so $\lnot p \wedge q = b_{n}$ for some $n< \omega$. From $\lnot p \wedge q \le c \wedge \lnot b$ we obtain $b_{n} \le c_{m} \wedge \lnot b$ for all $m\ge n$, and therefore $\lnot b_{n} \ge \lnot c_{m} \vee b$, for all $m\ge n$. Hence

$$ \Box (\lnot c \vee b) = \Box (\lnot q \vee p) = \Box \lnot b_{n} \ge \Box (\lnot c_{m} \vee b) \ge \Box (\lnot c \vee b). $$

Thus, we obtain $\Box (\lnot c\vee b)= \Box ( \lnot c_{m}\vee b)$ for all $m\ge n$. The required equation $\widehat{f}(\Box (\lnot c \vee b)) = \Box \widehat{f}(\lnot c \vee b)$ follows.$\Box$

We are now in the position to show that $\sigma ^{*}\rho \fancyscript{V}=\fancyscript{V}$, for any variety $\fancyscript{V}$ of Grz-algebras. The inclusion $\sigma ^{*}\rho \fancyscript{V}\subseteq \fancyscript{V}$ is clear. Since any variety is generated by its finitely generated members, to prove $\fancyscript{V} \subseteq \sigma ^{*}\rho \fancyscript{V}$ it is sufficient to show that all finitely generated $\mathfrak {A}\in \fancyscript{V}$ are in the variety generated by $\sigma \rho \fancyscript{V}$. Let $\mathfrak {A}\in \fancyscript{V}$ be generated by $\{a_{1},\ldots ,a_{n}\}$. $\sigma \rho \mathfrak {A}$ is (isomorphic to) a subalgebra of $\mathfrak {A}$. Consider the sequence

$$ [\sigma \rho \mathfrak {A} \cup \{a_{1}\}]_{BA},\dots ,[\sigma \rho \mathfrak {A} \cup \{a_{1},\dots ,a_{n}\}]_{BA}=\mathfrak {A}. $$

By Lemma 2, it follows by induction that

$$ [\sigma \rho \mathfrak {A} \cup \{a_{1},\ldots ,a_{i}\}]_{BA}\in \fancyscript{V}(\sigma \rho \mathfrak {A})\subseteq \sigma ^{*}\rho \fancyscript{V}, $$

for $1\le i \le n$. Thus, $\mathfrak {A}\in \sigma ^{*}\rho \fancyscript{V}$, as required.

Intuitionistic logic and its extensions can be embedded in modal logics different from normal extensions of S4 using different translations; for details and references, the reader can consult [10]. In the remainder of this chapter, we briefly consider extensions of Int with extra operators.

5.4 Blok-Esakia Theorems for Intuitionistic Modal Logics

Modal extensions of intuitionistic propositional logic are notoriously much harder to investigate than si-logics and standard (uni)modal logics. In fact, it is already non-trivial to define what an intuitionistic analogue of a given modal logic should be—for intuitionistic $\Box$ and $\Diamond$ are not supposed to be dual. Servi [18, 20], for instance, used a generalisation of the translation $T$ to argue that her systems were ‘true’ intuitionistic analogues of classical modal logics. In this section, we briefly discuss two extensions of the Blok-Esakia theorem to intuitionistic modal logics.

We begin by considering the most obvious basic system $\mathbf{IntK}_{\Box }$, which is obtained by adding to Int the standard axiom $\Box (p \wedge q) \leftrightarrow (\Box p \wedge \Box q)$ and the necessitation inference rule $\varphi /\Box \varphi$ of the minimal modal logic K ($\Diamond \varphi$ can be defined as $\lnot \Box \lnot \varphi$; note, however, that this $\Diamond$ does not distribute over disjunction). As before, ${\text {NExt}}\mathbf{IntK}_{\Box }$ denotes the family of logics of the form $\mathbf{IntK}_{\Box } \oplus \varGamma$, where $\varGamma$ is a set of modal formulas. An example of a logic in this family is Kuznetsov’s [41] intuitionistic provability logic

$$ \mathbf{I}^\triangle = \mathbf{IntK}_{\Box } \ \oplus \ p\rightarrow \Box p \ \oplus \ (\Box p\rightarrow p)\rightarrow p \ \oplus \ ((p\rightarrow q)\rightarrow p)\rightarrow (\Box q\rightarrow p), $$

an intuitionistic analogue of the provability logic GL. (Esakia suggested the name KM for this logic; see Muravitsky’s chapter in this volume for a detailed account.) Muravitskij [51, 52] actually proved that the lattices ${\text {NExt}}\mathbf{I}^\triangle$ and ${\text {NExt}}\mathbf{GL}$ are isomorphic (this result and some generalisations are discussed in Litak’s chapter).

A Kripke frame for $\mathbf{IntK}_{\Box }$ is a structure of the form $\mathfrak F = (W,R,R_{\Box })$, where $R$ is a partial order and $R_\Box$ a binary relation on $W$ such that $R \circ R_{\Box } \circ R = R_{\Box }$. The intuitionistic connectives are interpreted in $\mathfrak F$ by means of $R$, while $\Box$ is interpreted via $R_\Box$. Algebraically, every logic $L \in {\text {NExt}}\mathbf{IntK}_{\Box }$ corresponds to the variety of Heyting algebras with modal operators validating $L$. For more details on algebraic and relational semantics of these logics and their duality, the reader is referred to [71, 76].

We embed logics in ${\text {NExt}}\mathbf{IntK}_{\Box }$ into extensions of the fusion (aka independent join) $\mathbf{S4 }\otimes \mathbf{K }$ of the modal logics S4 and K. Assuming that the necessity operators in S4 and K are denoted by $\Box _I$ and $\Box$, respectively, we consider the translation $T$ which prefixes $\Box _{I}$ to every subformula of a given formula in the language of $\mathbf{IntK}_{\Box }$. As before, we say that $T$ embeds $L\in \text{ NExt }\mathbf{IntK}_{\Box }$ into $M\in \text{ NExt }(\mathbf{S4}\otimes \mathbf{K})$ if, for every (unimodal) formula $\varphi$,

$$ \varphi \in L \quad \text {iff} \quad T(\varphi ) \in M. $$

In this case $M$ is called a bimodal companion of $L$.

For every logic $M \in \text{ NExt }(\mathbf{S4}\otimes \mathbf{K})$, let

$$ \rho M = \{ \varphi \mid T(\varphi )\in M\}, $$

and let $\sigma$ be the map from $\text{ NExt }\mathbf{IntK}_{\Box }$ into $\text{ NExt }(\mathbf{S4}\otimes \mathbf{K})$ defined by taking

$$ \sigma (\mathbf{IntK}_{\Box }\oplus \varGamma ) = (\mathbf{Grz}\otimes \mathbf{K})\ \oplus \ mix \ \oplus \ T(\varGamma ), \quad \text {where} \quad mix = \Box _{I}\Box \Box _{I}p \leftrightarrow \Box p. $$

Here, the axiom $mix$ reflects the condition $R \circ R_{\Box }\circ R = R_{\Box }$ on frames for $\mathbf{IntK}_{\Box }$. The following extension of the embedding results discussed in Sect. 5.2 was proved in [76, 77]:

Theorem 2

(i) The map $\rho$ is a lattice homomorphism from $\mathrm{{\text {NExt}}}(\mathbf{S4}\otimes \mathbf{K})$ onto $\mathrm{{\text {NExt}}}\mathbf{IntK}_{\Box }$, which preservs decidability, Kripke completeness, tabularity and the finite model property.

(ii) Each logic $\mathbf{IntK}_{\Box }\oplus \varGamma$ is embedded by $T$ into any logic $M$ in the interval

$$ (\mathbf{S4}\otimes \mathbf{K}) \ \oplus \ T(\varGamma ) \ \subseteq \ M \ \subseteq \ (\mathbf{Grz}\otimes \mathbf{K}) \ \oplus \ mix \ \oplus \ T(\varGamma ). $$

(iii) The map $\sigma$ is an isomorphism from $\text{ NExt }\mathbf{IntK}_{\Box }$ onto $\text{ NExt }((\mathbf{Grz}\otimes \mathbf{K})\oplus mix)$ preserving the finite model property and tabularity.

Very few general completeness and decidability results are known for intuitionistic modal logics. The theorem above provides means for obtaining such results for logics in ${\text {NExt}}\mathbf{IntK}_{\Box }$. For example, one can show that if a si-logic $\mathbf{Int }+ \varGamma$ is decidable (Kripke complete or has the finite model property) then the logic $\mathbf{IntK}_{\Box } \oplus \varGamma$ enjoys the same property (for details and more results, the reader is referred to [76, 77]).

Intuitionistic modal logics with independent $\Box$ and $\Diamond$ can be defined as extensions of the basic system $\mathbf{IntK}_{\Box \Diamond }$, which contains the axioms and rules of $\mathbf{IntK}_{\Box }$ as well as the following axioms for $\Diamond$:

$$ \Diamond (p \vee q) \leftrightarrow \Diamond p \vee \Diamond q \qquad \text {and} \qquad \lnot \Diamond \bot . $$

Kripke frames for $\mathbf{IntK}_{\Box \Diamond }$ are of the form $(W,R,R_{\Box },R_\Diamond )$, where $R$ is a partial order (interpreting the intuitionistic connectives), while $R_\Box$ and $R_\Diamond$ are binary relations on $W$ (interpreting, respectively, $\Box$ and $\Diamond$) such that the following conditions hold: $R \circ R_{\Box } \circ R = R_{\Box }$ and $R^{-1} \circ R_{\Diamond } \circ R^{-1} = R_{\Diamond }$.

Perhaps the most prominent logics in ${\text {NExt}}\mathbf{IntK}_{\Box \Diamond }$ were constructed by Prior [59] and Fischer Servi [19, 20]. Fischer Servi introduced a weak connection between the necessity and possibility operators in her system

$$ \mathbf{FS} = \mathbf{IntK}_{\Box \Diamond } \ \oplus \ \Diamond (p \rightarrow q) \rightarrow (\Box p \rightarrow \Diamond q) \ \oplus \ (\Diamond p \rightarrow \Box q) \rightarrow \Box (p \rightarrow q). $$

Frames for $\mathbf{FS}$ satisfy the following conditions:

$$\begin{aligned} xR_\Diamond y \ \rightarrow \ \exists z \, (yRz \wedge xR_\Box z \wedge xR_\Diamond z),\\ xR_\Box y \ \rightarrow \ \exists z \, (xRz \wedge xR_\Box y \wedge zR_\Diamond y). \end{aligned}$$

A remarkable feature of FS is that the standard first-order translation not only embeds K into classical first-order logic but also FS into intuitionistic first-order logic; for details, consult [32, 70]. Another important extension of $\mathbf{IntK}_{\Box \Diamond }$ is the logic

$$\begin{aligned} \mathbf{MIPC} = \mathbf{FS} \ \oplus&\Box p \rightarrow p \ \oplus \ \Box p \rightarrow \Box \Box p \ \oplus \ \Diamond p \rightarrow \Box \Diamond p \ \oplus {}\\&p \rightarrow \Diamond p \ \oplus \ \Diamond \Diamond p \rightarrow \Diamond p \ \oplus \ \Diamond \Box p \rightarrow \Box p \end{aligned}$$

introduced by Prior [59]. MIPC is an intuitionistic analogue of the modal logic S5 in the sense that it is equivalent to the one-variable fragment of intuitionistic first-order logic in the same way as S5 is equivalent to the one-variable fragment of classical first-order logic. (Note, by the way, that the two-variable intuitionistic logic is undecidable [40], unlike the corresponding classical logic, which is NExpTime-complete [30].) MIPC is determined by the class of its Kripke frames $(W,R,R_{\Box },R_\Diamond )$, where $R_\Box$ is a quasi-order, $R_\Diamond = R^{-1}_\Box$ and $R_\Box = R \circ (R_\Box \cap R_\Diamond )$.

The extension of MIPC with the duality axiom $\lnot \Box \lnot p \rightarrow \Diamond p$ [21, 56, 64] is known as weak S5 and denoted by WS5. Bezhanishvili [2] showed that, for every formula $\varphi$, we have $\varphi \in \mathbf{WS5 }$ iff $\lnot \lnot \varphi \in \mathbf{MIPC }$ (remember that, according to Glivenko’s theorem, $\varphi \in \mathbf{Cl }$ iff $\lnot \lnot \varphi \in \mathbf{Int }$). Kripke frames $(W,R,R_{\Box },R_\Diamond )$, characterising WS5, are frames for MIPC such that $R_\Box$ is an equivalence relation on $W$.

Bezhanishvili [3] proved an analogue of the Blok-Esakia theorem for WS5 and the extension of Grz (in the language with $\Box _I$) with universal modalities. Modal logics with universal modalities were introduced by Goranko and Passy [28] who, for any (classical) modal logic $L$ with $\Box _I$, defined the (classical) bimodal logic $L_u$ with two boxes, $\Box _I$ and $\forall$, by taking

$$ L_u ~= L \oplus \{ \text {axioms of}\; \mathbf{S5 }{}\; \text {for}\; \forall \} \ \oplus \ \forall p \rightarrow \Box _I p. $$

For example, the logic $\mathbf{S4 }_u$ can be interpreted in topological spaces by regarding $\Box _I$ as the interior operator and $\forall$ as ‘for all points in the space.’ Because of this, $\mathbf{S4 }_u$ plays a prominent role in spatial representation and reasoning; see [22] and references therein. By adding to $\mathbf{S4 }_u$ the axiom $\forall (\Diamond _I p \rightarrow \Box _I p) \rightarrow \forall p \vee \forall \lnot p$, we obtain the logic $\mathbf{S4 }_u\mathbf{C }$ which is characterised by connected topological spaces [69].

Bezhanishvili [3] defined a translation $T$ from the language of WS5 to the language of $\mathbf{S4 }_u$ by extending the standard Gödel translation of Int into S4 with two more clauses $T(\Box \varphi ) = \forall T(\varphi )$ and $T(\Diamond \varphi ) = \exists T(\varphi )$, and showed that this translation is an embedding of WS5 into both $\mathbf{S4 }_u$ and $\mathbf{Grz }_u$. It also embeds the logic

$$ \mathbf{WS5 }\mathbf{C } = \mathbf{WS5 }\ \oplus \ \Box (p \vee \lnot p) \rightarrow (p \rightarrow \Box p) $$

into both $\mathbf{S4 }_u\mathbf{C }$ and $\mathbf{Grz }_u\mathbf{C }= \mathbf{Grz }_u \oplus \forall (\Diamond _I p \rightarrow \Box _I p) \rightarrow \forall p \vee \forall \lnot p$. Moreover, the following extension of the Blok-Esakia theorem holds for $T$:

• the lattice NExtWS5 is isomorphic to the lattice ${\text {NExt}}\mathbf{Grz }_u$, and

• the lattice NExtWS5 C is isomorphic to the lattice ${\text {NExt}}\mathbf{Grz }_u\mathbf{C }$.

A Blok-Esakia theorem for the lattice of all extensions of $\mathbf{IntK}_{\Box \Diamond }$ is obtained in [76]. In contrast to the target classical modal logics considered above, the modal logic constructed in [76] has, in addition to the S4/$\mathbf{Grz }$-modality, a modal operator that is not normal (but still has a natural Kripke semantics).

5.5 The Blok-Esakia Theorem for the Heyting-Brouwer Logic

In the 1970s, Cecylia Rauszer suggested the extension of the signature of intuitionistic logic by means of a new binary operator for coimplication, which we denote here by $\breve{\rightarrow }$. Algebraically, $\breve{\rightarrow }$ is defined in terms of intuitionistic disjunction in the same way as the intuitionistic implication is defined in terms of intuitionistic conjunction and thus re-establishes, in an extension of intuitionistic logic, the symmetry between classical disjunction and conjunction that is given up in the signature of intuitionistic logic. The translation $T$ of intuitionistic formulas to modal formulas can be extended by setting

$$ T(\varphi \breve{\rightarrow } \psi ) = \Diamond _{P}(T(\psi ) \wedge \lnot T(\varphi )), $$

where $\Diamond _{P}$ is the basic Priorean tense operator for ‘at some time in the past’ that is interpreted by the inverse of the accessibility relation for the modal $\Box$. To emphasise symmetry, in this section, we denote the modal operator $\Box$ by $\Box _{F}$ for ‘always in the future.’ It turns out that many properties of the translation $T$ still hold for this translation of coimplication in Priorean tense logic. In particular, a natural Blok-Esakia theorem holds. Interestingly, Leo Esakia [12, 14] considered both logics and made significant contributions to the study of algebras and their dual Kripke frames for both tense logics and intuitionistic logic extended by coimplication.

The basic logic in the extended language is called Heyting-Brouwer logic, $\mathbf{HB}$, and is axiomatised by adding to any standard Hilbert-style axiomatisation of $\mathbf{Int}$ the axioms (we set $\breve{\lnot } = p \breve{\rightarrow } \top$)

and the rule (RN): $p /\lnot \breve{\lnot }p$. $\mathbf{HB}$ and its first-order extensions have been investigated in [61–63].

In the same way as intuitionistic logic, $\mathbf{HB}$ is determined by Kripke frames that are partial orders and in which

• $w\models \varphi \breve{\rightarrow } \psi$ iff there exists $v$ with $vRw$, $v\models \psi$, and $v\not \models \varphi$.

An algebraic semantics for $\mathbf{HB}$ is given by Heyting-Brouwer algebras (aka double Heyting algebras, biHeyting-algebras, and Semi-Boolean algebras) which have been investigated in, for example, [39, 45, 62]. For recent progress in proof theory for $\mathbf{HB}$ we refer the reader to [8, 29, 58] (where, mostly, $\mathbf{HB}$ is called bi-intuitionistic logic).

The basic tense logic into which $\mathbf{HB}$ is embedded by $T$ is called $\mathbf{S4.t}$. It is the normal bimodal logic with operators $\Box _{F}$ and $\Box _{P}$ (and their duals $\Diamond _{F}$ and $\Diamond _{P}$) which both satisfy the axioms for $\mathbf{S4}$ and the Priorean tense axioms

$$ p \rightarrow \Box _{P}\Diamond _{F}p \quad \text {and} \quad p \rightarrow \Box _{F}\Diamond _{P}p. $$

In the same way as $\mathbf{S4}$, the tense logic $\mathbf{S4.t}$ is determined by Kripke frames that are quasi-orders. The following equivalence follows directly from completeness with respect to Kripke semantics: for all $\varphi$,

$$ \varphi \in \mathbf{HB} \quad \text{ iff } \quad T(\varphi )\in \mathbf{S4.t}. $$

We now extend the mappings $\tau$, $\rho$, and $\sigma$ between si-logics and normal extensions of $\mathbf{S4}$ to normal extensions of $\mathbf{HB}$ and $\mathbf{S4.t}$. A normal super-Heyting-Brouwer logic (shb-logic) is an extension of $\mathbf{HB}$ that is closed under modus ponens, substitution, and (RN). By NExt$L$ we denote the lattice of shb-logics containing a shb-logic $L$. For a set $\varGamma$ of intuitionistic formulas with coimplication, we denote by $\mathbf{HB}\oplus \varGamma$ the smallest shb-logic containing $\varGamma$. Similarly, a normal extension of $\mathbf{S4.t}$ is an extension of $\mathbf{S4.t}$ closed under substitution, modus ponens, $p/\Box _{P}p$, and $p/\Box _{F}p$. By NExt$L$ we denote the lattice of normal tense logics containing a normal tense logic $L$ and by $L\oplus \varGamma$ we denote the smallest normal extension of $L$ containing $\varGamma$.

The analogue of $\mathbf{Grz}$ in tense logic is given by $\mathbf{Grz.t}$, which is obtained from $\mathbf{S4.t}$ by setting

$$ \mathbf{Grz.t} = \mathbf{S4.t} \oplus \{\Box _{F} ( \Box _{F} ( p \rightarrow \Box _{F} p) \rightarrow p) \rightarrow p, \Box _{P} ( \Box _{P} ( p \rightarrow \Box _{P} p) \rightarrow p) \rightarrow p\}. $$

Note that we use the axiom for $\mathbf{Grz}$ for the future and the past. Using it for the future only would give a weaker logic without the finite model property [74] which is a tense companion of $\mathbf{HB}$ but not sufficiently strong for a Blok-Esakia theorem. We set

• for $L= \mathbf{HB} \oplus \varGamma$, $\tau L = \mathbf{S4.t}\oplus \{T(\varphi ) \mid \varphi \in \varGamma \}$,

• for $M\in \text{ NExt }\mathbf{S4.t}$, $\rho M=\{\varphi \mid T(\varphi )\in M\}$,

• for $L \in \text{ NExt }\mathbf{HB}$, $\sigma L = \mathbf{Grz.t}\oplus \tau L$.

Now, using an extension of the algebraic methods used in Blok’s thesis, the following is shown in [75]:

• 1. The map $\rho$ is a lattice homomorphism from $\text{ NExt }\mathbf{S4.t}$ onto $\text{ NExt }\mathbf{HB}$; $\tau$ is a lattice isomorphism from $\text{ NExt }\mathbf{HB}$ into $\text{ NExt }\mathbf{S4.t}$. The three maps $\rho$, $\tau$ and $\sigma$ preserve infinite sums and intersections of logics.

• 2. The map $\sigma$ is a lattice isomorphism from $\text{ NExt }\mathbf{HB}$ onto $\text{ NExt }\mathbf{S4.t}$.

Wolter [75] also considers extensions of those mappings and the Blok-Esakia theorem to non-normal super Heyting-Brouwer logics [logics that are not closed under (RN)] and modal extensions of super Heyting-Brouwer logic. However, in contrast to the situation for si-logics, the preservation properties of those mappings have not yet been investigated in any detail.