FAILURE OF ESAKIA’S THEOREM IN THE MONADIC SETTING

GURAM BEZHANISHVILI; LUCA CARAI

doi:10.1017/jsl.2026.10223

FAILURE OF ESAKIA’S THEOREM IN THE MONADIC SETTING

Part of: General logic

Published online by Cambridge University Press: 19 June 2026

GURAM BEZHANISHVILI

and

LUCA CARAI

Show author details

GURAM BEZHANISHVILI: Affiliation:
DEPARTMENT OF MATHEMATICAL SCIENCES NEW MEXICO STATE UNIVERSITY LAS CRUCES, NM 88003 USA E-mail: guram@nmsu.edu
LUCA CARAI*: Affiliation:
DIPARTIMENTO DI MATEMATICA “FEDERIGO ENRIQUES” UNIVERSITÀ DEGLI STUDI DI MILANO VIA CESARE SALDINI 50 20133 MILAN ITALY
*: E-mail: luca.carai.uni@gmail.com

Article contents

Abstract
Introduction
Preliminaries
Global Kuroda logic
Local Kuroda logic
Failure of Esakia’s theorem for MIPC$\mathsf {MIPC}$
Conclusions
Footnotes
References

Rights & Permissions

Abstract

Esakia’s theorem states that Grzegorczyk’s logic is the greatest modal companion of intuitionistic propositional calculus. We prove that already the one-variable fragment of intuitionistic predicate calculus does not have a greatest modal companion, yielding that Esakia’s theorem fails in the monadic setting.

Keywords

Intuitionistic logic modal logic Gödel translation modal companion

MSC classification

Primary: 03B20: Subsystems of classical logic (including intuitionistic logic) 03B45: Modal logic (including the logic of norms) 03B55: Intermediate logics

Information

Type: Article
Information: The Journal of Symbolic Logic , First View , pp. 1 - 22

DOI: https://doi.org/10.1017/jsl.2026.10223 [Opens in a new window]
Creative Commons: This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright: © The Author(s), 2026. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

1 Introduction

In [Reference Gödel21] Gödel suggested to interpret intuitionistic logic as a fragment of modal logic. McKinsey and Tarski [Reference McKinsey and Tarski26] proved that the Gödel translation embeds the intuitionistic propositional calculus $\mathsf {IPC}$ faithfully into the modal logic $\mathsf {S4}$ . There are many other modal logics above $\mathsf {S4}$ into which $\mathsf {IPC}$ embeds faithfully, known as modal companions of $\mathsf {IPC}$ (see, e.g., [Reference Chagrov and Zakharyaschev10, Section 9.6]). It is a well-known result of Esakia [Reference Esakia12] that the Grzegorczyk logic $\mathsf {Grz}$ is the greatest modal companion of $\mathsf {IPC}$ .

The situation becomes more complicated in the predicate case. Let $\mathsf {IQC}$ be the intuitionistic predicate calculus, $\mathsf {QS4}$ the predicate $\mathsf {S4}$ , and $\mathsf {QGrz}$ the predicate Grzegorczyk logic. It is a well-known result of Rasiowa and Sikorski [Reference Rasiowa and Sikorski32] that the Gödel translation embeds $\mathsf {IQC}$ faithfully into $\mathsf {QS4}$ . In [Reference Pankratyev30] it is claimed that it also embeds $\mathsf {IQC}$ faithfully into $\mathsf {QGrz}$ , and in [Reference Naumov28] it is claimed that $\mathsf {QGrz}$ is no longer the greatest modal companion of $\mathsf {IQC}$ (see also [Reference Gabbay, Shehtman and Skvortsov20, Theorem 2.11.14]). However, the proofs in [Reference Naumov28, Reference Pankratyev30] use the Flagg–Friedman translation [Reference Flagg and Friedman18] of $\mathsf {QS4}$ to $\mathsf {IQC}$ , which Inoué [Reference Inoué24] showed is not faithful.Footnote ¹ In fact, as we will see in Theorem 6.5, the extension of $\mathsf {QGrz}$ considered by Naumov is not a modal companion of $\mathsf {IQC}$ . Nevertheless, as we will see in Theorem 5.10, the monadic fragment of $\mathsf {IQC}$ , where we only consider formulas with one fixed variable, does not have a greatest modal companion. The full predicate version requires further examination (see Remark 6.6).

The study of the monadic fragment of classical predicate calculus was initiated by Hilbert and Ackermann [Reference Hilbert and Ackermann23], and Wajsberg [Reference Wajsberg34] proved that $\mathsf {S5}$ axiomatizes this fragment. Prior [Reference Prior31] introduced the monadic intuitionistic calculus $\mathsf {MIPC}$ , and Bull [Reference Bull9] proved that it axiomatizes the monadic fragment of $\mathsf {IQC}$ . The monadic fragment of $\mathsf {QS4}$ is axiomatized by $\mathsf {MS4}$ and that of $\mathsf {QGrz}$ by $\mathsf {MGrz}$ (see [Reference Bezhanishvili and Khan6, Reference Esakia13, Reference Fischer Servi15]). The Gödel translation embeds $\mathsf {MIPC}$ faithfully into both $\mathsf {MS4}$ and $\mathsf {MGrz}$ , but our main result shows that there is no greatest modal companion of $\mathsf {MIPC}$ , thus yielding a failure of Esakia’s theorem in the monadic setting.

We achieve this by introducing modal versions of the monadic Kuroda formula. The Kuroda formula ${\forall x\neg \neg P(x)\to \neg \neg \forall x P(x)}$ is not provable in $\mathsf {IQC}$ . Heyting considered this as one of the most striking features of $\mathsf {IQC}$ (see [Reference Heyting22, p. 108]). We introduce two natural modal versions of the monadic Kuroda formula ${\forall \neg \neg p\to \neg \neg \forall p}$ , which result in two extensions of $\mathsf {MS4}$ that we term the global and local Kuroda logics. The global Kuroda logic $\mathsf {GKur}$ is obtained by adding the Gödel translation of $\forall \neg \neg p\to \neg \neg \forall p$ to $\mathsf {MS4}$ , while the local Kuroda logic $\mathsf {LKur}$ is an appropriate weakening of $\mathsf {GKur}$ . We prove that $\mathsf {GKur}$ is a modal companion of $\mathsf {MIPC}+\forall \neg \neg p\to \neg \neg \forall p$ , that $\mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ , and that $\mathsf {LKur}$ is not comparable with $\mathsf {MGrz}$ . In addition, $\mathsf {MGrz}\vee \mathsf {LKur}=\mathsf {MGrz}\vee \mathsf {GKur}$ , thus yielding that $\mathsf {MIPC}$ can’t have the greatest modal companion.

We conclude the introduction by providing a brief semantic explanation of the validity of Esakia’s theorem in the propositional case and why it fails in the monadic case. An adequate semantics for $\mathsf {IPC}$ is given by the category $\mathbf {DF}_{\mathsf {IPC}}$ of descriptive intuitionistic frames and that for $\mathsf {S4}$ by the category $\mathbf {DF}_{\mathsf {S4}}$ of descriptive $\mathsf {S4}$ -frames (see, e.g., [Reference Chagrov and Zakharyaschev10, Theorem 8.36]). There is an embedding $\sigma \colon \mathbf {DF}_{\mathsf {IPC}} \to \mathbf {DF}_{\mathsf {S4}}$ , which has a left adjoint $\rho \colon \mathbf {DF}_{\mathsf {S4}} \to \mathbf {DF}_{\mathsf {IPC}}$ such that $\mathfrak {F} \cong \rho \sigma \mathfrak {F}$ for each $\mathfrak {F} \in \mathbf {DF}_{\mathsf {IPC}}$ (see, e.g., [Reference Chagrov and Zakharyaschev10, Sections 8.3 and 8.4] or [Reference Esakia, Bezhanishvili and Holliday14, Sections 2.2 and 2.5] for the algebraic formulation). If $\mathsf {M}$ is a modal companion of $\mathsf {IPC}$ , then for each $\mathfrak {F} \in \mathbf {DF}_{\mathsf {IPC}}$ there is $\mathfrak {G} \in \mathbf {DF}_{\mathsf {S4}}$ such that $\mathfrak {G} \vDash \mathsf {M}$ and $\mathfrak {F} \cong \rho \mathfrak {G}$ . This implies that $\sigma \mathfrak {F} \vDash \mathsf {M}$ . But $\mathsf {Grz}$ is the logic of $\{ \sigma \mathfrak {F} : \mathfrak {F} \in \mathbf {DF}_{\mathsf {IPC}}\}$ . Thus, $\mathsf {M} \subseteq \mathsf {Grz}$ , yielding Esakia’s theorem.

In the monadic case, an adequate semantics for $\mathsf {MIPC}$ is given by the category $\mathbf {DF}_{\mathsf {MIPC}}$ of descriptive $\mathsf {MIPC}$ -frames and that for $\mathsf {MS4}$ by the category $\mathbf {DF}_{\mathsf {MS4}}$ of descriptive $\mathsf {MS4}$ -frames. We still have a functor $\rho \colon \mathbf {DF}_{\mathsf {MS4}} \to \mathbf {DF}_{\mathsf {MIPC}}$ (see Theorem 3.6(3)). However, the analogue of $\sigma $ is no longer well defined, and it remains open whether $\rho $ has a right adjoint. It is this lack of a nice semantic correspondence in the monadic case that is responsible for the failure of Esakia’s theorem (as well as that of the Blok–Esakia theorem [Reference Bezhanishvili and Carai5]). We further discuss this in the conclusions, after establishing our main results.

2 Preliminaries

In this section we briefly recall $\mathsf {MIPC}$ , $\mathsf {MS4}$ , $\mathsf {MGrz,}$ and their semantics. Let $\mathcal {L_{\forall \exists }}$ be a propositional bimodal language, where the modalities are denoted by $\forall $ and $\exists $ .

Definition 2.1.

(1) The monadic intuitionistic propositional calculus $\mathsf {MIPC}$ is the smallest set of formulas of $\mathcal {L_{\forall \exists }}$ containing
1. (a) all theorems of $\mathsf {IPC}$ ;
2. (b) $\mathsf {S4}$ -axioms for $\forall $ : $\forall (p\land q)\leftrightarrow (\forall p\land \forall q)$ , $\forall p \rightarrow p$ , $\forall p \rightarrow \forall \forall p$ ;
3. (c) $\mathsf {S5}$ -axioms for $\exists $ : $\exists (p\vee q)\leftrightarrow (\exists p\vee \exists q)$ , $p \rightarrow \exists p$ , $\exists \exists p \rightarrow \exists p$ , $(\exists p \land \exists q) \rightarrow \exists (\exists p \land q)$ ;
4. (d) connecting axioms: $\exists \forall p\rightarrow \forall p$ , $\exists p \rightarrow \forall \exists p$ ;
and closed under modus ponens, substitution, and necessitation $(\varphi / \forall \varphi )$ .
(2) An extension of $\mathsf {MIPC}$ is a set of formulas of $\mathcal {L_{\forall \exists }}$ containing $\mathsf {MIPC}$ and closed under the above rules of inference.

Kripke semantics for $\mathsf {MIPC}$ was introduced in [Reference Ono29] (see also [Reference Fischer Servi17]). We recall that a quasi-order is a reflexive and transitive binary relation. Given a quasi-order $Q$ on a set $X$ , we recall that $U \subseteq X$ is a Q-upset if $x\in U$ and $xQy$ imply $y\in U$ .

Convention 2.2. For a quasi-order $Q$ on a set $X$ , we denote by $E_Q$ the equivalence relation defined by

$$ \begin{align*} x E_Q y \iff xQy \text{ and } yQx. \end{align*} $$

Definition 2.3. An $\mathsf {MIPC}$ -frame is a tuple $\mathfrak {F}=(X,R,Q)$ such that

(1) $R$ is a partial order on $X$ ;
(2) $Q$ is a quasi-order on $X$ ;
(3) $R \subseteq Q$ ;
(4) $x Q y \Longrightarrow \exists z \in X : x R z \; \& \; z E_Q y$ .

Commutative diagram showing a solid arrow Q from x to y, a dashed arrow R from x to there exists z, and a dashed line E sub Q between there exists z and y.

$\mathsf {MIPC}$ -frames provide a relational semantics for $\mathsf {MIPC}$ that extends the usual Kripke semantics for $\mathsf {IPC}$ (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev19, Section 10.2]). Let $\mathfrak {F}=(X,R,Q)$ be an $\mathsf {MIPC}$ -frame. A valuation on $\mathfrak {F}$ is a map associating an $R$ -upset to each propositional letter. To see how $\forall $ and $\exists $ are being interpreted in $\mathfrak {F}$ , let $x \in X$ and $v$ be a valuation on $\mathfrak {F}$ . Then, for each formula $\varphi $ of $\mathcal {L_{\forall \exists }}$ ,

$$ \begin{align*} x \vDash_v \forall \varphi & \iff (\forall y \in X) (x Q y \Rightarrow y \vDash_v \varphi);\\ x \vDash_v \exists \varphi & \iff (\exists y \in X) (x E_Q y \; \& \; y \vDash_v \varphi). \end{align*} $$

In [Reference Bull8] it was proved that $\mathsf {MIPC}$ has the finite model property (fmp for short). The proof contained a gap, which was corrected in [Reference Fischer Servi16, Reference Ono29]. As a consequence, we obtain the following theorem.

Theorem 2.4. $\mathsf {MIPC}$ is Kripke complete.

Since not every extension of $\mathsf {MIPC}$ is Kripke complete, we require a more general semantics using descriptive frames. Let $X$ be a topological space. We recall that a subset $U$ of $X$ is clopen if it is both closed and open, and that $X$ is zero-dimensional if clopen sets form a basis for $X$ . We also recall that $X$ is a Stone space if it is compact, Hausdorff, and zero-dimensional. A binary relation $R$ on $X$ is continuous provided that the image $R[x] := \{ y \in X : xRy \}$ is closed for each $x\in X$ and the inverse image $R^{-1}[U] := \{ y\in X : yRx$ for some $x\in U\}$ is clopen for each clopen $U$ of $X$ .

Definition 2.5. An $\mathsf {MIPC}$ -frame $\mathfrak F=(X,R,Q)$ is a descriptive $\mathsf {MIPC}$ -frame if $X$ is equipped with a Stone topology such that

(1) $R$ is a continuous partial order;
(2) $Q$ is a continuous quasi-order;
(3) if $U$ is a clopen $R$ -upset, then $Q[U]$ is a clopen $R$ -upset.

Definition 2.6. Let $\mathfrak {F}_1=(X_1,R_1,Q_1)$ and $\mathfrak {F}_2=(X_2,R_2,Q_2)$ be descriptive $\mathsf {MIPC}$ -frames. A map $f \colon X_1 \to X_2$ is a morphism of descriptive $\mathsf {MIPC}$ -frames if

(1) $f$ is continuous;
(2) $R_2[f(x)]=fR_1[x]$ for each $x \in X_1$ ;
(3) $Q_2[f(x)]=fQ_1[x]$ for each $x \in X_1$ ;
(4) $Q_2^{-1}[f(x)]= R_2^{-1}fQ_1^{-1}[x]$ for each $x\in X_1$ .

Remark 2.7. In other words, parts (2) and (3) of Definition 2.6 say that $f$ is a p-morphism with respect to both $R$ and $Q$ , while part (4) is weaker than saying that $f$ is a p-morphism with respect to the inverse of $Q$ .

Definition 2.8. Let $\mathbf {DF}_{\mathsf {MIPC}}$ be the category of descriptive $\mathsf {MIPC}$ -frames and their morphisms.

Remark 2.9. It is straightforward to see that isomorphisms in $\mathbf {DF}_{\mathsf {MIPC}}$ are homeomorphisms that preserve and reflect $R$ and $Q$ .

The algebraic semantics for $\mathsf {MIPC}$ is given by monadic Heyting algebras [Reference Monteiro and Varsavsky27]. Since descriptive $\mathsf {MIPC}$ -frames are exactly the duals of monadic Heyting algebras [Reference Bezhanishvili1, Theorem 17], by interpreting formulas as clopen $R$ -upsets of descriptive $\mathsf {MIPC}$ -frames, we obtain the following theorem.

Theorem 2.10. Each extension of $\mathsf {MIPC}$ is complete with respect to its class of descriptive $\mathsf {MIPC}$ -frames.

Remark 2.11. Because of Theorem 2.10 we mainly work with descriptive $\mathsf {MIPC}$ -frames, although most of our results can also be formulated in the language of monadic Heyting algebras.

We next turn our attention to $\mathsf {MS4}$ . Let $\mathcal {L}_{\Box \forall }$ be a propositional bimodal language with two modalities $\Box $ and $\forall $ . As usual, $\Diamond $ abbreviates $\neg \Box \neg $ and $\exists $ abbreviates $\neg \forall \neg $ .

Definition 2.12.

(1) The monadic $\mathsf {S4}$ , denoted $\mathsf {MS4}$ , is the smallest set of formulas of $\mathcal {L}_{\Box \forall }$ containing all theorems of the classical propositional calculus $\mathsf {CPC}$ , the $\mathsf {S4}$ -axioms for $\Box $ , the $\mathsf {S5}$ -axioms for $\forall $ , the left commutativity axiom
$$\begin{align*}\Box \forall p \to \forall \Box p, \end{align*}$$

and closed under modus ponens, substitution, $\Box $ -necessitation, and $\forall $ -necessitation.
(2) An extension of $\mathsf {MS4}$ is a set of formulas of $\mathcal {L}_{\Box \forall }$ containing $\mathsf {MS4}$ and closed under the above rules of inference.

Remark 2.13. We let $\blacksquare $ denote the compound modality $\Box \forall $ . It is immediate from the definition of $\mathsf {MS4}$ that $\blacksquare $ is an $\mathsf {S4}$ -modality and that both $\blacksquare p \to \Box p$ and $\blacksquare p \to \forall p$ are provable in $\mathsf {MS4}$ . Therefore, $\blacksquare $ is a master modality for $\mathsf {MS4}$ (see, e.g., [Reference Kracht25, p. 71]).

We will mainly be interested in the following extension of $\mathsf {MS4}$ .

Definition 2.14. The monadic Grzegorczyk logic, denoted $\mathsf {MGrz}$ , is the smallest extension of $\mathsf {MS4}$ containing the Grzegorczyk axiom

$$\begin{align*}\mathsf{grz} = \Box(\Box(p\to\Box p)\to p)\to p. \end{align*}$$

Kripke semantics for extensions of $\mathsf {MS4}$ was introduced by Esakia [Reference Esakia13]. To avoid confusion, we write $\mathfrak {F}=(X,R,Q)$ for an $\mathsf {MIPC}$ -frame and $\mathfrak {G}=(Y,R,E)$ for an $\mathsf {MS4}$ -frame.

Definition 2.15. An $\mathsf {MS4}$ -frame is a tuple $\mathfrak {G}=(Y,R,E)$ such that

(1) $R$ is a quasi-order on $Y$ ;
(2) $E$ is an equivalence relation on $Y$ ;
(3) $x E y \; \& \; y R z \Longrightarrow \exists u \in Y : x R u \; \& \; u E z$ .

$$ \begin{align*}includegraphics{JSL_2610223-FIGU0002-BW} \end{align*} $$ i n c l u d e g r a p h i c s upper J upper S upper L 2 Baseline 610223 minus upper F upper I upper G upper U Baseline 0002 minus upper B upper W

i n c l u d e g r a p h i c s upper J upper S upper L 2 Baseline 610223 minus upper F upper I upper G upper U Baseline 0002 minus upper B upper W

Kripke semantics for $\mathsf {S4}$ naturally extends to a relational semantics for $\mathsf {MS4}$ by interpreting the modality $\forall $ in $\mathsf {MS4}$ -frames via the equivalence relation $E$ . A valuation on an $\mathsf {MS4}$ -frame $\mathfrak {G}=(Y,R,E)$ is a map associating a subset of $Y$ to each propositional letter. Then, for each $x \in Y$ and formula $\varphi $ of $\mathcal {L}_{\Box \forall }$ , we have

$$ \begin{align*} x \vDash_v \Box \varphi & \iff (\forall y \in Y) (x R y \Rightarrow y \vDash_v \varphi);\\ x \vDash_v \forall \varphi & \iff (\forall y \in Y) (x E y \Rightarrow y \vDash_v \varphi). \end{align*} $$

Since both $\mathsf {MS4}$ and $\mathsf {MGrz}$ have the fmp (for the fmp of $\mathsf {MS4}$ see [Reference Bezhanishvili and Carai4, Section 6] and the references therein, and for the fmp of $\mathsf {MGrz}$ see [Reference Bezhanishvili and Khan6]), we obtain the following theorem.

Theorem 2.16. $\mathsf {MS4}$ and $\mathsf {MGrz}$ are Kripke complete.

As with extensions of $\mathsf {MIPC}$ , there are extensions of $\mathsf {MS4}$ that are Kripke incomplete. We thus work with descriptive $\mathsf {MS4}$ -frames.

Definition 2.17. An $\mathsf {MS4}$ -frame $\mathfrak G=(Y,R,E)$ is a descriptive $\mathsf {MS4}$ -frame if $Y$ is equipped with a Stone topology such that

(1) $R$ is a continuous quasi-order;
(2) $E$ is a continuous equivalence relation.

Definition 2.18. Let $\mathfrak {G}_1=(Y_1,R_1,E_1)$ and $\mathfrak {G}_2=(Y_2,R_2,E_2)$ be descriptive $\mathsf {MS4}$ -frames. A map $f \colon Y_1 \to Y_2$ is a morphism of descriptive $\mathsf {MS4}$ -frames if

(1) $f$ is continuous;
(2) $R_2[f(x)]=fR_1[x]$ for each $x \in Y_1$ ;
(3) $E_2[f(x)]=fE_1[x]$ for each $x \in Y_1$ .

Remark 2.19. Parts (2) and (3) of Definition 2.18 say that $f$ is a p-morphism with respect to both $R$ and $E$ .

Definition 2.20. Let $\mathbf {DF}_{\mathsf {MS4}}$ be the category of descriptive $\mathsf {MS4}$ -frames and their morphisms.

Remark 2.21. It is straightforward to see that isomorphisms in $\mathbf {DF}_{\mathsf {MS4}}$ are homeomorphisms that preserve and reflect $R$ and $E$ .

Convention 2.22. For an $\mathsf {MS4}$ -frame $(Y,R,E)$ , we denote by $Q_E$ the composition $E \circ R$ given by

$$ \begin{align*} x Q_E y \iff \exists z \in Y : x R z \text{ and } z E y. \end{align*} $$

Remark 2.23. We briefly compare $\mathsf {MIPC}$ -frames and $\mathsf {MS4}$ -frames. In an $\mathsf {MIPC}$ -frame $(X,R,Q)$ it is the quasi-order $Q$ that is primary and the equivalence relation $E_Q$ is defined from $Q$ . On the other hand, in an $\mathsf {MS4}$ -frame $(Y,R,E)$ it is the equivalence relation $E$ that is primary and the quasi-order $Q_E$ is defined from $E$ and $R$ . Nevertheless, there is a close connection between $\mathsf {MIPC}$ -frames and $\mathsf {MS4}$ -frames. Indeed, it follows from [Reference Bezhanishvili1, Section 2] that if $(X,R,Q)$ is an $\mathsf {MIPC}$ -frame, then $(X,R,E_Q)$ is an $\mathsf {MS4}$ -frame. Conversely, if $(Y,R,E)$ is an $\mathsf {MS4}$ -frame such that $R$ is a partial order, then $(Y,R,Q_E)$ is an $\mathsf {MIPC}$ -frame such that $E \subseteq E_{Q_E}$ , but in general $E \ne E_{Q_E}$ (see [Reference Bezhanishvili1, p. 24]). Therefore, this correspondence restricts to a bijection between $\mathsf {MIPC}$ -frames and those partially ordered $\mathsf {MS4}$ -frames in which $E = E_{Q_E}$ . (Note that $Q=Q_{E_Q}$ in every $\mathsf{MIPC}$ -frame.) Since every finite partially ordered $\mathsf {MS4}$ -frame is such (see [Reference Bezhanishvili1, Lemma 3(b)]), the correspondence further restricts to a bijection between finite $\mathsf {MIPC}$ -frames and finite partially ordered $\mathsf {MS4}$ -frames. But this bijection does not extend to an equivalence of the corresponding categories (viewed as full subcategories of $\mathbf {DF}_{\mathsf {MIPC}}$ and $\mathbf {DF}_{\mathsf {MS4}}$ , respectively) because a morphism between finite $\mathsf {MIPC}$ -frames is not necessarily a morphism between the corresponding finite $\mathsf {MS4}$ -frames. Furthermore, the bijection between finite $\mathsf {MIPC}$ -frames and finite partially ordered $\mathsf {MS4}$ -frames does not extend to descriptive frames. Indeed, there is a descriptive $\mathsf {MIPC}$ -frame $(X,R,Q)$ such that $(X,R,E_Q)$ is not a descriptive $\mathsf {MS4}$ -frame (see [Reference Bezhanishvili1, p. 32]). As we pointed out in the introduction (see also Section 6), it is this lack of balance between descriptive $\mathsf {MIPC}$ -frames and descriptive $\mathsf {MS4}$ -frames that will be responsible for the failure of the monadic version of Esakia’s theorem.

The algebraic semantics for $\mathsf {MS4}$ is given by monadic $\mathsf {S4}$ -algebras. It is a consequence of Jónsson–Tarski duality that descriptive $\mathsf {MS4}$ -frames are the duals of monadic $\mathsf {S4}$ -algebras (see, e.g., [Reference Bezhanishvili and Carai5, Theorem 3.11]). Thus, by interpreting formulas as clopen subsets of descriptive $\mathsf {MS4}$ -frames, we obtain the following theorem.

Theorem 2.24. Each extension of $\mathsf {MS4}$ is complete with respect to its class of descriptive $\mathsf {MS4}$ -frames.

In particular, $\mathsf {MGrz}$ is complete with respect to its descriptive frames, which we next recall.

Definition 2.25 (See, e.g., [Reference Esakia, Bezhanishvili and Holliday14, Definition 1.4.9]).

Let $R$ be a quasi-order on a set $X$ and $x \in X$ .

(1) We call $x$ maximal if $xRy$ implies $x=y$ . Let $\max X$ be the set of maximal points of $X$ .
(2) We call $x$ quasi-maximal if $xRy$ implies $yRx$ . Let $\mathrm {qmax}\ X$ be the set of quasi-maximal points of $X$ .

While the descriptive frames we work with have multiple relations, when we talk about maximal or quasi-maximal points, we always mean with respect to the relation $R$ . Esakia’s characterization of descriptive $\mathsf {Grz}$ -frames [Reference Esakia12] (see also [Reference Esakia, Bezhanishvili and Holliday14, Theorem 3.5.6]) yields the following characterization of descriptive $\mathsf {MGrz}$ -frames.

Theorem 2.26. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame. Then $\mathfrak {G}$ validates $\mathsf {MGrz}$ iff $\mathrm {qmax} U = \max U$ for every clopen $U \subseteq Y$ . In particular, a finite $\mathsf {MS4}$ -frame validates $\mathsf {MGrz}$ iff $R$ is a partial order.

We recall (see, e.g., [Reference Chagrov and Zakharyaschev10, p. 96]) that the Gödel translation $(-)^t$ of $\mathsf {IPC}$ into $\mathsf {S4}$ is defined by

$$ \begin{align*} & \bot^t = \bot\\ & p^t = \Box p \quad \mbox{for each propositional letter } p \\ & (\varphi \land \psi)^t = \varphi^t \land \psi^t \\ & (\varphi \lor \psi)^t = \varphi^t \lor \psi^t \\ & (\varphi \to \psi)^t = \Box (\neg \varphi^t \lor \psi^t). \end{align*} $$

StartLayout 1st Row 1st Column Blank 2nd Column normal up tack Superscript t Baseline equals normal up tack 2nd Row 1st Column Blank 2nd Column p Superscript t Baseline equals white medium square p for each propositional letter p 3rd Row 1st Column Blank 2nd Column left parenthesis phi and psi right parenthesis Superscript t Baseline equals phi Superscript t Baseline and psi Superscript t Baseline 4th Row 1st Column Blank 2nd Column left parenthesis phi or psi right parenthesis Superscript t Baseline equals phi Superscript t Baseline or psi Superscript t Baseline 5th Row 1st Column Blank 2nd Column left parenthesis phi right arrow psi right parenthesis Superscript t Baseline equals white medium square left parenthesis not phi Superscript t Baseline or psi Superscript t Baseline right parenthesis period EndLayout

Fischer Servi [Reference Fischer Servi15] (see also [Reference Fischer Servi16]) extended the Gödel translation to a translation of $\mathsf {MIPC}$ into $\mathsf {MS4}$ as follows:

$$ \begin{align*} (\forall \varphi)^t &= \blacksquare \varphi^t \\ (\exists \varphi)^t &= \exists \varphi^t. \end{align*} $$ StartLayout 1st Row 1st Column left parenthesis for all phi right parenthesis Superscript t 2nd Column equals black medium square phi Superscript t Baseline 2nd Row 1st Column left parenthesis there exists phi right parenthesis Superscript t 2nd Column equals there exists phi Superscript t Baseline period EndLayout

As a consequence of the fmp of $\mathsf {MIPC}$ , we have the following theorem.

Theorem 2.27 [Reference Esakia13, Reference Fischer Servi15].

For each formula $\varphi $ of $\mathcal {L_{\forall \exists }}$ ,

$$\begin{align*}\mathsf{MIPC} \vdash \varphi \iff \mathsf{MS4} \vdash \varphi^t \iff \mathsf{MGrz} \vdash \varphi^t. \end{align*}$$

The notions of a modal companion and the intuitionistic fragment (see, e.g., [Reference Chagrov and Zakharyaschev10, Section 9.6]) have obvious generalizations to the monadic setting.

Definition 2.28. Let $\mathsf {L}$ be an extension of $\mathsf {MIPC}$ and $\mathsf {M}$ an extension of $\mathsf {MS4}$ . We say that $\mathsf {M}$ is a modal companion of $\mathsf {L}$ and that $\mathsf {L}$ is the intuitionistic fragment of $\mathsf {M}$ provided

$$\begin{align*}\mathsf{L}\vdash\varphi \iff \mathsf{M}\vdash\varphi^t \end{align*}$$

for every formula $\varphi $ of $\mathcal {L_{\forall \exists }}$ .

Using this terminology, Theorem 2.27 states that both $\mathsf {MS4}$ and $\mathsf {MGrz}$ are modal companions of $\mathsf {MIPC}$ . Our aim is to show that $\mathsf {MGrz}$ is not the greatest modal companion of $\mathsf {MIPC}$ .

3 Global Kuroda logic

In this and next sections we will introduce two extensions of $\mathsf {MS4}$ , which will be utilized in Section 5 to prove our main result. For this we will use the monadic version of the well-known Kuroda formula ${\forall x \, \neg \neg P(x) \to \neg \neg \forall x \, P(x)}$ , which plays an important role in negation translations of predicate logics (see, e.g., [Reference Gabbay, Shehtman and Skvortsov20, Section 2.12] and [Reference Troelstra and van Dalen33, Section 2.3]).

A semantic criterion of when the monadic version of Kuroda’s formula is satisfied in descriptive $\mathsf {MIPC}$ -frames was developed in [Reference Bezhanishvili2]. We refer to this condition as the Kuroda principle ( $\mathsf {KP}$ ) and show that there are two natural versions of it for descriptive $\mathsf {MS4}$ -frames, which we term the global $\mathsf {KP}$ ( $\mathsf {GKP}$ ) and the local $\mathsf {KP}$ ( $\mathsf {LKP}$ ). These two principles give rise to two extensions of $\mathsf {MS4}$ . We provide an axiomatization of both and describe their connection to the monadic Kuroda logic. In this section we concentrate on the $\mathsf {GKP}$ . The $\mathsf {LKP}$ will be treated in the next section.

Definition 3.1. Let $\mathsf {kur} := \forall \neg \neg p \to \neg \neg \forall p$ be the monadic Kuroda formula and $\mathsf {Kur}:=\mathsf {MIPC}+\mathsf {kur}$ the monadic Kuroda logic.

Definition 3.2. We say that a descriptive $\mathsf {MIPC}$ -frame $\mathfrak F=(X,R,Q)$ satisfies the $\mathsf {KP}$ if

$$\begin{align*}\forall x\in X\,(x \in \max X \Longrightarrow E_Q[x] \subseteq \max X); \end{align*}$$

equivalently, $E_Q[\max X]=\max X$ .

Theorem 3.3 [Reference Bezhanishvili2, Lemma 37].

A descriptive $\mathsf {MIPC}$ -frame validates $\mathsf {Kur}$ iff it satisfies $\mathsf {KP}$ .

$\mathsf {KP}$ has an obvious generalization to descriptive $\mathsf {MS4}$ -frames.

Definition 3.4. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame. We say that $\mathfrak {G}$ satisfies the $\mathsf {GKP}$ if

$$\begin{align*}\forall x \in Y\,(x\in\mathrm{qmax}\ Y \Longrightarrow E[x] \subseteq \mathrm{qmax}\ Y); \end{align*}$$

equivalently, $E[\mathrm {qmax} Y] = \mathrm {qmax} Y$ .

We next recall the notion of the skeleton of a descriptive $\mathsf {MS4}$ -frame $\mathfrak {G}$ and show that $\mathfrak {G}$ satisfies $\mathsf {GKP}$ exactly when its skeleton satisfies $\mathsf {KP}$ .

Definition 3.5 [Reference Bezhanishvili, Brantley and Ilin3, p. 439].

For an $\mathsf {MS4}$ -frame $\mathfrak {G}=(Y,R,E)$ , define its skeleton $\rho \hspace {0.08em}\mathfrak {G}=(X,R',Q')$ as follows. Let $X:= Y/E_R$ be the quotient of $Y$ by the equivalence relation $E_R$ on $Y$ induced by $R$ (see Convention 2.2), and let $\pi \colon Y \to X$ be the quotient map. Define $R'$ on $X$ by

$$\begin{align*}\pi(x) R' \pi(y) \iff x R y. \end{align*}$$

Also, let $Q_E=E \circ R$ (see Convention 2.22), and define $Q'$ on $X$ by

$$\begin{align*}\pi(x) Q' \pi(y) \iff x Q_E y. \end{align*}$$

Theorem 3.6.

(1) [Reference Bezhanishvili, Brantley and Ilin3, Lemma 3.3] If $\mathfrak {G}$ is an $\mathsf {MS4}$ -frame, then $\rho \hspace {0.08em}\mathfrak {G}$ is an $\mathsf {MIPC}$ -frame.
(2) [Reference Bezhanishvili and Carai5, Theorem 5.14] If $\mathfrak {G}$ is a descriptive $\mathsf {MS4}$ -frame, then $\rho \hspace {0.08em}\mathfrak {G}$ equipped with the quotient topology is a descriptive $\mathsf {MIPC}$ -frame.
(3) [Reference Bezhanishvili and Carai5, Lemma 5.15] The assignment $\mathfrak {G}\mapsto \rho \hspace {0.08em}\mathfrak {G}$ extends to a functor $\rho \hspace {0.08em} \colon \mathbf {DF}_{\mathsf {MS4}} \to \mathbf {DF}_{\mathsf {MIPC}}$ .
(4) [Reference Bezhanishvili and Carai4, Proposition 4.11(1)] Let $\varphi $ be a formula of $\mathcal {L_{\forall \exists }}$ and $\mathfrak {G}$ a (descriptive) $\mathsf {MS4}$ -frame. Then
$$ \begin{align*} \rho \hspace {0.08em}\mathfrak {G} \vDash \varphi \iff\mathfrak {G} \vDash \varphi ^t. \end{align*} $$
Footnote ²

We recall that each extension $\mathsf {L}$ of $\mathsf {IPC}$ has a least modal companion $\tau \mathsf {L}$ (see, e.g., [Reference Chagrov and Zakharyaschev10, Corollary 9.58]). We generalize the definition of $\tau $ to the monadic setting.

Definition 3.7. For an extension $\mathsf {L}$ of $\mathsf {MIPC}$ , let $\tau \mathsf {L}$ be the extension of $\mathsf {MS4}$ defined by

$$\begin{align*}\tau\mathsf{L} := \mathsf{MS4} + \{\varphi^t : \mathsf{L} \vdash \varphi \}. \end{align*}$$

The following is an immediate consequence of Theorem 3.6(4).

Corollary 3.8. Let $\mathsf {L}$ be an extension of $\mathsf {MIPC}$ and $\mathfrak {G}$ a (descriptive) $\mathsf {MS4}$ -frame. Then

$$\begin{align*}\rho \hspace{0.08em}\mathfrak{G} \vDash \mathsf{L} \iff \mathfrak{G} \vDash \tau\mathsf{L}. \end{align*}$$

Proposition 3.9. Let $\Gamma $ be a set of formulas of $\mathcal {L_{\forall \exists }}$ . Then

$$\begin{align*}\tau(\mathsf{MIPC}+\Gamma)=\mathsf{MS4}+\{\gamma^t : \gamma \in \Gamma\}. \end{align*}$$

Proof. Let $\mathfrak {G}$ be a descriptive $\mathsf {MS4}$ -frame. Corollary 3.8 and Theorem 3.6(4) imply that

$$ \begin{align*} \mathfrak{G} \vDash \tau(\mathsf{MIPC}+\Gamma) \iff \rho \hspace{0.08em}\mathfrak{G} \vDash \mathsf{MIPC}+\Gamma \iff \mathfrak{G} \vDash \mathsf{MS4}+\{\gamma^t : \gamma \in \Gamma\}. \end{align*} $$

By Theorem 2.24, every extension of $\mathsf {MS4}$ is complete with respect to its class of descriptive $\mathsf {MS4}$ -frames. Thus, $\tau (\mathsf {MIPC}+\Gamma )=\mathsf {MS4}+\{\gamma ^t : \gamma \in \Gamma \}$ .

Remark 3.10. If $\mathsf {L}$ is an extension of $\mathsf {MIPC}$ , then it remains open whether $\tau \mathsf {L}$ is a modal companion of $\mathsf {L}$ .Footnote ³ The main issue here is the absence of a natural functor from $\mathbf {DF}_{\mathsf {MIPC}}$ to $\mathbf {DF}_{\mathsf {MS4}}$ that would allow to show that the functor $\rho \hspace {0.08em} \colon \mathbf {DF}_{\mathsf {MS4}} \to \mathbf {DF}_{\mathsf {MIPC}}$ is essentially surjective (i.e., every descriptive $\mathsf {MIPC}$ -frame is isomorphic to the skeleton of some descriptive $\mathsf {MS4}$ -frame). This is caused by the discrepancy between descriptive $\mathsf {MIPC}$ -frames and descriptive $\mathsf {MS4}$ -frames discussed in Remark 2.23.

Let $\mathsf {L}$ be an extension of $\mathsf {MIPC}$ . While we don’t know whether $\tau \mathsf {L}$ is a modal companion of $\mathsf {L}$ , we show that this is indeed the case provided $\mathsf {L}$ is Kripke complete.

Proposition 3.11. Let $\mathsf {L}$ be a Kripke complete extension of $\mathsf {MIPC}$ . Then $\tau \mathsf {L}$ is a modal companion of $\mathsf {L}$ .

Proof. It follows from the definition of $\tau \mathsf {L}$ that $\mathsf {L} \vdash \varphi $ implies $\tau \mathsf {L} \vdash \varphi ^t$ for every formula $\varphi $ of $\mathcal {L_{\forall \exists }}$ . To prove the reverse implication, suppose that $\mathsf {L} \nvdash \varphi $ . Since $\mathsf {L}$ is Kripke complete, there is an $\mathsf {MIPC}$ -frame $\mathfrak {F}=(X,R,Q)$ such that $\mathfrak {F} \vDash \mathsf {L}$ and $\mathfrak {F} \nvDash \varphi $ . By Remark 2.23, $\mathfrak {G}=(X,R,E_Q)$ is an $\mathsf {MS4}$ -frame such that $\rho \hspace {0.08em}\mathfrak {G}$ is isomorphic to $\mathfrak {F}$ . Therefore, $\mathfrak {G} \vDash \tau \mathsf {L}$ by Corollary 3.8, and $\mathfrak {G} \nvDash \varphi ^t$ by Theorem 3.6(4). Thus, $\tau \mathsf {L} \nvdash \varphi ^t$ .

Returning to $\mathsf {GKP}$ , we have the following lemma.

Lemma 3.12. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame.

(1) $E[\mathrm {qmax} Y] = E_{Q_E}[\mathrm {qmax} Y]$ .
(2) $\mathfrak {G}$ satisfies $\mathsf {GKP}$ iff
$$\begin{align*}\forall x \in Y\,(x\in\mathrm{qmax} Y \Longrightarrow E_{Q_E}[x] \subseteq \mathrm{qmax} Y); \end{align*}$$

equivalently, $E_{Q_E}[\mathrm {qmax} Y] = \mathrm {qmax} Y$ .

Proof. (1). The left-to-right inclusion is clear because $E \subseteq E_{Q_E}$ (see Remark 2.23). For the other inclusion, let $x \in \mathrm {qmax} Y$ , $y \in Y$ , and $xE_{Q_E}y$ . Then $x Q_E y$ , so there is $z \in Y$ with $xRz$ and $zEy$ . Since $x \in \mathrm {qmax} Y$ and $xRz$ , we have $z \in \mathrm {qmax} Y$ . Thus, $y \in E[\mathrm {qmax} Y]$ .

(2). This is immediate from (1).

Lemma 3.13. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame, $\rho \hspace {0.08em}\mathfrak {G} = (X,R',Q')$ , and ${\pi \colon Y \to X}$ the quotient map.

(1) $\pi ^{-1}[\max X]=\mathrm {qmax} Y$ .
(2) $\pi ^{-1}[E_{Q'}[A]]=E_{Q_E}[\pi ^{-1}[A]]$ for each $A \subseteq X$ .
(3) $\pi ^{-1}[E_{Q'}[\max X]]=E_{Q_E}[\mathrm {qmax} Y]$ .

Proof. (1). Let $y \in \pi ^{-1}[\max X]$ and $yRz$ for some $z \in Y$ . Then $\pi (y)R'\pi (z)$ , and hence $\pi (y)=\pi (z)$ because $\pi (y) \in \max X$ . Therefore, $z R y$ , and hence ${y \in \mathrm {qmax} Y}$ . Conversely, suppose that $y \in \mathrm {qmax} Y$ and $\pi (y) R' \pi (z)$ for some $z \in Y$ . Then $yRz$ , and so $zRy$ because $y \in \mathrm {qmax} Y$ . Thus, $y E_R z$ , which yields $\pi (y)=\pi (z)$ . Consequently, $\pi (y) \in \max X$ , and hence $y \in \pi ^{-1}[\max X]$ .

(2). By definition of $Q'$ , for each $y,z \in Y$ ,

$$\begin{align*}\pi(y) E_{Q'} \pi(z) \iff y E_{Q_E} z. \end{align*}$$

Therefore, $\pi ^{-1}[E_{Q'}[x]]=E_{Q_E}[\pi ^{-1}[x]]$ for each $x \in X$ . The result follows since $\pi ^{-1}$ , $E_{Q'}$ , and $E_{Q_E}$ commute with set-theoretic union.

(3). Applying (2) and (1),

$$\begin{align*}\pi^{-1}[E_{Q'}[\max X]]=E_{Q_E}[\pi^{-1}[\max X]] = E_{Q_E}[\mathrm{qmax} Y].\\[-37pt] \end{align*}$$

Proposition 3.14. A descriptive $\mathsf {MS4}$ -frame $\mathfrak {G}$ satisfies $\mathsf {GKP}$ iff $\rho \hspace {0.08em}\mathfrak {G}$ satisfies $\mathsf {KP}$ .

Proof. By Lemma 3.12(2), $\mathfrak {G}$ satisfies $\mathsf {GKP}$ iff $E_{Q_E}[\mathrm {qmax} Y]=\text{qmax} Y$ . On the other hand, by Definition 3.2, $\rho \hspace {0.08em}\mathfrak {G}=(X,R', Q')$ satisfies $\mathsf {KP}$ iff ${E_{Q'}[\max X] = \max X}$ . Thus, it is sufficient to show that $E_{Q_E}[\mathrm {qmax} Y]=\mathrm {qmax} Y$ iff $E_{Q'}[\max X] = \max X$ . Let $\pi \colon Y \to X$ be the quotient map. We have

$$\begin{align*}E_{Q_E}[\mathrm{qmax} Y]=\mathrm{qmax} Y &\iff \pi^{-1}[E_{Q'}[\max X]]=\pi^{-1}[\max X] \\ &\iff E_{Q'}[\max X] = \max X, \end{align*}$$

where the first equivalence follows from Lemma 3.13 and the second holds because $\pi $ is onto.

Definition 3.15. Let $\mathsf {GKur}=\tau (\mathsf {Kur})$ . We call $\mathsf {GKur}$ the global Kuroda logic.

Since $\mathsf {Kur}=\mathsf {MIPC} +\mathsf {kur}$ , as an immediate consequence of Proposition 3.9 we obtain the following proposition.

Proposition 3.16. $\mathsf {GKur}=\mathsf {MS4} + \mathsf {kur}^t$ .

The following theorem shows that $\mathsf {GKur}$ is semantically characterized by $\mathsf {GKP}$ .

Theorem 3.17. A descriptive $\mathsf {MS4}$ -frame validates $\mathsf {GKur}$ iff it satisfies $\mathsf {GKP}$ .

Proof. Let $\mathfrak {G}$ be a descriptive $\mathsf {MS4}$ -frame. Since $\mathsf {GKur} = \tau (\mathsf {Kur})$ , Corollary 3.8 yields that

$$\begin{align*}\rho \hspace{0.08em}\mathfrak{G} \vDash \mathsf{Kur} \iff \mathfrak{G} \vDash \mathsf{GKur}. \end{align*}$$

Theorem 3.3 implies that $\rho \hspace {0.08em}\mathfrak {G} \vDash \mathsf {Kur}$ iff $\rho \hspace {0.08em}\mathfrak {G}$ satisfies $\mathsf {KP}$ . By Proposition 3.14, $\rho \hspace {0.08em}\mathfrak {G}$ satisfies $\mathsf {KP}$ iff $\mathfrak {G}$ satisfies $\mathsf {GKP}$ . Thus, $\mathfrak {G} \vDash \mathsf {GKur}$ iff it satisfies $\mathsf {GKP}$ .

Remark 3.18. Since $\mathsf {GKP}$ is a purely order-theoretic condition that does not involve any topology, the class of monadic $\mathsf {S4}$ -algebras validating $\mathsf {GKur}$ is closed under taking canonical extensions. It follows that $\mathsf {GKur}$ is canonical, and hence Kripke complete (see, e.g., [Reference Chagrov and Zakharyaschev10, p. 135]). It is also natural to investigate whether $\mathsf {GKur}$ has the fmp and hence is decidable. Since this is less important for our current purposes, we leave it to future work.

Since $\mathsf {Kur}$ is Kripke complete (see [Reference Bezhanishvili2, p. 250]), as an immediate consequence of Proposition 3.11 we obtain the following theorem.

Theorem 3.19. $\mathsf {GKur}$ is a modal companion of $\mathsf {Kur}$ .

We end the section by providing a simple axiomatization of $\mathsf {GKur}$ . We abbreviate $\neg \blacksquare \neg $ by $\blacklozenge $ and point out that $\mathsf {MS4} \vdash \blacklozenge p \leftrightarrow \Diamond \exists p$ .

Proposition 3.20. $\mathsf {GKur} = \mathsf {MS4} + \blacksquare \Diamond \Box p \to \Diamond \blacksquare p = \mathsf {MS4} + \Box \blacklozenge p \to \blacklozenge \Box \Diamond p$ .

Proof. It is straightforward to check that

$$\begin{align*}\mathsf{MS4} \vdash \blacksquare \Diamond \Box p \to \Diamond \blacksquare p \iff \mathsf{MS4} \vdash \Box \blacklozenge p \to \blacklozenge \Box \Diamond p. \end{align*}$$

Therefore, we only show that $\mathsf {GKur} = \mathsf {MS4} + \blacksquare \Diamond \Box p \to \Diamond \blacksquare p$ . Since ${\mathsf {GKur} = \mathsf {MS4} + \mathsf {kur}^t} $ (see Proposition 3.16), it is sufficient to show that $ \mathsf {MS4} + \mathsf {kur}^t = \mathsf {MS4} + \blacksquare \Diamond \Box p \to \Diamond \Box \forall p. $ We have

$$\begin{align*}\mathsf{kur}^t=\Box (\blacksquare\Box \neg \Box \neg \Box p \to \Box\neg \Box\neg \blacksquare \Box p)=\Box (\blacksquare \Box \Diamond \Box p \to \Box\Diamond \blacksquare \Box p). \end{align*}$$

By necessitation,

$$\begin{align*}\mathsf{MS4} \vdash \Box (\blacksquare \Box \Diamond \Box p \to \Box\Diamond \blacksquare \Box p) \iff \mathsf{MS4} \vdash \blacksquare \Box \Diamond \Box p \to \Box\Diamond \blacksquare \Box p. \end{align*}$$

Since $\Box $ is an $\mathsf {S4}$ -modality and $\blacksquare $ is a master modality for $\mathsf {MS4}$ (see Remark 2.13), we have $\mathsf {MS4} \vdash \blacksquare \Box p \leftrightarrow \blacksquare p$ and $\mathsf {MS4} \vdash \Box \blacksquare p \leftrightarrow \blacksquare p$ . Thus, using equivalent replacement (see [Reference Chagrov and Zakharyaschev10, Theorem 3.65]),

$$ \begin{align*} \mathsf{MS4} \vdash \blacksquare \Box \Diamond \Box p \to \Box\Diamond \blacksquare \Box p & \iff \mathsf{MS4} \vdash \blacksquare \Diamond \Box p \to \Box\Diamond \blacksquare p\\ & \iff \mathsf{MS4} \vdash \blacksquare \Diamond \Box p \to \Diamond \blacksquare p, \end{align*} $$

where the last equivalence holds because $\mathsf {MS4} \vdash \blacksquare \varphi \to \Box \psi $ iff $\mathsf {MS4} \vdash \blacksquare \varphi \to \psi $ for any pair of formulas $\varphi ,\psi $ . Consequently, $\mathsf {MS4} + \mathsf {kur}^t = \mathsf {MS4} + \blacksquare \Diamond \Box p \to \Diamond \blacksquare p$ .

4 Local Kuroda logic

In this section we introduce the $\mathsf {LKP}$ and the corresponding logic, which will play a fundamental role in the proof of the failure of Esakia’s theorem in the monadic setting.

Definition 4.1. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame. We say that $\mathfrak {G}$ satisfies the $\mathsf {LKP}$ if

$$\begin{align*}\forall x \in Y\,(x\in\mathrm{qmax} Y \Longrightarrow \exists y \in E_R[x] : E[y] \subseteq \mathrm{qmax} Y). \end{align*}$$

Remark 4.2. While the $\mathsf {GKP}$ requires that the $E$ -equivalence class of each quasi-maximal point is inside $\mathrm {qmax} Y$ , the $\mathsf {LKP}$ asks that this only holds locally, meaning that each $E_R$ -equivalence class of a quasi-maximal point should contain a point whose $E$ -equivalence class is inside $\mathrm {qmax} Y$ . In the next proposition we show that the $\mathsf {GKP}$ is stronger than its local version.

Proposition 4.3. $\mathsf {GKP}$ is strictly stronger than $\mathsf {LKP}$ .

Proof. It is straightforward to see that $\mathsf {GKP}$ implies $\mathsf {LKP}$ . We describe a finite $\mathsf {MS4}$ -frame satisfying $\mathsf {LKP}$ but not $\mathsf {GKP}$ . Let $\mathfrak {H}=(Y,R,E)$ be the three-element frame depicted in Figure 1, where $R[a]=Y$ , $R[b]=R[c]=\{b,c\} = \mathrm {qmax} Y$ , $E[c]=\{c\}$ , and $E[a]=E[b]=\{a,b\}$ .

Figure 1

The frame $\mathfrak {H}$ .

A mathematical diagram showing a vertical arrow from node a pointing to a horizontal line that splits into two arrows pointing left to node b and right to node c. See long description.

Figure 1 Long description

The diagram consists of three black nodes labeled a, b, and c.

* Node a is at the bottom, enclosed within a large, tilted grey oval.

* A vertical arrow originates from node a and points upward to the center of a horizontal line.

* The horizontal line has arrowheads at both ends. The left arrowhead points to node b, which is also enclosed within the same tilted grey oval as node a.

* The right arrowhead points to node c, which is enclosed within a separate grey circle.

* The labels a, b, and c are placed outside their respective enclosing shapes.

It is straightforward to check that $\mathfrak {H}$ is an $\mathsf {MS4}$ -frame. Because it is finite, it is also a descriptive $\mathsf {MS4}$ -frame (whose topology is discrete). Since $a \in E[b]$ , $b \in \mathrm {qmax} Y$ , and $a \notin \mathrm {qmax} Y$ , we see that $\mathfrak {H}$ does not satisfy $\mathsf {GKP}$ . On the other hand, $c \in E_R[b]$ and $E[c] = \{ c \} \subseteq \mathrm {qmax} Y$ . Thus, $\mathfrak {H}$ satisfies $\mathsf {LKP}$ .

Remark 4.4.

(1) $\mathsf {KP}$ is equivalent to the condition that $E_Q[x]$ is clean for each $x \in \max X$ , meaning that $y,z \in E_Q[x]$ and $yRz$ imply $y=z$ (see [Reference Bezhanishvili, Brantley and Ilin3, Definition 3.6]).
(2) Similar equivalent conditions exist for both $\mathsf {GKP}$ and $\mathsf {LKP}$ . Call $E[x]$ in a descriptive $\mathsf {MS4}$ -frame quasi-clean if $y,z \in E[x]$ and $yRz$ imply $zRy$ . Then $\mathsf {GKP}$ is equivalent to the condition that $E[x]$ is quasi-clean for each ${x \in \mathrm {qmax} Y}$ . On the other hand, $\mathsf {LKP}$ is equivalent to the requirement that for each $x \in \mathrm {qmax} Y$ there is $y \in E_R[x]$ such that $E[y]$ is quasi-clean.

We next introduce the logic that is semantically characterized by $\mathsf {LKP}$ .

Definition 4.5. Let $ \mathsf {LKur} = \mathsf {MS4} + \blacksquare \Diamond \Box p \to \Diamond \forall p. $ We call $\mathsf {LKur}$ the local Kuroda logic.

Remark 4.6. It is straightforward to see that $\mathsf {LKur}$ can be equivalently defined as

$$\begin{align*}\mathsf{MS4} + \Box \exists p \to \blacklozenge \Box \Diamond p. \end{align*}$$

Lemma 4.7. $\mathsf {LKur} \subseteq \mathsf {GKur}$ .

Proof. Since $\mathsf {MS4} \vdash \Diamond \blacksquare p \to \Diamond \forall p$ , we have

$$\begin{align*}\mathsf{MS4} + \blacksquare \Diamond \Box p \to \Diamond \blacksquare p \vdash \blacksquare \Diamond \Box p \to \Diamond \forall p. \end{align*}$$

Thus, $\mathsf {LKur} \subseteq \mathsf {GKur}$ by Proposition 3.20.

To see that $\mathsf {LKP}$ gives a semantic characterization of $\mathsf {LKur}$ , we recall the following definition.

Definition 4.8. Let $\mathfrak {G}=(Y,R,E)$ be an $\mathsf {MS4}$ -frame and $A \subseteq Y$ . We let

$$ \begin{align*} \Diamond A & := R^{-1}[A] & \Box A & := \{ x\in Y : R[x] \subseteq A\}\\ \exists A & := E[A] & \forall A & := \{ x\in Y : E[x] \subseteq A\}\\ \blacklozenge A & := Q_E^{-1}[A] & \blacksquare A & := \{ x\in Y : Q_E[x] \subseteq A\}. \end{align*} $$

StartLayout 1st Row 1st Column lozenge upper A 2nd Column colon equals upper R Superscript negative 1 Baseline left bracket upper A right bracket 3rd Column white medium square upper A 4th Column colon equals StartSet x element of upper Y colon upper R left bracket x right bracket subset of or equal to upper A EndSet 2nd Row 1st Column there exists upper A 2nd Column colon equals upper E left bracket upper A right bracket 3rd Column for all upper A 4th Column colon equals StartSet x element of upper Y colon upper E left bracket x right bracket subset of or equal to upper A EndSet 3rd Row 1st Column black lozenge upper A 2nd Column colon equals upper Q Subscript upper E Superscript negative 1 Baseline left bracket upper A right bracket 3rd Column black medium square upper A 4th Column colon equals StartSet x element of upper Y colon upper Q Subscript upper E Baseline left bracket x right bracket subset of or equal to upper A EndSet period EndLayout

For a valuation $v$ on $\mathfrak {G}$ and a formula $\varphi $ of $\mathcal {L}_{\Box \forall }$ , we let $v(\varphi ) = \{y \in Y : y \vDash _v \varphi \}$ . The following is immediate.

Proposition 4.9. Let $\mathfrak {G}$ be an $\mathsf {MS4}$ -frame, $v$ a valuation on $\mathfrak {G} = (Y,R,E)$ , and $\varphi $ a formula of $\mathcal {L}_{\Box \forall }$ . For every $\bigcirc \in \{\Diamond , \Box , \exists , \forall , \blacklozenge , \blacksquare \}$ and $x \in Y$ ,

$$\begin{align*}x \vDash_v \bigcirc \varphi \iff x \in \bigcirc v(\varphi). \end{align*}$$

The following lemma is well known for descriptive $\mathsf {S4}$ -frames (see, e.g., [Reference Esakia, Bezhanishvili and Holliday14, Section 3.2]), and hence it also holds in descriptive $\mathsf {MS4}$ -frames.

Lemma 4.10. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame.

(1) $\mathrm {qmax} Y$ is a closed $R$ -upset.
(2) (Fine–Esakia) For every $x \in Y$ there is $y \in \mathrm {qmax} Y$ such that $xRy$ .

Recalling that $R$ -downsets are complements of $R$ -upsets, the following is a consequence of [Reference Esakia, Bezhanishvili and Holliday14, Lemma 3.2.20].

Proposition 4.11. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame and $U$ a closed $R$ -upset of $Y$ . If $x \notin U$ , then there is a clopen $R$ -downset $D$ of $Y$ such that $x \in D$ and $D \cap U = \varnothing $ .

Theorem 4.12. A descriptive $\mathsf {MS4}$ -frame validates $\mathsf {LKur}$ iff it satisfies $\mathsf {LKP}$ .

Proof. Let $\mathfrak {G}$ be a descriptive $\mathsf {MS4}$ -frame. Suppose that $\mathfrak {G}$ satisfies $\mathsf {LKP}$ . We show that $\mathfrak {G} \vDash \blacksquare \Diamond \Box p \to \Diamond \forall p$ . Let $V$ be a clopen subset of $\mathfrak {G}$ . Then $\blacksquare \Diamond \Box V$ consists of those points $x \in Y$ such that for every $y \in Q_E[x]$ there is $z \in R[y]$ with $R[z] \subseteq V$ . In particular, if $x$ is such a point and $y \in Q_E[x] \cap \mathrm {qmax} Y$ , then from $y \in \mathrm {qmax} Y$ and $yRz$ it follows that $zRy$ , and hence $y \in R[z] \subseteq V$ . By Lemma 4.10(2), there is $q \in R[x] \cap \mathrm {qmax} Y$ . Then $xRq$ and $\mathsf {LKP}$ implies that there is $t \in R[q]$ with $E[t] \subseteq \mathrm {qmax} Y$ . We show that $E[t] \subseteq V$ . Let $s\in E[t]$ . Since $xRqRtEs$ , we have $s \in Q_E[x] \cap \mathrm {qmax} Y$ , yielding that $s \in V$ . Therefore, $xRt$ and $E[t] \subseteq V$ . Thus, $x \in \Diamond \forall V$ , showing that $\blacksquare \Diamond \Box V \subseteq \Diamond \forall V$ for every clopen subset $V$ of $\mathfrak {G}$ . Consequently, $\mathfrak {G} \vDash \blacksquare \Diamond \Box p \to \Diamond \forall p$ .

In order to prove the converse implication, we establish the following:

Claim 4.13. Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame. If $\mathfrak {G}$ does not satisfy $\mathsf {LKP}$ , then there are a nonempty closed $Q_E$ -upset $U$ and a clopen $R$ -upset $V$ such that $\mathrm {qmax} Y \subseteq V$ and $U \subseteq E[V] \cap E[Y \setminus V]$ .

Proof of the claim.

Suppose that $\mathfrak {G}$ does not satisfy $\mathsf {LKP}$ . Then there is $q \in \mathrm {qmax} Y$ such that for every $t \in R[q]$ we have that $E[t] \nsubseteq \mathrm {qmax} Y$ . By Lemma 4.10(1), $\mathrm {qmax} Y$ is a closed $R$ -upset. Since $E[t] \nsubseteq \mathrm {qmax} Y$ , there is $s \in Y$ such that $t E s$ and $s \notin \mathrm {qmax} Y$ . Therefore, by Proposition 4.11, there is a clopen $R$ -downset $W_t$ such that $s \in W_t$ and $W_t \cap \mathrm {qmax} Y = \varnothing $ . Since $t \in E[W_t]$ for every $t \in R[q]$ , it follows that $R[q] \subseteq \bigcup \{ E[W_t] : t \in R[q]\}$ and hence

$$ \begin{align*} Q_E[q]=(E\circ R)[q] \subseteq \bigcup \{ E[W_t] : t \in R[q]\} .\end{align*} $$

Since $Q_E[q]$ is closed, compactness of $Y$ yields $t_1, \dots , t_n \in R[q]$ such that ${Q_E[q] \subseteq E[W_{t_1}] \cup \dots \cup E[W_{t_n}]}$ . Therefore,

$$\begin{align*}Q_E[q] \subseteq E[W_{t_1} \cup \dots \cup W_{t_n}]. \end{align*}$$

Let $V=Y \setminus (W_{t_1} \cup \dots \cup W_{t_n})$ . Then $Q_E[q] \subseteq E[Y \setminus V]$ . Since the $W_{t_i}$ are clopen $R$ -downsets such that $W_{t_i} \cap \mathrm {qmax} Y = \varnothing $ , we obtain that $V$ is a clopen $R$ -upset containing $\mathrm {qmax} Y$ . Thus, $R[q] \subseteq \mathrm {qmax} Y \subseteq V$ . Consequently, ${Q_E[q]=(E\circ R)[q] \subseteq E[V]}$ . Let $U=Q_E[q]$ . Then $U$ is a nonempty closed $Q_E$ -upset and $V$ is a clopen $R$ -upset such that $\mathrm {qmax} Y \subseteq V$ and $U \subseteq E[V] \cap E[Y \setminus V]$ .

Suppose now that $\mathfrak {G}$ does not satisfy $\mathsf {LKP}$ . Then Claim 4.13 implies that there are a nonempty closed $Q_E$ -upset $U$ and a clopen $R$ -upset $V$ such that $\mathrm {qmax} Y \subseteq V$ and $U \subseteq E[V] \cap E[Y \setminus V]$ . Let $q \in U \cap \mathrm {qmax} Y$ , which exists by Lemma 4.10(2). Then every $y \in Q_E[q]$ is in $U$ because $U$ is a $Q_E$ -upset. Applying Lemma 4.10(2) again, there is $z \in R[y] \cap U \cap \mathrm {qmax} Y$ . Since $U \cap \mathrm {qmax} Y$ is an $R$ -upset, we obtain that $R[z] \subseteq U \cap \mathrm {qmax} Y \subseteq V$ . Therefore, ${q \in \blacksquare \Diamond \Box V}$ . However, if $y \in R[q]$ , then $y \in U \subseteq E[Y \setminus V]$ . Thus, there is $z \in Y \setminus V$ such that $z \in E[y]$ . It follows that $q \notin \Diamond \forall V$ , showing that $\mathfrak {G} \nvDash \blacksquare \Diamond \Box p \to \Diamond \forall p$ .

Remark 4.14. $\mathsf {LKP}$ is a purely order-theoretic condition that does not involve topology. Thus, similarly to $\mathsf {GKur}$ (see Remark 3.18), we have that $\mathsf {LKur}$ is canonical, and hence Kripke complete. We leave the investigation of the fmp and decidability of $\mathsf {LKur}$ to future work.

Proposition 4.15.

(1) $\mathsf {LKur}$ is strictly contained in $\mathsf {GKur}$ .
(2) $\mathsf {MGrz} \vee \mathsf {LKur} = \mathsf {MGrz} \vee \mathsf {GKur}$ .

Proof. (1). By Lemma 4.7, $\mathsf {LKur} \subseteq \mathsf {GKur}$ . As observed in Proposition 4.3, there is a descriptive $\mathsf {MS4}$ -frame $\mathfrak {H}$ that satisfies $\mathsf {LKP}$ but not $\mathsf {GKP}$ . Thus, $\mathfrak {H} \vDash \mathsf {LKur}$ by Theorem 4.12, but $\mathfrak {H} \nvDash \mathsf {GKur}$ by Theorem 3.17. We conclude that $\mathsf {GKur} \nsubseteq \mathsf {LKur}$ .

(2). Let $\mathfrak {G}=(Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame that validates $\mathsf {MGrz} \vee \mathsf {LKur}$ . By Theorem 2.26, $\mathrm {qmax} Y = \max Y$ . By Theorem 4.12, $\mathfrak {G}$ satisfies $\mathsf {LKP}$ , and so for every $y \in \max Y$ there is $z \in E_R[y]$ with $E[z] \subseteq \max Y$ . Since $E_R[y] = \{y\}$ , we obtain that $E[y] \subseteq \max Y$ for every $y \in \max Y$ , and hence $\mathfrak {G}$ satisfies $\mathsf {GKP}$ . It then follows from Theorem 3.17 that $\mathfrak {G}\vDash \mathsf {GKur}$ . This shows that $\mathsf {GKur} \subseteq \mathsf {MGrz} \vee \mathsf {LKur}$ . Since $\mathsf {LKur} \subseteq \mathsf {GKur}$ by Lemma 4.7, we conclude that $\mathsf {MGrz} \vee \mathsf {LKur} = \mathsf {MGrz} \vee \mathsf {GKur}$ .

An alternative characterization of $\mathsf {Kur}$ is given in [Reference Bezhanishvili2] utilizing morphisms between descriptive $\mathsf {MIPC}$ -frames. Let $\mathfrak {K} = (Y,R,E)$ be the two-element $\mathsf {MS4}$ -frame depicted in Figure 2, where $Y=\{ a, b \}$ , $R[a]=Y$ , $R[b]=\{b\}$ , and $E[a]=E[b]=Y$ . By [Reference Bezhanishvili2, Theorem 43(a)], a descriptive $\mathsf {MIPC}$ -frame $\mathfrak {F}$ validates $\mathsf {Kur}$ iff there is no $\mathbf {DF}_{\mathsf {MIPC}}$ -morphism from a closed $Q$ -upset of $\mathfrak {F}$ onto the skeleton $\rho \hspace {0.08em}\mathfrak {K}$ . We show that a similar characterization holds for $\mathsf {LKur}$ .

Figure 2

The frame $\mathfrak {K}$ .

A vertical directed graph inside an oval. A solid black dot at the bottom labeled a has an upward arrow pointing to a solid black dot at the top labeled b.

Theorem 4.16. Let $\mathfrak {G} = (Y,R,E)$ be a descriptive $\mathsf {MS4}$ -frame. Then $\mathfrak {G} \vDash \mathsf {LKur}$ iff there is no $\mathbf {DF}_{\mathsf {MS4}}$ -morphism from a closed $Q_E$ -upset of $\mathfrak {G}$ onto $\mathfrak {K}$ .

Proof. To prove the left-to-right implication, since taking closed $Q_E$ -upsets and images of onto $\mathbf {DF}_{\mathsf {MS4}}$ -morphisms preserves the validity of formulas, it is sufficient to show that the frame $\mathfrak {K}$ depicted in Figure 2 does not validate the formula ${\blacksquare \Diamond \Box p \to \Diamond \forall p}$ axiomatizing $\mathsf {LKur}$ over $\mathsf {MS4}$ . Let $U=\{b\}$ . We have

$$\begin{align*}\blacksquare \Diamond \Box U = \blacksquare \Diamond U = \blacksquare Y = Y \quad \text{and} \quad \Diamond \forall U = \Diamond \varnothing = \varnothing. \end{align*}$$

Thus, $\blacksquare \Diamond \Box p \to \Diamond \forall p$ is not valid on $\mathfrak {K}$ .

We prove the contrapositive of the other implication. Suppose that $\mathfrak {G} \nvDash \mathsf {LKur}$ . By Theorem 4.12, $\mathfrak {G}$ does not satisfy $\mathsf {LKP}$ . Therefore, by Claim 4.13, there are a nonempty closed $Q_E$ -upset $U$ and a clopen $R$ -upset $V$ of $\mathfrak {G}$ such that $\mathrm {qmax} Y \subseteq V$ and $U \subseteq E[V] \cap E[Y \setminus V]$ . We define a map $f \colon U \to \mathfrak {K}$ by

$$\begin{align*}f(x)= \begin{cases} b & \text{if } x \in U \cap V,\\ a & \text{otherwise.} \end{cases} \end{align*}$$ f left parenthesis x right parenthesis equals StartLayout Enlarged left brace 1st Row 1st Column b 2nd Column if x element of upper U intersection upper V comma 2nd Row 1st Column a 2nd Column otherwise period EndLayout

We show that $f$ is a well-defined $\mathbf {DF}_{\mathsf {MS4}}$ -morphism. Since $U$ is a $Q_E$ -upset, $U$ is $E$ -saturated (i.e., $E[U]=U$ ). Therefore, from $U \ne \varnothing $ and $U \subseteq E[V] \cap E[Y \setminus V]$ it follows that $U \cap V$ and $U \setminus V$ are not empty. Thus, since $V$ is clopen in $Y$ , we obtain that $\{U \cap V, U \setminus V\}$ is a clopen partition of $U$ . Hence, $f$ is a well-defined continuous onto map. We next show that $f$ is a p-morphism with respect to $R$ . That $V$ is an $R$ -upset in $Y$ implies that $U \cap V$ is an $R$ -upset in $U$ . So, $fR[x] \subseteq R[f(x)]$ for every $x \in U$ . Since $\mathrm {qmax} Y \subseteq V$ , if $x \in U$ , Lemma 4.10(2) implies that there is $y \in U \cap \mathrm {qmax} Y \subseteq V$ with $xRy$ . So, if $f(x)=a$ , then there is $y \in U \cap V$ with $xRy$ , and hence $f(y)=b$ . Therefore, $R[f(x)] \subseteq fR[x]$ for every $x \in U$ . Finally, we show that $f$ is a p-morphism with respect to $E$ . Since $a E b$ in $\mathfrak {K}$ , it follows that $fE[x] \subseteq E[f(x)]$ for every $x \in U$ . Because $U$ is a $Q_E$ -upset, it follows from $U \subseteq E[V] \cap E[Y \setminus V]$ that for every $x \in U$ there are $y \in U \cap V$ and $z \in U \setminus V$ with $y,z \in E[x]$ . Therefore, $E[f(x)] \subseteq fE[x]$ for every $x \in U$ . This shows that $f$ is a $\mathbf {DF}_{\mathsf {MS4}}$ -morphism. Thus, $f$ is a $\mathbf {DF}_{\mathsf {MS4}}$ -morphism from the closed $Q_E$ -upset $U$ of $\mathfrak {G}$ onto $\mathfrak {K}$ .

Remark 4.17. Theorem 4.16 can be phrased using the language of splitting logics (see, e.g., [Reference Kracht25, Section 7.7] and [Reference Wolter35, Section 2.4]). Indeed, since the algebraic models of $\mathsf {MS4}$ form a variety with equationally definable principal congruences (EDPCs), it follows from the general considerations of Blok and Pigozzi [Reference Blok and Pigozzi7] that splitting logics above $\mathsf {MS4}$ are axiomatized by the Jankov–Fine formulas of finite rooted $\mathsf {MS4}$ -frames, where an $\mathsf {MS4}$ -frame $(Y,R,E)$ is rooted if there is $y \in Y$ such that $Q_E[y]=Y$ . By [Reference Chagrov and Zakharyaschev10, Corollary 9.64], if $\mathsf {L}$ is a splitting logic above $\mathsf {IPC}$ , then $\tau \mathsf {L}$ is a splitting logic above $\mathsf {S4}$ . In fact, if $\mathsf {L}$ is axiomatized by the Jankov–Fine formula of a finite $\mathsf {IPC}$ -frame $\mathfrak {F}$ , then $\tau \mathsf {L}$ is axiomatized by the Jankov–Fine formula of $\mathfrak {F}$ viewed as an $\mathsf {S4}$ -frame. We show that this is no longer true in the monadic setting. By [Reference Bezhanishvili2, Theorem 43(a)], $\mathsf {Kur}$ is the splitting logic above $\mathsf {MIPC}$ axiomatized by the Jankov–Fine formula of $\rho \hspace {0.08em}\mathfrak {K}$ . By Theorem 4.16, $\mathsf {LKur}$ is the splitting logic above $\mathsf {MS4}$ axiomatized by the Jankov–Fine formula of $\mathfrak {K}$ . On the other hand, $\tau (\mathsf {Kur}) = \mathsf {GKur}$ , which strictly contains $\mathsf {LKur}$ by Proposition 4.15(1). Thus, in the lattice of extensions of $\mathsf {MS4}$ , it is the behavior of $\mathsf {LKur}$ , rather than $\mathsf {GKur}$ , that is similar to that of $\mathsf {Kur}$ in the lattice of extensions of $\mathsf {MIPC}$ .

In the following section we will see that, unlike $\mathsf {GKur}$ , the logic $\mathsf {LKur}$ is not a modal companion of $\mathsf {Kur}$ . In fact, we will show that $\mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ . This observation is at the heart of the proof of the failure of Esakia’s theorem for $\mathsf {MIPC}$ .

5 Failure of Esakia’s theorem for $\mathsf {MIPC}$

In this section we show that the monadic analogue of Esakia’s theorem fails. In fact, we prove a stronger result: not only is $\mathsf {MGrz}$ not the greatest modal companion of $\mathsf {MIPC}$ , but $\mathsf {MIPC}$ has no greatest modal companion at all! We do this by establishing that $\mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ . Since $\mathsf {MGrz}\vee \mathsf {LKur}=\mathsf {MGrz}\vee \mathsf {GKur}$ (see Proposition 4.15(2)) and $\mathsf {GKur}$ is not a modal companion of $\mathsf {MIPC}$ (see Theorem 3.19), the result follows.

To see that $\mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ , we require the following lemma which shows that each finite $\mathsf {MIPC}$ -frame $\mathfrak {F}$ can be realized as the skeleton of an $\mathsf {LKur}$ -frame $\mathfrak {G}$ . Intuitively, $\mathfrak {G}$ is constructed by adding to $\mathfrak {F}$ a copy of its maximal layer so that each maximal element of $\mathfrak {F}$ is $E_R$ -related to its copy and the set of these new elements is $E$ -saturated in $\mathfrak {G}$ .

Lemma 5.1. If $\mathfrak {F}$ is a finite $\mathsf {MIPC}$ -frame, then there is a finite $\mathsf {LKur}$ -frame $\mathfrak {G}$ such that $\mathfrak {F} \cong \rho \hspace {0.08em}\mathfrak {G}$ .

Proof. Let $\mathfrak {F} =(X,R,Q)$ be a finite $\mathsf {MIPC}$ -frame. Consider a set $M$ disjoint from $X$ that is in bijective correspondence with $\max X$ . Let $g \colon M \to \max X$ be the bijection, $Y = X \cup M$ , and define $f \colon Y \to X$ by

$$\begin{align*}f(x) = \begin{cases} x & \text{if } x \in X,\\ g(x) & \text{if } x\in M. \end{cases} \end{align*}$$ f left parenthesis x right parenthesis equals StartLayout Enlarged left brace 1st Row 1st Column x 2nd Column if x element of upper X comma 2nd Row 1st Column g left parenthesis x right parenthesis 2nd Column if x element of upper M period EndLayout

Denote by $\overline {R}$ the binary relation on $Y$ defined by

$$\begin{align*}x \overline{R} y \iff f(x) R f(y). \end{align*}$$

It is straightforward to check that $\overline {R}$ is a quasi-order on $Y$ and that $f$ is a p-morphism from $(Y, \overline {R})$ to $(X,R)$ . Define a binary relation $\overline {E}$ on $Y$ by

$$\begin{align*}x \overline{E} y \iff \begin{cases} x,y \in X \text{ and } xE_Qy, \text{ or}\\ x, y \in M \text{ and } g(x)E_Qg(y). \end{cases} \end{align*}$$ StartLayout 1st Row x upper E overbar y long left right double arrow StartLayout Enlarged left brace 1st Row x comma y element of upper X and x upper E Subscript upper Q Baseline y comma or 2nd Row x comma y element of upper M and g left parenthesis x right parenthesis upper E Subscript upper Q Baseline g left parenthesis y right parenthesis period EndLayout EndLayout

Claim 5.2. $\mathfrak {G}=(Y, \overline {R}, \overline {E})$ is an $\mathsf {MS4}$ -frame.

Proof of the claim.

Since $E_Q$ is an equivalence relation on $X$ , we obtain that $\overline {E}$ is a well-defined equivalence relation on $Y$ . Therefore, it remains to check Definition 2.15(3). Let $x,y,z \in Y$ with $x \overline {E} y$ and $y \overline {R} z$ . We consider cases. First suppose that $x,y,z \in X$ . Then $x E_Q y$ and $y R z$ . Since, by Remark 2.23, $(X,R,E_Q)$ is an $\mathsf {MS4}$ -frame, there exists $u \in X$ such that $xRu$ and $uE_Qz$ . Thus, $x\overline {R} u$ and $u\overline {E} z$ .

The next case to consider is when $x,y \in X$ and $z \in M$ . Since $y \overline {R} z$ , we have that $y R g(z)$ . Since $(X,R,E_Q)$ is an $\mathsf {MS4}$ -frame, there is $u \in X$ such that $x R u$ and $u E_Q g(z)$ . Let $v \in \max X$ be such that $u R v$ . Then $v E_Q g(z)$ because $(X,R,E_Q)$ is an $\mathsf {MS4}$ -frame and $g(z) \in \max X$ . Since $x R v$ and $g \colon M \to \max X$ is a bijection, there is $m \in M$ ( $m=g^{-1}(v)$ ) such that $x \overline {R} m$ and $m \overline {E} z$ (because $g(m)\mathop {=}v E_Q g(z)$ ).

Observe that, since $x\overline {E} y$ , we have $x \in M$ iff $y \in M$ . Therefore, the last case to consider is when $x, y \in M$ . From $y \overline {R} z$ it follows that $f(y) R f(z)$ , and hence $f(z)=f(y)$ because $f(y) \in \max X$ (since $y \in M$ ). Because $f$ is injective on $M$ , we obtain that $z=y$ . So, $x \overline {R} x$ and $x \overline {E} y\mathop {=}z$ . We have thus shown that $\mathfrak {G}$ satisfies Definition 2.15(3). Consequently, $\mathfrak {G}$ is an $\mathsf {MS4}$ -frame.

Claim 5.3. $\mathfrak {G} \vDash \mathsf {LKur}$ .

Proof of the claim.

By Theorem 4.12, it is sufficient to verify that $\mathfrak {G}$ satisfies $\mathsf {LKP}$ . We first prove that $\mathrm {qmax} Y = \max X \cup M$ . Since $f^{-1}[\max X]=\max X \cup M$ , it is sufficient to show that $y \in \mathrm {qmax} Y$ iff $f(y) \in \max X$ . Suppose that $y \in \mathrm {qmax} Y$ and $f(y) R x$ . Since $f$ is onto, there is $z \in Y$ with $f(z)=x$ . Therefore, $f(y) R f(z)$ , and so $y \overline {R} z$ . Thus, $z \overline {R} y$ because $y$ is quasi-maximal. From $y \overline {R} z$ and $z \overline {R} y$ it follows that $f(y) R f (z)$ and $f(z) R f (y)$ . Since $R$ is a partial order, we conclude that $x=f(z)=f(y)$ . This shows that $f(y) \in \max X$ . Conversely, suppose that $f(y) \in \max X$ and $y \overline {R} z$ . Then $f(y) R f(z)$ , and so $f(y)=f(z)$ because $f(y)$ is maximal. Therefore, $f(z) R f(y)$ , and hence $z\overline {R} y$ . Thus, $y \in \mathrm {qmax} Y$ . This shows that $\mathrm {qmax} Y = \max X \cup M$ .

We now prove that $\mathfrak {G}$ satisfies $\mathsf {LKP}$ . Let $y \in \mathrm {qmax} Y$ . If $y \in M$ , then ${\overline {E}[y] \subseteq M \subseteq \mathrm {qmax} Y}$ by definition of $\overline {E}$ . Otherwise, $y \in \max X$ , and so ${y E_{\overline {R}} y' \in M}$ and $\overline {E}[y'] \subseteq M \subseteq \mathrm {qmax} Y$ . In either case, there is $z \in Y$ such that $y E_{\overline {R}} z$ and $\overline {E}[z] \subseteq \mathrm {qmax} Y$ . Therefore, $\mathfrak {G}$ satisfies $\mathsf {LKP}$ .

Claim 5.4. $\rho \hspace {0.08em}\mathfrak {G} \cong \mathfrak {F}$ .

Proof of the claim.

Since $R$ is a partial order and $y \overline {R} z$ iff $f(y) R f(z)$ for every $y,z \in Y$ , we have that $y E_{\overline {R}} z$ iff $f(y)=f(z)$ . Recalling that $Q_{\overline {E}}$ is the composition $\overline {E} \circ \overline {R}$ , we show that $y Q_{\overline {E}} z$ iff $f(y) Q f(z)$ for every $y,z \in Y$ . It follows from the definition of $\overline {E}$ that $y \overline {E} z$ implies $f(y) E_Q f(z)$ . Therefore, $y Q_{\overline {E}} z$ implies $f(y) Q_{E_Q} f(z)$ , and hence $f(y) Q f(z)$ because $\mathfrak {F}$ is an $\mathsf {MIPC}$ -frame. Thus, $y Q_{\overline {E}} z$ implies $f(y) Q f(z)$ . Conversely, suppose that $f(y) Q f(z)$ . Then there is $x \in X$ such that $f(y) R x$ and $x E_Q f(z)$ . Therefore, $y \overline {R} x$ because $f(y)Rx\mathop {=}f(x)$ . Since $x E_Q f(z)$ , we either have that $z \in X$ and $x E_Q z$ or that $z \in M$ and $x E_Q g(z)$ . In the former case, $y \overline {R} x$ and $x \overline {E} z$ , so $y Q_{\overline {E}} z$ . In the latter case, $y \overline {R} x$ , $x \overline {E} g(z)$ , and $g(z) \overline {R} z$ . Thus, $y(\overline {R} \circ \overline {E} \circ \overline {R})z$ . We have that $\overline {R}, \overline {E} \subseteq Q_{\overline {E}}$ and $Q_{\overline {E}}$ is transitive because $Q_{\overline {E}} = \overline {E} \circ \overline {R}$ and $\mathfrak {G} = (Y, \overline {R}, \overline {E})$ is an $\mathsf {MS4}$ -frame by Claim 5.2. Thus, $y Q_{\overline {E}} z$ in the latter case as well. This proves that $y Q_{\overline {E}} z$ iff $f(y) Q f(z)$ . It is then straightforward to see that $f$ induces a map $f' \colon \rho \hspace {0.08em}\mathfrak {G} \to \mathfrak {F}$ sending the equivalence class $E_{\overline {R}}[y]$ to $f(y)$ . Since $y \overline {R} z$ iff $f(y) R f(z)$ and $y Q_{\overline {E}} z$ iff $f(y) Q f(z)$ for every $y,z \in Y$ , it follows that $f'$ is a bijection of $\mathsf {MIPC}$ -frames that preserves and reflects both relations. Therefore, by Remark 2.9, $f' \colon \rho \hspace {0.08em}\mathfrak {G} \to \mathfrak {F}$ is an isomorphism of $\mathsf {MIPC}$ -frames.

The above three claims finish the proof.

Remark 5.5. It is open whether Lemma 5.1 generalizes to arbitrary descriptive $\mathsf {MIPC}$ -frames. In fact, it remains open whether the functor $\rho \colon \mathbf {DF}_{\mathsf {MS4}} \to \mathbf {DF}_{\mathsf {MIPC}}$ is essentially surjective (see Remark 3.10).

Remark 5.6. Since the $\mathsf {MS4}$ -frames $\mathfrak {H}$ and $\mathfrak {K}$ shown in Figures 1 and 2 will play a fundamental role in this section, we point out that the construction employed in the proof of Lemma 5.1 applied to the $\mathsf {MIPC}$ -frame $\rho \hspace {0.08em}\mathfrak {K}$ yields a frame isomorphic to $\mathfrak {H}$ . It then follows from Lemma 5.1 that $\mathfrak {H}$ is an $\mathsf {LKur}$ -frame and that $\rho \hspace {0.08em}\mathfrak {K}$ and $\rho \hspace {0.08em}\mathfrak {H}$ are isomorphic $\mathsf {MIPC}$ -frames.

We are now ready to prove that the local Kuroda logic is a modal companion of $\mathsf {MIPC}$ .

Theorem 5.7. $\mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ .

Proof. It is sufficient to show that for every formula $\varphi $ of $\mathcal {L_{\forall \exists }}$ we have that $\mathsf {MIPC} \nvdash \varphi $ implies $\mathsf {LKur} \nvdash \varphi ^t$ . Suppose that $\mathsf {MIPC} \nvdash \varphi $ . Since $\mathsf {MIPC}$ has the fmp, there is a finite $\mathsf {MIPC}$ -frame $\mathfrak {F}$ such that $\mathfrak {F} \nvDash \varphi $ . By Lemma 5.1, there is an $\mathsf {LKur}$ -frame $\mathfrak {G}$ such that $\mathfrak {F} \cong \rho \hspace {0.08em}\mathfrak {G}$ . Therefore, $\rho \hspace {0.08em}\mathfrak {G} \nvDash \varphi $ , and so $\mathfrak {G} \nvDash \varphi ^t$ by Theorem 3.6(4). Thus, $\mathsf {LKur} \nvdash \varphi ^t$ .

Theorem 5.8.

(1) $\mathfrak {K} \vDash \mathsf {MGrz}$ but $\mathfrak {K} \nvDash \mathsf {LKur}$ .
(2) $\mathfrak {H} \vDash \mathsf {LKur}$ but $\mathfrak {H} \nvDash \mathsf {MGrz}$ .
(3) $\mathsf {MGrz}$ and $\mathsf {LKur}$ are incomparable.

Proof. (1). Since $\mathfrak {K}$ is a finite $\mathsf {MS4}$ -frame in which $R$ is a partial order, $\mathfrak {K} \vDash \mathsf {MGrz}$ by Theorem 2.26. On the other hand, $\mathfrak {K} \nvDash \mathsf {LKur}$ by Theorem 4.16.

(2). As was observed in Remark 5.6, $\mathfrak {H} \vDash \mathsf {LKur}$ . On the other hand, $\mathfrak {H}\nvDash \mathsf {MGrz}$ by Theorem 2.26 because it contains a quasi-maximal point that is not maximal.

(3). This is immediate from (1) and (2).

By Theorem 5.8, $\mathsf {MGrz}$ cannot be the greatest modal companion of $\mathsf {MIPC}$ because it is incomparable with $\mathsf {LKur}$ , which is also a modal companion of $\mathsf {MIPC}$ by Theorem 5.7. This already implies that the natural generalization of Esakia’s theorem to the monadic setting does not hold. We show that even more is true by proving that there is no greatest modal companion of $\mathsf {MIPC}$ .

Proposition 5.9. $\mathsf {MGrz} \vee \mathsf {LKur}$ is not a modal companion of $\mathsf {MIPC}$ .

Proof. By Proposition 4.15(2), $\mathsf {GKur} \subseteq \mathsf {MGrz} \vee \mathsf {LKur}$ . By Theorem 3.19, $\mathsf {Kur}$ is the intuitionistic fragment of $\mathsf {GKur}$ . Therefore, the intuitionistic fragment of ${\mathsf {MGrz} \vee \mathsf {LKur}}$ contains $\mathsf {Kur}$ , which is a proper extension of $\mathsf {MIPC}$ . Thus, $\mathsf {MGrz} \vee \mathsf {LKur}$ is not a modal companion of $\mathsf {MIPC}$ .

Theorem 5.10 (Failure of Esakia’s theorem for $\mathsf {MIPC}$ ).

There is no greatest modal companion of $\mathsf {MIPC}$ .

Proof. Suppose that there is a greatest modal companion $\mathsf {M}$ of $\mathsf {MIPC}$ . By Theorems 2.27 and 5.7, both $\mathsf {MGrz}$ and $\mathsf {LKur}$ are modal companions of $\mathsf {MIPC}$ , and hence $\mathsf {MGrz} \vee \mathsf {LKur} \subseteq \mathsf {M}$ . Therefore, the intuitionistic fragment of $\mathsf {MGrz} \vee \mathsf {LKur}$ is contained in the intuitionistic fragment of $\mathsf {M}$ which is $\mathsf {MIPC}$ , and hence $\mathsf {MGrz} \vee \mathsf {LKur}$ is a modal companion of $\mathsf {MIPC}$ . But this contradicts Proposition 5.9. Thus, $\mathsf {M}$ does not exist.

Remark 5.11. Although there is no greatest modal companion of $\mathsf {MIPC}$ , a standard argument utilizing Zorn’s lemma shows that every modal companion of $\mathsf {MIPC}$ is contained in a maximal modal companion of $\mathsf {MIPC}$ . We leave it as an open problem to determine the cardinality of the set of maximal modal companions of $\mathsf {MIPC}$ , and whether $\mathsf {MGrz}$ is one of those.

6 Conclusions

We have demonstrated that Esakia’s theorem that $\mathsf {Grz}$ is the greatest modal companion of $\mathsf {IPC}$ fails as soon as we add to the language monadic quantification of one fixed variable. As we pointed out in the introduction, the reason why Esakia’s theorem holds in the propositional case could be summarized as follows: the category of descriptive $\mathsf {IPC}$ -frames is equivalent to the category of partially ordered descriptive $\mathsf {S4}$ -frames and $\mathsf {Grz}$ is complete with respect to the latter category. If $\mathsf {M}$ is a modal companion of $\mathsf {IPC}$ , then this category is a full subcategory of the category of descriptive $\mathsf {M}$ -frames, yielding that $\mathsf {M}$ is contained in $\mathsf {Grz}$ .

The situation changes considerably in the monadic setting since the addition of monadic modalities breaks the above correspondence between the two semantics. Indeed, while $Q$ is a continuous relation in a descriptive $\mathsf {MIPC}$ -frame $\mathfrak {F}=(X,R,Q)$ , the relation $E_Q$ may no longer be continuous. On the other hand, in a descriptive $\mathsf {MS4}$ -frame $\mathfrak {G}=(Y,R,E)$ , the relation $E$ is continuous. In addition, a morphism between descriptive $\mathsf {MIPC}$ -frames does not have to be a p-morphism with respect to $E_Q$ , while a morphism between descriptive $\mathsf {MS4}$ -frames must be a p-morphism with respect to $E$ . Thus, while the embedding $\sigma \colon \mathbf {DF}_{\mathsf {IPC}}\to \mathbf {DF}_{\mathsf {S4}}$ yields an equivalence between $\mathbf {DF}_{\mathsf {IPC}}$ and the category of partially ordered descriptive $\mathsf {S4}$ -frames, its natural extension to the monadic setting is not even well defined (neither on objects nor on morphisms). Consequently, although $\mathsf {MGrz}$ is complete with respect to the category of partially ordered descriptive $\mathsf {MS4}$ -frames [Reference Bezhanishvili and Khan6], if $\mathsf {M}$ is a modal companion of $\mathsf {MIPC}$ , the latter category is no longer a full subcategory of the category of descriptive $\mathsf {M}$ -frames, resulting in the failure of the monadic version of Esakia’s theorem. One way to remedy this is to add appropriate axioms to restore the semantic balance enjoyed in the case of $\mathsf {IPC}$ and $\mathsf {Grz}$ . This will be discussed in a follow-up paper.

We conclude the article by addressing Naumov’s claim that

$$ \begin{align*}{\mathsf {QGrz}+\Box \exists xP(x) \to \Diamond \exists x\Box P(x)} \end{align*} $$

is a modal companion of $\mathsf {IQC}$ that strictly contains $\mathsf {QGrz}$ (see [Reference Gabbay, Shehtman and Skvortsov20, Theorem 2.11.14] and [Reference Naumov28]). More specifically, we show that $\mathsf {MGrz} + \Box \exists p \to \Diamond \exists \Box p$ is equal to $\mathsf {MGrz}\vee \mathsf {GKur}$ , from which we derive that Naumov’s logic is not a modal companion of $\mathsf {IQC}$ . Therefore, while we verified Naumov’s claim that $\mathsf {QGrz}$ is not the greatest modal companion of $\mathsf {IQC}$ for the monadic fragments of these logics, the full predicate case requires further study (see Remark 6.6 for more details).

Definition 6.1. Let $\mathsf {N} = \mathsf {MS4} + \Box \exists p \to \Diamond \exists \Box p$ . We call $\mathsf {N}$ the Naumov logic.

Because $\mathsf {MS4} \vdash \blacklozenge p \leftrightarrow \Diamond \exists p$ (see the paragraph before Proposition 3.20), the following is straightforward.

Lemma 6.2. $\mathsf {N} = \mathsf {MS4} + \Box \exists p \to \blacklozenge \Box p = \mathsf {MS4} + \blacksquare \Diamond p \to \Diamond \forall p$ .

By Proposition 4.15(2), $\mathsf {LKur}$ and $\mathsf {GKur}$ coincide over $\mathsf {MGrz}$ . The next proposition shows that over $\mathsf {MGrz}$ they also coincide with $\mathsf {N}$ .

Proposition 6.3. $\mathsf {MGrz} \vee \mathsf {GKur} = \mathsf {MGrz} \vee \mathsf {LKur} = \mathsf {MGrz} \vee \mathsf {N}$ .

Proof. It is sufficient to show that $\mathsf {MGrz} \vee \mathsf {LKur} = \mathsf {MGrz} \vee \mathsf {N}$ . Since $\mathsf {LKur} = \mathsf {MS4} + {\blacksquare \Diamond \Box p \to \Diamond \forall p}$ and $\mathsf {N} = \mathsf {MS4} + \blacksquare \Diamond p \to \Diamond \forall p$ (see Lemma 6.2), it is enough to show that $\mathsf {MGrz} \vdash \blacksquare \Diamond \Box p \leftrightarrow \blacksquare \Diamond p$ , which can be seen as follows. It is well known that the McKinsey formula $\Box \Diamond p \to \Diamond \Box p$ is a theorem of $\mathsf {Grz}$ . Therefore, $\mathsf {Grz} \vdash \Box \Diamond \Box p \leftrightarrow \Box \Diamond p$ , and so $\mathsf {MGrz} \vdash \blacksquare \Box \Diamond \Box p \leftrightarrow \blacksquare \Box \Diamond p$ . Thus, since $\blacksquare $ is a master modality, $\mathsf {MGrz} \vdash \blacksquare \Diamond \Box p \leftrightarrow \blacksquare \Diamond p$ (see the proof of Proposition 3.20).

Remark 6.4. Let $\mathsf {MS4.1} = \mathsf {MS4} + \Box \Diamond p \to \Diamond \Box p$ . By arguing as in the proof of the previous proposition, $\mathsf {MS4.1} \vee \mathsf {LKur} = \mathsf {MS4.1} \vee \mathsf {N}$ . It follows from [Reference Esakia11, p. 154] (see also [Reference Chagrov and Zakharyaschev10, Proposition 3.46]) that descriptive $\mathsf {MS4.1}$ -frames are exactly those descriptive $\mathsf {MS4}$ -frames in which every quasi-maximal point is maximal. Therefore, by arguing as in the proof of Proposition 4.15(2), we also have that $\mathsf {MS4.1} \vee \mathsf {LKur} = \mathsf {MS4.1} \vee \mathsf {GKur}$ . Thus, $\mathsf {GKur}$ , $\mathsf {LKur}$ , and $\mathsf {N}$ are all instances of Kuroda-like logics that collapse over $\mathsf {MS4.1}$ . It is natural to investigate such principles in more detail.

Theorem 6.5. $\mathsf {QGrz}+\Box \exists xP(x) \to \Diamond \exists x\Box P(x)$ is not a modal companion of $\mathsf {IQC}$ .

Proof. It is clear that the logic $\mathsf {MGrz} \vee \mathsf {N}$ is contained in the monadic fragment of $\mathsf {QGrz}+\Box \exists xP(x) \to \Diamond \exists x\Box P(x)$ . It follows from Propositions 5.9 and 6.3 that $\mathsf {MGrz} \vee \mathsf {N}$ is not a modal companion of $\mathsf {MIPC}$ . Therefore, ${\mathsf {QGrz}+\Box \exists xP(x) \to \Diamond \exists x\Box P(x)}$ proves the translation of a one-variable formula that is not a theorem of $\mathsf {IQC}$ , and hence it cannot be a modal companion of $\mathsf {IQC}$ .

Remark 6.6. As we pointed out in the introduction, Pankratyev [Reference Pankratyev30] claimed that $\mathsf {QGrz}$ is a modal companion of $\mathsf {IQC}$ , however his proof relied on the Flagg–Friedman translation [Reference Flagg and Friedman18] of $\mathsf {QS4}$ to $\mathsf {IQC}$ , which is not faithful [Reference Inoué24]. Therefore, it remains open whether $\mathsf {QGrz}$ is a modal companion of $\mathsf {IQC}$ . Unfortunately, Kripke completeness of $\mathsf {IQC}$ does not help since it relies on non-noetherian predicate Kripke frames which are not models of $\mathsf {QGrz}$ . A possible approach would be to use the more general Kripke bundle semantics [Reference Gabbay, Shehtman and Skvortsov20, Chapter 5] which would then require to prove that $\mathsf {IQC}$ is complete with respect to noetherian Kripke bundles. As far as we know, this remains an open problem.

If $\mathsf {QGrz}$ ends up being a modal companion of $\mathsf {IQC}$ , Naumov’s claim that $\mathsf {QGrz}$ is not the greatest such would also require further investigation. As we saw in Theorem 6.5, the logic $\mathsf {QGrz}+\Box \exists xP(x) \to \Diamond \exists x\Box P(x)$ is not going to be useful for this purpose. It is more convenient to consider

$$\begin{align*}\mathsf{QLKur} := \mathsf{QS4} + \Box \forall x \Diamond \Box P(x) \to \Diamond \forall x P(x), \end{align*}$$

which is the predicate version of $\mathsf {LKur}$ , and is not comparable with $\mathsf {QGrz}$ . However, this approach requires a proof that $\mathsf {QLKur}$ is a modal companion of $\mathsf {IQC}$ . By Remark 4.14, $\mathsf {LKur}$ is Kripke complete, from which it follows that $\mathsf {LKur}$ axiomatizes the monadic fragment of $\mathsf {QLKur}$ . Therefore, Theorem 5.7 yields that the monadic fragment of $\mathsf {QLKur}$ is a modal companion of $\mathsf {MIPC}$ . However, it remains open whether $\mathsf {QLKur}$ is a modal companion of $\mathsf {IQC}$ .

Acknowledgments

We would like to thank the referee for careful reading and useful comments which have improved the presentation.

Footnotes

1 We thank Valentin Shehtman for drawing our attention to [Reference Inoué24].

2 For an equivalent algebraic formulation of this result see [Reference Fischer Servi15, Theorem 5].

3 For similar issues in the predicate case see [Reference Gabbay, Shehtman and Skvortsov20, Remark 2.11.13].

References

Bezhanishvili, G., Varieties of monadic Heyting algebras. II. Duality theory . Studia Logica , vol. 62 (1999), no. 1, pp. 21–48.Google Scholar

Bezhanishvili, G., Varieties of monadic Heyting algebras. III . Studia Logica , vol. 64 (2000), no. 2, pp. 215–256.Google Scholar

Bezhanishvili, G., Brantley, K., and Ilin, J., Monadic intuitionistic and modal logics admitting provability interpretations . Journal of Symbolic Logic , vol. 88 (2023), no. 1, pp. 427–467.Google Scholar

Bezhanishvili, G. and Carai, L., Temporal interpretation of monadic intuitionistic quantifiers . Review of Symbolic Logic , vol. 16 (2023), no. 1, pp. 164–187.Google Scholar

Bezhanishvili, G. and Carai, L., Failure of the Blok-Esakia theorem in the monadic setting . Annals of Pure and Applied Logic , vol. 176 (2025), no. 4, Article no. 103527.Google Scholar

Bezhanishvili, G. and Khan, M., The monadic Grzegorczyk logic . Annals of Pure and Applied Logic , vol. 177 (2026), no. 10, Article no. 103793.Google Scholar

Blok, W. J. and Pigozzi, D., On the structure of varieties with equationally definable principal congruences. I . Algebra Universalis , vol. 15 (1982), no. 2, pp. 195–227.Google Scholar

Bull, R. A., A modal extension of intuitionist logic . Notre Dame Journal of Formal Logic , vol. 6 (1965), no. 2, pp. 142–146.Google Scholar

Bull, R. A., MIPC as the formalisation of an intuitionist concept of modality . Journal of Symbolic Logic , vol. 31 (1966), no. 4, pp. 609–616.Google Scholar

Chagrov, A. and Zakharyaschev, M., Modal Logic , Oxford Logic Guides, 35, The Clarendon Press, Oxford University Press, New York, 1997.Google Scholar

Esakia, L., On the theory of modal and superintuitionistic systems , Logical Inference (Russian) (V. A. Smirnov, editor), Nauka, Moscow, 1979, pp. 147–172.Google Scholar

Esakia, L., On the variety of Grzegorczyk algebras , Studies in Nonclassical Logics and Set Theory (Russian) (A. I. Mikhailov, editor), Nauka, Moscow, 1979, pp. 257–287.Google Scholar

Esakia, L., Provability logic with quantifier modalities , Intensional Logics and the Logical Structure of Theories (Russian) (V. A. Smirnov and M. N. Bezhanishvili, editors), Metsniereba, Tbilisi, 1988, pp. 4–9.Google Scholar

Esakia, L., Heyting Algebras: Duality Theory , Trends in Logic, 50 (Bezhanishvili, G. and Holliday, W., editors), Springer, 2019. Translated from the Russian by A. Evseev.Google Scholar

Fischer Servi, G., On modal logic with an intuitionistic base . Studia Logica , vol. 36 (1977), no. 3, pp. 141–149.Google Scholar

Fischer Servi, G., The finite model property for MIPQ and some consequences . Notre Dame Journal of Formal Logic , vol. 19 (1978), no. 4, pp. 687–692.Google Scholar

Fischer Servi, G., Semantics for a class of intuitionistic modal calculi . Bulletin of the Section of Logic , vol. 7 (1978), no. 1, pp. 26–29.Google Scholar

Flagg, R. C. and Friedman, H., Epistemic and intuitionistic formal systems . Annals of Pure and Applied Logic , vol. 32 (1986), no. 1, pp. 53–60.Google Scholar

Gabbay, D. M., Kurucz, A., Wolter, F., and Zakharyaschev, M., Many-Dimensional Modal Logics: Theory and Applications , Studies in Logic and the Foundations of Mathematics, 148, North-Holland, Amsterdam, 2003.Google Scholar

Gabbay, D. M., Shehtman, V. B., and Skvortsov, D. P., Quantification in Nonclassical Logic , vol. 1, Studies in Logic and the Foundations of Mathematics, 153, Elsevier B. V., Amsterdam, 2009.Google Scholar

Gödel, K., Eine interpretation des intuitionistischen Aussagenkalküls . Ergebnisse eines Mathematischen Kolloquiums , vol. 4 (1933), pp. 39–40.Google Scholar

Heyting, A., Intuitionism: An Introduction , Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1956.Google Scholar

Hilbert, D. and Ackermann, W., Grundzüge der Theoretischen Logik , Grundlehren der Mathematischen Wissenschaften, 27, Springer, Cham, 1928. (German), English translation: Principles of Mathematical Logic, edited by Robert E. Luce, New York: Chelsea Publishing Co. 1950.Google Scholar

Inoué, T., Flagg and Friedman’s translation is not faithful . Zeitschrift für mathematische Logik und Grundlagen der Mathematik , vol. 38 (1992), nos. 5–6, pp. 551–554.Google Scholar

Kracht, M., Tools and Techniques in Modal Logic , Studies in Logic and the Foundations of Mathematics, 142, North-Holland, Amsterdam, 1999.Google Scholar

McKinsey, J. C. C. and Tarski, A., Some theorems about the sentential calculi of Lewis and Heyting . Journal of Symbolic Logic , vol. 13 (1948), pp. 1–15.Google Scholar

Monteiro, A. and Varsavsky, O., Álgebras de Heyting monádicas , Actas de las X Jornadas de la Unión Matemática Argentina, Bahía Blanca , 1957, pp. 52–62.Google Scholar

Naumov, P. G., Modal logics that are conservative over intuitionistic predicate calculus . Moscow University Mathematics Bulletin (Russian) , vol. 6 (1991), pp. 86–90.Google Scholar

Ono, H., On some intuitionistic modal logics . Kyoto University , vol. 13 (1977), no. 3, pp. 687–722.Google Scholar

Pankratyev, N. A., Predicate calculus and arithmetic with Grzegorczyk logic . Moscow University Mathematics Bulletin (Russian) , vol. 5 (1989), pp. 83–85.Google Scholar

Prior, A. N., Time and Modality , The Clarendon Press, Oxford University Press, New York, 1957. (English).Google Scholar

Rasiowa, H. and Sikorski, R., Algebraic treatment of the notion of satisfiability . Fundamenta Mathematicae , vol. 40 (1953), pp. 62–95.Google Scholar

Troelstra, A. S. and van Dalen, D., Constructivism in Mathematics , vol. 1, Elsevier, Amsterdam, 1988.Google Scholar

Wajsberg, M., Ein erweiterter Klassenkalkül . Monatshefte für Mathematik und Physik , vol. 40 (1933), no. 1, pp. 113–126. English translation: An extended class calculus, in M. Wajsberg, Logical Works, edited by S. J. Surma, Ossolineum 1977, pp. 50–61.Google Scholar

Wolter, F., Lattices of modal logics , Ph.D. thesis, Free University of Berlin, 1993.Google Scholar

Figure 1 The frame H$\mathfrak {H}$.Figure 1 long description.

Figure 2 The frame K$\mathfrak {K}$.

Article contents

FAILURE OF ESAKIA’S THEOREM IN THE MONADIC SETTING

Abstract

Keywords

MSC classification

Information

1 Introduction

2 Preliminaries

Definition 2.25 (See, e.g., [Reference Esakia, Bezhanishvili and Holliday14, Definition 1.4.9]).

Theorem 2.27 [Reference Esakia13, Reference Fischer Servi15].

3 Global Kuroda logic

Theorem 3.3 [Reference Bezhanishvili2, Lemma 37].

Definition 3.5 [Reference Bezhanishvili, Brantley and Ilin3, p. 439].

4 Local Kuroda logic

Proof of the claim.

5 Failure of Esakia’s theorem for $\mathsf {MIPC}$

Proof of the claim.

Proof of the claim.

Proof of the claim.

Theorem 5.10 (Failure of Esakia’s theorem for $\mathsf {MIPC}$ ).

6 Conclusions

Acknowledgments

Footnotes

References

Save article to Kindle

Save article to Dropbox

Save article to Google Drive

Reply to: Submit a response

Your details

You have entered the maximum number of contributors

Conflicting interests