Decidable fragments of first-order modal logics with counting quantifiers over varying domains

TL;DR

This paper analyzes the computational complexity of one-variable fragments of first-order modal logics with counting quantifiers over varying domains, providing tight bounds for satisfiability problems in different settings.

Contribution

It establishes optimal complexity bounds for the satisfiability of these fragments, including cases with binary and unary encoding of counting quantifiers over different domain types.

Findings

Optimal NExpTime upper bounds for minimal first-order modal logic QK with counting quantifiers.

PSpace-completeness for unary-encoded counting quantifiers over expanding domains.

ExpTime-hardness for decreasing domains with unary-encoded counting quantifiers.

Abstract

This paper explores the computational complexity of various natural one-variable fragments of first-order modal logics with the addition of counting quantifiers, over both constant and varying domains. The addition of counting quantifiers provides us a rich language with which to succinctly express statements about the quantity of objects satisfying a given first-order property, using a single variable. Optimal NExpTime upper-bounds are provided for the satisfiability problems of the one-variable fragment of the minimal first-order modal logic QK, over both constant and expanding/decreasing domain models, where counting quantifiers are encoded as binary strings. For the case where the counting quantifiers are encoded as unary strings, or are restricted to a finite set of quantifiers, it is shown that the satisfiability problem over expanding domains is PSpace-complete, whereas over decreasing domains the problem is shown to be ExpTime-hard.

Equations

$$\phi ::=P_i(x_{i_1},\dots ,x_{i_n})\mid \neg \phi \mid ({\phi }_1\wedge {\phi }_2)\mid ◊\phi \mid {\exists }_{\le c}x\phi$$

$$\begin{array}[]{lcl}\mathfrak{M},w\models^{\mathfrak{h}}P_{i}(x_{1},\dots,x_{n})&\ \stackrel{{\scriptstyle{\mbox{\scriptsize}}}}{{\Longleftrightarrow}}&\big{(}\mathfrak{h}(x_{1}),\dots,\mathfrak{h}(x_{n})\big{)}\in\mathfrak{I}(w,P_{i}),\\[5.0pt] \mathfrak{M},w\models^{\mathfrak{h}}\neg\varphi&\stackrel{{\scriptstyle{\mbox{\scriptsize}}}}{{\Longleftrightarrow}}&\mathfrak{M},w\not\models^{\mathfrak{h}}\varphi,\\[5.0pt] \mathfrak{M},w\models^{\mathfrak{h}}(\varphi_{1}\land\varphi_{2})&\stackrel{{\scriptstyle{\mbox{\scriptsize}}}}{{\Longleftrightarrow}}&\mathfrak{M},w\models^{\mathfrak{h}}\varphi_{1}\mbox{ and }\mathfrak{M},w\models^{\mathfrak{h}}\varphi_{2},\\[5.0pt] \mathfrak{M},w\models^{\mathfrak{h}}\Diamond\varphi&\stackrel{{\scriptstyle{\mbox{\scriptsize}}}}{{\Longleftrightarrow}}&wRv\mbox{ and }\mathfrak{M},v\models^{\mathfrak{h}}\varphi,\ \mbox{for some $v\in W$},\end{array}$$

$$\mathfrak{M},w{\models }^{\mathfrak{h}}({\exists }_{\le c}x\phi )\stackrel{\text{mbox}}{⟺}\left|\{a\in D:\mathfrak{M},w{\models }^{\mathfrak{h}(x/a)}\phi \}\right|\le c,$$

$$({\exists }_{\le c}x\xi )\in t\stackrel{\text{mbox}}{⟺}\sum _{t^{\prime }\in T(\xi )}\mu (t^{\prime })\le c,$$

$$\exists v\in W;w\prec v\text{mbox}and\xi \in r_i(v)⟹◊\xi \in r_i(w),$$

$$◊\xi \in r_i(w)⟹\exists v\in W;w\prec v\text{mbox}and\xi \in r_i(v),$$

$$\mu_{w}(t)=\min\big{(}{\left|{\{i\in I:r_{i}(w)=t\}}\right|},\ C+1\big{)}.$$

$${\mathrm{tp}}_w^{\mathfrak{M}}[a]=\{\xi \in \mathsf{sub}(\phi ):\mathfrak{M},w{\models }^a\xi \},$$

$$T_w$$

$${\mu }_w(t)$$

$$({\exists }_{\le c}x\xi )\in {\mathrm{tp}}_w^{\mathfrak{M}}[a]$$

$$\stackrel{\text{mbox}}{⟺}\left|\{b\in D:\mathfrak{M},w{\models }^b\xi \}\right|\le c,$$

$$\stackrel{\text{mbox}}{⟺}\sum _{t^{\prime }\in T_w(\xi )}\left|\{b\in D:{\mathrm{tp}}_w^{\mathfrak{M}}[b]=t^{\prime }\}\right|\le c,$$

$$\stackrel{\text{mbox}}{⟺}\sum _{t^{\prime }\in T_w(\xi )}{\mu }_w(t^{\prime })\le c.$$

$$f_a(w)={\mathrm{tp}}_w^{\mathfrak{M}}[a],$$

$$\mathfrak{I}(w,P_{j})=\big{\{}i\in I:P_{j}(x)\in r_{i}(w)\big{\}},$$

$$\mathfrak{M},w{\models }^i\psi \stackrel{\text{mbox}}{⟺}\psi \in r_i(w),$$

$$\mathfrak{M},w{\models }^i{P}_j(x)\stackrel{\text{mbox}}{⟺}i\in \mathfrak{I}(w,P_j)\stackrel{\text{mbox}}{⟺}{P}_j(x)\in r_i(w).$$

$$\mathfrak{M},w{\models }^i\neg \xi \stackrel{\text{mbox}}{⟺}\mathfrak{M},w/{\models }^i\xi \stackrel{\text{mbox}(I.H.)}{⟺}\xi \notin r(w)\stackrel{\text{mbox}(tp1)}{⟺}\neg \xi \in r_i(w).$$

$$\mathfrak{M},w{\models }^i({\xi }_1\wedge {\xi }_2)$$

$$\stackrel{\text{mbox}(I.H.)}{⟺}{\xi }_1\in r_i(w)\text{mbox}and{\xi }_2\in r_i(w),$$

$$\stackrel{\text{mbox}(tp2)}{⟺}({\xi }_1\wedge {\xi }_2)\in r_i(w).$$

$$\mathfrak{M},w{\models }^i◊\xi$$

$$\displaystyle\stackrel{{\scriptstyle{\mbox{\scriptsize(I.H.)}}}}{{\Longleftrightarrow}}\quad w\prec v\ \mbox{and}\ \xi\in r_{i}(v),\quad\mbox{for some $v\in W$},$$

$$\stackrel{\text{mbox}}{⟺}◊\alpha \in r_i(w)\text{mbox}by\text{ref}qm:coherenceand\text{ref}qm:saturation.$$

$$\mathfrak{M},w{\models }^i({\exists }_{\le c}x\xi )$$

$$\stackrel{\text{mbox}(I.H.)}{⟺}\left|\{j\in I:\xi \in r_j(w)\}\right|\le c$$

$$\stackrel{\text{mbox}}{⟺}\sum _{t\in T_w(\xi )}\left|\{j\in I:r_j(w)=t\}\right|\le c$$

$$\stackrel{\text{mbox}\text{ref}qm:runs}{⟺}\sum _{t\in T_w(\xi )}{\mu }_w(t)\le c$$

$$\stackrel{\text{mbox}\text{ref}qs:saturation}{⟺}({\exists }_{\le c}x\xi )\in r(w).$$

$$\left|W\right|\le m^2{2}^{8(nm)}C\text{mbox}and\left|I\right|\le m{2}^{5(nm)}C.$$

$$W_{k+1}=\big{\{}v_{(w,t,\alpha)}\in W\ :\ w\in W_{k},\ t\in T_{w},\mbox{ and }\Diamond\alpha\in t\big{\}},$$

$$W^{\prime }=\bigcup _{k=0}^m{W}_{k}u{\prec }^{\prime }v\stackrel{\text{mbox}}{⟺}u\prec v,\text{mbox}and{\text{q}}^{\prime }(u)=\text{q}(u),$$

$$I^{\prime }$$

$${\mathfrak{R}}^{\prime }$$

$$\left|W^{\prime }\right|$$

$$\left|I^{\prime }\right|$$

Full text

1 Introduction

Following the negative results of Church and Turing on the Entschiedungsproblem, there was a surge of interest in the 1920–30s in establishing where lay the boundary between decidable and undecidable fragments of classical first-order logic (see the monograph [5], and references therein). First-order modal logics, by contrast, have enjoyed far less attention, despite their numerous applications in temporal query languages [6, 7] and in modelling of distributed or multi-agent systems [8, 3].

This lack of attention is arguably not a result of disinterest, but rather a result of the relatively weak expressive power required to obtain undecidability results. For example, while the two-variable fragment of classical first-order logic is decidable [11], even the two-variable, monadic fragment of many first-order modal logics is already undecidable [18]. There is, therefore, a practical demand for finding expressive fragments of first-order modal logics that retain their decidability, and establishing where the boundary between decidability and undecidability lies.

One approach is to consider the one-variable fragment, which is typically decidable whenever the underlying modal logic is decidable [missing]. However, these are often too weakly expressive for most practical uses. More expressive, yet still often decidable, are the monodic fragments, in which the modalities de re (about the thing) are restricted to formulas containing at most one free variable, with no restrictions are placed on modalities de dicto (about the statement) [16, 37].

Another approach is to expand the language with countably many counting quantifiers ${\exists_{\leq m}}$ able to succinctly express statements about the quantity of objects satisfying a given property, without requiring many auxiliary variables to address each such object independently. Our choice of how to encode the numerical bound $m$ associated with our counting quantifiers may potentially affect the computational complexity of our satisfiability problem, depending on whether we choose a succinct binary encoding for $m$ or a more verbose unary encoding. For the purposes of upper bounds, it is the binary encoding that is the more stringent. Counting quantifiers, in the form of cardinality restrictions on concepts, also play a central role in several expressive fragments of description logics [1, 2].

It is well-known that counting quantifiers can be safely added to the two-variable fragment of classical first-order logic without increasing the complexity of its satisfiability problem. Moreover, it makes no difference, whether our counting quantifiers are encoded as unary strings [24] or as binary strings [25]. They, therefore, suggest an attractive direction in the quest to gain greater expressive power from finite variable fragments of first-order modal logics, without jeopardizing their decidability. Some examples of first-order formulas with counting quantifiers include:

• •

“At most four components are believed to be faulty”:

{\exists_{\leq 4}}x\big{(}\mathsf{Component}(x)\land\Box\mathsf{Faulty}(x)\big{)}

• •

“It is possible that there is life on more than one planet”:

\Diamond{\exists_{\geq 2}}x\big{(}\mathsf{Planet}(x)\land\mathsf{hasLife}(x)\big{)},

• •

Generalised Barcan formula:

${\exists_{\leq c}}x\Diamond P(x)\to\Diamond{\exists_{\leq c}}x\,P(x)$, for $c<\omega$.

Unfortunately, the the addition of counting quantifiers is not always so amicable in the case of first-order modal logics, where even the most modest admission of counting quantifiers can result in a jump from decidability to the undecidable [15], or even the highly undecidable [13].

Turning our attention towards more practical first-order modal logics, this paper explores several decidable one-variable fragments over both constant and varying domains that are permitted to either expand or contract relative to the modal accessibility relation. Furthermore, we shall see that over varying domains, the choice of encoding for the numerical bounds appearing in the counting quantifiers can have a dramatic effect on the overall complexity. As too can placing any finite bound on subscripts appearing in the quantifiers, regardless of their encoding. Table 1, below, summarizes the results contained herein.

1.1 Outline of paper

In Section 2, we introduce the the one-variable fragment of first-order logic with counting quantifiers and establish the definitions for the fragments of first-order modal logics with which we shall be working. In Section 3 we consider first-order logics over over constant domains and show that the satisfiability problem for the one variable fragment of $\mathbf{Q}^{\#}\!{\mathbf{K}}$ where our quantifier subscripts are encoded as binary strings, is NExpTime-complete. This results is extended, in Section 4, to logics over expanding and decreasing domains.

In Section 5, we investigate the affect that the choice of encoding of the counting quantifiers has on the complexity, over expanding domains, while Section 6 presents partial results over decreasing domains. In Section 7 we explore the connections between the aforementioned first-order modal logics with counting quantifiers and two-dimensional products of propositional modal logics related to von Wright’s logic of ‘elsewhere’. We conclude with a discussion of some open problems in Section 8.

2 Preliminaries

2.1 First-order Modal Logics with Counting Quantifiers

The reader is assumed to be familiar with the basics of propositional and first-order modal logics, such as can be found in Fitting and Mendelsohn [9], for example. In what follows, we shall consider the first-order modal language comprising a countably infinite set of predicate symbols $\mathsf{Pred}=\{P_{0},P_{1},\dots\}$, each with an associated arity, together with a set of first-order variables $\mathsf{Var}=\{x_{0},x_{1},\dots\}$. We will write $\mathcal{QML}$ to denote the set of all traditional (counting-free) first-order modal formulas with a sole quantifier ${\exists}$, and distinguish this from the set $\mathcal{Q^{\#}\!ML}$ of all first-order modal formulas with counting quantifiers defined by the following grammar:

[TABLE]

where $P_{i}\in\mathsf{Pred}$ is an $n$-ary predicate symbol, $x,x_{i_{1}},\dots,x_{i_{n}}\in\mathsf{Var}$ are first-order variables, and $c\in\mathbb{N}$ is encoded as a binary string. For the language where counting quantifier subscripts are encoded as unary strings, we denote $\mathcal{Q^{\#}\!ML}_{un}$. The other Boolean connectives are defined in the usual way, with the addition of the usual dual modal operator $\Box\varphi:=\neg\Diamond\neg\varphi$. We will identify the counting free fragment $\mathcal{QML}$ to be a sublogic of $\mathcal{Q^{\#}\!ML}$ with the abbreviations ${\exists}x\varphi:=\neg{\exists_{\leq 0}}x\varphi$ and $\forall x\varphi:=\neg{\exists}x\neg\varphi={\exists_{\leq 0}}x\neg\varphi$.

Other counting quantifiers ${\exists_{\geq c}}x\varphi$ and ${\exists_{=c}}x\varphi$ can similarly be expressed in terms of ${\exists_{\leq c}}x\varphi$. It should be noted that the ‘obvious’ definition ${\exists_{=c}}x\varphi:={\exists_{\leq c}}x\varphi\land{\exists_{\geq c}}x\varphi$ leads to an exponential increase in the size of the formula over the succinct abbreviation. This, however, can be avoided by rewriting ${\exists_{=c}}\varphi:={\exists_{\leq c}}xQ(x)\land{\exists_{\geq c}}xQ(x)\land\forall x(Q(x)\leftrightarrow\varphi)$, for some fresh monadic predicate symbol $Q\in\mathsf{Pred}$.

We distinguish between the fragments $\mathcal{Q^{\#}\!ML}$ having unbounded counting quantifiers and the fragments $\mathcal{Q^{\#}\!ML}_{k}$ whose formulas that do not contain quantifiers with subscripts larger than $k<\omega$. For each $\ell<\omega$, let $\mathcal{Q^{\#}\!ML}^{\ell}$ denote the $\ell$-variable fragment comprising only those formulas containing the variables $x_{1},\dots,x_{\ell}$, and denote by $\mathcal{Q^{\#}\!ML}^{\ell}_{k}=\mathcal{Q^{\#}\!ML}^{\ell}\cap\mathcal{Q^{\#}\!ML}_{k}$ the $\ell$-variable fragment with quantifiers subscripts not exceeding $k$.

We define $\mathsf{sub}(\varphi)\subseteq\mathcal{Q^{\#}\!ML}$ to be the set of all subformulas of $\varphi$, $\mathsf{md}({\varphi})<\omega$ to be the modal depth of $\varphi$, taken to be the maximum nesting depth of modal operators, and $\mathsf{cap}(\varphi)<\omega$ to be the capacity of $\varphi$, taken to be the value of the largest quantifier subscript occurring in $\varphi$.

2.2 Semantics

Formulas of $\mathcal{Q^{\#}\!ML}$ are interpreted in first-order Kripke models of the form $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, where $\mathfrak{F}=(W,R)$ is a unimodal Kripke frame comprising a set of possible wolds $W$ and a binary accessibility relation $R\subseteq W\times W$ on $W$, $D$ is a non-empty set of domain objects from which the domain function $\mathfrak{d}:W\to({2^{D}}-\{\emptyset\})$ selects a non-empty subset $\mathfrak{d}(w)\subseteq D$, for each $w\in W$. Finally, $\mathfrak{I}:W\times\mathsf{Pred}\to\bigcup_{n<\omega}D^{n}$ is a function associating each $w\in W$ and and each $n$-ary predicate symbol $P_{i}\in\mathsf{Pred}$ with a $n$-ary relation $\mathfrak{I}(w,P_{i})\subseteq\mathfrak{d}(w)^{n}$ on $\mathfrak{d}(w)$.

In general, there may be no proscription on the behaviour of the domain function $\mathfrak{d}$, in what we call varying domain models. However, of most interest to us are those cases where the domain of interpretation is constant or is permitted to either only expand or only contract relative to the direction of the underlying Kripke frame. We say that the model is:

• –

a constant domain model if $\mathfrak{d}(u)=\mathfrak{d}(v)$ for all $u,v\in W$,

• –

an expanding domain model if $\mathfrak{d}(u)\subseteq\mathfrak{d}(v)$, whenever $uRv$, and

• –

a decreasing domain model if $\mathfrak{d}(u)\supseteq\mathfrak{d}(v)$, whenever $uRv$.

Given a model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$ and a variable assignment $\mathfrak{h}:\mathsf{Var}\to D$, mapping variables to domain objects, we define satisfiability in $\mathfrak{M}$ in the standard way by taking:

[TABLE]

for all $w\in W$, where $P_{i}\in\mathsf{Pred}$ is an $n$-ary predicate symbol. Counting quantifiers are interpreted, by taking:

[TABLE]

for $c\in\mathbb{N}$, where ${\left|{X}\right|}$ denotes the cardinality of $X$, and $\mathfrak{h}(x/a):\mathsf{Var}\to D$ is the variable assignment that agrees with $\mathfrak{h}$ on all variables except $x$, for which it assigns the value $a\in D$. In the case where $\varphi$ contains only a single variable $x\in\mathsf{Var}$, it will be convenient to write $\mathfrak{M},w\models^{a}\varphi$ in place of $\mathfrak{M},w\models^{\mathfrak{h}}\varphi$, where $a=\mathfrak{h}(x)$ is the assignment of $x$.

We say that a formula $\varphi$ is valid in $\mathfrak{M}$ if $\mathfrak{M},w\not\models^{\mathfrak{h}}\neg\varphi$, for all $w\in W$ under any variable assignment $\mathfrak{h}$. For each propositional modal logic $\mathbf{L}$, there is an associated first-order modal logic $\mathbf{Q}^{\#}\!{\mathbf{L}}$ (resp. $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{exp}}$, $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{dec}}$) taken to be the set of all first-order modal formulas that are valid in every constant (resp. expanding, decreasing) domain model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$ whose underlying Kripke frame $\mathfrak{F}$ is a frame for $\mathbf{L}$. We say that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{L}}$ (resp. $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{exp}}$, $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{dec}}$) if $\varphi$ is satisfiable in some constant (resp. expanding, decreasing) domain model whose underlying Kripke frame is a frame for $\mathbf{L}$.

The fragment $\mathbf{Q}^{\#}\!{\mathbf{L}}\cap\mathcal{K}$ is said to have the poly-size (resp. exponential-sized) domain property if every formula $\varphi\in\mathcal{K}$ that is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{L}}$ can be satisfied in a model in which $D$ is at most polynomial (resp. exponential) in the size of $\varphi$. Similarly, we say that $\mathbf{Q}^{\#}\!{\mathbf{L}}\cap\mathcal{K}$ poly-size (resp. exponential-sized) model property if every formula $\varphi\in\mathcal{K}$ that is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{L}}$ can be satisfied in a model in which both $\mathfrak{F}$ and $D$ are at most polynomial (resp. exponential) in the size of $\varphi$.

Throughout the remainder of this paper, we will be chiefly concerned with various fragments of the logics $\mathbf{Q}^{\#}\!{\mathbf{K}}$, $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$, characterized by the class of all frames. However, owing to a standard ‘bulldozing’ argument (see [4]), we may assume without any loss of generality that if $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$ (resp. $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$, $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$), then it must be satisfiable in a model whose underlying Kripke frame is an irreflexive, intransitive tree of depth $\leq\mathsf{md}({\varphi})$.

3 Logics with unbounded quantifiers over constant domains

We note, first, that the satisfiability problem for the counting-free fragment of $\mathbf{Q}^{\#}\!{\mathbf{K}}$ in one-variable is NExpTime-complete [22], while that of the two-variable monadic fragment is already undecidable [18, 10]. The effect of adding even the most modest counting quantifiers ${\exists_{\leq c}}x$, for $c\in\{0,1\}$, to the decidable one-variable fragment of $\mathbf{Q}^{\#}\!{\mathbf{K4.3}}$, whose models are based on linear frames, is known to result in undecidability [13]111Many of these results are presented in the context of two-dimensional propositional modal logics, the connection with which is explored in Section 7..

In marked contrast to these negative results, in this section we show that endowing the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{QML}^{1}$ with infinitely many counting quantifiers ${\exists_{\leq m}}$, for each $m\in\mathbb{N}$, does not result in any increase in the computational complexity of its satisfiability problem over its counting-free counterpart; indeed the problem remains NExpTime-complete. This result was first proved in [14].

Theorem 3.1**.**

The satisfiability problem for the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ with unbounded counting quantifiers is NExpTime-complete.

We show that for a formula $\varphi$ to be satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$, it must be satisfiable in a model that is at most exponential in the size of $\varphi$; *i.e.*the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ has the exponential fmp. This provides us with an effective mechanism by which to check the satisfiability of any formula $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$ — nondeterministically select a ‘small’ model whose size is at most exponential in $\varphi$, and check whether it satisfies $\varphi$. Since model-checking can be performed in polynomial time in the size of the model and size of the formula, we obtain an NExpTime upper-bound on the complexity of the satisfiability problem for $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$.

Theorem 3.2**.**

The one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ with unbounded quantifiers has the exponential fmp.

To prove this, we employ a version of the method of quasimodels [35, 20]. Our quasimodels closely resemble full Kripke models, however, each first-order structure is replaced with a quasistate, which can be finitely represented. The basic structure of our quasimodels may still be infinite, so we require additional non-trivial ‘pruning’ techniques to ensure that large quasimodels can be reduced to smaller finite quasimodels without sacrificing satisfiability. Therein lies the crux of the problem we must solve.

First, let us fix some arbitrary first-order modal formula $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$, and throughout what follows, let $n={\left|{\mathsf{sub}(\varphi)}\right|}$ denote the number of subformulas of $\varphi$, $m=\mathsf{md}({\varphi})$ denote the modal depth of $\varphi$, and $C=\mathsf{cap}(\varphi)$ denote the value of the largest quantifier subscript occurring in $\varphi$. In particular we note that $n,m\leq\left\|{\varphi}\right\|$, while $C\leq 2^{\left\|{\varphi}\right\|}$, owing to the binary encoding of the quantifier subscripts.

Definition 3.3** (Types and Quasistates).**

We define a type for $\varphi$ to be any subset $t\subseteq\mathsf{sub}(\varphi)$ that is Boolean-saturated in the sense that:

1. (tp1)

for all $\neg\psi\in\mathsf{sub}(\varphi)$, $\neg\psi\in t$ if and only if $\psi\not\in t$, and 2. (tp2)

for all $(\psi_{1}\land\psi_{2})\in\mathsf{sub}(\varphi)$, $(\psi_{1}\land\psi_{2})\in t$ if and only if $\psi_{1}\in t$ and $\psi_{2}\in t$.

A quasistate for $\varphi$ is defined to be a pair $(T,\mu)$ such that:

1. (qs1)

$T$ is a non-empty set of types for $\varphi$, 2. (qs2)

$\mu:T\to\{1,\dots,C,C+1\}$ is a bounded ‘multiplicity’ function, 3. (qs3)

(${\exists_{\leq c}}$-saturation) For all $t\in T$ and $({\exists_{\leq c}}x\ \xi)\in\mathsf{sub}(\varphi)$,

[TABLE]

where $T(\xi)=\{t\in T\ :\ \xi\in t\}$ denotes the set of types belonging to $T$ that contain the formula $\xi\in\mathcal{Q^{\#}\!ML}^{1}$.

Note that the size of each quasistate cannot exceed the number of distinct types for $\varphi$, which is to say that ${\left|{T}\right|}\leq 2^{n}$, and ${\left|{\mu}\right|}\leq(C+1)\cdot{\left|{T}\right|}\leq(C+1)2^{n}$, since $\mu\subseteq T\times\{1,\dots,C+1\}$. The multiplicity function indicates how many ‘duplicates’ of each type are required in order to transform the quasistate into an appropriate first-order structure. Note that $\varphi$ is indifferent to any duplicates in excess of the value of its largest quantifier subscript, and does not discern between ‘large’ quantities which are beyond its ‘vocabulary’.

Definition 3.4** (Quasimodels).**

A basic structure for $\varphi$ is a triple $(W,\prec,\textbf{{q}})$, where $(W,\prec)$ is an intransitive, irreflexive tree of depth $\leq m$, and q is a function associating each $w\in W$ with a quasistate $\textbf{{q}}(w)=(T_{w},\mu_{w})$. A run through $(W,\prec,\textbf{{q}})$ is a function $r:W\to\bigcup_{w\in W}T_{w}$ associating each $w\in W$ with a type $r(w)\in T_{w}$. A quasimodel for $\varphi$ is a 5-tuple $\mathfrak{Q}=(W,\prec,\textbf{{q}},I,\mathfrak{R})$ such that:

1. (qm1)

$(W,\prec,\textbf{{q}})$ is a basic structure for $\varphi$, $I$ is a non-empty set of indices, and $\mathfrak{R}=\{r_{i}:i\in I\}$ is an set of runs through $(W,\prec,\textbf{{q}})$ indexed by $I$, 2. (qm2)

There is some $w_{0}\in W$ and $t_{0}\in T_{w_{0}}$ such that $\varphi\in t_{0}$, 3. (qm3)

(coherence) For all $i\in I$, $w\in W$ and $\Diamond\xi\in\mathsf{sub}(\varphi)$,

[TABLE] 4. (qm4)

(saturation) For all $i\in I$, $w\in W$ and $\Diamond\xi\in\mathsf{sub}(\varphi)$,

[TABLE] 5. (qm5)

For all $w\in W$ and $t\in T_{w}$,

[TABLE]

The following lemma establishes that our quasimodels precisely capture the notion of satisfiability with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$, and that every quasimodel for $\varphi$ can be effectively transformed into model for $\varphi$ of proportional size.

Lemma 3.5**.**

Let $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$ be an arbitrary formula in one-variable. Then $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$ iff there is a quasimodel for $\varphi$.

Proof.

Suppose that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$. Then $\mathfrak{M},w_{0}\models^{a_{0}}\varphi$ for some first-order Kripke model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, where $\mathfrak{F}=(W,R)$ is an irreflexive, intransitive tree of depth $\leq m$, with $w_{0}\in W$.

With each $w\in W$ and $a\in D$, we associate the type

[TABLE]

and define a basic structure $(W,R,\textbf{{q}})$, by taking $\textbf{{q}}(w)=(T_{w},\mu_{w})$, for all $w\in W$, where

[TABLE]

for all $t\in T_{w}$. It is straightforward to check that $\textbf{{q}}(w)$ is a quasistate, for each $w\in W$. Indeed, suppose that $\mathrm{tp}^{\mathfrak{M}}_{w}[a]\in T_{w}$ and that $({\exists_{\leq c}}x\ \xi)\in\mathsf{sub}(\varphi)$, for some $c\leq C$. Then we have that:

[TABLE]

The final equivalence follows from the fact that each summand strictly less than $(C+1)$, since $c\leq C$. Hence, it follows from the definition that $\mu_{w}(t)={\left|{\{b\in D\ :\ \mathrm{tp}^{\mathfrak{M}}_{w}[b]=t^{\prime}\}}\right|}$, for all $t^{\prime}\in T_{w}(\xi)$. For each index $a\in D$, we define a run $f_{a}:W\to{2^{\mathsf{sub}(\varphi)}}$ by taking

[TABLE]

for all $w\in W$. We then take $\mathfrak{R}=\{r_{a}:a\in D\}$ to be the set of all such runs through $(W,R,\textbf{{q}})$, with indices from $D$. Note that there may be many indices in $D$ that correspond to the same run. It is straightforward to check that $(W,R,\textbf{{q}},D,\mathfrak{R})$ is a quasimodel for $\varphi$.

Conversely, suppose that $\mathfrak{Q}=(W,\prec,\textbf{{q}},I,\mathfrak{R})$ is a quasimodel for $\varphi$. We define a first-order Kripke model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, by taking $\mathfrak{F}:=(W,\prec)$, $D=\mathfrak{d}(w):=I$ for all $w\in W$, and

[TABLE]

for all predicate symbols $P_{j}\in\mathsf{Pred}$ and $w\in W$. It remains to check that $\mathfrak{M}$ is a model for $\varphi$. We claim that

[TABLE]

for all $w\in W$, $i\in I$, and $\psi\in\mathsf{sub}(\varphi)$.

The case where $\psi$ is an atomic formula follows immediately from the definitions. So suppose that (I.H.) holds for all formulas of size $<k$, and let $\psi$ be a formula of size $k$. The cases where $\psi$ is a Boolean combination of smaller formulas follow from the definition of a type, leaving us with two cases:

• \killcontents
• –

Case $\psi=P_{j}(x)$: This follows immediately from the definition of $P_{j}^{I(w)}$, since

[TABLE]

• –

Case $\psi=\neg\xi$: We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$: We have that

[TABLE]

\endkillcontents

• –

Case $\psi=\Diamond\xi$: We have that

[TABLE]

• –

Case $\psi={\exists_{\leq c}}x\ \xi$: We have that

[TABLE]

The penultimate equivalence follows, again, from the fact that each summand strictly less than $(C+1)$, since $c\leq C$. Hence, it follows from (qm5) that $\mu_{w}(t)={\left|{\{j\in I\ :\ r_{j}(w)=t\}}\right|}$, for all $t\in T_{w}(\xi)$.

Hence, it follow that $\mathfrak{M},w\models^{i}\psi$ if and only if $\psi\in r_{i}(w)$, for all $\psi\in\mathsf{sub}(\varphi)$, as required. By (qm2), there is some $w_{0}\in W$ and $t_{0}\in T_{w_{0}}$ such that $\varphi\in t_{0}$, while by (qm5) we have that there is some $i_{0}\in I$ such that $r_{i_{0}}(w_{0})=t_{0}$. Hence, it follows from (I.H.) that $\mathfrak{M},w_{0}\models^{i_{0}}\varphi$, which is to say that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$, as required. ∎

Hence, to show that the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ has the exponential fmp, it is enough to show that every quasimodel for $\varphi$ can be transformed into a finite quasimodel in which both $W$ and $I$ are at most exponential in the size of $\varphi$.

Lemma 3.6**.**

Let $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$ be an arbitrary formula in one-variable. If $\varphi$ has a quasimodel, then $\varphi$ has a quasimodel $\mathfrak{Q}=(W,\prec,\textbf{{q}},I,\mathfrak{R})$ such that:

[TABLE]

Proof.

Let $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$ and suppose that $\mathfrak{Q}=(W,\prec,\textbf{{q}},I,\mathfrak{R})$ is a quasimodel for $\varphi$. The proof follows two stages: the first involves pruning both the basic structure and the set of runs so that they are both at most exponential in the size of $\varphi$. During this stage we inadvertently destroy some of the defining properties of our quasimodel; in particular the saturation condition (qm4). In the second stage we remedy this deficiency by adding multiple ‘copies’ of each quasistate and performing ‘surgery’ on a finite set of runs to repair saturation.

Step 1)

First, it follows from (qm2) that there is some $w_{0}\in W$ and $t_{0}\in T_{w_{0}}$ such that $\varphi\in t_{0}$. By (qm5), for each $w\in W$ and each $t\in T_{w}$ we may fix some run $s_{(w,t)}\in\mathfrak{R}$ such that $s_{(w,t)}(w)=t$. Take $\mathfrak{S}(w)=\{s_{(w,t)}:t\in T_{w}\}$ be to the set comprising all such runs, for each $w\in W$. In particular, we note that ${\left|{\mathfrak{S}(w)}\right|}={\left|{T_{w}}\right|}\leq 2^{n}$. Furthermore, by (qm4), for each $\Diamond\alpha\in t$ we may fix some $v=v_{(w,t,\alpha)}\in W$ such that $w\prec v$ and $\alpha\in s_{(w,t)}(v)$. We now define inductively a sequence of (finite) subsets $W_{k}\subseteq W$, for $k=0,\dots,m$, by taking $W_{0}=\{w_{0}\}$, and

[TABLE]

for $k<m$. We then define a new basic structure $(W^{\prime},\prec^{\prime},\textbf{{q}}^{\prime})$, by taking

[TABLE]

for all $u,v\in W^{\prime}$.

Let $\mathfrak{S}=\bigcup\{\mathfrak{S}(w):w\in W^{\prime}\}$, and note that $\mathfrak{S}$ is finite since it is a finite union of finite sets of runs. However, $\mathfrak{S}$ need not be plentiful enough to accommodate condition (qm5). Hence we must extend $\mathfrak{S}$ to a ‘small’ subset $\mathfrak{R}^{\prime}$ of $\mathfrak{R}$ by choosing sufficiently many runs so as to satisfy (qm5).

More precisely, for each $w\in W^{\prime}$, $t\in T_{w}$ and $m<\mu_{w}(t)$ we can fix some $r_{(w,t,m)}\in\mathfrak{R}$ such that $r_{(w,t,m)}(w)=t$, and $r_{(w,t,m)}\not=r_{(w,t,m^{\prime})}$ for $m\not=m^{\prime}$. The existence of sufficiently many such runs is guaranteed by (qm5). Furthermore, we may assume without any loss of generality that $r_{(w,t,0)}=s_{(w,t)}\in\mathfrak{S}(w)$, as defined above. We may then take

[TABLE]

and define $\mathfrak{Q}^{\prime}=(W^{\prime},\prec^{\prime},\textbf{{q}}^{\prime},\mathfrak{R}^{\prime})$. We note that:

[TABLE]

Furthermore, from our construction we have that $\mathfrak{Q}^{\prime}$ satisfies each of the conditions (qm1), (qm2), (qm3), and (qm5), as can be easily verified. However $\mathfrak{Q}^{\prime}$ fails to satisfy the saturation condition (qm4). To remedy this, we diverge from the techniques of [35, 20] by extending our basic structure with not one but multiple ‘copies’ of each quasistate; each associated with a given transposition of runs.

Step 2)

Let $\mathsf{Sym}({I^{\prime}})$ denote the set of all permutations $\sigma:I^{\prime}\to I^{\prime}$ on the set of indices $I^{\prime}$, with $\mathsf{id}\in\mathsf{Sym}({I^{\prime}})$ denoting the identity function. For each $w\in W^{\prime}$ and each $i\in I^{\prime}$, let $\tau_{(w,i)}\in\mathsf{Sym}({I^{\prime}})$ denote the permutation that transposes $r_{i}$ and $s_{(w,t)}\in\mathfrak{S}(w)$, where $t=r_{i}(w)$. Let $\mathsf{Trans}({w})=\{\tau_{(w,i)}:i\in I^{\prime}\}$ denote the set of all such transpositions. In particular, we have that ${\left|{\mathsf{Trans}({w})}\right|}\leq{\left|{I^{\prime}}\right|}$ is at most exponential in the size of $\varphi$.

In what follows, we construct a new basic structure based on some ‘small’ subset of $W^{\prime}\times\mathsf{Sym}({I^{\prime}})$. Naturally, we cannot construct a basic structure out of the set of all pairs from $W^{\prime}\times\mathsf{Sym}({I^{\prime}})$ if we are to insist on an exponential upper bound on the size of the quasimodel, since ${\left|{\mathsf{Sym}({I^{\prime}})}\right|}={\left|{I^{\prime}}\right|}!$. Instead, for each $(w,\sigma)\in W^{\prime}\times\mathsf{Sym}({I^{\prime}})$, we may define a small set of successors $S(w,\sigma)\subseteq W^{\prime}\times\mathsf{Sym}({I^{\prime}})$, by taking:

[TABLE]

for all $w\in W^{\prime}$ and $\sigma\in\mathsf{Sym}({I^{\prime}})$. We construct a new sequence of sets $W_{k}^{\prime}\subseteq W^{\prime}\times\mathsf{Sym}({I^{\prime}})$, for $k=0,\dots,m$, by taking

[TABLE]

for $k<m$. Define a new basic structure $(W^{\prime\prime},\prec^{\prime\prime},\textbf{{q}}^{\prime\prime})$, by taking:

[TABLE]

and $\textbf{{q}}^{\prime\prime}(u,\sigma)=\textbf{{q}}^{\prime}(u)$, for all $(u,\sigma),(v,\rho)\in W^{\prime\prime}$.

Finally, for each run $i\in I^{\prime}$ we define a new run $\widehat{r}_{i}$ through $(W^{\prime\prime},\prec^{\prime\prime},\textbf{{q}}^{\prime\prime})$, by taking $\widehat{r}_{i}(w,\sigma)=r_{\sigma(i)}(w)$, for all $(w,\sigma)\in W^{\prime\prime}$. That is to say that the new run $\widehat{r}_{i}$ behaves at $(w,\sigma)\in W^{\prime\prime}$ as $r_{\sigma(i)}\in\mathfrak{R}^{\prime}$ does at $w\in W^{\prime}$. Take $I^{\prime\prime}=I^{\prime}$ and let $\mathfrak{R}^{\prime\prime}=\{\widehat{r}_{i}:i\in I^{\prime\prime}\}$ be the set of all such runs. We may then define a new quasimodel $\mathfrak{Q}^{\prime\prime}=(W^{\prime\prime},\prec^{\prime\prime},\textbf{{q}}^{\prime\prime},I^{\prime\prime},\mathfrak{R}^{\prime\prime})$, and note that

[TABLE]

both remaining at most exponential in the size of $\varphi$, as required. All that remains is to show that $\mathfrak{Q}^{\prime\prime}$ is, indeed, a quasimodel for $\varphi$.

• —

It follows from the construction that $\varphi\in t_{0}$ for some $t_{0}\in T_{w_{0}}=T_{(w_{0},\mathsf{id})}$, where $(w_{0},\mathsf{id})\in W^{\prime}$, as required for(qm2).

• —

For (qm3), suppose that $i\in I^{\prime\prime}$, $(w,\sigma),(v,\rho)\in W^{\prime\prime}$ and $\Diamond\alpha\in\mathsf{sub}(\varphi)$ are such that $(w,\sigma)\prec^{\prime\prime}(v,\rho)$ and $\alpha\in\widehat{r}(v,\rho)$.

By definition we have that $(v,\rho)\in S(w,\sigma)$, which is to say that $w\prec v$ and $\rho=\tau\circ\sigma$ for some transposition $\tau\in\mathsf{Trans}({w})$. Hence we have that

[TABLE]

where $j=\tau(\sigma(i))\in I^{\prime}$. Since $\mathfrak{Q}^{\prime}$ is coherent and $w\prec^{\prime}v$, we have that $\Diamond\alpha\in r_{j}(w)$. However, we have that $\tau\in\mathsf{Trans}({w})$ and hence by definition $r_{\tau(\sigma(i))}(w)=r_{\sigma(i)}(w)$, since $\tau$ transposes only runs that coincide at $w$. In particular, we have that $\Diamond\alpha\in r_{\sigma(i)}(w)$, which is to say that $\Diamond\alpha\in\widehat{r}_{i}(w,\sigma)$, as required.

• —

For (qm4), suppose that $i\in I^{\prime}$, $(w,\sigma)\in W^{\prime\prime}$ and $\Diamond\alpha\in\mathsf{sub}(\varphi)$ are such that $\Diamond\alpha\in\widehat{r}_{i}(w,\sigma)$. This is to say that $\Diamond\alpha\in r_{\sigma(i)}(w)$. Let $t=r_{\sigma(i)}(w)$ and let $s_{(w,t)}\in\mathfrak{S}(w)$ be such that $s_{(w,t)}(w)=t$. By construction there is some $v=v_{(w,t,\alpha)}\in W^{\prime}$ such that $w\prec^{\prime}v$ and $\alpha\in s_{(w,t)}(v)$.

Let $\tau=\tau_{(w,\sigma(i))}\in\mathsf{Trans}({w})$ be the transposition that swaps $r_{\sigma(i)}\in\mathfrak{R}^{\prime}$ and $s_{(w,t)}\in\mathfrak{S}(w)$. It follows from the construction that there is some $(v,\tau\circ\sigma)\in S(w,\sigma)\subseteq W^{\prime\prime}$ such that

[TABLE]

and $(w,\sigma)\prec^{\prime\prime}(v,\tau\circ\sigma)$, as required.

• —

For (qm5), suppose that $(w,\sigma)\in W^{\prime\prime}$ and $t\in T_{(w,\sigma)}=T_{w}$ and consider the following sets:

[TABLE]

Note that the $\sigma$ maps bijectively from $X$ onto $Y$, since by definition $\widehat{r}_{i}(w,\sigma)=r_{\sigma(i}(w)$. Hence $i\in X$ if and only if $\sigma(i)\in Y$, and thus ${\left|{X}\right|}={\left|{Y}\right|}$.

That is to say that the number of runs passing through each type remains unaffected by Step 2 of our construction. It then follows from the definitions that

[TABLE]

as required.

Thus completes the proof of Lemma 3.6. ∎

Theorem 3.2 now follows from Lemmas 3.5–3.6, and hence the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ has the exponential fmp. Consequently, as described above, we may exploit this exponential fmp to answer the satisfiability problem in NExpTime, thereby completing the proof of Theorem 3.1.

It follows that the satisfiability problems for each of the one-variable fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ with finitely bounded quantifier subscripts are similarly NExpTime-complete; sandwiched, as they are, between the unbounded fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ and the NExpTime-hard one-variable counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{QML}^{1}$ [22]. Furthermore, the satisfiability problem for the fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}_{un}^{1}$, in which the counting quantifiers are encoded as unary strings, can be polynomially reduced to that of $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ by transcribing the subscripts into binary. Consequently, it shares the same NExpTime upper-bound.

Corollary 3.7**.**

The satisfiability problem for each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}_{un}^{1}$ is NExpTime-complete, for $\ell<\omega$.

4 Logics with unbounded quantifiers over expanding or decreasing domains

It is well-established that the satisfiability problems for the counting-free fragments of $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$ are both polynomially reducible to that of $\mathbf{Q}^{\#}\!{\mathbf{K}}$, by relativizing the domain function with an auxiliary monadic predicate symbol $\mathcal{E}\in\mathsf{Pred}$, demarcating those domain objects that actually exist [9, 36].

The same is true over the language with counting quantifiers, where the same trick can also be employed. Let $\varphi\in\mathcal{Q^{\#}\!ML}$ be an arbitrary formula first-order modal formula with counting quantifiers, and let $\mathcal{E}\in\mathsf{Pred}$ be a fresh predicate symbol not occurring in $\varphi$. We define the relativization $\varphi^{\mathcal{E}}$ via the function $(\cdot)^{\mathcal{E}}:\mathsf{sub}(\varphi)\to\mathcal{Q^{\#}\!ML}$, defined inductively, by taking

[TABLE]

We may, thereby, reduce the satisfiability problem for $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}$ to that of $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}$, by specifying the expanding or decreasing nature of $\mathcal{E}$, by defining:

[TABLE]

respectively, where $m=\mathsf{md}({\varphi})$ is the modal depth of $\varphi$.

Proposition 4.1**.**

Let $\varphi\in\mathcal{Q^{\#}\!ML}$ be an arbitrary first-order modal formula. Then we have the following equivalences:

• (i)

$\varphi$* is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ if and only if $(\zeta_{\mathit{exp}}\land\varphi^{\mathcal{E}})$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$,*

• (ii)

$\varphi$* is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$ if and only if $(\zeta_{\mathit{dec}}\land\varphi^{\mathcal{E}})$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$,*

Proof.

The proof is via a routine induction, analogous to that of [36, Proposition 2.4]. ∎

This yields the following immediate consequence of Theorem 3.1.

Corollary 4.2**.**

The satisfiability problem for the one-variable fragment $L\cap\mathcal{Q^{\#}\!ML}^{1}$ with unbounded quantifiers is decidable in NExpTime, for $L\in\{\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}},\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\}$.

What prevents us from encoding constant domains within varying domain models is our inability to prevent the domains from expanding or contracting beyond the scope of our formulas. However, the addition of counting quantifiers allows us to make specific demands on the size of each domain.

The following theorem provides a matching lower bound, by exploiting the exponential domain property of $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$, proved in Theorem 3.1, together with the succinct binary encoding of counting quantifiers. The intuition is that with unbounded quantifiers, we can specify the exact size of the first-order domains, forcing them to be remain constant in all possible worlds lie within the scope of the formula. The binary encoding allows us to succinctly specify the (possibly) exponential size of the domains.

Theorem 4.3**.**

The satisfiability problem for the one-variable fragment $L\cap\mathcal{Q^{\#}\!ML}^{1}$ with unbounded counting quantifiers is NExpTime-complete, for $L\in\{\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}},\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\}$.

Proof.

The upper-bound has already been established by Corollary 4.2. The proof for the lower-bound is via a reduction from the satisfiability problem for the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$, over constant domains.

To this end, let $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$ be an arbitrary formula in one variable, whose counting quantifiers are encoded as binary strings. Since the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ has the exponential finite domain property, there is some monotonic function f(n)\in O\big{(}2^{n^{k}}\big{)} such that if $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$ then $\varphi$ is satisfiable in a model in which the size of each first-order domain does not exceed $N=f(\left\|{\varphi}\right\|)$.

We define $\zeta$ to be the conjunction of $\zeta_{\mathit{exp}}$, $\zeta_{\mathit{dec}}$ and the following formula:

[TABLE]

where $\top(x):=P_{0}(x)\lor\neg P_{0}(x)$. Note that the size of $\zeta$ is at most logarithmic in the size of $N$, owing to the binary encoding of the quantifier subscripts.

We claim that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$ if and only if $(\zeta\land\varphi^{\mathcal{E}})$ is satisfiable with respect to $\mathbf{L}$, for $\mathbf{L}\in\{\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}},\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\}$.

• ($\Rightarrow$)

Suppose $\mathfrak{M},r\models^{a_{0}}(\zeta\land\varphi^{\mathcal{E}})$, for some first-order Kripke model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, with $a_{0}\in\mathfrak{d}(r)$, where $\mathfrak{d}$ is either expanding or decreasing. Without loss of generality, we may assume that $\mathfrak{F}=(W,R)$ is an irreflexive, intransitive tree of depth $\leq m$. Whence, by (2), it follows that $\mathfrak{M},w\models^{a}{\exists_{\leq N}}\top(x)\land\neg{\exists_{\leq(N-1)}}\top(x)$, for all $w\in W$ and $a\in\mathfrak{d}(w)$. Consequently, we have that ${\left|{\mathfrak{d}(w)}\right|}=N$, for all $w\in W$, and since $\mathfrak{d}$ is assumed to be either increasing or decreasing, we must have that $\mathfrak{d}(u)=\mathfrak{d}(v)$, for all $u,v\in W$. It then follows from $\zeta_{\mathit{exp}}$ and $\zeta_{\mathit{dec}}$ that $\mathfrak{I}(u,\mathcal{E})=\mathfrak{I}(v,\mathcal{E})$, for all $w,v\in W$.

We define a new constant domain model $\mathfrak{M}^{\prime}=(\mathfrak{F},D,\mathfrak{d}^{\prime},\mathfrak{I}^{\prime})$ over $\mathfrak{F}$, by taking $\mathfrak{d}^{\prime}(w)=\mathfrak{I}(w,\mathcal{E})$, for all $w\in W$ and $\mathfrak{I}^{\prime}(w,P_{i})=\mathfrak{I}(w,P_{i})$, for all predicate symbols $P_{i}$ occurring in $\varphi$.

We prove, by induction on the length of $\psi\in\mathsf{sub}(\varphi)$ that

[TABLE]

for all $w\in W$ and $a\in\mathfrak{d}^{\prime}(w)$.

The cases where $\psi$ is an atomic formula or a Boolean combination of smaller formulas are straightforward and follow from the definitions. So suppose that $\psi$ is of the form $\Diamond\xi$ or ${\exists_{\leq c}}x\xi$, for some $\xi\in\mathsf{sub}(\varphi)$ and $c\in\mathbb{N}$. In which case we have the following:

• \killcontents
• –

Case $\psi=P_{i}(x)$: We have that

[TABLE]

• –

Case $\psi=\neg\xi$: We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$: We have that

[TABLE]

\endkillcontents

• –

Case $\psi=\Diamond\xi$: We have that

[TABLE]

• –

Case $\psi={\exists_{\leq c}}x\ \xi$: We have that

[TABLE]

Hence, we have that $\mathfrak{M}^{\prime},w\models^{a}\psi$ if and only if $\mathfrak{M},w\models^{a}\psi^{\mathcal{E}}$, for all $\psi\in\mathsf{sub}(\varphi)$. In particular, we have that $\mathfrak{M}^{\prime},r\models^{a_{0}}\varphi$, which is to say that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$.

• ($\Leftarrow$)

Suppose that $\mathfrak{M},r\models^{a_{0}}\varphi$ for some first-order constant domain model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, with $a_{0}\in\mathfrak{d}(r)$. Again, without any loss of generality, we may assume that $\mathfrak{F}=(W,R)$ is an irreflexive intransitive tree of depth $\leq m$, with root $r\in W$. Moreover, since $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ has the $f(n)$-sized domain property, we may assume that ${\left|{D}\right|}\leq N$, where $N=f(\left\|{\varphi}\right\|)$ is an most exponential in the size of $\varphi$. Hence, there must be some injective enumeration $\iota:D\to\{0,1,\dots,N-1\}$ of $D$, assigning to each object $a\in D$, a unique index $\iota(a)<N$.

We define a new model $\mathfrak{M}^{\prime}=(\mathfrak{F},D^{\prime},\mathfrak{d}^{\prime},\mathfrak{I}^{\prime})$ by taking $D^{\prime}=\{0,1,2,\dots,N-1\}$, and $\mathfrak{d}^{\prime}(w)=D^{\prime}$, for all $w\in W$ and,

[TABLE]

for all predicate symbols $P_{i}\in\mathsf{Pred}$ occurring in $\varphi$.

We prove, by induction on the length of $\psi\in\mathsf{sub}(\varphi)$ that

[TABLE]

for all $w\in W$ and $a\in\mathfrak{d}(w)$.

• \killcontents
• –

Case $\psi=P_{i}(x)$: We have that

[TABLE]

• –

Case $\psi=\neg\xi$: We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$: We have that

[TABLE]

\endkillcontents

• –

Case $\psi=\Diamond\xi$: We have that

[TABLE]

• –

Case $\psi=({\exists_{\leq c}}x\ \xi)$: We have that

[TABLE]

Hence, we have that $\mathfrak{M}^{\prime},\models^{a}\psi^{\mathcal{E}}$ if and only if $\mathfrak{M},w\models^{a}\psi$, for all $\psi\in\mathsf{sub}(\varphi)$. In particular, we have that $\mathfrak{M}^{\prime},r\models^{a_{0}}\varphi$. Furthermore, it is straightforward to check that $\mathfrak{M}^{\prime},r\models^{a_{0}}\zeta$, since each $\mathfrak{d}^{\prime}(w)$ contains precisely $N$ elements, and $\mathfrak{I}^{\prime}(u,\mathcal{E})=\mathfrak{I}^{\prime}(v,\mathcal{E})$, for all $u,v\in W$. Hence, we have that $\mathfrak{M},r\models^{a_{0}}(\zeta\land\varphi^{\mathcal{E}})$, which is to say that $(\zeta\land\varphi^{\mathcal{E}})$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$, and consequently with respect to both $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$.

Since the satisfiability problem for the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{Q^{\#}\!ML}^{1}$ is NExpTime-hard, so too must be the satisfiability problem for the one-variable fragment $\mathbf{L}\cap\mathcal{Q^{\#}\!ML}^{1}$, for both $\mathbf{L}\in\{\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}},\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\}$, as required. ∎

Note, above, that $\zeta$ is not restricted to any quantifier bounded fragment $\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$. Furthermore, this reduction relies heavily on the succinct binary encoding of the subscripts, without which we would be unable to specify the exponential size of the domains while maintaining the polynomial bound on the size of $\zeta$.

In the proceeding sections, we shall see that both of these assumptions are crucial to the success of Theorem 4.3, and without which the computational complexity of the satisfiability problem can be greatly reduced.

5 Logics with bounded quantifiers over expanding domains

In this section we show that placing any finite bound on the quantifier subscripts significantly reduces the computational complexity of the satisfiability problem for the resulting fragment, from NExpTime-complete to PSpace-complete.

Similarly, if we were to encode the quantifier subscripts as unary strings—a practice that is common within other branches of logic, such as description logics [2, 17]—then we also observe the same reduction in complexity. In both cases, the results hinges on the fact that the domains for any first-order Kripke model for $\varphi$ can be chosen to be at most polynomial in the size of $\varphi$ and $C=\mathsf{cap}(\varphi)$. Note that $C$ is bounded by some fixed constant for $\varphi\in\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ and is at most linear in $\varphi$ when encoded as a unary string.

Lemma 5.1**.**

Given an arbitrary first-order modal formula $\varphi\in\mathcal{Q^{\#}\!ML}^{1}$. If $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ then, $\varphi$ can be satisfied in a model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},I)$ such that,

[TABLE]

where $n={\left|{\mathsf{sub}(\varphi)}\right|}$, $m=\mathsf{md}({\varphi})$ and $C=\mathsf{cap}(\varphi)$.

Proof.

Suppose that $\varphi\in\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}$. Then $\mathfrak{M},r\models^{a_{0}}\varphi$ for some expanding first-order Kripke model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, where $\mathfrak{F}=(W,R)$ is an irreflexive, intransitive tree of depth at most $m=\mathsf{md}({\varphi})$ with root $r\in W$. For each $w\in W$, and $\psi\in\mathsf{sub}(\varphi)$, let

[TABLE]

count the number of elements in $\mathfrak{d}(w)$ satisfying $\psi$, up to a maximum of $(C+1)$, beyond which $\varphi$ lacks that vocabulary to discern. For each $i<n(w,\varphi)$, choose some fixed witness $a_{\psi,i}\in\mathfrak{d}(w)$ such that $\psi\in\mathrm{tp}^{\mathfrak{M}}_{w}[a_{\psi,i}]$, and $a_{\psi,i}\not=a_{\psi,j}$, for $i\not=j$. We then define a ‘small’ subset $D_{w}\subseteq\mathfrak{d}(w)$, by taking

[TABLE]

for all $w\in W$. It follows that ${\left|{D_{w}}\right|}\leq n(C+1)$, for all $w\in W$. We may now define a new domain function $\mathfrak{d}^{\prime}:W\to D$, inductively, by taking

[TABLE]

where $v$ is the (unique) predecessor of $w$, so that $\mathfrak{d}^{\prime}(v)\subseteq\mathfrak{d}^{\prime}(w)$ whenever $vRw$. Furthermore, we note that ${\left|{\mathfrak{d}^{\prime}(w)}\right|}\leq{\left|{\mathfrak{d}^{\prime}(v)}\right|}+n(C+1)$, from which we can may infer that ${\left|{\mathfrak{d}^{\prime}(w)}\right|}\leq nm(C+1)$, as required.

We define a new model $\mathfrak{M}^{\prime}=(\mathfrak{F},D,\mathfrak{d}^{\prime},\mathfrak{I}^{\prime})$, over $\mathfrak{F}$ by taking $\mathfrak{I}^{\prime}(w,P_{i})=\mathfrak{I}(w,P_{i})\cap\mathfrak{d}^{\prime}(w)$, for all $w\in W$ and all predicate symbols $P_{i}\in\mathsf{Pred}$ occurring in $\varphi$.

It follows from a straightforward induction on this size of $\psi\in\mathsf{sub}(\varphi)$, that

[TABLE]

for all $w\in W$ and $a\in\mathfrak{d}^{\prime}(w)$. The only non-trivial case is where $\psi$ is of the form ${\exists_{\leq c}}x\xi$, for some $\xi\in\mathsf{sub}(\varphi)$ and $c\in\mathbb{N}$. In which case we have that:

• \killcontents
• –

Case $\psi=P_{i}(x)$:   We have that

[TABLE]

• –

Case $\psi=\neg\xi$:   We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$:   We have that

[TABLE]

• –

Case $\psi=\Diamond\xi$:   We have that

[TABLE]

\endkillcontents

• –

Case $\psi=({\exists_{\leq c}}x\ \xi)$:

[TABLE]

Hence, it follows that $\mathfrak{M}^{\prime},r\models^{a_{0}}\varphi$, as required. ∎

Note that, in general, the bound given in (3) is exponential in the size of $\varphi$ owing to the binary encoding of subscripts. However, if $\varphi\in\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ belongs to any of the quantifier bound fragments, then $C<\ell$ is at most constant. Likewise, if the quantifiers are encoded as unary strings, then $C$ is also at most linear in the size of $\varphi$.

Corollary 5.2**.**

Each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ and $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}_{un}^{1}$ possess the poly-size domain property.

We can exploit this polysize domain property to construct a tableau algorithm, in the style of Ladner’s K-WORLD algorithm [21], that answers the satisfiability problem using at most polynomial space. For succinctness, the approach taken here follows the presentation given by Spaan [31].

Theorem 5.3**.**

*Let $\mathcal{K}\subseteq\mathcal{Q^{\#}\!ML}$ be any fragment of $\mathcal{Q^{\#}\!ML}$ such that $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{K}$ has the pol-sized domain property. Then the satisfiability problem for $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{K}$ is PSpace-complete. *

Theorem 5.4**.**

Let $\mathcal{K}\subseteq\mathcal{Q^{\#}\!ML}$ be any fragment of $\mathcal{Q^{\#}\!ML}$ such that $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{K}$ has the pol-sized domain property. Then the satisfiability problem for $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{K}$ is PSpace-complete.

Proof.

In what follows, let $I_{n}=\{0,\dots,(n-1)\}$ denote the set of natural numbers $<n$. We define a recursive function QK-WORLD that takes five parameters: a natural number $k\in\mathbb{N}$ controlling the recursion depth and ensuring termination, a set of fomulas $\Sigma$, two positive integers $N,t\in\mathbb{Z}^{+}$, and a labelling function $\lambda:I_{t}\to{2^{\Sigma}}$ associating each integer $i\leq t$ with a set of formulas $\lambda(i)\subseteq\Sigma$. Note that we can encode $\lambda$ succintly as a list of pairs

[TABLE]

whose size is at most $t\times{\left|{\Sigma}\right|}$. We shall refer to $G(\lambda)$ as the ‘graph’ of $\lambda$.

For $k<\omega$, the function $\textsf{QK-WORLD}_{\Sigma,N}(k,t,\lambda)$ returns TRUE if and only if the following conditions are met222For completeness, a more detailed description of how QK-WORLD may be implemented is described in Appendix A.:

1. (tab1)

For each $i<t$, we require that $\lambda(i)$ is Boolean saturated subset of $\Sigma$, which is to say that:

• (i)

$\neg\psi\in\lambda(i)$ if and only if $\psi\not\in\lambda(i)$, for all $\neg\psi\in\Sigma$, and

• (ii)

$(\psi_{1}\land\psi_{2})\in\lambda(i)$ if and only if $\{\psi_{1},\psi_{2}\}\subseteq\lambda(i)$, for all $(\psi_{1}\land\psi_{2})\in\Sigma$, 2. (tab2)

For each $i<t$ and $({\exists_{\leq c}}x\ \psi)\in\Sigma$, we require that

[TABLE] 3. (tab3)

If $k>0$, then for each $i<t$ and $\Diamond\psi\in\lambda(i)$, there exists some $t^{\prime}\in\{t,\dots,N\}$ and a labelling function $\lambda^{\prime}:I_{t^{\prime}}\to{2^{\Sigma}}$, such that:

• (i)

$\psi\in\lambda^{\prime}(i)$,

• (ii)

$\xi\in\lambda^{\prime}(j)$ only if $\Diamond\xi\in\lambda(j)$, for all $\Diamond\xi\in\Sigma$ and $j\leq t$,

• (iii)

And $\textsf{QK-WORLD}_{\Sigma,N}(\psi;k-1,t^{\prime},\lambda^{\prime})$ returns TRUE.

As with the K-WORLD function as described by Spaan [31], the above function is non-deterministic as it must explore all possible choices for the parameters $t^{\prime}$ and $\lambda^{\prime}$ demanded by condition (tab3). However, by appealing to Savitch’s theorem [26], we require only that the algorithm uses at most a polynomial amount of space along any possible computation.

Each of the checks for (tab1) can be performed ‘in-place’ on the graph of $\lambda$. The only part that requires further scrutiny is the additional check on the consistency of the counting quantifiers in (tab2), which can be achieved by with the aid of a counter that is incremented for every $\psi\in\lambda(j)$ located from among those $j<t$ and then compared against whether $({\exists_{\leq c}}\psi)\in\lambda(i)$, for each $i<t$. The additional space requirements for such a counter is at most linear in the size of $t$ (or even logarithmic if the counter is encoded in binary). If $k=0$ then there is nothing to check for (tab3). Otherwise, each of the checks (tab3)(i)–(tab3)(ii) can also be performed ‘in-place’ on the graphs of $\lambda$ and $\lambda^{\prime}$, both of which are at most polynomial in the size of $N$ and ${\left|{\Sigma}\right|}$. Finally, the depth of the recursion required for (tab3)(iii) is bounded by $k$, and so it follows that (tab3) can be perfomed in polynomial space.

For soundness and correctness, we claim that $\textsf{QK-WORLD}_{\Sigma,N}(k,t,\lambda)$ returns TRUE if and only if there is some expanding domain model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, with domain $D=I_{N}$, such that:

1. (I.H.1)

$\mathfrak{F}$ is an irreflexive, intransitive tree of depth $\leq k$, 2. (I.H.2)

${\left|{\mathfrak{d}(r)}\right|}=t$, where $r$ is the root of $\mathfrak{F}$, 3. (I.H.3)

$M,r\models^{j}\psi$ if and only if $\psi\in\lambda(j)$, for all $j<t$ and $\psi\in\Sigma$.

We prove this by induction on $k$, so let $k\geq 0$ be fixed, and if $k>0$ then suppose that the claim holds for all $m<k$:

• ($\Rightarrow$)

Suppose that $\textsf{QK-WORLD}_{\Sigma,N}(k,t,\lambda)$ returns TRUE. If $k>0$ then, by (tab3), for each $i<t$ and $\Diamond\psi\in\lambda(i)$, there must be some $t\in\mathbb{N}$ such that $t\leq t^{\prime}\leq N$ and $\lambda_{i,\psi}:I_{t_{i,\psi}}\to{2^{\Sigma}}$ such that $\psi\in\lambda_{i,\psi}(i)$ and $\textsf{QK-WORLD}_{\Sigma,N}(k-1,t_{i,\psi},\lambda_{i,\psi})$ returns TRUE. By the induction hypothesis, there is some expanding model $\mathfrak{M}_{i,\psi}=(\mathfrak{F}_{i,\psi},D_{i,\psi},\mathfrak{d}_{i,\psi},\mathfrak{I}_{i,\psi})$ satisfying conditions ((I.H.1))–((I.H.3)). From this (possibly empty) collection of models, we define a new expanding domain model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, by taking $\mathfrak{F}$ to be the result of connecting each of the trees $\mathfrak{F}_{i,\psi}$ together at a common root $r$. We define $\mathfrak{d}$ by taking $\mathfrak{d}(w)=\mathfrak{d}_{i,\psi}(w)$, whenever $w$ belongs to $\mathfrak{F}_{i,\psi}$, and setting $\mathfrak{d}(r)=I_{t}$, so that ${\left|{\mathfrak{d}(r)}\right|}=t$. Similarly, let $\mathfrak{I}(w,P_{j})=\mathfrak{I}_{i,\psi}(w,P_{j})$ whenever $w$ belongs to $\mathfrak{F}_{i,\psi}$ and let

[TABLE]

for all $P_{i}\in\mathsf{Pred}$ occurring in $\varphi$.

It follows from this construction that $\mathfrak{F}$ is an irreflexive, intranstive tree of depth $\leq k$, as required for (I.H.1), while ${\left|{\mathfrak{d}(r)}\right|}=t$, as required for (I.H.2). Finally, it follows from a routine induction that $\mathfrak{M},r\models^{i}\xi$ if and only if $\xi\in\lambda(i)$, as required for (I.H.3).

\killcontents

• –

For ((tab1))(i)

[TABLE]

• –

For ((tab1))(ii)

[TABLE]

• –

For ((tab2)), we have that

[TABLE]

\endkillcontents

• ($\Leftarrow$)

Conversely, suppose that there is a expanding domain model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$ satisfying ((I.H.1))–((I.H.3)). It is a routine exercise to show that each $\lambda(i)$ is Boolean saturated, as required for (tab1), and that $({\exists_{\leq c}}x\psi)\in\lambda(i)$ if and only if ${\left|{\{j<t:\psi\in\lambda(j)\}}\right|}\leq c$, for all $i<t$, as required for (tab2).

If $k=0$ then (tab3) holds vacuously. Otherwise, suppose that $i<t$ and $\Diamond\psi\in\lambda(i)$. By ((I.H.3)), we must have that $\mathfrak{M},r\models^{i}\Diamond\psi$, which is to say that there is some $w\in W$ such that $rRw$ and $\mathfrak{M},w\models^{i}\psi$. Choose $t^{\prime}={\left|{\mathfrak{d}(w)}\right|}$ and let $\eta:I_{t^{\prime}}\to\mathfrak{d}(w)$ be an enumeration of $\mathfrak{d}(w)$ such that $\eta(i)=i$, for all $i<t$. We may then choose $\lambda^{\prime}:I_{t^{\prime}}\to{2^{\Sigma}}$ by taking

[TABLE]

for all $j<t^{\prime}$. In particular, we have that $\psi\in\lambda^{\prime}(i)$, as required to (tab3)(i). Furthermore, if $\xi\in\lambda^{\prime}(j)$, for some $j<t$, then by definition we have that $\mathfrak{M},w\models^{j}\xi$, from which it follows that $\mathfrak{M},r\models^{j}\Diamond\xi$, since $j\in\mathfrak{d}(r)$. Consequently, it follows from (I.H.3) that that $\Diamond\psi\in\lambda(j)$, as required for (tab3)(ii). Finally, for (tab3)(iii), we note that the submodel $\mathfrak{M}_{i,\psi}=(\mathfrak{F}^{\prime},D,\mathfrak{d}^{\prime},\mathfrak{I}^{\prime})$, where $\mathfrak{F}_{i,\psi}$ is the irreflexive, intransitive subtree of $\mathfrak{F}$ generated by $w$, satisfies conditions (i)–(iii). Whence, by the induction hypothesis, we have that $\textsf{QK-WORLD}_{\Sigma,N}(k-1,t^{\prime},\lambda^{\prime})$ returns TRUE, thereby satisfying (tab3). Hence, we conclude that $\textsf{QK-WORLD}_{\Sigma,N}(k,t,\lambda)$ meets all the condition (tab1)–(tab3), and therefore returns TRUE, as required.

By Lemma 5.1, we have that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ if and only if it can be satisfied in an expanding domain model based on an irreflexive, intransitive tree of depth $\leq m=\mathsf{md}({\varphi})$, whose domains do not exceed $N=nm(C+1)$. Hence it follows that $\varphi$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$ if and only if there exists some $t<N$ and some $\lambda:I_{t}\to{2^{\Sigma}}$ such that $\textsf{QK-WORLD}_{\Sigma,N}(m,t,\lambda)$ returns TRUE, where $\Sigma=\mathsf{sub}(\varphi)$, thereby completing the proof. ∎

It is noteworthy that despite the lofty NExpTime-completness of the satisfiability problem for the one-variable counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}\cap\mathcal{QML}^{1}$ over constant domains, each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ over expanding domains shares the same computational complexity as the underlying propositional modal logic $\mathbf{K}$, for $\ell<\omega$ [21]. However, despite this, the countable union of each of these PSpace-complete fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$, results in the full one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}^{1}$, whose satisfiability problem is, once again, NExpTime-complete.

Note that despite the existence of tableau algorithms for $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{QML}$ in the current literature [9], the question as to the computational complexity of any of its decidable fragments (and of the one-variable fragment, in particular) appears to have been, hitherto, unexamined.

Consequently, Theorem 5.4 also offers the following new result for the one-variable, counting-free fragment of $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}$.

Corollary 5.5**.**

The satisfiability problem for the one-variable, counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{exp}}\cap\mathcal{QML}^{1}$ is PSpace-complete.

6 Logics with bounded quantifiers over decreasing domains

Unlike for logics over expanding domains, we cannot escape the possibility that our decreasing models may require exponentially large domains; that is to say, they do not possess the poly-size domain property. This is true even if we restrict ourselves to the one-variable counting-free fragment $\mathcal{QML}^{1}$, as evidenced by the following formula, adapted from [22]:

[TABLE]

Note that each $\theta_{n}$, for $n<\omega$, can only be satisfied in models in which the domain at the root node is exponential in the size of $\theta_{n}$. As a result, we cannot emulate the proof of Theorem 5.4 over decreasing domain models to provide us with a PSpace upper-bound on the complexity of $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$. Indeed, we may show that over decreasing domains, the satisfiability problem for the one-variable fragment is ExpTime-hard, even if we restrict ourself to using only the counting-free quantifiers ${\exists}x$ and $\forall x$. Despite the lack of counting quantifiers, the comutational complexity of this fragments appears to have not yet been uncovered inthe current literature.

Theorem 6.1**.**

The satisfiability problem for the one-variable counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{0}^{1}$ is ExpTime-hard.

Proof.

The proof is via a reduction from the ExpTime-complete satisfiability problem for the propositional bimodal logic $\mathbf{K}_{u}$, characterised by the class of all bimodal Kripke frames $\mathfrak{F}=(W,R_{1},R_{2})$, where $R_{2}=W\times W$ is the universal relation on $W$ [31] (or [20, Theorem 1.27]).

To this end, let $\varphi\in\mathcal{ML}_{u}$ an arbitrary bimodal propositional formula in the modal language having a universal modality. Let $S,T\in\mathsf{Pred}$ be unary predicate symbols, and for each propositional variable $p_{k}\in\mathsf{sub}(\varphi)$ we associate a fresh unary predicate symbol $P_{k}\in\mathsf{Pred}$. In addition to these, we reserve a fresh auxilliary predicate symbol $Q_{\psi}\in\mathsf{Pred}$, for each subformula $\psi\in\mathsf{sub}(\varphi)$. We then define the translation $(\cdot)^{\dagger}:\mathsf{sub}(\varphi)\to\mathcal{QML}^{1}$, by taking

[TABLE]

Furthermore, take $\zeta$ to be the conjunction of the following formulas:

[TABLE]

We claim that $\varphi$ is satisfiable with respect to $\mathbf{K}_{u}$ if and only if $(\zeta\land\varphi^{\dagger})$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$.

• ($\Leftarrow$)

Suppose that $(\zeta\land\varphi^{\dagger})$ is satisfiable with repsect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$, which is to say that $\mathfrak{M},r\models^{a_{0}}\zeta$ and $\mathfrak{M},r\models^{a_{0}}\varphi^{\dagger}$, for some first-order decreasing model $\mathfrak{M}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, where $\mathfrak{F}$ is an irreflexive intransitive tree.

We define a new Kripke frame $\mathfrak{F}^{\prime}=(W^{\prime},R^{\prime})$ by taking $W^{\prime}=\mathfrak{d}(r)$ and

[TABLE]

for all $a,b\in W^{\prime}$. We define a propositional valuation $\mathfrak{V}$ by taking $\mathfrak{V}(p_{i})=\mathfrak{I}(r,P_{i})$, for all $p_{i}\in\mathsf{sub}(\varphi)$.

We prove by induction on the size of $\psi\in\mathsf{sub}(\varphi)$ that

[TABLE]

for all $a\in W^{\prime}$. The cases where $\psi$ is an atomic formula or a Boolean combination of smaller formulas are straightforward and follow from the definitions. So suppose that $\psi$ is of the form $\Diamond\xi$ or ${\exists_{\leq c}}x\xi$, for some $\xi\in\mathsf{sub}(\varphi)$ and $c\in\mathbb{N}$. In which case we have the following:

• \killcontents
• –

Case $\psi=p_{i}$:   This follows immediately from the definition of $\mathfrak{I}(w,P_{i})$ since

[TABLE]

• –

Case $\psi=\neg\xi$:   We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$:   We have that

[TABLE]

\endkillcontents

• –

Case $\psi=\Diamond_{u}\xi$:   We have that

[TABLE]

• –

Case $\psi=\Diamond\xi$:   If $\mathfrak{M}^{\prime},a\models\Diamond\xi$ then there is some $b\in W^{\prime}$ such that $aR^{\prime}b$ and $\mathfrak{M}^{\prime},b\models\xi$. By the induction hypothesis, we have that $\mathfrak{M},r\models^{b}\xi^{\dagger}$. Whence, by (4), we have that $\mathfrak{M},r\models^{b}\Box Q_{\xi}(x)$. By the definition of $R^{\prime}$, there is some $u\in W$ such that $rRu$, $a\in\mathfrak{I}(u,S)$ and $b\in\mathfrak{I}(u,T)$. It follows that $\mathfrak{M},u\models^{b}T(x)\land Q_{\xi}(x)$ and so $\mathfrak{M},u\models^{a}S(x)\land{\exists}x(T(x)\land Q_{\xi}(x))$. Therefore, $\mathfrak{M},r\models^{a}\Diamond(S(x)\land{\exists}x(T(x)\land Q_{\xi}(x)))$, which is to say that $\mathfrak{M},r\models^{a}(\Diamond\xi)^{\dagger}$, as required.

Conversely, suppose that $\mathfrak{M},r\models^{a}\Diamond(S(x)\land{\exists}x(T(x)\land Q_{\xi}(x)))$. Then there is some $u\in W$ such that $\mathfrak{M},u\models^{a}S(x)\land{\exists}x(T(x)\land Q_{\xi}(x))$. It follows that $a\in\mathfrak{I}(u,S)$ and there is some $b\in\mathfrak{I}(u,T)\subseteq\mathfrak{d}(u)$ such that $\mathfrak{M},u\models^{b}Q_{\xi}(x)$. Note that by the definition of $R^{\prime}$, we have that $aR^{\prime}b$. Furthermore, since $\mathfrak{M}$ is decreasing, we have that $b\in\mathfrak{d}(r)\supseteq\mathfrak{d}(u)$, and so $\mathfrak{M},r\models^{b}\Diamond Q_{\xi}(x)$. Whence, by (5), we have that $\mathfrak{M},r\models^{b}\xi^{\dagger}$, and so it follows from the induction hypothesis that $\mathfrak{M}^{\prime},b\models\xi$. We then have that $\mathfrak{M}^{\prime},a\models\Diamond\xi$, as required.

Hence it follows that $\mathfrak{M}^{\prime},a\models\psi$ if and only if $\mathfrak{M},r\models^{a}\psi^{\dagger}$, for all $\psi\in\mathsf{sub}(\varphi)$ and $a\in W^{\prime}$. In particular, we have that $\mathfrak{M}^{\prime},a_{0}\not\models\varphi$, which is to say that $\varphi$ is satisfiable with respect to $\mathbf{K}_{u}$, as required.

• ($\Leftarrow$)

Suppose that $\varphi$ is satisfiable with respect to $\mathbf{K}_{u}$. Then $\mathfrak{M},r\not\models\varphi$ for some propositional Kripke model $\mathfrak{M}=(\mathfrak{F}_{u},\mathfrak{V})$, where $\mathfrak{F}=(W,R)$ is an irreflexive, intranstive tree and $\mathfrak{F}_{u}=(W,R,W\times W)$.

We construct a new frame $\mathfrak{F}^{\prime}=(W^{\prime},R^{\prime})$ by taking

[TABLE]

where $\circ\not\in W$ is a newly introduced root node, from which all other worlds are accessible. We construct a first-order Kripke model on $\mathfrak{F}^{\prime}$ by taking $\mathfrak{M}^{\prime}=(\mathfrak{F}^{\prime},D^{\prime},\mathfrak{d},\mathfrak{I})$, where $D^{\prime}=W$, $\mathfrak{d}(\circ)=\mathfrak{d}(w)=D^{\prime}$, for all $w\in W$, and taking:

[TABLE]

for all $u\in W$, with

[TABLE]

for all $p_{i}\in\mathsf{sub}(\varphi)$.

We prove by induction on the size of $\psi\in\mathsf{sub}(\varphi)$ that

[TABLE]

for all $w\in W$. Again, the cases where $\psi$ is an atomic formula or a Boolean combination of smaller formulas are straightforward and follow from the definitions. So suppose that $\psi$ is of the form $\Diamond\xi$ or ${\exists_{\leq c}}x\xi$, for some $\xi\in\mathsf{sub}(\varphi)$ and $c\in\mathbb{N}$. We then have the following cases:

• \killcontents
• –

Case $\psi=p_{i}$:   This follows immediately from the definition of $\mathfrak{I}(\circ,P_{i})$, since

[TABLE]

• –

Case $\psi=\neg\xi$:   We have that

[TABLE]

• –

Case $\psi=(\xi_{1}\land\xi_{2})$:   We have that

[TABLE]

• –

Case $\psi=\Diamond_{u}\xi$:   We have that

[TABLE]

\endkillcontents

• –

Case $\psi=\Diamond\xi$:   If $\mathfrak{M}^{\prime},\circ\models^{w}\Diamond(S(x)\land{\exists}x(T(x)\land Q_{\xi}(x)))$, then there is some $u\in W$ such that $\mathfrak{M},u\models^{w}S(x)\land{\exists}x(T(x)\land Q_{\xi}(x))$. It follows from the definition of $\mathfrak{I}(u,S)$ that $u=w$. Furthermore, there is some $v\in W$ such that $\mathfrak{M},u\models^{v}T(x)\land Q_{\xi}(x)$. By the definitions of $\mathfrak{I}(u,T)$ and $\mathfrak{I}(u,Q_{\xi})$, we have that $uRv$ and $\mathfrak{M},v\models\xi$. Hence $\mathfrak{M},u\models\Diamond\xi$, which is to say that $\mathfrak{M},w\models\Diamond\xi$, since $u=w$, as required.

Conversely, suppose that $\mathfrak{M},w\models\Diamond\xi$. Then there is some $v\in W$ such that $wRv$ and $\mathfrak{M},v\models\xi$. It follows from the definition that $w\in\mathfrak{I}(w,S)$, $v\in\mathfrak{I}(w,Q_{\xi})$ and $v\in\mathfrak{I}(w,T)$. We then have that $\mathfrak{M}^{\prime},w\models^{w}S(x)\land{\exists}x(T(x)\land Q_{\xi}(x))$. Furthermore, since $\circ R^{\prime}w$, for all $w\in W$, we have that $\mathfrak{M}^{\prime},\circ\models^{w}\Diamond(S(x)\land{\exists}x(T(x)\land Q_{\xi}(x)))$, which is to say that $\mathfrak{M}^{\prime},\circ\models^{w}(\Diamond\xi)^{\dagger}$, as required.

Hence it follows that $\mathfrak{M}^{\prime},\circ\models^{w}\psi^{\dagger}$ if and only if $\mathfrak{M},w\models\psi$, for all $\psi\in\mathsf{sub}(\varphi)$ and $w\in W$. In particular, we have that $\mathfrak{M}^{\prime},\circ\models^{r}\varphi^{\dagger}$. Therefore, it remains to show that $\mathfrak{M}^{\prime},\circ\models^{r}\zeta$.

• –

For (5), suppose that $w\in W$ is such that $\mathfrak{M}^{\prime},\circ\models^{w}\Diamond Q_{\psi}(x)$. Then there is some $u\in W^{\prime}$ such that $\circ R^{\prime}u$ and $\mathfrak{M}^{\prime},u\models^{w}Q_{\psi}(x)$. By definition we have that $\mathfrak{M},w\models\psi$. It then follows from (I.H.4) that $\mathfrak{M}^{\prime},\circ\models^{w}\psi^{\dagger}$. Consequently, we have that $\mathfrak{M}^{\prime}\circ\models^{a_{0}}\forall x(\Diamond Q_{\psi}(x)\to\psi^{\dagger})$.

• –

For (4), suppose that $w\in W$ is such that $\mathfrak{M}^{\prime},\circ\models^{w}\psi^{\dagger}$. Then by (I.H.4), we have that $\mathfrak{M},w\models\psi$. By definition, $w\in\mathfrak{I}(u,Q_{\psi})$, for all $u\in W$ and so $M^{\prime},\circ\models^{w}\Box Q_{\psi}(x)$. Consequently, we have that $\mathfrak{M}^{\prime},\circ\models^{a_{0}}\forall x(\psi^{\dagger}\to\Box Q_{\psi}(x))$.

Hence, we have that $\mathfrak{M}^{\prime},\circ\models^{r}(\zeta\land\varphi^{\dagger})$, which is to say that $(\zeta\land\varphi^{\dagger})$ is satisfiable with respect to $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}$, as required.

Since the satisfiability problem for the propositional modal logic $\mathbf{K}_{u}$ is ExpTime-hard, so too must be that of the one-variable counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{0}^{1}$, as required. ∎

This result, together with that of Theorem 3.1, places the complexity of the satisfiability problem for each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$, and that of $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{un}^{1}$ between ExpTime-hard and NExpTime. However, it remains open as to where their precise complexities lie.

Question 6.2**.**

Is the complexity of the satisfiability problem for each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$, strictly less than that of their union $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}^{1}$?

Question 6.3**.**

Is the complexity of the satisfiability problem for $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{0}^{1}$ strictly less than that of $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{1}^{1}$?

7 Applications to two-dimensional propositional modal logics

First-order modal logics are intimately related to another extensively studied formalism; that of many-dimensional modal logics [30, 27, 20, 19, 23]. Given a countably infinite set of propositional variables $\mathsf{Prop}=\{p_{0},p_{1},\dots\}$, let $\mathcal{ML}_{2}$ denote the set of bimodal formulas defined in accordance to the following grammar:

[TABLE]

where $p_{i}\in\mathsf{Prop}$, and $\Diamond_{h}$ and $\Diamond_{v}$ are modal operators, with subscripts suggestive of the ‘horizontal’ and ‘vertical’ dimensions in which they are to operate. Formulas of $\mathcal{ML}_{2}$ are interpreted over Kripke models $\mathfrak{M}=(\mathfrak{F},\mathfrak{V})$, where $\mathfrak{F}=(W,R_{h},R_{v})$ is a bimodal Kripke frame, with $R_{h},R_{v}\subseteq W^{2}$, and $\mathfrak{V}:\mathsf{Prop}\to{2^{W}}$ is a propositional valuation on $\mathfrak{F}$. Satisfiability is defined in the usual way with $\Diamond_{j}\varphi$ being interpreted by the relation $R_{j}$, for $j=h,v$. Of particular interest are product models in which the two modal operators act orthogonally: We define the product of two unimodal frames $\mathfrak{F}_{h}=(W_{h},R_{h})$ and $\mathfrak{F}_{v}=(W_{v},R_{v})$ to be the bimodal frame $\mathfrak{F}_{h}\times\mathfrak{F}_{v}=(W_{h}\times W_{v},\overline{R}_{h},\overline{R}_{v})$, where

[TABLE]

for all $u,u^{\prime}\in W_{h}$ and $v,v^{\prime}\in W_{v}$. A formula $\varphi\in\mathcal{ML}_{2}$ is said to be satisfiable with respect to $L_{h}\times L_{v}$ if it is satisfiable in some product model $\mathfrak{F}_{h}\times\mathfrak{F}_{v}$, where $\mathfrak{F}_{h}$ and $\mathfrak{F}_{v}$ are frames for $L_{h}$ and $L_{v}$, respectively.

The product construction was first described by Segerberg in [27] for the case where both components were frames for $\mathbf{S5}$, and was later generalised to arbitrary frames by Shehtman [30].

A natural extension of the product construction is to consider subframes of product frames, in which only a subset of the possible worlds of $\mathfrak{F}_{h}\times\mathfrak{F}_{v}$ are possible. We say that $\mathfrak{G}=(W,R_{h},R_{v})$ is:

• –

an expanding product model if $(u,v)\in W$ implies $(u,v^{\prime})\in W$, and

• –

a decreasing product model if $(u,v^{\prime})\in W$ implies $(u,v)\in W$,

whenever $vR_{h}v^{\prime}$.

It was observed by Wasjberg [34] that the one-variable fragment of first-order logic can be interpreted as a syntactic variant of the modal logic $\mathbf{S5}$ of all equivalence frames. This can be naturally extended to the one-variable fragment of first-order modal logics under the translation that maps $\Diamond\varphi:=\Diamond_{h}\varphi$ and $({\exists}x\varphi):=\Diamond_{v}\varphi$ [10]. From this, we obtain the following proposition.

Proposition 7.1**.**

(i)* The satisfiablity problem for $\mathbf{L}\times\mathbf{S5}$ is equivalent to that of $\mathbf{Q}^{\#}\!{\mathbf{L}}\cap\mathcal{QML}^{1}$. (ii) The satisfiablity problem for $\mathbf{L}\times^{\mathit{sf}}\mathbf{S5}$ is equivalent to that of $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{sf}}\cap\mathcal{QML}^{1}$, for $\mathit{sf}\in\{\mathit{exp},\mathit{dec}\}$.*

A closely related sub-logic of $\mathbf{S5}$ is von Wright’s ‘logic of elsewhere’ $\mathbf{Diff}$, characterized by the class of all difference frames of the form $(W,R_{\neq})$ in which $uR_{\neq}v$ if and only of $u\not=v$, for all $u,v\in W$ [33]. Segerberg later provided a complete axiomatisation for $\mathbf{Diff}$, identifying it as the logic of all symmetric, weakly-transitive frames, with the following axioms [28]:

[TABLE]

By extending Wajsberg’s result for $\mathbf{S5}$, we can reduce the satisfiability problem for $\mathbf{L}\times\mathbf{Diff}$ to that of with a fragment of $\mathbf{Q}^{\#}\!{\mathbf{L}}\cap\mathcal{Q^{\#}\!ML}_{1}^{1}$, with the aid of some counting quantifiers.

Proposition 7.2**.**

(i)* The satisfiablity problem for $\mathbf{L}\times\mathbf{Diff}$ is equivalent to that of $\mathbf{Q}^{\#}\!{\mathbf{L}}\cap\mathcal{Q^{\#}\!ML}_{1}^{1}$. (ii) The satisfiablity problem for $\mathbf{L}\times^{\mathit{sf}}\mathbf{Diff}$ is equivalent to that of $\mathbf{Q}^{\#}\!{\mathbf{L}}^{\mathit{sf}}\cap\mathcal{Q^{\#}\!ML}_{1}^{1}$, for $\mathit{sf}\in\{\mathit{exp},\mathit{dec}\}$.*

Proof.

Let $\varphi\in\mathcal{ML}_{2}$ be a propositional bimodal formula, and let $P_{i}\in\mathsf{Pred}$ be a unary predicate symbol associated with each propositional variable $p_{i}\in\mathsf{sub}(\varphi)$. We define the translation $(\cdot)^{\dagger}:\mathcal{ML}_{2}\to\mathcal{Q^{\#}\!ML}_{1}^{1}$ by taking

[TABLE]

for each $p_{i}\in\mathsf{sub}(\varphi)$. Take $\zeta\in\mathcal{Q^{\#}\!ML}_{1}^{1}$ to be the following conjunction:

[TABLE]

where ${\exists}^{\neq}x\ \psi:=(\neg\psi^{\dagger}\land\neg{\exists_{\leq 0}}x\ \psi^{\dagger})\lor\neg{\exists_{\leq 1}}x\ \psi^{\dagger}$ specifies the existence of some other domain object satisfying $\psi$. Note that, since $\left\|{\psi^{\dagger}}\right\|\leq\left\|{\psi}\right\|$, for all $\psi\in\mathsf{sub}(\varphi)$, we have that $\zeta$ is at most polynomial in the size of $\varphi$.

For each subframe product model $\mathfrak{M}=(\mathfrak{G},\mathfrak{V})$, where $\mathfrak{G}\subseteq\mathfrak{F}_{h}\times\mathfrak{F}_{v}$, we associate a first-order Kripke model $\mathfrak{M}^{\star}=(\mathfrak{F},D,\mathfrak{d},\mathfrak{I})$, by taking $\mathfrak{F}=(W_{h},R_{h})$, $D=W_{v}$, $\mathfrak{d}(u)=\{v\in W_{v}:(u,v)\in V\}$ and

[TABLE]

for all $u\in W_{h}$, $p_{i}\in\mathsf{Prop}$ and $\psi\in\mathsf{sub}(\varphi)$. It then follows from a routine induction that $\varphi$ is satisfiable in $\mathfrak{M}$ if and only if $(\zeta\land\varphi^{\dagger})$ is satisfiable in $\mathfrak{M}^{\star}$. Furthermore, it is straightforward to check that $\mathfrak{M}^{\star}$ is an expanding (resp. decreasing) domain model precisely when $\mathfrak{M}$ is an expanding (resp. decreasing) product model, therby completing the proof. ∎

By taking $\mathbf{L}$ to be the minimal modal logic $\mathbf{K}$, Propositions 7.1 and 7.2 yield the following corollaries of Theorems 3.1,5.4, and 6.1:

Corollary 7.3**.**

The satisfiability problem for:

• (i)

$\mathbf{K}\times\mathbf{Diff}$* is *NExpTime-complete333Is is already well-established that $\mathbf{K}\times\mathbf{S5}$ is also NExpTime-complete [22].,

• (ii)

$\mathbf{K}\times^{\mathit{exp}}\mathbf{L}$* is PSpace-complete, for $\mathbf{L}\in\{\mathbf{S5},\mathbf{Diff}\}$,*

• (iii)

$\mathbf{K}\times^{\mathit{dec}}\mathbf{L}$* is ExpTime-hard in NExpTime, for $\mathbf{L}\in\{\mathbf{S5},\mathbf{Diff}\}$.*

These results mark a stark contrast against the negative results one often faces when taking two-dimenisonal products with von Wright’s logic, which are often vastly more complex than their corresponding $\mathbf{S5}$-counterparts. In particular, the satisfiability problem for $\mathbf{K}_{u}\times\mathbf{Diff}$ is undecidable [15], while that of $\mathbf{K}_{u}\times\mathbf{S5}$ is decidable in N2ExpTime [20, Theorem 6.5]. A similar jump in complexity arises for products in which the horizontal component is characterised by some class of linear orders, such as with $\mathbf{K4.3}\times\mathbf{S5}$ whose satisfibility problem is decidable in 2ExpTime, whereas that of $\mathbf{K4.3}\times\mathbf{Diff}$ is undecidable [13].

8 Discussion

Throughout this paper, we have focused our attention on fragments of $\mathcal{Q^{\#}\!ML}$ comprising a single first-order variable, owing to the wealth of negative results that already exist for two-variable modal logics [18]. However, there remains scope to investigate the role of counting quantifiers to fragments that lie beyong the one-variable fragment, such as the monodic fragment, briefly described in Section 1 [36]

However, it should be noted that there is no immediate application of the techniques developed in [36], which the authors employed to prove that the (counting-free) monodic fragment of $\mathbf{Q}^{\#}\!{\mathbf{K^{\ast}}}$ is decidable, where $\mathbf{K^{\ast}}$ denotes the bimodal logic of all frames whose second relation is the transitive closure of the first. It is known, however, that even the one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K^{\ast}}}\cap\mathcal{Q^{\#}\!ML}_{1}^{1}$, whose sole counting quantifiers are ${\exists_{\leq 0}}x$ and ${\exists_{\leq 1}}x$, is already non-recursively enumerable [15] (indeed, even highly undecidable [12, Theorem 8.5]).

The one-variable counting-free fragment $\mathbf{Q}^{\#}\!{\mathbf{K4}}\cap\mathcal{QML}^{1}$ is known to admit filtration and so it’s satsifiability problem can be decided in N2ExpTime [29, 20], where $\mathbf{K4}$ is the logic of all transitive frames. However, it remains open whether the the satisfiability problem for the full one-variable fragment $\mathbf{Q}^{\#}\!{\mathbf{K4}}\cap\mathcal{Q^{\#}\!ML}^{1}$ or for any of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K4}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$ are decidable, for $0<\ell<\omega$. It is tempting to consider whether the results of Section 5, can be adapted to provide a similar PSpace upper-bound on the satisfaibility problem for $\mathbf{Q}^{\#}\!{\mathbf{K4}}^{\mathit{exp}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, analogous to Ladner’s $\mathsf{K4\mbox{-}WORLD}$ algorithm. However, this approach fails since the finite domain property, proved in Lemma 5.1, was contingent on every posible world having at most one predecessor. Indeed, it is not difficult to construct examples of satisfiable formulas that cannot be satisfied in models having only finitely many domain elements [20, Theorem 5.32].

The main question left open in this paper asks what is the precisely complexity of the satisfiability problem for each of the fragments $\mathbf{Q}^{\#}\!{\mathbf{K}}^{\mathit{dec}}\cap\mathcal{Q^{\#}\!ML}_{\ell}^{1}$, for $\ell<\omega$. One might suppose that, given the lack of the poly-size domain property, that one may be able to derive an NExpTime-hard lower-bound via a reduction from the $(2^{n}\times 2^{n})$-tiling problem [32], a la Marx [22]. However, the reduction employed by Marx relies heavily on both left and right commutativity between the modal operators and first-order quantifiers.

Indeed, part of the problem we face with logics over decreasing domains is the inability for branches to ‘communicate’ directly with one another as they do in constant domain models, where every object in one branch is shared between every other branch of the model. Contrast this with the situation in decreasing domain models, where the first-order domains at each of the leaves of the underlying frame may be wholly disjoint from one another. There may, therefore, be hope that an ExpTime algorithm for this fragment may yet be uncovered.

Appendix A Implementation of QKworld Algorithm