Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames

Abstract

1 Introduction

Propositional modal logics are, in Moshe Vardi’s famous words [38], robustly decidable. In stark contrast, predicate modal logics might be said to be robustly undecidable: they are hopelessly undecidable even in situations where the classical predicate logic |$\textbf{QCl}$| is algorithmically well behaved. Thus, whereas the monadic and two-variable fragments of |$\textbf{QCl}$| are both decidable, even with equality [4], most modal—and closely related superintuitionistic—predicate logics are undecidable even in languages with only one monadic predicate letter and only two individual variables, without constants, function symbols or equality [26].

That monadic fragments of modal predicate logics are undecidable has first been observed by Saul Kripke, who proved [14] that every sublogic of |$\textbf{QS5}$| that includes |$\textbf{QCl}$| is undecidable with two monadic predicate letters—in such logics, a classical predicate formula |$Q(x, y)$| can be simulated by a modal formula |$\Diamond (P_{1}(x) \wedge P_{2}(y))$|⁠, thus bringing into the monadic modal logic the undecidability [4] of the classical logic of a single binary predicate; this construction has come to be known as Kripke’s trick [13]. A few years after Kripke, it was shown by Maslov, Mints and Orevkov [16] that the fragment of the intuitionistic predicate logic |$\textbf{QInt}$| with a single monadic predicate letter is undecidable. Later, it was shown by Gabbay and Shehtman [8] that monadic fragments of modal and superintuitionistic logics of constant domains are undecidable with only two individual variables; later still, Kontchakov, Kurucz and Zakharyaschev [13] extended this result to |$\textbf{QInt}$| and to modal logics of expanding domains. Later still, it was proven [26] that most standard modal and superintuitionistic predicate logics are undecidable in languages with only two variables and only one monadic predicate letter. To obtain decidability, it does not help, as one might expect from experience with modal and superintuitionistic propositional logics, to consider monadic fragments of logics of Kripke frames with only finitely many possible worlds: while every recursively enumerable propositional logic of Kripke frames with finitely many worlds¹ is decidable [12], in predicate logic restriction to such frames leads to lack of recursive enumerability [27, 29].

The way to avoiding undecidability in modal predicate logic, surely, lies through defeating Kripke’s trick. One way to achieve this is to restrict the form of modal formulas to make the trick syntactically impossible to implement: following this approach, Wolter and Zakharyaschev [40] consider fragments of modal predicate logics with a decidable modal-free subfragment and the monodic use of modalities whereby modal operators may only be applied to formulas with at most one parameter. Wolter and Zakharyaschev [40] prove that so obtained fragments, which they call monodic, of some undecidable predicate logics—among them, |$\textbf{QK}$|⁠, |$\textbf{QT}$|⁠, |$\textbf{QK4}$| and |$\textbf{QS4}$|—are decidable. Monodic fragments are, probably, largest known decidable fragments of modal predicate logics, subsuming one-variable fragments that have long been known to be decidable [7, 9].

Is it possible to defeat Kripke’s trick semantically? Can we identify semantic conditions under which the trick does not work? In the first part of this paper, we do just that: we prove that monadic fragments of modal predicate logics are decidable—with any number of variables and the unrestricted use of modal operators, and even with equality—over a single Kripke frame containing only finitely many possible worlds, even though their domains may be infinite. Since modal validity is preserved under formation of disjoint unions, this means that monadic fragments of modal predicate logics are decidable over a finite class of Kripke frames each containing only finitely many worlds. Compare this with the situation in propositional logics: there, proofs of the finite frame property usually give us an upper bound on the size of Kripke frames refuting formulas not in the logic; in monadic predicate logic, on the other hand, decidability obtains provided we are given such an upper bound a priori. We then use the obtained decidability result to establish upper complexity bounds, which match the known lower bounds [27, 29], for monadic fragments of modal and superintuitionistic logics of frames with an arbitrary finite number of possible worlds; we also use the obtained result to prove decidability of monadic fragments with equality of logics |$\textbf{QAlt}^=_{n}$| and |$\textbf{QTAlt}^=_{n}$|⁠.

We make a brief note on the kind of modal predicate logics we consider in this paper: since modal logics of expanding domains are reducible to modal logics of constant domains [7, Proposition 3.20], it suffices to prove decidability—in any setting, including ours—only for the latter; our proofs, however, apply simultaneously to the logics of expanding and constant domains; hence, we explicitly consider both.

The paper is structured as follows. Section 2 contains preliminaries on modal predicate logics. In Section 3, we prove decidability of the monadic fragment of the logic of a finite class of Kripke frames each with finitely many possible worlds, but possibly infinite domains of worlds. In Section 4, we use the result of Section 3 to obtain upper bounds for monadic fragments of modal logics of classes of Kripke frames where each frame has an arbitrary finite number of possible worlds and to prove decidability of logics |$\textbf{QAlt}_{n}$| and |$\textbf{QTAlt}_{n}$|⁠. In Section 5, we extend the results of Sections 3 and 4 to languages with equality. In Section 6, we briefly discuss modal predicate logics of frames with a distinguished world. In Section 7, after introducing preliminaries on superintuitionistic predicate logics, we obtain upper bounds for monadic fragments of superintuitionistic logics of Kripke frames with an arbitrary finite number of possible worlds.

2 Preliminaries on modal predicate logics

We use the following notation for sets of numbers: |$\mathbb{N} = \{0, 1, 2, \ldots \}$|⁠; |$\mathbb{N}^{+} = \mathbb{N} - \{0\}$|⁠.

We shall be mostly concerned with monadic formulas, i.e. those containing no predicate letters other than monadic ones (later, in Section 5, we shall also allow equality). The set of monadic |$\mathcal{M}\mathcal{L}$|-formulas is denoted by |$\mathcal{M}\mathcal{L}_{\textit{mon}}$|⁠.

A normal modal predicate logic is a set of formulas containing the validities of the classical predicate logic and formulas of the form |$\Box (\varphi \rightarrow \psi ) \rightarrow (\Box \varphi \rightarrow \Box \psi )$|⁠, and closed under Predicate Substitution, Modus Ponens, Generalisation and Necessitation.² In the rest of the paper, with the exception of Section 6, modal predicate logic always means normal modal predicate logic. A monadic fragment of a modal predicate logic |$L$| is the set |$L \cap \mathcal{M}\mathcal{L}_{\textit{mon}}$| of its monadic formulas.

A Kripke frame is a pair |$\mathfrak{F} = \langle W,R\rangle $|⁠, where |$W$| is a non-empty set of possible worlds and |$R$| is a binary accessibility relation on |$W$|⁠. We say that a Kripke frame |$\langle W, R \rangle $| is finite if |$W$| is a finite set. It should be clear that finite Kripke frames can be represented as words in a finite alphabet; we say that a class |$\mathscr{C}$| of finite Kripke frames is decidable or recursively enumerable if the corresponding language is, respectively, decidable or recursively enumerable.

We use the standard notation for binary relations: if |$R \subseteq W \times W$| and |$X \subseteq W$|⁠, then

• |$R^{0}$| is the identity on |$W$|⁠; |$R^{n+1} = R \circ R^{n}$| whenever |$n \in \mathbb{N}$|⁠;

• |$R^{\ast } = \bigcup \limits _{{n = 0}}^{\infty } R^{n}$|⁠; i.e. |$R^{\ast }$| is the reflexive transitive closure of |$R$|⁠;

• |$R(w) = \{ v \in X: w R v \}$|⁠;

• |$R(X) = \bigcup \{ R(w): w \in X \}$|⁠;

• |$R \upharpoonright X = R \cap (X \times X)$|⁠.

A Kripke frame |$\mathfrak{F} = \langle W, R \rangle $| is rooted at |$w_{0} \in W$|, and |$w_{0}$| is a root of |$\mathfrak{F}$|⁠, if |$W = R^{\ast }(w_{0})$|⁠. A Kripke frame is rooted if it has a root. An augmented frame is rooted if its base is a rooted Kripke frame. Observe that a rooted augmented frame |$\langle W,R, D\rangle $| satisfies (2.2) if, and only if, it has a constant domain, i.e. |$D_{w} = D_{v}$| whenever |$w, v \in W$|⁠.

A Kripke model is a tuple |$\mathfrak{M} = \langle W,R,D,I\rangle $|⁠, where |$\langle W,R, D\rangle $| is an augmented frame and |$I$|⁠, the interpretation of predicate letters with respect to worlds in |$W$|⁠, is a function sending a world |$w\in W$| and an |$n$|-ary predicate letter |$P$| to an |$n$|-ary relation |$I(w,P)$| on |$D(w)$|⁠; in particular, if |$P$| is nullary, then |$I(w,P) \subseteq D^{0}_{w} = \{ \langle \rangle \}$|⁠; we often write |$P^{I, w}$| instead of |$I(w,P)$|⁠. A model |$\langle W, R, D, I \rangle $| is said to be a model over the augmented frame |$\langle W, R, D\rangle $|⁠. An assignment in a model is a map sending each individual variable to an element of |$D^{+}$|⁠. We write |$g^{\prime} \stackrel{x}{=} g$| if assignments |$g$| and |$g^{\prime}$| differ in at most the value of the variable |$x$|⁠.

The truth of an |$\mathcal{M}\mathcal{L}$|-formula |$\varphi $| at a world |$w$| of a model |$\mathfrak{M} = \langle W,R,D,I\rangle $| under an assignment |$g$| is defined by recursion:

• |$\mathfrak{M},w\models ^{g} P(x_{1},\ldots ,x_{n})$| if |$\langle g(x_{1}),\ldots ,g(x_{n})\rangle \in P^{I, w}$|⁠;

• |$\mathfrak{M},w \not \models ^{g} \bot $|⁠;

• |$\mathfrak{M},w\models ^{g}\varphi _{1} \rightarrow \varphi _{2}$| if |$\mathfrak{M},w \not \models ^{g}\varphi _{1}$| or |$\mathfrak{M},w\models ^{g}\varphi _{2}$|⁠;

• |$\mathfrak{M},w\models ^{g}\Box \varphi _{1}$| if |$\mathfrak{M},w^{\prime}\models ^{g}\varphi _{1}$| whenever |$w^{\prime} \in R(w)$|⁠;

• |$\mathfrak{M},w\models ^{g}\forall x\,\varphi _{1}$| if |$\mathfrak{M},w\models ^{g^{\prime}}\varphi _{1}$| whenever |$g^{\prime} \stackrel{x}{=} g$| and |$g^{\prime}(x)\in D_{w}$|⁠.

We say that a formula |$\varphi $| is true at a world  |$w$| of a model |$\mathfrak{M}$|⁠, and write |$\mathfrak{M},w\models \varphi $|⁠, if |$\mathfrak{M},w\models ^{g} \varphi $| holds for every |$g$| sending the parameters of |$\varphi $| to elements of |$D_{w}$|⁠. We say that a formula |$\varphi $| is valid at a world |$w$| of an augmented frame |$\boldsymbol{\mathfrak{F}}$|, and write |$\boldsymbol{\mathfrak{F}}, w \models \varphi $|⁠, if |$\mathfrak{M},w\models \varphi $| holds for every model |$\mathfrak{M}$| over |$\boldsymbol{\mathfrak{F}}$|⁠. We say that a formula |$\varphi $| is valid on an augmented frame |$\boldsymbol{\mathfrak{F}}$|, and write |$\boldsymbol{\mathfrak{F}} \models \varphi $|⁠, if |$\boldsymbol{\mathfrak{F}}, w \models \varphi $| holds for every world |$w$| of |$\boldsymbol{\mathfrak{F}}$|⁠. We say that a formula |$\varphi $| is valid on a Kripke frame |$\mathfrak{F}$|, and write |$\mathfrak{F} \models \varphi $|⁠, if |$\varphi $| is valid on every augmented frame over |$\mathfrak{F}$|⁠. We say that a formula |$\varphi $| is valid on a class |$\mathscr{C}$| of Kripke frames, and write |$\mathscr{C} \models \varphi $|⁠, if |$\varphi $| is valid on every Kripke frame from |$\mathscr{C}$|⁠; similarly for augmented frames. A set |$\varGamma $| of formulas is valid on an augmented frame or on a Kripke frame if every formula from |$\varGamma $| is valid on the said frame.

We shall occasionally use the following notation. Let |$\mathfrak{M} = \langle W,R,D,I\rangle $| be a model, |$w \in W$| and |$a_{1}, \ldots , a_{n} \in D_{w}$|⁠; let also |$\varphi (x_{1}, \ldots , x_{n})$| be a formula with no parameters other than |$x_{1}, \ldots , x_{n}$|⁠, and let |$g$| be an assignment with |$g(x_{1}) = a_{1}, \ldots , g(x_{n}) = a_{n}$|⁠. Then |$\mathfrak{M}, w \models \varphi (a_{1}, \ldots , a_{n})$| means the same as |$\mathfrak{M}, w \models ^{g} \varphi (x_{1}, \ldots , x_{n})$|⁠.

A modal predicate logic is Kripke complete if it coincides with the set of formulas valid on some class of augmented frames. Observe that, if |$\mathscr{C}$| is a class of Kripke frames, then logics |${{\texttt{ML}}} \mathscr{C}$| and |${{\texttt{ML}}_{{\textit{c}}}} \mathscr{C}$| are Kripke complete.

Let |$J$| be a non-empty set. The disjoint union of a class |$\{ \mathfrak{F}_{j} \,: j \in J\}$| of Kripke frames, with |$\mathfrak{F}_{j} = \langle W_{j}, R_{j} \rangle $|⁠, is the Kripke frame |$\bigsqcup \limits _{j \in J} \mathfrak{F}_{j} = \langle W, R \rangle $| defined by

• |$W = \bigcup \{ W_{j} \times \{j\}: j \in J \}$|⁠;

• |$ \langle w, j \rangle R \langle w^{\prime}, j^{\prime} \rangle \iff j = j^{\prime} ~\&~ w R_{j} w^{\prime}$|⁠.

A Kripke frame |$\langle W^{\prime}, R^{\prime} \rangle $| is a subframe of a Kripke frame |$\langle W, R \rangle $| if |$W^{\prime} \subseteq W$| and |$R^{\prime} = R \upharpoonright W^{\prime}$|⁠. The following is well known and straightforward to check:

3 Main observation

The main technical observation of the present paper is that refutability of a monadic formula on a finite Kripke frame implies its refutability on a finite augmented frame of a bounded size.

We next generalise Theorem 3.3 to logics of those Kripke frames that are not necessarily finite, but whose branching factor is bounded by a natural number. If |$n \in \mathbb{N}$|⁠, we say that a Kripke frame |$\langle W, R \rangle $| is |$n$|-alternative if |$|R(w)| \leqslant n$| whenever |$\langle W, R \rangle \in \mathscr{C}$| and |$w \in W$|⁠.

We conclude this section by noticing that, in the statement of Theorem 3.5, the requirement that |$\mathscr{C}$| be recursively enumerable is crucial. Recall that, if |$A, B \subseteq \mathbb{N}$|⁠, then |$A$| is recursive relative to  |$B$|⁠, also written as |$A \leqslant _{R} B$|⁠, provided there exists an algorithm for membership in |$A$| that uses an oracle for membership in |$B$|⁠. Intuitively, |$A \leqslant _{R} B$| means that membership in |$B$| is at least as hard to decide as membership in |$A$|⁠. Sets |$A$| and |$B$| are recursively equivalent of both |$A \leqslant _{R} B$| and |$B \leqslant _{R} A$|⁠. If a set is not a subset of |$\mathbb{N}$|⁠, then it is identified, in this context, with the set of the Gödel numbers of its elements.

Since the formulas |$\alpha _{n}$| used in the proof of Proposition 3.6 are, in fact, propositional, the propositional fragment of each logic |$\textbf{L}^{A}$| and |$\textbf{L}_{{\texttt{c}}}^{A}$| is undecidable provided |$A$| is undecidable. We do not know counterexamples to Theorem 3.5 with decidable propositional fragments.

4 Some corollaries on logics without equality

We now use the results of Section 3 to answer questions concerning algorithmic complexity of modal logics of monadic predicates left unanswered in our previous work [27].

First, we introduce some notation. If |$L$| is a modal predicate logic, then the logic of the class of finite Kripke frames validating |$L$| is denoted by |$L_{\textit{wfin}}$|⁠; observe that every logic |$L_{\textit{wfin}}$| is, by definition, Kripke complete. If |$L$| is a modal predicate logic and |$\varphi $| a modal formula, then |$L \oplus \varphi $| denotes the smallest normal modal predicate logic that includes |$L \cup \{\varphi \}$|⁠; similarly for propositional logics. If |$L$| is a predicate modal logic, then |$L\textbf{.bf}$| denotes the logic |$L \oplus \boldsymbol{bf}$|⁠, where |$\boldsymbol{bf} = \forall x\, \Box P(x) \rightarrow \Box \forall x\, P(x)$| is the Barcan formula; the Barcan formula is valid precisely on augmented frames with locally constant domains [10, Proposition 3.4.2]. If |$L$| is a normal modal propositional logic, then |$\textbf{Q}L$| denotes the smallest normal modal predicate logic that includes |$L$|⁠. The following is well known and easy to check:

If |$L$| is a modal propositional logic, then |${{\texttt{KF}}} L$| denotes the class of Kripke frames validating |$L$|⁠.

We now recall the following result [27, Theorem 3.9] on lower bounds for the logics mentioned in Lemma 4.2:

Therefore, we obtain the following:

Recall that a modal propositional logic is elementary if it is determined by a class of Kripke frames satisfying a classical first-order condition on the accessibility relation.

In particular, we obtain the following:

We note that Theorem 4.4 means that logics |$\textbf{Q}L_{\textit{wfin}}$| and |$\textbf{Q}L.\textbf{bf}_{\textit{wfin}}$|⁠, with |$L$| satisfying the statement of theorem, are not recursively embeddable into their monadic fragments. Indeed, these logics are all conservative extensions of the |$\varSigma ^{0}_{1}$|-hard classical first-order logic (to see this, observe that each of them admits a frame containing a world with an infinite domain); hence, they are all |$\varSigma ^{0}_{1}$|-hard. On the other hand, by Theorem 4.4, the monadic fragments of these logics are |$\varPi ^{0}_{1}$|-complete. We briefly mention the motivation for the question of whether a logic is embeddable into its own fragment. To prove that a fragment |$F$| of a logic |$L$| has the same algorithmic complexity as the full logic |$L$|⁠, one can either independently establish the complexity both of |$F$| and of |$L$| or, else, to (say, recursively or polytime) embed |$L$| into |$F$|⁠. For example, one can prove that fragments with a few propositional variables, typically one or two, of many modal propositional logics have the same complexity as full logics either by independently establishing the complexity of finite-variable fragments [2, 5, 11, 20, 22] or by showing that full logics are polytime embeddable into those fragments [21, 23, 25, 30–32]. In predicate modal logic, the first approach is almost exclusively used [8, 13, 14, 26–29], with very few exceptions [16], but the second approach has an advantage: apart from establishing computational complexity of a fragment, it produces an explicit embedding of a logic into its own fragment; moreover, as a rule, such an embedding is informative since it respects the structure of formulas.

Recall that a modal predicate logic |$L$| is strongly Kripke complete with respect to a class |$\mathscr{C}$| of Kripke frames if |$L = {{\texttt{ML}}} \mathscr{C}$| and, moreover, every |$L$|-consistent set of closed formulas is satisfiable in a model over a Kripke frame validating |$L$|⁠. The following is known [36]:

Let |$\mathfrak{F} = \langle W, R \rangle $| be a Kripke frame; if there exists |$m \in \mathbb{N}^{+}$| such that |$R^{m-1}(W)\ne \varnothing $| and |$R^{m}(W)=\varnothing $|⁠, then |$m$| is called the depth of |$\mathfrak{F}$|⁠; otherwise, the depth of |$\mathfrak{F}$| is infinite. It is well known and easy to check that, for every |$m \in \mathbb{N}^{+}$|⁠, a Kripke frame |$\mathfrak{F}$| validates |$\Box ^{m} \bot $| if, and only if, the depth of |$\mathfrak{F}$| is at most |$m$|⁠. Since a constant propositional formula is valid on the canonical frame of every logic it belongs to, adding constant propositional formulas to a logic preserves strong Kripke completeness; hence, Proposition 4.7 implies the following:

We now state our decidability results:

We note that, if |$L = \textbf{QAlt}_{n}$|⁠, |$L = \textbf{QTAlt}_{n}$| or |$L = \textbf{Alt}_{n}\oplus \Box ^{m}\bot $|⁠, then we do not need separate statements about the logics |$L_{\textit{wfin}}$| and |$L\textbf{.bf}_{\textit{wfin}}$|⁠, since, in this case, |$L_{\textit{wfin}} = L$| and |$L\textbf{.bf}_{\textit{wfin}} = L\textbf{.bf}$|⁠.

5 Modal logics with equality

The classical predicate logic of monadic predicates is decidable even if the language contains equality [3]. In this section, we show that the results of Sections 3 and 4 hold true for languages with equality. Whereas in the classical predicate logic the treatment of equality as identity (‘normal models’) and as congruence are equivalent, in modal logic, in general, they are not. We, therefore, consider them separately. We also consider a special type of equality as congruence, called closed equality, which, unlike identity, is modally definable, but is equivalent to identity over some classes of augmented frames.

5.1 Preliminaries on modal logics with equality

A modal predicate language with equality |$\mathcal{M}\mathcal{L}^=$| is obtained by adding to a modal predicate language, as described in Section 2, a designated binary predicate letter =. Formulas of |$\mathcal{M}\mathcal{L}^=$| are called modal formulas with equality. A monadic formula with equality is a formula of |$\mathcal{M}\mathcal{L}^=$| containing no predicate letters other than monadic ones and equality; the set of all such formulas is denoted by |$\mathcal{M}\mathcal{L}^=_{\textit{mon}}$|⁠.

If |$L$| is a modal predicate logic, then |$L^=$| and |$L^{ce}$| denote the smallest modal predicate logics with, respectively, equality and closed equality that include |$L$|⁠. If |$L$| is a modal predicate logic with equality or with closed equality, then by its monadic fragment with equality we mean the set |$L \cap \mathcal{M}\mathcal{L}^=_{\textit{mon}}$|⁠.

• |$\mathfrak{M}, w \models ^{g} x = y$| if |$g(x) \equiv _{w} g(y)$|⁠,

and the other truth clauses are as in the Kripke semantics described in Section 2. Truth and validity are defined analogously to the Kripke semantics described in Section 2.

• |$\mathfrak{M}, w \models ^{g} x = y$| if |$g(x) = g(y)$|⁠.

We define the following classes of augmented frames with equality over a class |$\mathscr{C}$| of Kripke frames:

• |${{\texttt{AF}}^{\simeq }} \mathscr{C} = \{ \langle W, R, D, \equiv \rangle : \langle W, R \rangle \in \mathscr{C}\}$|⁠;

• |${{\texttt{AF}}^{\textit{ce}}} \mathscr{C}$| and |${{\texttt{AF}}^{\textit{id}}} \mathscr{C}$| are the subclasses of |${{\texttt{AF}}^{\simeq }} \mathscr{C}$| containing all the augmented frames with, respectively, closed equality and identity from |${{\texttt{AF}}^{\simeq }} \mathscr{C}$|⁠;

• |${{\texttt{AF}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$|⁠, |${{\texttt{AF}}^{\textit{ce}}_{{\textit{c}}}} \mathscr{C}$| and |${{\texttt{AF}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$| are the subclass of, respectively, |${{\texttt{AF}}^{\simeq }} \mathscr{C}$|⁠, |${{\texttt{AF}}^{\textit{ce}}} \mathscr{C}$| and |${{\texttt{AF}}^{\textit{id}}} \mathscr{C}$| containing all the augmented frames with locally constant domains from a respective class.

We write |${{\texttt{AF}}^{\simeq }} \mathfrak{F}$| instead of |${{\texttt{AF}}^{\simeq }} \{ \mathfrak{F} \}$| and similarly for |${{\texttt{AF}}^{\simeq }_{{\textit{c}}}} \{ \mathfrak{F} \}$|⁠, |${{\texttt{AF}}^{\textit{ce}}} \{ \mathfrak{F} \}$|⁠, |${{\texttt{AF}}^{\textit{ce}}_{{\textit{c}}}} \{ \mathfrak{F} \}$|⁠, |${{\texttt{AF}}^{\textit{id}}} \{ \mathfrak{F} \}$| and |${{\texttt{AF}}^{\textit{id}}_{{\textit{c}}}} \{ \mathfrak{F} \}$|⁠. If |$\mathscr{C}$| is a class of Kripke frames, we define the following sets of formulas:

• |${{\texttt{ML}}}^{\simeq } \mathscr{C}$| and |${{\texttt{ML}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$| are sets of |$\mathcal{M}\mathcal{L}^=$|-formulas valid on, respectively, |${{\texttt{AF}}^{\simeq }} \mathscr{C}$| and |${{\texttt{AF}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$|⁠;

• |${{\texttt{ML}}}^{\textit{ce}} \mathscr{C}$|⁠, |${{\texttt{ML}}}^{\textit{ce}}_{{\textit{c}}} \mathscr{C}$|⁠, |${{\texttt{ML}}^{\textit{id}}} \mathscr{C}$| and |${{\texttt{ML}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$| are sets of |$\mathcal{M}\mathcal{L}^=$|-formulas valid on, respectively, |${{\texttt{AF}}^{\textit{ce}}} \mathscr{C}$|⁠, |${{\texttt{AF}}^{\textit{ce}}_{{\textit{c}}}} \mathscr{C}$|⁠, |${{\texttt{AF}}^{\textit{id}}} \mathscr{C}$| and |${{\texttt{AF}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$|⁠.

It is easy to check that |${{\texttt{ML}}}^{\simeq } \mathscr{C}$| and |${{\texttt{ML}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$| are modal predicate logics with equality and that |${{\texttt{ML}}}^{\textit{ce}} \mathscr{C}$|⁠, |${{\texttt{ML}}}^{\textit{ce}}_{{\textit{c}}} \mathscr{C}$|⁠, |${{\texttt{ML}}^{\textit{id}}} \mathscr{C}$| and |${{\texttt{ML}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$| are modal predicate logics with closed equality.

In certain cases, but not always, the semantic treatment of = as identity can be captured syntactically by axioms of closed equality [37, Theorem 1]:

The following is easy to check:

Recall that, if |$L$| is a modal predicate logic, with or without equality, then |$L$| is said to be strongly Kripke complete with respect to a class |$\mathscr{C}$| of augmented frames with equality if every |$L$|-consistent set of formulas is satisfied in a Kripke model over a frame from |$\mathscr{C}$|⁠; this notion is analogous to strong completeness with respect to a class of Kripke frames introduced earlier. We shall make use of the following result on the transfer of completeness:

5.2 Results on modal logics with equality

We now prove the analogue of Lemma 3.1 for modal logics with equality:

From Lemma 5.5, we obtain analogues of Theorems 3.3, 3.4 and 3.5 for modal logics with equality:

In particular, we obtain the following:

The logics |$\textbf{Q}L^=_{\textit{wfin}}$|⁠, |$\textbf{Q}L\textbf{.bf}^=_{\textit{wfin}}$|⁠, |$\textbf{Q}L^{\textit{ce}}_{\textit{wfin}}$| and |$\textbf{Q}L\textbf{.bf}^{\textit{ce}}_{\textit{wfin}}$| mentioned in Theorem 5.9 are all conservative extensions of the |$\varSigma ^{0}_{1}$|-hard classical first-order logic; hence, they are all |$\varSigma ^{0}_{1}$|-hard. Since, by Theorem 5.9, their monadic fragments are |$\varPi ^{0}_{1}$|-complete, the full logics are not recursively embeddable into their monadic fragments with equality.

We next establish decidability of the logics |$\textbf{QAlt}^=_{n}$|⁠, |$\textbf{QAlt}^{ce}_{n}$|⁠, |$\textbf{QTAlt}^=_{n}$| and |$\textbf{QTAlt}^{ce}_{n}$|⁠, as well as their counterparts with the Barcan formula. We use the following well-known fact [37, Theorem 1]:

The following is also true:

6 Modal logics of frames with a distinguished world

Constructions described in Sections 3 and 5 are also applicable to logics of frames with a distinguished world. Recall from Section 2 that a Kripke frame |$\mathfrak{F} = \langle W, R \rangle $| is rooted at |$d \in W$| if |$W = R^{\ast }(d)$|⁠. If |$\mathfrak{F}$| is a Kripke frame rooted at |$d$|⁠, then a tuple |$\mathfrak{F}_{d} = \langle \mathfrak{F},d \rangle $| is called a frame with a distinguished world |$d$|; if |$\mathfrak{F} = \langle W, R \rangle $|⁠, we also write |$\langle W, R, d \rangle $| for |$\langle \mathfrak{F},d \rangle $|⁠. The modal logic of a frame |$\mathfrak{F}_{d}$| with a distinguished world is defined as follows: |${{\texttt{ML}}} \mathfrak{F}_{d} = \{\varphi : \mathfrak{F}, d \models \varphi \}$|⁠; i.e. the logic contains the formulas valid in |$\mathfrak{F}$| at |$d$| (rather than at every world of |$\mathfrak{F}$|⁠); logics of classes of frames with a distinguished world are defined analogously. Such logics are not necessarily normal, as defined in Section 2; they are quasi-normal, i.e. they satisfy all the requirements for normal modal logics except, possibly, closure under Necessitation (observe that every quasi-normal logic extends |$\textbf{QK}$|⁠). Axiomatically, quasi-normal modal logics are defined as deductive systems without the postulated rule of Necessitation.⁶

Figure 1.

Frame |$\mathfrak{F}_{d}$| with |$d = w_{0}^{0}$|⁠.

Open in new tabDownload slide

The frame |$\mathfrak{F}_{d}$| is infinite and, for every |$n\in \mathbb{N}$|⁠, contains a point that sees |$n$| worlds; hence, |$\mathfrak{F}_{d}$| does not satisfy the requirements of either Theorem 3.2 or Theorem 3.4. Nevertheless, since determining membership in |${{\texttt{ML}}} \mathfrak{F}_{d}$| involves evaluation of formulas only at |$d$| and, so, only the worlds accessible from |$d$| in the number of steps not exceeding the modal depth of a formula are pertinent to the evaluation, the constructions of Sections 3 and 5 can be easily adjusted to prove decidability of the monadic fragment of both |${{\texttt{ML}}} \mathfrak{F}_{d}$| and of its counterpart with equality.

It should be clear that this example is easily generalizable. If |$\mathfrak{F}_{d} = \langle W, R, d \rangle $| is a Kripke frame with a distinguished world, denote by |$\mathfrak{F}^{n}_{d}$| the subframe of |$\mathfrak{F}_{d}$| with the set of worlds |$\bigcup \{ w \in W: w \in R^{k}(d), 0 \leqslant k \leqslant n\}$|⁠.

The argument equally applies to logics with equality (the notation is analogous to that of Section 5):

7 Superintuitionistic logics

In this section, we use the results of Section 3 to obtain algorithmic upper bounds for monadic superintuitionistic logics of finite Kripke frames; this answers questions left open in our earlier work [29].

7.1 Preliminaries

An unrestricted intuitionistic predicate language (without equality) contains countably many individual variables; for every |$n \in \mathbb{N}$|⁠, countably many |$n$|-ary predicate letters; the propositional constant |$\bot $|⁠; the binary connectives |$\wedge $|⁠, |$\vee $| and |$\to $|⁠; and the quantifier symbols |$\exists $| and |$\forall $|⁠. Formulas are defined in the usual way. A language with equality is obtained by adding a designated binary predicate letter =. As in modal languages, monadic formulas are those with only monadic predicate letters, and monadic formulas with equality are those containing only monadic predicate letters and =.

If |$L$| is a superintuitionistic predicate logic (with or without equality) and |$\varphi $| a formula, then |$L + \varphi $| denotes the smallest superintuitionistic logic including |$L \cup \{\varphi \}$|⁠.

A Kripke frame |$\mathfrak{F} = \langle W,R\rangle $| is intuitionistic if |$R$| is a partial order on |$W$|⁠. An intuitionistic augmented frame is an augmented frame based on an intuitionistic Kripke frame. An intuitionistic Kripke model is a Kripke model over an intuitionistic augmented frame where the interpretation |$I$| satisfies the heredity condition: |$wRw^{\prime}$| implies |$I(w,P) \subseteq I(w^{\prime},P)$|⁠, for every |$w, w^{\prime} \in W$| and every predicate letter |$P$|⁠. Assignments in models are defined as in the modal semantics. The truth of a formula |$\varphi $| at a world |$w$| of a model |$\mathfrak{M}$| under an assignment |$g$| is defined by recursion:

• |$\bullet $|

  |$\mathfrak{M},w \Vdash ^{g} P(x_{1},\ldots ,x_{n})$| if |$\langle g(x_{1}),\ldots ,g(x_{n})\rangle \in P^{I,w}$|⁠;

• |$\bullet $|

  |$\mathfrak{M},w\not \Vdash ^{g} \bot $|⁠;

• |$\mathfrak{M},w\Vdash ^{g}\varphi _{1}\wedge \varphi _{2}$| if |$\mathfrak{M},w\Vdash ^{g}\varphi _{1}$| and |$\mathfrak{M},w\Vdash ^{g}\varphi _{2}$|⁠;

• |$\bullet $|

  |$\mathfrak{M},w\Vdash ^{g}\varphi _{1}\vee \varphi _{2}$| if |$\mathfrak{M},w\Vdash ^{g}\varphi _{1}$| or |$\mathfrak{M},w\Vdash ^{g}\varphi _{2}$|⁠;

• |$\bullet $|

  |$\mathfrak{M},w\Vdash ^{g}\varphi _{1}\to \varphi _{2}$| if |$\mathfrak{M},w^{\prime} \not \Vdash ^{g}\varphi _{1}$| or |$\mathfrak{M},w^{\prime}\Vdash ^{g}\varphi _{2}$| whenever |$w^{\prime}\in R(w)$|⁠;

• |$\bullet $|

  |$\mathfrak{M},w\Vdash ^{g}\exists x\,\varphi _{1}$| if |$\mathfrak{M},w\Vdash ^{g^{\prime}}\varphi _{1}$|⁠, for some assignment |$g^{\prime}$| such that |$g^{\prime} \stackrel{x}{=} g$| and |$g^{\prime}(x)\in D(w)$|⁠;

• |$\bullet $|

  |$\mathfrak{M},w\Vdash ^{g}\forall x\,\varphi _{1}$| if |$\mathfrak{M},w^{\prime}\Vdash ^{g^{\prime}}\varphi _{1}$| whenever |$w^{\prime}\in R(w)$|⁠, |$g^{\prime} \stackrel{x}{=} g$| and |$g^{\prime}(x)\in D(w^{\prime})$|⁠.

Validity is defined analogously to the modal semantics. If |$\mathscr{C}$| is a class of intuitionistic Kripke frames, then the set of formulas valid on every frame in |$\mathscr{C}$| and the set of formulas valid on every augmented frame with constant domains over a frame from |$\mathscr{C}$| are denoted by, respectively, |${{\texttt{siL}}} \mathscr{C}$| and |${{\texttt{siL}}_{{\textit{c}}}} \mathscr{C}$|⁠; both sets are superintuitionistic predicate logics.

If |$L$| is a superintuitionistic predicate logic, then |$L.\textbf{cd}$| denotes the logic |$L + \boldsymbol{cd}$|⁠, where |$\boldsymbol{cd} = \forall x\, (P(x) \vee q) \rightarrow \forall x P(x) \vee q$| is the constant domain axiom, which is valid precisely on augmented intuitionistic frames with locally constant domains [10, Proposition 3.4.2]. The notation |$L_{\textit{wfin}}$| has the same meaning as for modal logics.

An intuitionistic augmented frame with equality is an augmented frame with equality over an intuitionistic Kripke frame. An intuitionistic model with equality is a model with equality over an intuitionistic augmented frame with equality and satisfying the heredity condition for interpretations. Truth of formulas |$x = y$| is defined as in the modal semantics with equality. The following is well known [37] and easy to check:

Notation |${{\texttt{siL}}^{\simeq }} \mathscr{C}$|⁠, |${{\texttt{siL}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$|⁠, |${{\texttt{siL}}^{\textit{de}}} \mathscr{C}$|⁠, |${{\texttt{siL}}^{\textit{de}}_{{\textit{c}}}} \mathscr{C}$|⁠, |${{\texttt{siL}}^{\textit{id}}} \mathscr{C}$| and |${{\texttt{siL}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$| has the meaning similar to notation, respectively, |${{\texttt{ML}}}^{\simeq } \mathscr{C}$|⁠, |${{\texttt{ML}}^{\simeq }_{{\textit{c}}}} \mathscr{C}$|⁠, |${{\texttt{ML}}}^{\textit{ce}} \mathscr{C}$|⁠, |${{\texttt{ML}}}^{\textit{ce}}_{{\textit{c}}} \mathscr{C}$|⁠, |${{\texttt{ML}}^{\textit{id}}} \mathscr{C}$| and |${{\texttt{ML}}^{\textit{id}}_{{\textit{c}}}} \mathscr{C}$| for modal logic. An analogue of Proposition 5.2 holds for superintuitionistic logics [37].

7.2 Corollaries of results on modal logics

We now obtain, using the results of Sections 3 and 5 together with the properties of the Gödel–Tarski translation, upper bounds for monadic superintuitionistic logics determined by finite intuitionistic Kripke frames. We start with two technical results:

We next recall the definitions of some superintuitionistic propositional logics:

• |$\bullet $|

  |$\textbf{KC}$| is the logic of convergent partial orders;

• |$\bullet $|
  |$\textbf{KP} = \textbf{Int} + (\neg \varphi \rightarrow \psi \vee \chi ) \rightarrow ((\neg \varphi \rightarrow \psi ) \vee (\neg \varphi \rightarrow \chi ))$| is the logic of the class of frames satisfying the following condition on accessibility relation:

  $$\begin{align*} & \begin{array}{c} \forall x \forall y \forall z\, ( xRy \wedge xRz \rightarrow yRz \vee zRy \vee \exists u\, ( xRu \wedge uRy \wedge uRz \wedge \\ \wedge \forall v\, ( uRv \rightarrow \exists w\, ( vRw \wedge ( yRw \vee zRw ))))). \end{array} \end{align*}$$

We also recall that, if |$\varphi $| is a propositional formula with a single nullary letter, then |$\textbf{Int} + \varphi $| is the propositional logic of some generated subframe of the frame known as the Rieger–Nishimura ladder [17]; see also [6, Section 8.7].

If |$L$| is a superintuitionistic predicate logic, the notation |$L_{\textit{wfin}}$| has the meaning analogous to the meaning of this notation for modal logics; similarly for the notation |${{\texttt{KF}}} L$| in case |$L$| is a superintuitionistic propositional logic.

We now recall the following result [29, Theorem 3.8] on lower bounds for the logics mentioned in Lemma 7.6:

Since the logics |$\textbf{Q}L_{\textit{wfin}}$| and |$\textbf{Q}L\textbf{.cd}_{\textit{wfin}}$| mentioned in Theorem 7.8 are |$\varSigma ^{0}_{1}$|-hard [29, Remark 3.4] and, by Theorem 7.8, their monadic fragments are |$\varPi ^{0}_{1}$|-complete, it follows that the full logics are not recursively embeddable into their monadic fragments.

8 Conclusion

Table 1 summarizes the complexity results presented in this paper.

It should be clear that all the results on modal logics presented in this paper hold not only for monomodal, but also for multimodal languages with several unary modal operators: none of our proofs require any conceptual changes in a multimodal setting. Constructions of Sections 3 and 5 are applicable to logics of frames with sets of distinguished worlds and to logics of frames with non-normal worlds; such frames are used [15] in the semantics for non-normal modal logics [41], i.e. those not extending |$\textbf{QK}$|⁠.

Observe that (2.2) is an instance of (8.1) with |$n = 0$|⁠; condition (8.1) corresponds to the formula |$\Box ^{n} \boldsymbol{bf}$|⁠. Therefore, our techniques are applicable to logics of the form |$L_{\textit{wfin}}$|⁠, where |$L = L^{\prime} \oplus \Box ^{n} \boldsymbol{bf}$|⁠. The condition (8.1) naturally arises in the context of the boxing of predicate modal logics studied by Shehtman [35, Section 3].

Acknowledgements

We are grateful to anonymous reviewers for helping to improve the paper. This research was supported by Russian Science Foundation, project 21-18-00195.

Footnotes

References