# Algorithmic properties of first-order modal logics of linear Kripke frames
in restricted languages††thanks: To appear in Journal of Logic and
Computation, https://doi.org/10.1093/logcom/exab030

Mikhail Rybakov  Institute for Information Transmission Problems of Russian
Academy of Sciences, Moscow 127051, Russia  Dmitry Shkatov  School of Computer
Science and Applied Mathematics, University of the Witwatersrand,
Johannesburg, WITS2050, South Africa<EMAIL_ADDRESS>
(August 29, 2024)

###### Abstract

We study the algorithmic properties of first-order monomodal logics of frames
$\langle\mathds{N},\leqslant\rangle$, $\langle\mathds{N},<\rangle$,
$\langle\mathds{Q},\leqslant\rangle$, $\langle\mathds{Q},<\rangle$,
$\langle\mathds{R},\leqslant\rangle$, $\langle\mathds{R},<\rangle$, as well as
some related logics, in languages with restrictions on the number of
individual variables as well as the number and arity of predicate letters. We
show that the logics of frames based on $\mathds{N}$ are
$\Pi^{1}_{1}$-hard—thus, not recursively enumerable—in languages with two
individual variables, one monadic predicate letter and one proposition letter.
We also show that the logics of frames based on $\mathds{Q}$ and $\mathds{R}$
are $\Sigma^{0}_{1}$-hard in languages with the same restrictions. Similar
results are obtained for a number of related logics.

##  1 Introduction

How algorithmically expressive are first-order modal logics? More expressive,
it is reasonable to assume, than the classical first-order logic
$\mathbf{QCl}$—just as propositional modal logics are, as a rule,
computationally harder than the classical propositional logic. (In this
context, it is natural to consider logics as sets of validities, rather than
as calculi: understood as calculi conservatively extending $\mathbf{QCl}$ with
a recursively enumerable set of axioms and finitary rules of inference, first-
order modal logics are a priori $\Sigma^{0}_{1}$-complete.111The reader in
need of a reminder of the basic concepts of computability theory may consult
[41].) Numerous first-order modal logics are, however, just as algorithmically
expressive as $\mathbf{QCl}$, i.e. $\Sigma^{0}_{1}$-complete: some—such as
$\mathbf{QK}$, $\mathbf{QT}$, $\mathbf{QD}$, $\mathbf{QKB}$, $\mathbf{QKTB}$,
$\mathbf{QS4}$ and $\mathbf{QS5}$—are recursively axiomatizable over
$\mathbf{QCl}$; others—such as logics of elementary classes of Kripke
frames—are recursively embeddable [47, 43] into $\mathbf{QCl}$ by the standard
translation [5, 11], [21, Section 3.12]. This suggests a need for a more fine-
grained analysis, which takes into account the algorithmic expressivity not
only of full logics but also of their fragments obtained by placing
restrictions on the structure of formulas. Such analysis allows us to
distinguish $\Sigma^{0}_{1}$-complete modal logics from $\mathbf{QCl}$ by
algorithmic expressivity: while the monadic fragment of $\mathbf{QCl}$ is
decidable [32, 4], the monadic fragments of most $\Sigma^{0}_{1}$-complete
modal logics are not [31]; while the two-variable fragment of $\mathbf{QCl}$
is decidable [37, 25], the two-variable fragments of most
$\Sigma^{0}_{1}$-complete modal logics are not [30]. This leads to the study
of the algorithmic properties of the fragments of first-order modal logics.

This study is also motivated by an underdevelopment, relative to
$\mathbf{QCl}$ [9], of the algorithmic classification problem for first-order
modal logics—an effort to identify their maximal decidable and minimal
undecidable fragments. Despite extensive literature [31, 34, 36, 38, 16, 3,
19, 61, 30, 46, 49], whose summary can be found in the Introduction to the
authors’ earlier article [49], much less is known about the algorithmic
properties of the fragments of first-order modal, and closely related
superintuitionistic, logics than about the algorithmic properties of the
fragments of $\mathbf{QCl}$.

The algorithmic properties of one-variable and two-variable fragments of
first-order modal logics are also of interest due to close links between those
fragments and, respectively, two-dimensional and three-dimensional
propositional modal logics [20, 18, 52].

In the present paper, we attempt to identify the minimal undecidable fragments
of the first-order monomodal logics of frames
$\langle\mathds{N},\leqslant\rangle$, $\langle\mathds{N},<\rangle$,
$\langle\mathds{Q},\leqslant\rangle$, $\langle\mathds{Q},<\rangle$,
$\langle\mathds{R},\leqslant\rangle$ and $\langle\mathds{R},<\rangle$, as well
as of closely related linear orders.222Preliminary results on the logics of
$\langle\mathds{N},\leqslant\rangle$ and $\langle\mathds{N},<\rangle$ were
reported in a conference paper [48]. The present article improves on the
earlier paper in two respects. First, we obtain stronger results on the logics
of frames based on the naturals by proving $\Sigma^{1}_{1}$-hardness for
weaker languages; the results reported in this article are plausibly optimal,
as discussed in Section 7. Second, we report results on logics of the
rationals (and hence on $\mathbf{QS4.3}$, $\mathbf{QK4.3.D.X}$ and
$\mathbf{QK4.3}$), the reals and infinite ordinals distinct from $\omega$. The
logics of these structures are of interest on at least three counts.

First, the structures themselves are of interest, for at least two reasons.
They have long been considered natural models of the flow of time [39, 23,
17]; therefore, their study has been stimulated by the long-standing interest
in temporal reasoning. Even though we focus on monomodal languages, since our
results are negative, they do apply to more expressive languages with
modalities for the past as well as the future. On a more basic level perhaps,
the structures based on the naturals, the rationals and the reals are so
fundamental to mathematics that the properties of the corresponding logics are
of intrinsic mathematical significance: the classical theories of these
structures, both first-order and second-order, have been extensively studied;
in particular, it has long been known that the monadic second-order theory of
$\langle\mathds{N},<\rangle$ is decidable [14].

Second, the logics considered here call for techniques substantially different
from those used in the previous studies [31, 19, 30, 46, 49] of the
algorithmic properties of fragments of monomodal predicate logics. For most
such logics, known undecidability proofs for fragments with a single monadic
predicate letter, a restriction considered here, require a transformation of
models that increases their branching factor. The methods the authors used
earlier [46, 49] intrinsically rely on increasing the branching factor of
models, a feature inherited from the propositional-level techniques [26, 12,
42, 44, 45, 50] those methods are based on. On the other hand, the
construction by Blackburn and Spaan [8], which is propositional but, in
principle, adaptable to first-order logics, does not seem to be readily
applicable to logics of transitive frames since it relies on the use of a
modal operator suitable for counting transitions along the accessibility
relation of a frame. The techniques used here should, therefore, be of
relevance to the study of the algorithmic properties of fragments of monomodal
logics of structures with a resticted branching factor, including trees.

Third, the logics of frames $\langle\mathds{N},\leqslant\rangle$ and
$\langle\mathds{N},<\rangle$ are algorithmically hard—as follows from Theorem
4.2 below, they are $\Pi^{1}_{1}$-hard. Most research into the algorithmic
properties of monomodal, and closely related superintuitionistic, predicate
logics has been focused on decidability and undecidability. The only study to
date [49], as far as we know, of the algorithmic properties of fragments of
not recursively enumerable monomodal predicate logics concerns logics of
frames with finite sets of worlds (likewise, very few results [16, Theorem 1,
p. 272], [51] are known on algorithmic properties of fragments of not
recursively enumerable superintuitionistic predicate logics). While it is
natural that decidability and undecidability are the main concern of the
Classical Decision Problem [9], the study of the algorithmic properties of
modal first-order logics should, we believe, involve identifying minimal
fragments that are as hard—in pertinent classes of the arithmetical, or the
analytical, hierarchy—as the full logics.

The algorithmic properties of fragments of not recursively enumerable logics
have been, however, extensively studied in the context of first-order
languages more expressive than monomodal ones considered here—most recently,
by Hodkinson, Wolter and Zakharyaschev [28, 61] (for a summary, see [18,
Chapter 11]; for earlier work, see [2, 57, 58, 1, 35]). The methods used here
have been inspired by those of Wolter and Zakharyaschev [61, Theorem 2.3], who
encode a $\Sigma^{1}_{1}$-hard tiling problem in a first-order language with
two modal operators, one corresponding to a basic accessibility relation and
the other to its reflexive transitive closure. A similar result [28, Theorem
2] has been obtained by Hodkinson, Wolter and Zakharyaschev for the first-
order temporal logic of $\langle\mathds{N},\leqslant\rangle$ in the language
with two temporal operators: ‘‘next,’’ corresponding to the immediate
successor relation on $\mathds{N}$, and ‘‘always in the future,’’
corresponding to its reflexive transitive closure, the partial order
$\leqslant$ (both operators can be expressed with a binary temporal operator
‘‘until’’).333We touch on such languages in Section 7. Another similar result
[60, Theorem 5.6] has been obtained by Wolter for the first-order logics
containing, alongside the individual knowledge operators, the common knowledge
operator whose semantics involves the reflexive transitive closure of the
union of the accessibility relations for the individual knowledge operators.
We extend herein to monomodal logics, which do not have expressive power for
capturing the reflexive transitive closures of accessibility relations,
techniques developed by Hodkinson, Wolter, and Zakharyaschev [28, 60, 61].

The paper is structured as follows. In Section 2, we introduce preliminaries
on first-order modal logic. In Section 3, we prove that satisfiability for the
logic of $\langle\mathds{N},\leqslant\rangle$ is $\Sigma^{1}_{1}$-hard in
languages with two individual variables, a single monadic predicate letter and
a single proposition letter. In Section 4, the results of Section 3 are
extended to logics of frames $\langle\mathds{N},R\rangle$, where $R$ is a
binary relation between $<$ and $\leqslant$, and to frames based on infinite
ordinals of a special form. In Section 5, we prove, by modifying the argument
of Sections 3 and 4, that satisfiability for logics of
$\langle\mathds{Q},\leqslant\rangle$, $\langle\mathds{Q},<\rangle$,
$\langle\mathds{R},\leqslant\rangle$ and $\langle\mathds{R},<\rangle$ is
$\Pi^{0}_{1}$-hard in languages with the same restrictions. In Section 6, we
briefly mention some corollaries of the results proven earlier. We conclude,
in Section 7, by discussing first-order temporal logics with modalities
‘‘next’’ and ‘‘always in the future,’’ as well as questions for future study.

##  2 Preliminaries

An unrestricted first-order predicate modal language contains countably many
individual variables; countably many predicate letters of every arity,
including 0 (nullary predicate letters are also called proposition letters);
the propositional constant $\bot$ (falsity), the binary propositional
connective $\rightarrow$, the unary modal connective $\Box$ and the quantifier
$\forall$. Formulas as well as the symbols $\top$, $\neg$, $\vee$, $\wedge$,
$\leftrightarrow$, $\exists$ and $\Diamond$ are defined in the usual way. We
also use the abbreviations $\Box^{0}\varphi=\varphi$,
$\Box^{n+1}\varphi=\Box\Box^{n}\varphi$ and
$\Diamond^{n}\varphi=\neg\Box^{n}\neg\varphi$, for every $n\in\mathds{N}$.

When parentheses are omitted, unary connectives and quantifiers are assumed to
bind tighter than $\wedge$ and $\vee$, which are assumed to bind tighter than
$\rightarrow$ and $\leftrightarrow$. We usually write atomic formulas in
prefix notation; for some predicate letters we, however, use infix.

A normal predicate modal logic is a set of formulas containing the validities
of the classical first-order predicate logic $\mathbf{QCl}$, as well as the
formulas of the form
$\Box(\varphi\rightarrow\psi)\rightarrow(\Box\varphi\rightarrow\Box\psi)$, and
closed under predicate substitution, modus ponens, generalisation and
necessitation.444The reader wishing a reminder of the definition of these
closure conditions may consult [21, Definition 2.6.1]; for a detailed
discussion of predicate substitution, consult [21, §2.3, §2.5].

In this paper, we are interested in predicate logics defined using the Kripke
semantics.555For Kripke semantics for predicate modal logics, see [53, 55, 29,
15, 22, 10, 24], [21, §3.1].

A Kripke frame is a tuple $\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$; if $wRv$, we say that $v$ is accessible from $w$ and that $w$ sees $v$.

A predicate Kripke frame with expanding domains is a tuple
$\mathfrak{F}_{D}=\langle W,R,D\rangle$, where $\langle W,R\rangle$ is a
Kripke frame and $D$ is a function from $W$ into the set of non-empty subsets
of some set, the domain of $\mathfrak{F}_{D}$; the function $D$ is required to
satisfy the condition that $wRw^{\prime}$ implies $D(w)\subseteq
D(w^{\prime})$. The set $D(w)$, also denoted by $D_{w}$, is the domain of $w$.
We also consider predicate frames satisfying the stronger condition that
$D(w)=D(w^{\prime})$, for every $w,w^{\prime}\in W$; such frames are predicate
frames with a constant domain.666More precisely, such predicate frames are
known as predicate frames with globally constant domains. For connected
predicate frames, the global constancy condition given above is equivalent to
the local constancy condition requiring that $D(w)=D(w^{\prime})$ whenever
$wRw^{\prime}$. Since the frames we consider are rooted, and therefore
connected, the distinction between global and local constancy is immaterial
for the purposes of this paper. Predicate frame simpliciter means a predicate
frame with expanding domains.

A Kripke model is a tuple $\mathfrak{M}=\langle W,R,D,I\rangle$, where
$\langle W,R,D\rangle$ is a predicate Kripke frame and $I$, the interpretation
of predicate letters with respect to worlds in $W$, is a function assigning to
a world $w\in W$ and an $n$-ary predicate letter $P$ an $n$-ary relation
$I(w,P)$ on $D(w)$—i.e., $I(w,P)\subseteq D_{w}^{n}$. In particular, if $p$ is
a proposition letter, then $I(w,P)\subseteq D_{w}^{0}=\\{\langle\rangle\\}$;
thus, we can identify truth with $\\{\langle\rangle\\}$ and falsity with
$\varnothing$. We often write $P^{I,w}$ instead of $I(w,P)$. We say that a
model $\langle W,R,D,I\rangle$ is based on the frame $\langle W,R\rangle$ and
is based on the predicate frame $\langle W,R,D\rangle$.

We use the standard notation for binary relations: the $n$-fold, for each
$n\in\mathds{N}^{+}$, composition of a binary relation $R$ is denoted by
$R^{n}$; if $R$ is a binary relation on a non-empty set $W$ and $w\in W$, then
$R(w)=\\{v\in W:wRv\\}$.

An assignment in a model is a function $g$ associating with every individual
variable $x$ an element $g(x)$ of the domain of the underlying predicate
frame. We write $g^{\prime}\stackrel{{\scriptstyle x}}{{=}}g$ if assignment
$g^{\prime}$ differs from assignment $g$ in at most the value of $x$.

The truth of a formula $\varphi$ at a world $w$ of a model $\mathfrak{M}$
under an assignment $g$ is defined recursively:

  * •

$\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}$, where $P$ is an $n$-ary predicate
letter;

  * •

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

  * •

$\mathfrak{M},w\models^{g}\varphi_{1}\rightarrow\varphi_{2}$ if
$\mathfrak{M},w\models^{g}\varphi_{1}$ implies
$\mathfrak{M},w\models^{g}\varphi_{2}$;

  * •

$\mathfrak{M},w\models^{g}\Box\varphi_{1}$ if
$\mathfrak{M},w^{\prime}\models^{g}\varphi_{1}$, for every $w^{\prime}\in
R(w)$;

  * •

$\mathfrak{M},w\models^{g}\forall x\,\varphi_{1}$ if
$\mathfrak{M},w\models^{g^{\prime}}\varphi_{1}$, for every $g^{\prime}$ such
that $g^{\prime}\stackrel{{\scriptstyle x}}{{=}}g$ and $g^{\prime}(x)\in
D_{w}$.

Observe that, if $\mathfrak{M}=\langle W,R,D,I\rangle$ is a Kripke model,
$w\in W$ and $I_{w}(P)=I(w,P)$, then $\mathfrak{M}_{w}=\langle
D_{w},I_{w}\rangle$ is a classical model, or structure.

We shall often 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 whose free variables are among
$x_{1},\ldots,x_{n}$ and $g$ an assignment with
$g(x_{1})=a_{1},\ldots,g(x_{n})=a_{n}$. Then, we write
$\mathfrak{M},w\models\varphi(a_{1},\ldots,a_{n})$ instead of
$\mathfrak{M},w\models^{g}\varphi(x_{1},\ldots,x_{n})$. This notation is
unambiguous since the languages we consider lack constants and the truth value
of $\varphi(x_{1},\ldots,x_{n})$ does not depend on the values of variables
other than $x_{1},\ldots,x_{n}$.

A formula $\varphi$ is true at a world $w$ of a model $\mathfrak{M}$ (in
symbols, $\mathfrak{M},w\models\varphi$, or simply $w\models\varphi$ if
$\mathfrak{M}$ is clear from the context) if
$\mathfrak{M},w\models^{g}\varphi$, for every $g$ assigning to free variables
of $\varphi$ elements of $D_{w}$. A formula $\varphi$ is true in a model
$\mathfrak{M}$ (in symbols, $\mathfrak{M}\models\varphi$) if
$\mathfrak{M},w\models\varphi$, for every world $w$ of $\mathfrak{M}$. A
formula $\varphi$ is valid on a predicate frame $\mathfrak{F}_{D}$ if
$\varphi$ is true in every model based on $\mathfrak{F}_{D}$. A formula
$\varphi$ is valid on a frame $\mathfrak{F}$ (in symbols,
$\mathfrak{F}\models\varphi$) if $\varphi$ is valid on every predicate frame
$\langle\mathfrak{F},D\rangle$. These notions, and the corresponding notation,
can be extended to sets of formulas, in a natural way.

We shall often rely on the following observation: if a model $\mathfrak{M}$ is
based on a predicate frame with a constant domain, then
$\mathfrak{M},w\models\varphi$ if, and only if,
$\mathfrak{M},w\models^{g}\varphi$, for every assignment $g$.

Let $\mathfrak{C}$ be a class of Kripke frames. The set of formulas valid on
every frame in $\mathfrak{C}$ is a predicate modal logic, which we denote by
$\mathbf{L}(\mathfrak{C})$; we write $\mathbf{L}(W,R)$ instead of
$\mathbf{L}(\\{\langle W,R\rangle\\})$. The set of formulas valid on every
predicate frame with a constant domain based on some frame in $\mathfrak{C}$
also is a predicate modal logic, which we denote by
${\mathbf{L}_{c}}(\mathfrak{C})$; we write ${\mathbf{L}_{c}}(W,R)$ instead of
${\mathbf{L}_{c}}(\\{\langle W,R\rangle\\})$.

##  3 The first-order logic of $\langle\mathds{N},\leqslant\rangle$

In this section, we prove that satisfiability for
$\mathbf{L}(\mathds{N},\leqslant)$ is $\Sigma^{1}_{1}$-hard—hence,
$\mathbf{L}(\mathds{N},\leqslant)$ is $\Pi^{1}_{1}$-hard, and therefore not
recursively enumerable—in languages with two individual variables, one monadic
predicate letter and one proposition letter.

###  3.1 Reduction from a tiling problem

We do so by encoding the following $\Sigma^{1}_{1}$-complete [27, Theorem 6.4]
$\mathds{N}\times\mathds{N}$ recurrent tiling problem. We are given a set of
tiles, a tile $t$ being a $1\times 1$ square, with a fixed orientation, whose
edges are colored with $\textit{left}(t)$, $right(t)$, $up(t)$ and $down(t)$.
A tile type is a quadruplet of edge colors. Each tile has a type from the set
$T=\\{t_{0},\ldots,t_{s}\\}$, tiles of each type being in an unlimited supply.
A tiling is an arrangement of tiles on the rectangular
$\mathds{N}\times\mathds{N}$ grid so that the edge colors of the adjacent
tiles match, both horizontally and vertically. We are to determine whether
there exists a tiling of the grid in which a tile of type $t_{0}$ occurs
infinitely often in the leftmost column, i.e., whether there exists a function
$f:\mathds{N}\times\mathds{N}\to T$ such that, for every $n,m\in\mathds{N}$,

  * ($T_{1}$) $right(f(n,m))=\textit{left}(f(n+1,m))$;

  * ($T_{2}$) $up(f(n,m))=\textit{down}(f(n,m+1))$;

  * ($T_{3}$) the set $\\{m\in\mathds{N}:f(0,m)=t_{0}\\}$ is infinite.

The idea of the encoding we use is based on the work of Hodkinson, Wolter and
Zakharyaschev [28, Theorem 2] (also see [18, Theorem 11.1]; similar
constructions have been used elsewhere [56, 33, 61, 30]), but the encoding
itself is more involved since our language lacks the ‘‘next’’ operator
available to them (we touch on languages with ‘‘next’’ in Section 7). To make
the underlying idea clearer, we construct, in the initial encoding, a formula
of two individual variables without regard for the number of predicate letters
involved; subsequently, we reduce the formula thus obtained to a formula with
a single monadic and a single proposition letter.

Let $\triangleleft$ be a binary predicate letter, $M$ and $P_{t}$—for every
$t\in T$—monadic predicate letters and $p$ a proposition letter.

Given a formula $\varphi$ in such a language, define

$\begin{array}[]{c}\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}\varphi=\Diamond(p\wedge\Diamond(\neg
p\wedge\varphi));\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}^{0}\varphi=\varphi;\quad\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}^{n+1}\varphi=\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}^{n}\varphi,\mbox{ for every
}n\in\mathds{N}.\end{array}$

The operator $\Diamond$ $\Diamond$ forces a transition to a different world
when evaluating a formula $\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}\varphi$ in a reflexive model, just as $\Diamond$
does in an irreflexive one. To make this explicit, we define, given a model
based on the frame $\langle\mathds{N},\leqslant\rangle$, a binary relation
$R_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}$ on
$\mathds{N}$ by

$\begin{array}[]{lcl}wR_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}v&\leftrightharpoons&\mbox{$v\not\models p$ and,
for some $u\in\mathds{N}$, both $w\leqslant u\leqslant v$ and $u\models
p$.}\end{array}$

Thus, $R_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}$ is
irreflexive and transitive.

We also define

$\begin{array}[]{lcl}U(x)&=&\displaystyle\bigwedge\limits_{t\in T}\neg
P_{t}(x).\end{array}$

In such a language, define (for brevity, in formulas we write $l$, $r$, $u$
and $d$ instead of left, right, up and down)

$\begin{array}[]{rcl}A_{0}&=&\exists x\,\Box\,U(x);\\\ A_{1}&=&\exists
x\,(\neg U(x)\wedge M(x));\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
A_{2}&=&\forall x\exists y\,(x\triangleleft y);\vskip 6.0pt plus 2.0pt minus
2.0pt\\\ A_{3}&=&\forall x\forall y\,(x\triangleleft y\rightarrow\Box(\exists
x\,M(x)\rightarrow x\triangleleft y));\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
A_{4}&=&\forall x\forall y\,(x\triangleleft
y\rightarrow\Box(M(x)\leftrightarrow\neg p\wedge\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}M(y)\wedge\neg\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}^{2}M(y));\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
A_{5}&=&\displaystyle\forall x\forall y\,\Box\bigwedge\limits_{t\in
T}\big{(}M(x)\wedge P_{t}(y)\rightarrow\Box(M(x)\rightarrow
P_{t}(y))\big{)};\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
A_{6}&=&\displaystyle\forall x\,\Box\bigwedge\limits_{t\in
T}(P_{t}(x)\rightarrow\bigwedge\limits_{\mathclap{t^{\prime}\neq t}}\neg
P_{t^{\prime}}(x));\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
A_{7}&=&\displaystyle\forall x\forall y\,\Box\bigwedge\limits_{t\in
T}(x\triangleleft y\wedge
P_{t}(x)\rightarrow\bigvee\limits_{\mathclap{r(t)=l(t^{\prime})}}P_{t^{\prime}}(y));\vskip
6.0pt plus 2.0pt minus 2.0pt\\\ A_{8}&=&\displaystyle\forall x\forall
y\,\Box\bigwedge\limits_{t\in T}\big{(}M(x)\wedge
P_{t}(y)\rightarrow\Box(\exists y\,(x\triangleleft y\wedge
M(y))\rightarrow\bigvee\limits_{\mathclap{u(t)=d(t^{\prime})}}P_{t^{\prime}}(y))\big{)};\vskip
6.0pt plus 2.0pt minus 2.0pt\\\ A_{9}&=&\forall
x\,(M(x)\rightarrow\Box\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}P_{t_{0}}(x)).\end{array}$

Let $A$ be the conjunction of $A_{0}$ through $A_{9}$. Observe that $A$
contains only two individual variables.

The relation ${\triangleleft}$ can be thought of as the immediate successor
relation on the domain ${D}_{0}$ of the world $0$ where $A$ is being
evaluated. An element $a\in{D}_{0}$ such that $w\models M(a)$ can be thought
of as marking, or labelling, world $w$; thus, we say that $a$ is a mark of
$w$. Then, $A_{2}$ asserts that every element of $D_{0}$ has an immediate
successor, while $A_{3}$ asserts that the immediate successor relation
persists throughout the part of the frame where worlds are marked by elements
of $D_{0}$. Given that, $A_{1}$ and $A_{4}$ imply the existence of an infinite
sequence $a_{0}\triangleleft a_{1}\triangleleft a_{2}\triangleleft\ldots$ of
elements of $D_{0}$ such that every world refuting $p$ is marked, as we shall
see uniquely, by some element of the sequence; they also imply that the order
of the marks of successive, with respect to $\leqslant$, worlds agrees with
the relation $\triangleleft$. This, as we shall see, gives us an
$\mathds{N}\times\mathds{N}$ grid whose rows correspond to the worlds of
$\langle\mathds{N},\leqslant\rangle$ and whose columns correspond to the
elements of the sequence $a_{0}\triangleleft a_{1}\triangleleft
a_{2}\triangleleft\ldots\,$. Building on this, $A_{5}$ through $A_{9}$
describe a sought tiling of thus obtained grid. (The element of $D_{0}$ whose
existence is asserted by $A_{0}$ is not part of the tiling—its presence shall
be relied upon in a subsequent reduction.)

###### Lemma 3.1

There exists a recurrent tiling of $\mathds{N}\times\mathds{N}$ satisfying
($T_{1}$) through ($T_{3}$) if, and only if,
$\langle\mathds{N},\leqslant\rangle\not\models\neg A$.

Proof. (‘‘if’’) Suppose $\mathfrak{M},w_{0}\models A$, for some model
$\mathfrak{M}=\langle\mathds{N},\leqslant,D,I\rangle$ and some world
$w_{0}\in\mathds{N}$. Since truth of formulas is preserved under taking
generated submodels,777The notions of generated subframe and generated
submodel for predicate modal logics are straightforward extensions of the
respective notions [7, Section 2.1] for propositional modal logics. we may
assume $w_{0}=0$.

Since $0\models A_{1}$, there exists $a_{0}\in D_{0}$ such that $0\not\models
U(a_{0})$ and $0\models M(a_{0})$. Since $0\models A_{2}$, we obtain an
infinite sequence $a_{0},a_{1},a_{2},\ldots$ of elements of $D_{0}$ such that
$a_{0}\triangleleft^{I,0}a_{1}\triangleleft^{I,0}a_{2}\triangleleft^{I,0}\ldots\,\,$.
Since $0\models A_{3}$, we obtain that
$a_{0}\triangleleft^{I,w}a_{1}\triangleleft^{I,w}a_{2}\triangleleft^{I,w}\ldots\,$,
for every $w\in\mathds{N}$ such that $w\models\exists x\,M(x)$.

Since $0\models A_{4}$, we obtain, for every $w,n\in\mathds{N}$,

$None$ $\begin{array}[]{lcl}w\models
M(a_{n})&\Longleftrightarrow&\left\\{\begin{array}[]{l}w\phantom{{}^{\prime}}\not\models
p;\\\ w^{\prime}\models M(a_{n+1}),\mbox{ for some }w^{\prime}\in
R_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}(w);\\\
w^{\prime\prime}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}^{2}(w)\mbox{ implies }w^{\prime\prime}\not\models
M(a_{n+1}).\end{array}\right.\end{array}$

Thus, a mark changes from $a_{n}$ to $a_{n+1}$ once we pass through a world,
or an unbroken non-empty sequence of worlds, satisfying $p$ to a world
refuting $p$.

We now show that a mark remains unchanged until we have reached a world
satisfying $p$, i.e., that for every $u,u^{\prime},n\in\mathds{N}$,

$None$ $\begin{array}[]{l}\mbox{if $u\models M(a_{n})$, $u\not\models p$,
$u^{\prime}\not\models p$, and no $v$ with $u\leqslant v\leqslant u^{\prime}$
or $u^{\prime}\leqslant v\leqslant u$}\\\ \mbox{satisfies $v\models p$, then
$u^{\prime}\models M(a_{n})$.}\end{array}$

Assume that $u\models M(a_{n})$, $u\not\models p$, $u^{\prime}\not\models p$,
and that no $v$ with $u\leqslant v\leqslant u^{\prime}$ or
$u^{\prime}\leqslant v\leqslant u$ satisfies $v\models p$. Then, by ($1$),
there exists $w^{\prime}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(u)$ such that $w^{\prime}\models M(a_{n+1})$, and
$w^{\prime\prime}\not\models M(a_{n+1})$, for every $w^{\prime\prime}\in
R^{2}_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}(u)$. Let
us fix the said $w^{\prime}$. It follows immediately from the assumption that,
for every $w,n\in\mathds{N}$,

$\begin{array}[]{lcl}w\in R^{n}_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(u)&\Longleftrightarrow&w\in
R^{n}_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(u^{\prime}).\end{array}$

Therefore, $w^{\prime}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(u^{\prime})$, and $w^{\prime\prime}\in
R^{2}_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(u^{\prime})$ implies $w^{\prime\prime}\not\models
M(a_{n+1})$, for every $w^{\prime\prime}\in\mathds{N}$. Since by assumption
$u^{\prime}\not\models p$, we obtain, by ($1$), that $u^{\prime}\models
M(a_{n})$.

We next show that a mark of every world is unique, i.e. for every
$w,n\in\mathds{N}$ and every $j\in\mathds{N}^{+}$,

$None$ $\begin{array}[]{lcl}w\models M(a_{n})&\mbox{implies}&w\not\models
M(a_{n+j}).\end{array}$

Assume $w\models M(a_{n})$. By ($1$), there exists $w^{\prime}\in
R^{j+1}_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}(w)$
such that $w^{\prime}\models M(a_{n+j+1})$. Since $j\geqslant 1$ and
$R_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}$ is
transitive, $w^{\prime}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}^{2}(w)$. Therefore, by ($1$), $w\not\models
M(a_{n+j})$.

We next show that every element $a_{n}$ is tiled at every world marked by some
element $a_{m}$, i.e. that for every $w,m,n\in\mathds{N}$,

$None$ $\begin{array}[]{lcl}w\models M(a_{m})&\mbox{implies}&\mbox{$w\models
P_{t}(a_{n})$, for some $t\in T$.}\end{array}$

We proceed by induction on $m$.

As we have seen, $0\not\models U(a_{0})$, i.e., $0\models P_{t}(a_{0})$, for
some $t\in T$. Since $0\models A_{7}$, for every $n\in\mathds{N}$, there
exists $t\in T$ such that $0\models P_{t}(a_{n})$. Since $0\models A_{5}$, for
every $w,v,m,n\in\mathds{N}$ and every $t\in T$,

$None$ $\begin{array}[]{lcl}\mbox{$w\models M(a_{m})$, $v\models M(a_{m})$ and
$w\models P_{t}(a_{n})$}&\mbox{imply}&\mbox{$v\models
P_{t}(a_{n})$.}\end{array}$

Therefore, ($4$) holds for $m=0$.

Assume ($4$) holds for $m\geqslant 0$ and suppose $w\models M(a_{m+1})$. We
claim that, then, there exists $w^{\prime}$ such that $w^{\prime}<w$ and
$w^{\prime}\models M(a_{m})$. To prove the claim we, first, observe that there
exists $w^{\prime}$ such that $w^{\prime}\not\models p$ and $w\in
R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(w^{\prime})$: otherwise, by ($2$), $w\models
M(a_{0})$, in contradiction with ($3$). Fix the said $w^{\prime}$. We next
show that $w^{\prime\prime}\in R^{2}_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(w^{\prime})$ implies $w^{\prime\prime}\not\models
M(a_{m+1})$. Assume $w^{\prime\prime}\in
R^{2}_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(w^{\prime})$. Then, $w^{\prime\prime}\in
R_{\scriptsize\mbox{$\Diamond$}\hskip 0.70004pt\mbox{$\Diamond$}}(w)$. Since
$w\models M(a_{m+1})$, by ($1$) and ($2$), $w^{\prime\prime}\models
M(a_{m+2})$ and thus, by ($3$), $w^{\prime\prime}\not\models M(a_{m+1})$.
Last, since $w^{\prime}\not\models p$, we obtain, by ($1$), $w^{\prime}\models
M(a_{m})$, thereby proving the claim.

Now, let $n\in\mathds{N}$ be given. By inductive hypothesis, there exists $t$
such that $w^{\prime}\models P_{t}(a_{n})$. Since $0\models A_{8}$, this
implies that $w\models P_{t^{\prime}}(a_{n})$, for some $t^{\prime}\in T$.
Thus, ($4$) is proven.

In view of ($5$), for every $m\in\mathds{N}$, we may pick an arbitrary world
marked by $a_{m}\in D_{0}$ to be part of the sought tiling. For definiteness,
let, for every $m\in\mathds{N}$,

$w_{m}=\min\\{w\in\mathds{N}:w\models M(a_{m})\\}.$

By ($4$), for every $n,m\in\mathds{N}$, there exists $t\in T$ such that
$w_{m}\models P_{t}(a_{n})$; it follows from $0\models A_{6}$ that such $t$ is
unique. We can, therefore, define a function
$f\colon\mathds{N}\times\mathds{N}\to T$ by

$\begin{array}[]{lcl}f(n,m)=t&\mbox{ whenever }&w_{m}\models
P_{t}(a_{n}).\end{array}$

We next show that $f$ satisfies ($T_{1}$) through ($T_{3}$).

Since $0\models A_{7}$, the condition ($T_{1}$) is, evidently, satisfied.

To see that ($T_{2}$) is satisfied, assume $f(n,m)=t$. Then, $w_{m}\models
P_{t}(a_{n})$, by definition of $f$. From the definition of $w_{m}$ we know
that $w_{m}\models M(a_{m})$. Since $0\models A_{8}$, if $v\geqslant w_{m}$
and $v\models M(a_{m+1})$, then $v\models P_{t^{\prime}}(a_{n})$, for some
$t^{\prime}$ with $up(t)=down(t^{\prime})$. We next show that
$w_{m+1}\geqslant w_{m}$. Assume otherwise: let $w_{m+1}<w_{m}$. From the
definition of $w_{m+1}$ we know that $w_{m+1}\models M(a_{m+1})$. Therefore,
by ($2$) and $(3)$, $w_{m}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}(w_{m+1})$. Since $w_{m}\models M(a_{m})$, there
exists, by ($1$), $w^{\prime}\in R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}^{2}(w_{m})$ such that $w^{\prime}\models
M(a_{m+2})$. Since $R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}$ is transitive, $w^{\prime}\in
R_{\scriptsize\mbox{$\Diamond$}\hskip
0.70004pt\mbox{$\Diamond$}}^{2}(w_{m+1})$, in contradiction with the third
clause of ($1$). Thus, we have shown that $w_{m+1}\geqslant w_{m}$. Hence,
$w_{m+1}\models P_{t^{\prime}}(a_{n})$, for some $t^{\prime}$ with
$up(t)=down(t^{\prime})$. Therefore, ($T_{2}$) is satisfied.

It remains to show that ($T_{3}$) is satisfied. Since $0\models M(a_{0})$ and
$0\models A_{9}$, the set $\\{w\in\mathds{N}:w\not\models p\mbox{ and
}w\models P_{t_{0}}(a_{0})\\}$ is infinite. It follows from $0\models
M(a_{0})$, ($1$) and ($2$) that, for every $w\in\mathds{N}$, if $w\not\models
p$, then there exists $m\in\mathds{N}$ such that $w\models M(a_{m})$.
Therefore, by ($5$), the set $\\{w_{m}:m\in\mathds{N}\mbox{ and }w_{m}\models
P_{t_{0}}(a_{0})\\}$ is infinite. Hence, ($T_{3}$) is satisfied.

Thus, $f$ is a required function.

$\vdots$$0$$1$$2$$3$$4$$5$$6$$7$$M(0)$$M(1)$$M(2)$$M(3)$$p$$p$$p$$p$$P_{f(0,0)}(0)$$P_{f(1,0)}(1)$$P_{f(2,0)}(2)$$P_{f(3,0)}(3)$$\ldots$$P_{f(0,1)}(0)$$P_{f(1,1)}(1)$$P_{f(2,1)}(2)$$P_{f(3,1)}(3)$$\ldots$$P_{f(0,2)}(0)$$P_{f(1,2)}(1)$$P_{f(2,2)}(2)$$P_{f(3,2)}(3)$$\ldots$$P_{f(0,3)}(0)$$P_{f(1,3)}(1)$$P_{f(2,3)}(2)$$P_{f(3,3)}(3)$$\ldots$$\vdots$$\vdots$$\vdots$$\vdots$$0$$\lhd$$1$$\lhd$$2$$\lhd$$3$$\ldots$
Figure 1: Model $\mathfrak{M}_{0}$

(‘‘only if’’) Suppose $f$ is a function satisfying ($T_{1}$) through
($T_{3}$). We obtain a model based on $\langle\mathds{N},\leqslant\rangle$
satisfying $A$.

Let $\mathcal{D}=\mathds{N}\cup\\{-1\\}$ and $D(w)=\mathcal{D}$, for every
$w\in\mathds{N}$.

Let $\mathfrak{M}_{0}=\langle\mathds{N},\leqslant,D,I\rangle$ be a model such
that, for every $w\in\mathds{N}$ and every $a,b\in{\cal D}$,

$\begin{array}[]{lcl}\mathfrak{M}_{0},w\models a\triangleleft
b&\leftrightharpoons&\mbox{$w$ is even and $b=a+1$;}\vskip 3.0pt plus 1.0pt
minus 1.0pt\\\ \mathfrak{M}_{0},w\models p&\leftrightharpoons&\mbox{$w$ is
odd;}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ \mathfrak{M}_{0},w\models
M(a)&\leftrightharpoons&\mbox{$w=2a$;}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
\mathfrak{M}_{0},w\models P_{t}(a)&\leftrightharpoons&\mbox{for some
$m\in\mathds{N}$, both $w=2m$ and $f(a,m)=t$.}\end{array}$

It is straightforward to check that $\mathfrak{M}_{0},0\models A$, so we leave
this to the reader. $\Box$

Thus, in the proof of the ‘‘if’’ part of Lemma 3.1, we obtained a grid for the
tiling by treating the worlds of model $\mathfrak{M}$ as rows and elements
$a_{0},a_{1},a_{2},\ldots$ of the domain $D_{0}$ of the world $0$ satisfying
$A$ as columns.

###  3.2 Elimination of the binary predicate letter

We next eliminate, following ideas of Kripke’s [31], the binary predicate
letter $\triangleleft$ of formula $A$, without increasing the number of
individual variables in the resultant formula.

From now on, we assume, for ease of notation, that $A$ contains monadic
predicate letters $P_{0},\ldots,P_{s}$—rather than $P_{t}$, for each
$t\in\\{t_{0},\ldots,t_{s}\\}$—to refer to the tile types.

Recall that Kripke’s construction [31] transforms a model $\mathfrak{M}$
satisfying, at world $w$, a formula containing a binary predicate letter, and
no modal connectives, so that, for every pair of elements of the domain of
$w$, a fresh world accessible from $w$ is introduced to $\mathfrak{M}$. This
construction cannot be applied here in a straightforward manner, for two
reasons.

First, since we are working with the frame
$\langle\mathds{N},\leqslant\rangle$, we may not introduce fresh worlds to a
model satisfying $A$; we, rather, have to use the worlds from $\mathds{N}$ to
simulate $\triangleleft$. Second, since $\triangleleft$ occurs within the
scope of the modal connective in $A$, we need to simulate the interpretation
of $\triangleleft$ not just at the world satisfying $A$, but at every world
accessible from it.

We resolve these difficulties by working with the model $\mathfrak{M}_{0}$
defined in the ‘‘only if’’ part of the proof of Lemma 3.1, rather than with an
arbitrary model satisfying $A$, and relying on $\mathfrak{M}_{0}$ being based
on a frame with a constant domain and on the interpretation of $\triangleleft$
being identical at every world of $\mathfrak{M}_{0}$.

Let $P_{s+1}$ and $P_{s+2}$ be monadic predicate letters distinct from
$M,P_{0},\ldots,P_{s}$ and from each other, and let $\cdot^{\prime}$ be the
function substituting

$\begin{array}[]{lcl}\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}(P_{s+1}(x)\wedge
P_{s+2}(y))&\mbox{for}&x\triangleleft y.\end{array}$

###### Lemma 3.2

There exists a recurrent tiling of $\mathds{N}\times\mathds{N}$ satisfying
($T_{1}$) through ($T_{3}$) if, and only if,
$\langle\mathds{N},\leqslant\rangle\not\models\neg A^{\prime}$.

Proof. (‘‘if’’) Suppose $\mathfrak{M},w_{0}\models A^{\prime}$, for some model
$\mathfrak{M}=\langle\mathds{N},\leqslant,D,I\rangle$ and some world $w_{0}$,
which can be assumed to be $0$.

The argument is essentially the same as in the proof of the ‘‘if’’ part of
Lemma 3.1. The only, inconsequential, difference is that
$\mbox{$\Diamond$}\hskip 1.00006pt\mbox{$\Diamond$}(P_{s+1}(x)\wedge
P_{s+2}(y))$ now plays the role of $x\triangleleft y$: for every
$w\in\mathds{N}$, the relation $I(w,\triangleleft)\subseteq D_{w}\times D_{w}$
is replaced by the relation

$\\{\langle a,b\rangle\in D_{w}\times
D_{w}:\mathfrak{M},w\models\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}(P_{s+1}(a)\wedge P_{s+2}(b))\\}.$

Since $\mathfrak{M},0\models A^{\prime}$, the two relations are
indistinguishable, for every $w\in\mathds{N}$, with respect to the properties
we rely on in the proof.

(‘‘only if’’) Suppose $f$ is a function satisfying ($T_{1}$) through
($T_{3}$). Let $\mathfrak{M}_{0}=\langle\mathds{N},\leqslant,D,I\rangle$ be
the model defined in the ‘‘only if’’ part of the proof of Lemma 3.1. As we
have seen, $\mathfrak{M}_{0},0\models A$. We use $\mathfrak{M}_{0}$ to obtain
a model satisfying $A^{\prime}$.

Let $\alpha$ be the infinite sequence

$0,\,\,0,1,\,\,0,1,2,\,\,0,1,2,3,\,\,0,1,2,3,4,\,\,\ldots$

and let $\alpha_{k}$, for each $k\in\mathds{N}$, be the $k$th element of
$\alpha$.

Let
$\mathfrak{M}^{\prime}_{0}=\langle\mathds{N},\leqslant,D,I^{\prime}\rangle$ be
a model such that, for every $w,c\in\mathds{N}$,

$\begin{array}[]{lcl}\mathfrak{M}^{\prime}_{0},w\models
P_{s+1}(c)&\leftrightharpoons&\mbox{for some $m\in\mathds{N}$, both $w=2m$ and
$c=\alpha_{m}$;}\vskip 6.0pt plus 2.0pt minus 2.0pt\\\
\mathfrak{M}^{\prime}_{0},w\models P_{s+2}(c)&\leftrightharpoons&\mbox{for
some $m\in\mathds{N}$, both $w=2m$ and $c=\alpha_{m}+1$,}\end{array}$

and for every $w\in\mathds{N}$ and every $S\in\\{P_{0},\ldots,P_{s},M,p\\}$,

$\begin{array}[]{lcl}I^{\prime}(w,S)&=&I(w,S).\end{array}$

We show that $\mathfrak{M}^{\prime}_{0},0\models A^{\prime}$.

Since $\mathfrak{M}_{0},0\models A$, it suffices to prove that, for every
$m\in\mathds{N}$ and every $a,b\in\mathcal{D}$,

$\begin{array}[]{lcl}\mathfrak{M}_{0},2m\models a\triangleleft
b&\Longleftrightarrow&\mathfrak{M}^{\prime}_{0},2m\models\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}(P_{s+1}(a)\wedge P_{s+2}(b)).\end{array}$

Assume $\mathfrak{M}_{0},2m\models a\triangleleft b$. Then, $b=a+1$, by
definition of $\mathfrak{M}_{0}$. Choose $k\in\mathds{N}$ so that $k>m$ and
$\alpha_{k}=a$; by definition of $\alpha$, such a number $k$ certainly exists.
By definition of $\mathfrak{M}^{\prime}_{0}$, both
$\mathfrak{M}^{\prime}_{0},2k\not\models p$ and
$\mathfrak{M}^{\prime}_{0},2k\models P_{s+1}(a)\wedge P_{s+2}(b)$. By the same
definition, $\mathfrak{M}^{\prime}_{0},2k-1\models p$. Hence,
$\mathfrak{M}^{\prime}_{0},2m\models\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}(P_{s+1}(a)\wedge P_{s+2}(b))$.

Conversely, assume $\mathfrak{M}^{\prime}_{0},2m\models\mbox{$\Diamond$}\hskip
1.00006pt\mbox{$\Diamond$}(P_{s+1}(a)\wedge P_{s+2}(b))$. Then, for some
$v>2m$, both $\mathfrak{M}^{\prime}_{0},v\not\models p$ and
$\mathfrak{M}^{\prime}_{0},v\models P_{s+1}(a)\wedge P_{s+2}(b)$. By
definition of $\mathfrak{M}^{\prime}_{0}$, we have
$\mathfrak{M}_{0},v\not\models p$; hence $v=2k$, for some $k>m$. Also by
definition of $\mathfrak{M}^{\prime}_{0}$, both $a=\alpha_{k}$ and
$b=\alpha_{k}+1$; hence, $b=a+1$. Therefore, $\mathfrak{M}_{0},2m\models
a\triangleleft b$, by definition of $\mathfrak{M}_{0}$. $\Box$

###  3.3 Elimination of monadic predicate letters

We lastly simulate the occurrences of letters $p,M,P_{0},\ldots,P_{s+2}$ in
$A^{\prime}$ with one monadic and one proposition letter, without increasing
the number of individual variables in the resultant formula.

Let $P$ be a monadic letter distinct from $M,P_{0},\ldots,P_{s+2}$, and let
$q$ be a proposition letter distinct from $p$.

For a formula $\varphi$ in the language containing $P$ and $q$, define

$\begin{array}[]{c}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}\varphi=\Diamond(\forall
x\,P(x)\wedge\Diamond(\neg\forall x\,P(x)\wedge\varphi));\vskip 6.0pt plus
2.0pt minus 2.0pt\\\ \mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{0}\varphi=\varphi;\quad\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+1}\varphi=\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n}\varphi,\mbox{ for every
}n\in\mathds{N}.\end{array}$

Define, for every $n\in\\{0,\ldots,s+2\\}$,

$\begin{array}[]{rcl}\beta_{n}(x)&=&\exists y\,\big{(}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+4}(q\wedge
P(y))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+5}(q\wedge P(y))\,\wedge\\\ &&\phantom{\mu\wedge
P(x)\wedge\exists y\,[}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}(\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+1}(q\wedge
P(y))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+2}(q\wedge P(y))\wedge P(x))\big{)};\vskip 6.0pt
plus 2.0pt minus 2.0pt\\\ \beta_{n}(y)&=&\exists
x\,\big{(}\mbox{$\Diamond$}\hskip 1.60004pt\mbox{$\Diamond$}^{s+4}(q\wedge
P(x))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+5}(q\wedge P(x))\,\wedge\\\ &&\phantom{\mu\wedge
P(y)\wedge\exists x\,[}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}(\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+1}(q\wedge
P(x))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+2}(q\wedge P(x))\wedge P(y))\big{)}.\\\
\end{array}$

Let $\cdot^{\ast}$ be the function replacing

  * •

$P_{n}(x)$ with $\beta_{n}(x)$, for every $n\in\\{0,\ldots,s+2\\}$;

  * •

$P_{n}(y)$ with $\beta_{n}(y)$, for every $n\in\\{0,\ldots,s+2\\}$;

  * •

$M(x)$ with $q\wedge P(x)$;

  * •

$M(y)$ with $q\wedge P(y)$.

Let $A_{i}^{\ast}$, for each $i$ with $0\leqslant i\leqslant 8$ and $i\neq 4$,
be the result of applying the function $\cdot^{\ast}$ to $A^{\prime}_{i}$.
Also, let

$\begin{array}[]{lcl}A_{4}^{\ast}&=&\forall x\forall
y\,\big{(}\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}(\beta_{s+1}(x)\wedge\beta_{s+2}(y))\,\rightarrow\vskip
3.0pt plus 1.0pt minus 1.0pt\\\ &&\phantom{\forall x\forall
y\,(\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}(\beta_{s+1}}\Box(q\wedge
P(x)\leftrightarrow\neg\forall x\,P(x)\wedge\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+4}(q\wedge
P(y))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+5}(q\wedge P(y)))\big{)},\end{array}$

and

$\begin{array}[]{lcl}A^{\ast}_{9}&=&\forall x\,(q\wedge
P(x)\rightarrow\Box\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}\beta_{0}(x)).\end{array}$

Lastly, let $A^{\ast}$ be the conjunction of $A_{0}^{\ast}$ through
$A_{9}^{\ast}$. Observe that $A^{\ast}$ contains only two individual
variables, a monadic letter $P$ and a proposition letter $q$.

We shall show that $A^{\ast}$ is satisfiable if, and only if, there exists a
recurrent tiling satisfying ($T_{1}$) through ($T_{3}$).

$\vdots$$\vdots$$\vdots$$w_{0}$$w_{m}$$w_{m+1}$$v_{m}^{0}$$v_{m}^{1}$$v_{m}^{s}$$v_{m}^{s+1}$$v_{m}^{s+2}$$\bar{w}_{m}$$\bar{v}_{m}^{0}$$\bar{v}_{m}^{1}$$\bar{v}_{m}^{s+1}$$\bar{v}_{m}^{s+2}$$q$$q$$q$$P(0)$$P(m)$$P(m+1)$$\forall
x\,P(x)$$\forall x\,P(x)$$\forall x\,P(x)$$\forall x\,P(x)$$\forall
x\,P(x)$$\beta_{f(0,\,\,0)}(0)$$\beta_{f(1,\,\,0)}(1)$$\beta_{f(2,\,\,0)}(2)$$\beta_{f(3,\,\,0)}(3)$$\ldots$$\beta_{f(0,m)}(0)$$\beta_{f(1,m)}(1)$$\beta_{f(2,m)}(2)$$\beta_{f(3,m)}(3)$$\ldots$$\beta_{f(0,m+1)}(0)$$\beta_{f(1,m+1)}(1)$$\beta_{f(2,m+1)}(2)$$\beta_{f(3,m+1)}(3)$$\ldots$$P(n)\Longleftrightarrow
f(n,m)=t_{0}$$P(n)\Longleftrightarrow f(n,m)=t_{1}$$P(n)\Longleftrightarrow
f(n,m)=t_{s}$$P(\alpha_{m})$$P(\alpha_{m}+1)$ Figure 2: Model
$\mathfrak{M}_{0}^{\ast}$

To obtain a model satisfying $A^{\ast}$, we ‘‘stretch out’’ the model
$\mathfrak{M}^{\prime}_{0}$ defined in the ‘‘only if’’ part of the proof of
Lemma 3.2 to include ‘‘additional’’ worlds whose sole purpose is to simulate
the interpretation of letters $P_{0},\ldots,P_{s+2}$ at worlds of
$\mathfrak{M}^{\prime}_{0}$. We ‘‘insert’’ $s+3$ worlds between worlds $m$ and
$m+1$ to simulate the interpretation of letters $P_{0},\ldots,P_{s+2}$ at $m$.
The interpretation of $P_{n}$, for each $n\in\\{0,\ldots,s+2\\}$, at $m$ is
simulated by the interpretation of letter $P$ at a newly inserted world ‘‘$n$
steps away from’’ $m+1$. To be able to step through the newly defined model,
we also ‘‘insert’’ extra worlds satisfying $\forall x\,P(x)$; these play the
same role the worlds satisfying $p$ played in $\mathfrak{M}^{\prime}_{0}$. The
proposition letter $q$ marks off the ‘‘old’’ worlds from
$\mathfrak{M}^{\prime}_{0}$. The resultant model is depicted in Figure 2,
where $\beta_{f(a,b)}(x)$ stands for $\beta_{n}(x)$, where $n$ is such that
$f(a,b)=t_{n}$.

###### Lemma 3.3

There exists a recurrent tiling of $\mathds{N}\times\mathds{N}$ satisfying
($T_{1}$) through ($T_{3}$) if, and only if,
$\langle\mathds{N},\leqslant\rangle\not\models\neg A^{\ast}$.

Proof. (‘‘if’’) Suppose $\mathfrak{M},w_{0}\models A^{\ast}$, for some model
$\mathfrak{M}=\langle\mathds{N},\leqslant,D,I\rangle$ and some world $w_{0}$,
which can be assumed to be $0$.

The argument is essentially the same as in the proof of the ‘‘if’’ part of
Lemma 3.2, the only difference being that we use

  * •

$\beta_{n}(x)$ instead of $P_{n}(x)$;

  * •

$\beta_{n}(y)$ instead of $P_{n}(y)$;

  * •

$q\wedge P(x)$ instead of $M(x)$;

  * •

$q\wedge P(y)$ instead of $M(y)$.

(‘‘only if’’) Suppose $f$ is a function satisfying ($T_{1}$) through
($T_{3}$). Let
$\mathfrak{M}^{\prime}_{0}=\langle\mathds{N},\leqslant,D,I^{\prime}\rangle$ be
the model defined in the ‘‘only if’’ part of the proof of Lemma 3.2. As we
have seen, $\mathfrak{M}^{\prime}_{0},0\models A^{\prime}$. We use
$\mathfrak{M}^{\prime}_{0}$ to obtain a model satisfying $A^{\ast}$.

We think of the worlds from $\mathds{N}$ as being labeled, in the ascending
order,

$\begin{array}[]{l}w_{0}^{\phantom{i}},\bar{w}_{0}^{\phantom{i}},v^{s+2}_{0},\bar{v}^{s+2}_{0},\ldots,v^{0}_{0},\bar{v}^{0}_{0},\\\
w_{1}^{\phantom{i}},\bar{w}_{1}^{\phantom{i}},v^{s+2}_{1},\bar{v}^{s+2}_{1},\ldots,v^{0}_{1},\bar{v}^{0}_{1},\\\
w_{2}^{\phantom{i}},\bar{w}_{2}^{\phantom{i}},\ldots\,,\end{array}$

i.e., we put $w_{0}=0$, $\bar{w}_{0}^{\phantom{i}}=1$, $v^{s+2}_{0}=2$, etc.

Let $\mathfrak{M}_{0}^{\ast}=\langle\mathds{N},\leqslant,D,I^{\ast}\rangle$ be
a model such that, for every $u\in\mathds{N}$

$\begin{array}[]{lcll}\mathfrak{M}_{0}^{\ast},u\models
q&\leftrightharpoons&\mbox{$u=w_{m}$, for some $m\in\mathds{N}$,}\end{array}$

and for every $u\in\mathds{N}$ and every $a\in\mathcal{D}$, the relation
$\mathfrak{M}_{0}^{\ast},u\models P(a)$ holds if, and only if, one of the
following conditions is satisfied:

  * •

$u=w_{m}$ and $\mathfrak{M}^{\prime}_{0},2m\models M(a)$, for some
$m\in\mathds{N}$;

  * •

$u=v^{n}_{m}$ and $\mathfrak{M}^{\prime}_{0},2m\models P_{n}(a)$, for some
$m\in\mathds{N}$ and some $n\in\\{0,\ldots,s+2\\}$;

  * •

$u=\bar{w}_{m}$, for some $m\in\mathds{N}$;

  * •

$u=\bar{v}^{n}_{m}$, for some $m\in\mathds{N}$ and some
$n\in\\{0,\ldots,s+2\\}$.

Thus, by definition of $\mathfrak{M}^{\ast}_{0}$,

$None$ $\begin{array}[]{lcl}\mathfrak{M}^{\ast}_{0},w_{m}\models q\wedge
P(a)&\Longleftrightarrow&a=m.\end{array}$

We now prove that $\mathfrak{M}_{0}^{\ast},w_{0}\models A^{\ast}$.

First, we show that

$None$ $\begin{array}[]{lcl}\mathfrak{M}^{\ast}_{0},u\models\forall
x\,P(x)&\Longleftrightarrow&u\in\\{\bar{w}_{m}:m\in\mathds{N}\\}\cup\\{\bar{v}^{n}_{m}:m\in\mathds{N},0\leqslant
n\leqslant s+2\\}.\end{array}$

The right-to-left implication is immediate from the definition of
$\mathfrak{M}^{\ast}_{0}$.

For the converse, assume
$u\notin\\{\bar{w}_{m}:m\in\mathds{N}\\}\cup\\{\bar{v}^{n}_{m}:m\in\mathds{N},0\leqslant
n\leqslant s+2\\}$.

We have four cases to consider.

Case $u=w_{m}$: The definition of $\mathfrak{M}^{\ast}_{0}$ implies that
$\mathfrak{M}^{\ast}_{0},w_{m}\not\models P(c)$, for every
$c\in\mathcal{D}-\\{m\\}$. Since $\mathcal{D}-\\{m\\}\neq\varnothing$, we
obtain $\mathfrak{M}^{\ast}_{0},w_{m}\not\models\forall x\,P(x)$.

Case $u=v^{s+1}_{m}$: The definition of $\mathfrak{M}^{\ast}_{0}$ implies that
$\mathfrak{M}^{\ast}_{0},v^{s+1}_{m}\models P(a)$ if, and only if,
$\mathfrak{M}^{\prime}_{0},2m\models P_{s+1}(a)$, which by definition of
$\mathfrak{M}^{\prime}_{0}$, holds if, and only if, $\mathfrak{M}_{0},0\models
a\triangleleft b$ and $\alpha_{m}=a$. Therefore,
$\mathfrak{M}^{\ast}_{0},v^{s+1}_{m}\not\models P(c)$, for every
$c\in\mathcal{D}-\\{\alpha_{m}\\}$. Since
$\mathcal{D}-\\{\alpha_{m}\\}\neq\varnothing$, we obtain
$\mathfrak{M}^{\ast}_{0},v^{s+1}_{m}\not\models\forall x\,P(x)$.

Case $u=v^{s+2}_{m}$: The definition of $\mathfrak{M}^{\ast}_{0}$ implies that
$\mathfrak{M}^{\ast}_{0},v^{s+2}_{m}\models P(a)$ if, and only if,
$\mathfrak{M}^{\prime}_{0},2m\models P_{s+2}(a)$, which by definition of
$\mathfrak{M}^{\prime}_{0}$, holds if, and only if, $a=\alpha_{m}+1$.
Therefore, $\mathfrak{M}^{\ast}_{0},v^{s+2}_{m}\not\models P(c)$, for every
$c\in\mathcal{D}-\\{\alpha_{m}+1\\}$. Since
$\mathcal{D}-\\{\alpha_{m}+1\\}\neq\varnothing$, we obtain
$\mathfrak{M}^{\ast}_{0},v^{s+2}_{m}\not\models\forall x\,P(x)$.

Case $u=v^{n}_{m}$, where $n\in\\{0,\ldots,s\\}$: By definitions of
$\mathfrak{M}^{\ast}_{0}$ and $\mathfrak{M}^{\prime}_{0}$,

$\begin{array}[]{lclcl}\mathfrak{M}^{\ast}_{0},v^{n}_{m}\models
P(a)&\Longleftrightarrow&\mathfrak{M}^{\prime}_{0},2m\models
P_{n}(a)&\Longleftrightarrow&\mathfrak{M}_{0},2m\models P_{n}(a).\end{array}$

The definition of $\mathfrak{M}_{0}$ implies that
$\mathfrak{M}_{0},2m\not\models P_{n}(-1)$. Therefore,
$\mathfrak{M}^{\ast}_{0},v^{n}_{m}\not\models P(-1)$; hence,
$\mathfrak{M}^{\ast}_{0},v^{n}_{m}\not\models\forall x\,P(x)$.

Thus, $\mathfrak{M}^{\ast}_{0},u\not\models\forall x\,P(x)$, and so ($7$) is
proven.

Next, we show that, for every $m\in\mathds{N}$, every $n\in\\{0,\ldots,s+2\\}$
and every $a\in\mathcal{D}$,

$None$
$\begin{array}[]{lcl}\mathfrak{M}_{0}^{\ast},w_{m}\models\beta_{n}(a)&\Longleftrightarrow&\mathfrak{M}^{\prime}_{0},2m\models
P_{n}(a).\end{array}$

First, define a binary relation ${R}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}$ on $\mathds{N}$ by

$\begin{array}[]{lcl}wR_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}v&\leftrightharpoons&v\not\models\forall
x\,P(x)\mbox{ and, for some $u\in\mathds{N}$, both }w\leqslant u\leqslant
v\mbox{ and }u\models\forall x\,P(x).\end{array}$

Now, assume $\mathfrak{M}^{\prime}_{0},2m\models P_{n}(a)$.

By ($6$), $\mathfrak{M}_{0}^{\ast},w_{m+1}\models q\wedge P(m+1)$. By ($7$)
and the definition of $\mathfrak{M}_{0}^{\ast}$,

  * •

$w_{m+1}\in R^{s+4}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(w_{m})-R^{s+5}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(w_{m})$;

  * •

$w_{m}<v^{n}_{m}$;

  * •

$w_{m+1}\in R^{n+1}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(v^{n}_{m})-R^{n+2}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(v^{n}_{m})$;

  * •

$\mathfrak{M}_{0}^{\ast},v^{n}_{m}\models P(a)$.

Therefore, $\mathfrak{M}_{0}^{\ast},w_{m}\models\beta_{n}(a)$.

Conversely, assume $\mathfrak{M}_{0}^{\ast},w_{m}\models\beta_{n}(a)$.

Then,

$\mathfrak{M}_{0}^{\ast},w_{m}\models\exists y\,(\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+4}(q\wedge
P(y))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{s+5}(q\wedge P(y))).$

Hence, there exist $u\in\mathds{N}$ and $b\in\mathcal{D}$ such that

$\mathfrak{M}_{0}^{\ast},u\models q\wedge P(b)\mbox{ and }u\in
R^{s+4}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(w_{m})-R^{s+5}_{\scriptsize\mbox{$\Diamond$}\hskip
1.12003pt\mbox{$\Diamond$}}(w_{m}).$

By definition of $\mathfrak{M}^{\ast}_{0}$ and by ($6$), the only choices for
$u$ and $b$ are, respectively, $w_{m+1}$ and $m+1$. Hence,

$\mathfrak{M}_{0}^{\ast},w_{m}\models\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}(\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+1}(q\wedge
P(m+1))\wedge\neg\mbox{$\Diamond$}\hskip
1.60004pt\mbox{$\Diamond$}^{n+2}(q\wedge P(m+1))\wedge P(a)).$

Thus, by definition of $\mathfrak{M}_{0}^{\ast}$, we obtain
$\mathfrak{M}_{0}^{\ast},v^{n}_{m}\models P(a)$ and, hence,
$\mathfrak{M}^{\prime}_{0},2m\models P_{n}(a)$. Thus, ($8$) is proven.

From ($6$), ($7$) and ($8$), we obtain $\mathfrak{M}_{0}^{\ast},w_{0}\models
A_{i}^{\ast}$, for each $i$ with $0\leqslant i\leqslant 8$ and $i\neq 4$.
Furthermore, based on ($6$), ($7$) and ($8$), it is straightforward to check
that $\mathfrak{M}_{0}^{\ast},w_{0}\models A^{\ast}_{4}$ and
$\mathfrak{M}_{0}^{\ast},w_{0}\models A^{\ast}_{9}$.

Thus, $\mathfrak{M}_{0}^{\ast},w_{0}\models A^{\ast}$. $\Box$

From Lemma 3.3 we immediately obtain the following result:

###### Theorem 3.4

Satisfiability for $\mathbf{L}(\mathds{N},\leqslant)$ is $\Sigma^{1}_{1}$-hard
in languages with two individual variables, one monadic predicate letter and
one proposition letter.

##  4 Logics of discrete linear orders

We now generalise Theorem 3.4 to logics of descrete linear orders other than
$\langle\mathds{N},\leqslant\rangle$.

We first consider logics of frames based on $\mathds{N}$. Let $R$ be a binary
relation on $\mathds{N}$ between $<$ and $\leqslant$. Define

$\begin{array}[]{lcl}\Box^{+}\varphi&=&\varphi\wedge\Box\varphi.\end{array}$

Then, the relation $\leqslant$ is the reflexive closure of $R$ and, hence, it
is the accessibility relation associated with the operator $\Box^{+}$: for
every model $\mathfrak{M}=\langle\mathds{N},R,D,I\rangle$, every
$w\in\mathds{N}$ and every assignment $g$,

$\begin{array}[]{lcl}\mathfrak{M},w\models^{g}\Box^{+}\varphi&\Longleftrightarrow&\mbox{$\mathfrak{M},w^{\prime}\models^{g}\varphi$,
for every $w^{\prime}\in\mathds{N}$ such that $w\leqslant
w^{\prime}$.}\end{array}$

Let $A^{+}$ to be the formula obtained from $A^{\ast}$ by replacing every
occurrence of $\Box$ with an occurrence of $\Box^{+}$. The noted
correspondence between $\Box^{+}$ and $\leqslant$, as well as their connection
with, respectively, $\Box$ and $R$, give us the following analogue of Lemma
3.3:

###### Lemma 4.1

There exists a recurrent tiling of $\mathds{N}\times\mathds{N}$ satisfying
($T_{1}$) through ($T_{3}$) if, and only if,
$\langle\mathds{N},R\rangle\not\models\neg A^{+}$.

From Lemma 4.1, we obtain the analogue of Theorem 3.4 for
$\mathbf{L}(\mathds{N},R)$. Moreover, since none of the arguments made so far
depend on the assumption of properly expanding domains, we obtain the
following generalisation of Theorem 3.4:

###### Theorem 4.2

Let $R$ be a binary relation on $\mathds{N}$ between $<$ and $\leqslant$, and
let $L$ be a logic such that $\mathbf{L}(\mathds{N},R)\subseteq
L\subseteq\mathbf{L}_{c}(\mathds{N},R)$. Then, satisfiability for $L$ is
$\Sigma^{1}_{1}$-hard in languages with two individual variables, one monadic
predicate letter and one proposition letter.

$\vdots$$\vdots$$\vdots$$\vdots$$0$$n-1$$n$$n+1$$n+2$$0$$n-1$$n$$n+1$$n+2$$\mathfrak{G}_{n}$$\mathfrak{H}_{n}$
Figure 3: Frames $\mathfrak{G}_{n}$ and $\mathfrak{H}_{n}$

As we next observe, Theorem 4.2 covers countably many logics, countably many
pairs of which are incompatible. First, note that $\mathbf{L}(\mathds{N},<)$
and $\mathbf{L}(\mathds{N},\leqslant)$ are incompatible. Let

$\begin{array}[]{lcl}Z&=&\Box(\Box p\rightarrow p)\rightarrow(\Diamond\Box
p\rightarrow\Box p);\\\ \mbox{\it ref}&=&\Box p\rightarrow p.\end{array}$

It is well known [23] that $\langle\mathds{N},<\rangle\models Z$, but
$\langle\mathds{N},\leqslant\rangle\not\models Z$; hence,
$\mathbf{L}(\mathds{N},<)\not\subseteq\mathbf{L}(\mathds{N},\leqslant)$. It is
also clear that $\langle\mathds{N},\leqslant\rangle\models\mbox{\it ref}$, but
$\langle\mathds{N},<\rangle\not\models\mbox{\it ref}$; hence, ${\bf
L}(\mathds{N},\leqslant)\not\subseteq{\bf L}(\mathds{N},<)$.

Generalising this observation, we obtain countably many logics, countably many
pairs of which are incompatible. Let

$\begin{array}[]{lcl}\XBox\varphi&=&(q\wedge\Box(\neg
q\rightarrow\varphi))\vee(\neg q\wedge\Box(q\rightarrow\varphi)).\end{array}$

Let $\mathfrak{G}_{n}$ be the irreflexive chain $0,\ldots,n-1$, followed by
the infinite reflexive chain $n,n+1,\ldots\,$, shown in Figure 3 on the left.
Dually, let $\mathfrak{H}_{n}$ be the reflexive chain $0,\ldots,n-1$, followed
by the infinite irreflexive chain $n,n+1,\ldots\,$, shown in Figure 3 on the
right.

We show that ${\bf L}(\mathfrak{G}_{k})\neq{\bf L}(\mathfrak{G}_{m})$ and
${\bf L}(\mathfrak{H}_{k})\neq{\bf L}(\mathfrak{H}_{m})$ provided $k\neq m$.
Indeed, $k>m$ implies
$\mathbf{L}(\mathfrak{G}_{k})\subseteq\mathbf{L}(\mathfrak{G}_{m})$: if
$\mathfrak{G}_{m},s\not\models\varphi$ then
$\mathfrak{G}_{k},s\not\models\varphi$ since $\mathfrak{G}_{m}$ is a generated
subframe of $\mathfrak{G}_{k}$. Also,
$\mathfrak{G}_{n}\models\Box^{n}\mbox{\it ref}$, but
$\mathfrak{G}_{n+1},0\not\models\Box^{n}\mbox{\it ref}$. Hence,
$\mathbf{L}(\mathfrak{G}_{k})\neq\mathbf{L}(\mathfrak{G}_{m})$ if $k\neq m$. A
similar argument, using the formula $\XBox^{n}Z$ to distinguish
$\mathbf{L}(\mathfrak{H}_{n+1})$ from $\mathbf{L}(\mathfrak{H}_{n})$, shows
that $\mathbf{L}(\mathfrak{H}_{k})\neq\mathbf{L}(\mathfrak{H}_{m})$ if $k\neq
m$.

Thus, we have infinitely many logics ${\bf L}(\mathfrak{G}_{n})$ and
infinitely many logics ${\bf L}(\mathfrak{H}_{n})$. Note that, for every
$k,m\in\mathds{N}$, logics ${\bf L}(\mathfrak{G}_{k})$ and ${\bf
L}(\mathfrak{H}_{m})$ are incompatible since, for every $k,m\in\mathds{N}$,
both $\Box^{k+m}\mbox{\it ref}\in{\bf L}(\mathfrak{G}_{k})-{\bf
L}(\mathfrak{H}_{m})$ and $\XBox^{k+m}Z\in{\bf L}(\mathfrak{H}_{m})-{\bf
L}(\mathfrak{G}_{k})$.

From Theorem 4.2, we obtain the following:

###### Corollary 4.3

Satisfiability for ${\mathbf{L}_{c}}(\mathds{N},\leqslant)$,
$\mathbf{L}(\mathds{N},<)$ and ${\mathbf{L}_{c}}(\mathds{N},<)$ is
$\Sigma^{1}_{1}$-hard in languages with two individual variables, one monadic
predicate letter and one proposition letter.

The frame $\langle\mathds{N},<\rangle$ is isomorphic to the structure
$\langle\omega,<\rangle$, where $\omega$ is the least infinite ordinal and
$<$, as for all ordinals, is the membership relation on $\omega$. We next
generalise Theorem 4.2 to logics of frames based on infinite ordinals of a
special form, which include $\omega$.

###### Theorem 4.4

Let $\alpha=\omega\cdot m+k$, for some $m$ with $1\leqslant m<\omega$ and some
$k<\omega$, let $R$ be a binary relation on $\alpha$ between $<$ and its
reflexive closure $\leqslant$, and let $L=\mathbf{L}(\alpha,R)$. Then,
satisfiability for $L$ is $\Sigma^{1}_{1}$-hard in languages with two
individual variables, one monadic predicate letter and one proposition letter.

Proof. The proof is similar to that of Theorem 4.2. We only comment on how to
obtain an analogue of Lemma 3.1, an encoding of the recurrent tiling problem
in $\mathbf{L}(\alpha,\leqslant)$. (For the general case of an arbitrary
relation between $<$ and $\leqslant$, we use $\Box^{+}$ instead of $\Box$.)

Since the frame $\langle\alpha,\leqslant\rangle$ may contain a world that does
not see another world, we need to define a variant of the formula $A_{9}$
suitable for such a situation:

$\begin{array}[]{lcl}A^{\bullet}_{9}&=&\forall
x\,\big{(}(M(x)\rightarrow\Box(\exists
y\,M(y)\rightarrow\mbox{$\Diamond$}\hskip 1.00006pt\mbox{$\Diamond$}(\exists
y\,M(y)\rightarrow P_{t_{0}}(x)))\big{)}.\end{array}$

Let $A^{\bullet}$ be the conjunction of formulas $A_{0}$ through $A_{8}$ from
Section 3, as well as $A^{\bullet}_{9}$. We claim that there exists a
recurrent tiling satisfying ($T_{1}$) through ($T_{3}$) if, and only if,
$\langle\alpha,\leqslant\rangle\not\models\neg A^{\bullet}$.

Assume $\mathfrak{M},u_{0}\models A^{\bullet}$, for some model
$\mathfrak{M}=\langle\alpha,\leqslant,D,I\rangle$ and some world
$u_{0}\in\alpha$. Then, there exists in $\alpha$ a last copy of $\omega$ that
has the following property: it contains a world $w$ marked by an element, say
$a_{k}$, of the sequence
$a_{0}\triangleleft^{I,u_{0}}a_{1}\triangleleft^{I,u_{0}}a_{2}\triangleleft^{I,u_{0}}\ldots\,$
of elements of $D(u_{0})$ whose existence follows from
$\mathfrak{M},u_{0}\models A_{2}$. Then, a tiling can be obtained from the
said copy of $\omega$, similarly to the way it was done in the proof of the
‘‘if’’ part of Lemma 3.1: columns are simulated by elements
$a_{0},a_{1},a_{2},\ldots$ of $D(u_{0})$; rows are simulated by worlds
$w_{k},w_{k+1},w_{k+2},\ldots$ such that

  * •

$w_{k}=w$,

  * •

$w_{k}<w_{k+1}<w_{k+2}<\ldots\,$,

  * •

$w_{k+n}\models M(a_{k+n})$, for every $n\in\mathds{N}$;

and a tiling function $f\colon\mathds{N}\times\mathds{N}\to T$ is defined by

$\begin{array}[]{lcl}f(n,m)=t&\mbox{ whenever }&w_{k+m}\models
P_{t}(a_{n}).\end{array}$

Thus defined $f$ clearly satisfies ($T_{1}$) and ($T_{2}$). Also, since
$\mathfrak{M},u_{0}\models A^{\bullet}_{9}$, the set

$\\{w_{k+m}:m\in\mathds{N}\mbox{ and }w_{k+m}\models P_{t_{0}}(a_{0})\\}$

is infinite; hence, $f$ satisfies ($T_{3}$) and so is a required function.

For the converse, we use the first copy of $\omega$ contained in $\alpha$ for
the satisfaction of $A^{\bullet}$: first, we define the interpretation of all
the letters occurring in $A^{\bullet}$ on the said copy of $\omega$ as in the
proof of the ‘‘only if’’ part of Lemma 3.1; second, we define the
interpretation of letters $p$, $M$, $P_{t}$, for each $t\in T$, and
$\triangleleft$ to be empty at every world not belonging to the said copy of
$\omega$; last, we define $U$ to be an arbitrary non-empty subset of the
domain of every world not belonging to the said copy of $\omega$. Then,
$A^{\bullet}$ is true at the least, with respect to $\leqslant$, world of
$\alpha$; hence, it is satisfiable. $\Box$

##  5 Logics of dense and continuous linear orders

It is not clear whether $\Sigma^{1}_{1}$-hardness results analogous to Theorem
4.4 can be obtained for logics of linear orders distinct from those mentioned
there. Perhaps the most significant logics of linear orders not covered by
Theorem 4.4 are logics of the rationals and the reals with natural partial and
strict orders, i.e. $\mathbf{L}(\mathds{Q},\leqslant)$,
$\mathbf{L}(\mathds{Q},<)$, $\mathbf{L}(\mathds{R},\leqslant)$ and
$\mathbf{L}(\mathds{R},<)$.

The proof of Lemma 3.1 does not carry over to either
$\mathbf{L}(\mathds{Q},\leqslant)$ or $\mathbf{L}(\mathds{R},\leqslant)$ since
we cannot ensure, given a model of the formula $A$ based on either
$\langle\mathds{Q},\leqslant\rangle$ or $\langle\mathds{R},\leqslant\rangle$,
that the tiling defined as in the proof of Lemma 3.1 satisfies $(T_{3})$. In
the case of $\mathbf{L}(\mathds{Q},\leqslant)$, no such tiling exists:
$\mathbf{L}(\mathds{Q},\leqslant)$ is recursively enumerable [13] and hence
$\Sigma^{0}_{1}$-complete. The case of $\mathbf{L}(\mathds{R},\leqslant)$
might turn out to be similar as it is not known whether
$\mathbf{L}(\mathds{R},\leqslant)$ is distinct from
$\mathbf{L}(\mathds{Q},\leqslant)$. (The superintuitionistic logics of
$\langle\mathds{Q},\leqslant\rangle$ and $\langle\mathds{R},\leqslant\rangle$
coincide [54, p. 701] and are $\Sigma^{0}_{1}$-complete [59, Theorem 1]; on
the other hand, the superintuitionistic, and hence modal, logics of predicate
frames with constant domains over $\langle\mathds{Q},\leqslant\rangle$ and
$\langle\mathds{R},\leqslant\rangle$ differ [59, Theorem 2].)

A slight modification of the proof of Lemma 3.1 shows, however, that
satisfiability for $\mathbf{L}(\mathds{Q},\leqslant)$ and
$\mathbf{L}(\mathds{R},\leqslant)$ is $\Pi^{0}_{1}$-hard—hence,
$\mathbf{L}(\mathds{Q},\leqslant)$ and $\mathbf{L}(\mathds{R},\leqslant)$ are
$\Sigma^{0}_{1}$-hard—in languages with two variables, one monadic predicate
letter and one proposition letter: simply leaving out the argument for
($T_{3}$), we obtain a reduction to satisfiability for
$\mathbf{L}(\mathds{Q},\leqslant)$ and $\mathbf{L}(\mathds{R},\leqslant)$ in
appropriate languages of the $\Pi^{0}_{1}$-complete [6], [9, Appendix A.4]
$\mathds{N}\times\mathds{N}$ tiling problem whose solution is required to
satisfy ($T_{1}$) and ($T_{2}$), but not ($T_{3}$). We do, rather, establish a
more general result.

Define $B$ to be the conjunction of formulas $A_{0}$ through $A_{8}$ (i.e.,
leave out $A_{9}$ from the formula $A$ defined in Section 3).

###### Lemma 5.1

Let $\langle W,\leqslant\rangle$ be a partial linear order containing an
infinite ascending chain of pairwise distinct elements of $W$. Then, there
exists a tiling of $\mathds{N}\times\mathds{N}$ satisfying $(T_{1})$ and
$(T_{2})$ if, and only if, $\langle W,\leqslant\rangle\not\models\neg B$.

Proof. (‘‘if’’) The proof is identical to that the ‘‘if’’ part of Lemma 3.1,
except that we leave out the argument for ($T_{3}$).

(‘‘only if’’) Suppose $f$ is a function satisfying ($T_{1}$) and ($T_{2}$). We
obtain a model based on $\langle W,\leqslant\rangle$ satisfying $B$.

Let $D_{w}=\mathds{N}\cup\\{-1\\}$, for every $w\in W$. To define the
interpretation function $I$ on $\langle W,\leqslant,D\rangle$, we use elements
of the infinite ascending chain $w_{0}\leqslant w_{1}\leqslant
w_{2}\leqslant\ldots$ of worlds from $W$ that exists by assumption: we define
$I$ so that, for every $k\in\mathds{N}$ and every $a,b\in\mathcal{D}$,

$\begin{array}[]{lcl}\mathfrak{M},w_{k}\models a\triangleleft
b&\leftrightharpoons&\mbox{$k$ is even and $b=a+1$;}\vskip 3.0pt plus 1.0pt
minus 1.0pt\\\ \mathfrak{M},w_{k}\models p&\leftrightharpoons&\mbox{$k$ is
odd;}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ \mathfrak{M},w_{k}\models
M(a)&\leftrightharpoons&\mbox{$k=2a$;}\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
\mathfrak{M},w_{k}\models P_{t}(a)&\leftrightharpoons&\mbox{$k=2m$ and
$f(a,m)=t$, for some $m\in\mathds{N}$,}\end{array}$

and, for every $v\not\in\\{w_{i}:i\in\mathds{N}\\}$ and every predicate letter
$S$ of $B$,

$I(v,S)=I(w_{m},S),\mbox{ where }m=\min\\{k\in\mathds{N}:v\leqslant w_{k}\\}.$

It is straightforward to check that $\mathfrak{M},w_{0}\models B$, so we leave
this to the reader. $\Box$

Using a modification of the formula $B$ obtained by replacing every occurrence
of $\Box$ by that of $\Box^{+}$, we can prove the following analogue of
Theorem 4.2 (the proof uses Lemma 5.1 in the same way Theorem 4.2 used Lemma
3.1):

###### Theorem 5.2

Let $\langle W,<\rangle$ be a strict linear order containing an infinite
ascending chain of pairwise distinct elements of $W$. Let $\leqslant$ be the
reflexive closure of $<$ and $R$ a binary relation between $<$ and
$\leqslant$. Let $L$ be a logic such that $\mathbf{L}(W,R)\subseteq
L\subseteq\mathbf{L}_{c}(W,R)$. Then, satisfiability for $L$ is
$\Pi^{0}_{1}$-hard—hence, $L$ is $\Sigma^{0}_{1}$-hard—in languages with two
individual variables, one monadic predicate letter and one proposition letter.

###### Corollary 5.3

Logics $\mathbf{L}(\mathds{Q},\leqslant)$,
${\mathbf{L}_{c}}(\mathds{Q},\leqslant)$, $\mathbf{L}(\mathds{Q},<)$,
${\mathbf{L}_{c}}(\mathds{Q},<)$, $\mathbf{L}(\mathds{R},\leqslant)$,
${\mathbf{L}_{c}}(\mathds{R},\leqslant)$, $\mathbf{L}(\mathds{R},<)$ and
${\mathbf{L}_{c}}(\mathds{R},<)$ are $\Sigma^{0}_{1}$-hard in languages with
two individual variables, one monadic predicate letter and one proposition
letter.

Well-known axiomatically defined predicate modal logics coincide with some
logics mentioned in Corollary 5.3. Let $\mathbf{K}$ be the minimal
propositional normal modal logic and, for a set of formulas $\Gamma$ and a
formula $\varphi$, let $\Gamma\oplus\varphi$ be the closure of
$\Gamma\cup\\{\varphi\\}$ under modus ponens, necessitation and propositional
substitution. Recall the following definitions of propositional modal logics:

$\begin{array}[]{lcl}\mathbf{S4.3}&=&\mathbf{K}\oplus\mathit{ref}\oplus\Box
p\rightarrow\Box\Box p\oplus\Box(\Box p\rightarrow q)\vee\Box(\Box
q\rightarrow p);\vskip 3.0pt plus 1.0pt minus 1.0pt\\\
\mathbf{K4.3.D.X}&=&\mathbf{K}\oplus\Box p\rightarrow\Box\Box
p\oplus\Box(\Box^{+}p\rightarrow q)\vee\Box(\Box^{+}q\rightarrow
p)\oplus\Diamond\top\oplus\Box\Box p\rightarrow\Box p.\end{array}$

For a propositional modal logic $L$, denote by $\mathbf{Q}L$ the minimal
predicate modal logic containing $\mathbf{QCl}\cup L$. It follows from the
definitions of $\mathbf{S4.3}$ and $\mathbf{K4.3.D.X}$ given above that logics
$\mathbf{QS4.3}$ and $\mathbf{QK4.3.D.X}$ are finitely axiomatizable and,
hence, recursively enumerable, i.e., they are in $\Sigma^{0}_{1}$.

It is well known [13] that $\mathbf{QS4.3}=\mathbf{L}(\mathds{Q},\leqslant)$
and $\mathbf{QK4.3.D.X}=\mathbf{L}(\mathds{Q},<)$. We, therefore, obtain the
following result:

###### Corollary 5.4

The logics $\mathbf{QS4.3}$ and $\mathbf{QK4.3.D.X}$ are
$\Sigma^{0}_{1}$-complete in languages with two individual variables, one
monadic predicate letter and one proposition letter.

Thus, $\mathbf{L}(\mathds{Q},\leqslant)$ and $\mathbf{L}(\mathds{Q},<)$ are
$\Sigma^{0}_{1}$-complete in languages with two individual variables, one
monadic predicate letter and one proposition letter.

##  6 Some other logics

In this section, we note some corollaries of Theorem 5.2 other than those
mentioned in Corollary 5.3. We also note that a straightforward modification
of the proof of Theorem 5.2 establishes $\Sigma^{0}_{1}$-completeness of the
logic $\mathbf{QK4.3}$ in the languages we consider.

The first corollary concerns logics of infinite ordinals: as before, for
ordinals, by $<$ and $\leqslant$ we mean, respectively, the relation $\in$ and
its reflexive closure.

###### Corollary 6.1

Let $\alpha$ be an infinite ordinal. Then, $\mathbf{L}(\alpha,<)$,
${\mathbf{L}_{c}}(\alpha,<)$, $\mathbf{L}(\alpha,\leqslant)$ and
${\mathbf{L}_{c}}(\alpha,\leqslant)$ are $\Sigma^{0}_{1}$-hard in languages
with two individual variables, one monadic predicate letter and one
proposition letter.

The second concerns logics of non-standard models of the elementary theories
of some of the structures considered thus far (the elementary theory of the
structure $\mathfrak{A}$ is denoted by ${\sf Th}(\mathfrak{A})$):

###### Corollary 6.2

Let $\mathfrak{A}$ be one of the structures
$\langle\mathds{N},{\leqslant}\rangle$, $\langle\mathds{N},{<}\rangle$,
$\langle\mathds{Q},{\leqslant}\rangle$, $\langle\mathds{Q},{<}\rangle$,
$\langle\mathds{R},{\leqslant}\rangle$ and $\langle\mathds{R},{<}\rangle$, and
let $\mathfrak{F}$ be a non-standard classical first-order model of ${\sf
Th}(\mathfrak{A})$. Then, $\mathbf{L}(\mathfrak{F})$ and
${\mathbf{L}_{c}}(\mathfrak{F})$ are $\Sigma^{0}_{1}$-hard in languages with
two individual variables, one monadic predicate letter and one proposition
letter.

Lastly, a slight modification of the argument of Section 5 gives us the
following result on $\mathbf{QK4.3}$, the logic of strict linear orders [13].
We recall that

$\begin{array}[]{lcl}\mathbf{K4.3}&=&\mathbf{K}\oplus\Box p\rightarrow\Box\Box
p\oplus\Box(\Box^{+}p\rightarrow q)\vee\Box(\Box^{+}q\rightarrow
p).\end{array}$

Thus, $\mathbf{QK4.3}$ is finitely axiomatizable and, hence, recursively
enumerable.

###### Corollary 6.3

The logic $\mathbf{QK4.3}$ is $\Sigma^{0}_{1}$-complete in languages with two
individual variables, one monadic predicate letter and one proposition letter.

Proof. One can show that the formula $A^{+}$ defined in Section 4 is
satisfiable in a model based on a $\mathbf{QK4.3}$-frame if, and only if,
there exists a tiling of $\mathds{N}\times\mathds{N}$ satisfying $(T_{1})$ and
$(T_{2})$. We only notice that, in the proof of the ‘‘only if’’ part, we need
to show that the model satisfying $A^{+}$ is infinite—this readily follows by
$A_{1}$, $A_{2}$ and $A^{+}_{4}$. $\Box$

##  7 Discussion

We now discuss some questions arising out of the present work.

The first question is whether our main result, Theorem 4.2, can be
strengthened to languages with two variables and a single monadic predicate
letter: is the ‘‘extra’’ proposition letter necessary?

For the majority of natural predicate modal—and closely related
superintuitionistic—logics similar results have been obtained [46, 49, 51] for
languages with a single monadic predicate letter (the number of variables—two
[46] or three [49, 51]—depends on the logic). Those results do not, however,
cover some notable logics—the known results for the predicate counterparts of
propositional modal logics $\mathbf{GL.3}$, $\mathbf{Grz.3}$ and $\mathbf{S5}$
involve ‘‘extra’’ proposition letters [46, Discussion]. The propositional
modal logics of frames $\langle\mathds{N},\leqslant\rangle$ and
$\langle\mathds{N},<\rangle$—in common with $\mathbf{GL.3}$, $\mathbf{Grz.3}$
and $\mathbf{S5}$—are NP-complete, i.e., not as computationally hard (provided
PSPSACE $\neq$ NP) as PSPACE-hard propositional logics whose first-order
counterparts are known to be undecidable in languages with a few variables and
a single monadic predicate letter. Whether this observation points to a
genuine connection is unclear; the hypothesis, however, seems to be worth
investigating. It seems at least plausible that predicate logics of
$\langle\mathds{N},\leqslant\rangle$ and $\langle\mathds{N},<\rangle$ are
decidable in languages with two variables and a single monadic letter.

We note that a stronger result, $\Sigma^{1}_{1}$-hardness of satisfiability
for languages with two variables and a single monadic letter, is relatively
easily obtainable for the logics of the naturals in the more expressive
language containing, alongside $\Box$, the unary operator $\ocircle$
(‘‘next’’) with the truth condition
$\mathfrak{M},n\models^{g}\ocircle\varphi\mbox{ if
}\mathfrak{M},n+1\models^{g}\varphi$. The resultant logic is a notational
variant of the first-order quantified linear time temporal logic
$\mathbf{QLTL}$ with temporal operators $\Box$ (interpreted as ‘‘always in the
future’’) and $\ocircle$—even without the more expressive binary operator
‘‘until.’’ It is well known [28, Theorem 2] that satisfiability for
$\mathbf{QLTL}(\Box,\ocircle)$ is $\Sigma^{1}_{1}$-hard in languages with two
variables and only monadic predicate letters: the proof, which inspired the
proofs presented above, is a reduction of the recurrent
$\mathds{N}\times\mathds{N}$ tiling problem described in Section 3. Since the
number of tile types in the recurrent tiling problem is unbounded, [28,
Theorem 2] establishes $\Sigma^{1}_{1}$-hardness for languages with an
unlimited supply of monadic predicate letters. The proof of [28, Theorem 2]
can, however, be modified to establish $\Sigma^{1}_{1}$-hardness for languages
with a single monadic predicate letter. Perhasps the easiest way is to modify
the formulas used in the original proof [28] so that the satisfying model has
equal-seized gaps (non-empty sequences of worlds) between the worlds
corresponding to the tiling; the size of the gaps is proportional to the
number of tile types. The binary letter can then be modelled as in the proof
of Lemma 3.2 above. To model all the monadic letters with a single one, we use
the following observation. If $f$ is a tiling function satisfying ($T_{1}$)
through ($T_{3}$), then for every $m\in\mathds{N}$, there do not exist
$t,t^{\prime}\in T$ such that $t\neq t^{\prime}$ and, for every
$n\in\mathds{N}$, both $f(n,m)=t$ and $f(n,m)=t^{\prime}$: an entire row
cannot be tiled simultaneously with tiles of two distinct types. Therefore, a
construction similar to the one used in the proof of Lemma 3.3 above would not
produce a model where two successive worlds satisfy $\forall x\,P(x)$. Hence,
we can use $\ocircle\forall x\,P(x)\wedge{\ocircle}{\ocircle}\forall x\,P(x)$
in place of the proposition letter $q$ in the final reduction. This gives us
the following result:

###### Theorem 7.1

Satisfiability for $\mathbf{QLTL}(\Box,\ocircle)$ is $\Sigma^{1}_{1}$-hard in
languages with two individual variables and a single monadic predicate letter.

The second question arising out of the present work is whether stronger lower
bounds are obtainable for the logics of the reals—provided they are distinct
from the logics of the rationals. One approach would be to attempt to adapt
techniques developed by Reynolds and Zakharyaschev [40] for proving
$\Sigma^{1}_{1}$-hardness of products of two propositional modal logics of
linearly ordered frames. In particular, Reynolds and Zakharyaschev establish
[40, Theorem 6.1] $\Sigma^{1}_{1}$-hardness of product logics satisfying two
conditions: first, the product logic admits a frame with infinite ascending
chains along both accessibility relations; second, the order relation
associated with one of the factor logics is Dedekind complete. Even though
this setup appears similar to predicate modal logics of the reals, it is not
immediately clear how to apply the techniques of Reynolds and Zakharyaschev
[40] in our circumstances since it is not obvious how an infinite linear
partial or strict order, which has to be transitive, can be defined on domains
of a predicate Kripke model using formulas with only two variables.

The third question is whether our results are tight. We are not aware of
upper-bound results for logics considered here, the exception being the logics
of the rationals, which are, as mentioned in Section 5,
$\Sigma^{0}_{1}$-complete. Thus, a search for upper bounds appears to be an
interesting topic of future study.

The final question we mention is whether analogous results can be obtained for
superintuitionistic logic of $\langle\mathds{N},\leqslant\rangle$. Whether
this can be done is unclear to us: the techniques used here appear unsuitable
for superintuitionistic logics given the difficulty of modelling the changing
values of tile types on a linear frame with a hereditary valuation.

## Acknowledgements

We are grateful to Valentin Shehtman for discussions of an earlier version of
the paper. We are indebted to the anonymous reviewers for helping to improve
the paper.

## References

  * [1] Martin Abadi.  The power of temporal proofs.  Theoretical Computer Science, 65(1):35–83, 1989.
  * [2] H. Andréka, I. Németi, and I. Sain.  Completeness problems in verification of programs and program schemes.  In J. Bečvář, editor, Mathematical Foundations of Computer Science 1979. MFCS 1979., volume 74 of Lecture Notes in Computer Science. Springer, 1979.
  * [3] Sergei Artemov and Giorgie Dzhaparidze.  Finite Kripke models and predicate logics of provability.  The Journal of Symbolic Logic, 55(3):1090–1098, 1990.
  * [4] H. Behmann.  Beiträige zür Algebra der Logik, inbesondere zum Entscheidungsproblem.  Mathematische Annalen, 86:163–229, 1922.
  * [5] Johan Van Benthem.  Modal Logic and Classical Logic.  Bibliopolis, 1985.
  * [6] Robert Berger.  The Undecidability of the Domino Problem, volume 66 of Memoirs of AMS.  AMS, 1966.
  * [7] Patrick Blackburn, Maarten de Rijke, and Yde Venema.  Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2001.
  * [8] Patrick Blackburn and Edith Spaan.  A modal perspective on the computational complexity of attribute value grammar.  Journal of Logic, Language, and Information, 2:129–169, 1993.
  * [9] Egon Börger, Erich Grädel, and Yuri Gurevich.  The Classical Decision Problem.  Springer, 1997.
  * [10] Torben Braüner and Silvio Ghilardi.  First-order modal logic.  In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 549–620. Elsevier, 2007.
  * [11] Alexander Chagrov and Mikhail Rybakov.  Standard translations of non-classical formulas and relative decidability of logics.  In Annals of the research seminar of the Center for Logic of the Institute of Philosophy of the Russian Academy of Sciences, volume XIV, pages 81–98. Russian Academy of Sciences, 2000.  In Russian.
  * [12] Alexander Chagrov and Mikhail Rybakov.  How many variables does one need to prove PSPACE-hardness of modal logics?  In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, Advances in Modal Logic 4, pages 71–82. King’s College Publications, 2003.
  * [13] Giovanna Corsi.  Quantified modal logics of positive rational numbers and some related systems.  Notre Dame Journal of Formal Logic, 34(2):263–283, 1993.
  * [14] Calvin C. Elgot.  Decision problems of finite automata design and related arithmetics.  Transactions of the American Mathematical Society, 98(1):21—51, 1961.
  * [15] Melvin Fitting and Richard L. Mendelsohn.  First-Order Modal Logic, volume 277 of Synthese Library.  Kluwer Academic Publishers, 1998.
  * [16] Dov Gabbay.  Semantical Investigations in Heyting’s Intuitionistic Logic.  D. Reidel, 1981.
  * [17] Dov Gabbay, Ian Hodkinson, and Mark Reynolds.  Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, volume 28 of Oxford Logic Guides.  Oxford University Press, 1994.
  * [18] Dov Gabbay, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev.  Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 2003.
  * [19] Dov Gabbay and Valentin Shehtman.  Undecidability of modal and intermediate first-order logics with two individual variables.  The Journal of Symbolic Logic, 58(3):800–823, 1993.
  * [20] Dov Gabbay and Valentin Shehtman.  Products of modal logics, Part 1.  Logic Journal of the IGPL, 6(1):73–146, 1998.
  * [21] Dov Gabbay, Valentin Shehtman, and Dmitrij Skvortsov.  Quantification in Nonclassical Logic, Volume 1, volume 153 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 2009.
  * [22] James W. Garson.  Quantification in modal logic.  In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, vol. 3, pages 267–323. Springer, Dordrecht, 2001.
  * [23] Robert Goldblatt.  Logics of Time and Computation, volume 7 of CSLI Lecture Notes.  Center for the Study of Language and Information, second edition, 1992\.
  * [24] Robert Goldblatt.  Quantifiers, Propositions and Identity: Admissible Semantics for Quantified Modal and Substructural Logics.  Lecture Notes in Logic. Cambridge University Press, 2011.
  * [25] Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi.  On the decision problem for two-variable first-order logic.  Bulletin of Symbolic Logic, 3(1):53–69, 1997.
  * [26] Joseph Y. Halpern.  The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic.  Artificial Intelligence, 75(2):361–372, 1995.
  * [27] David Harel.  Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness.  Journal of the ACM, 33(224–248), 1986.
  * [28] Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev.  Decidable fragments of first-order temporal logics.  Annals of Pure and Applied Logic, 106:85–134, 2000.
  * [29] G. E. Hughes and M. J. Cresswell.  A New Introduction to Modal Logic.  Routledge, 1996.
  * [30] Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev.  Undecidability of first-order intuitionistic and modal logics with two variables.  Bulletin of Symbolic Logic, 11(3):428–438, 2005.
  * [31] Saul Kripke.  The undecidability of monadic modal quantification theory.  Zeitschrift für Matematische Logik und Grundlagen der Mathematik, 8:113–116, 1962.
  * [32] Leopold Löwenheim.  Über Möglichkeiten im Relativkalkül.  Mathematische Annalen, 76(4):447–470, 1915.
  * [33] Maarten Marx.  Complexity of products of modal logics.  Journal of Logic and Computation, 9(2):197–214, 1999.
  * [34] Sergei Maslov, Gregory Mints, and Vladimir Orevkov.  Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables.  Soviet Mathematics Doklady, 6:918–920, 1965.
  * [35] Stephan Merz.  Decidability and incompleteness results for first-order temporal logics of linear time.  Journal of Applied Non-Classical Logics, 2(2):139–156, 1992.
  * [36] Gregory Mints.  Some calculi of modal logic.  Trudy Matematicheskogo Instituta imeni V. A. Steklova, 98:88–111, 1968.  in Russian.
  * [37] Michael Mortimer.  On languages with two variables.  Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, pages 135–140, 1975.
  * [38] Hiroakira Ono.  On some intuitionistic modal logics.  Publications of the Research Institute for Mathematical Sciences, 13(3):687–722, 1977.
  * [39] Arthur Prior.  Past, Present, and Future.  Oxford University Press, 1967.
  * [40] Mark Reynolds and Michael Zakharyaschev.  On the products of linear modal logics.  Journal of Logic and Computation, 11(6):909–931, 2001.
  * [41] Hartley Rogers.  Theory of Recursive Functions and Effective Computability.  McGraw-Hill, 1967.
  * [42] Mikhail Rybakov and Dmitry Shkatov.  Complexity and expressivity of propositional dynamic logics with finitely many variables.  Logic Journal of the IGPL, 26(5):539–547, 2018.
  * [43] Mikhail Rybakov and Dmitry Shkatov.  A recursively enumerable Kripke complete first-order logic not complete with respect to a first-order definable class of frames.  In G. Metcalfe G. Bezhanishvili, G. D’Agostino and T. Studer, editors, Advances in Modal Logic, volume 12, pages 531–540. College Publications, 2018.
  * [44] Mikhail Rybakov and Dmitry Shkatov.  Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables.  In B. Fischer B. and T. Uustalu, editors, Theoretical Aspects of Computing–ICTAC 2018, volume 11187 of Lecture Notes in Computer Science, pages 396–414, 2018.
  * [45] Mikhail Rybakov and Dmitry Shkatov.  Complexity of finite-variable fragments of propositional modal logics of symmetric frames.  Logic Journal of the IGPL, 27(1):60–68, 2019.
  * [46] Mikhail Rybakov and Dmitry Shkatov.  Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter.  Studia Logica, 107(4):695–717, 2019.
  * [47] Mikhail Rybakov and Dmitry Shkatov.  Recursive enumerability and elementary frame definability in predicate modal logic.  Journal of Logic and Computation, 30(2):549–560, 2020.
  * [48] Mikhail Rybakov and Dmitry Shkatov.  Algorithmic properties of first-order modal logics of the natural number line in restricted languages.  In Nicola Olivetti, Rineke Verbrugge, Sara Negri, and Gabriel Sandu, editors, Advances in Modal Logic, volume 13, pages 523–539. College Publications, 2020\.
  * [49] Mikhail Rybakov and Dmitry Shkatov.  Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages.  Journal of Logic and Computation, 30(7):1305–1329, 2020.
  * [50] Mikhail Rybakov and Dmitry Shkatov.  Complexity of finite-variable fragments of products with K.  Journal of Logic and Computation, 31(2):426–443, 2021.
  * [51] Mikhail Rybakov and Dmitry Shkatov.  Algorithmic properties of first-order superintuitionistic logics of finite Kripke frames in restricted languages.  Journal of Logic and Computation, 31(2):494–522, 2021.
  * [52] Valentin Shehtman and Dmitry Shkatov.  On one-variable fragments of modal predicate logics.  In Proceedings of SYSMICS2019, pages 129–132. Institute for Logic, Language and Computation, University of Amsterdam, 2019.
  * [53] Valentin Shehtman and Dmitrij Skvortsov.  Semantics of non-classical first order predicate logics.  In P. Petkov, editor, Mathematical Logic, pages 105–116. Plenum Press, New York, 1990.
  * [54] Dmitrij Skvortsov.  A remark on superintuitionistic predicate logics of Kripke frames with constant and with nested domains.  Journal of Logic and Computation, 21(4):697–713, 2009.
  * [55] Dmitrij Skvortsov and Valentin Shehtman.  Maximal Kripke-type semantics for modal and superintuitionistic predicate logics.  Annals of Pure and Applied Logic, 63(1):69–101, 1993.
  * [56] Edith Spaan.  Complexity of Modal Logics.  PhD thesis, University of Amsterdam, 1993.
  * [57] Andrzej Szalas.  Concerning the semantic consequence relation in first-order temporal logic.  Theoretical Computer Science, 47:329–334, 1986.
  * [58] Andrzej Szalas and Leszek Holenderski.  Incompleteness of first-order temporal logic with until.  Theoretical Computer Science, 57:317–325, 1988.
  * [59] Mitio Takano.  Ordered sets R and Q as bases of Kripke models.  Studia Logica, 46:137–148, 1987.
  * [60] Frank Wolter.  First order common knowledge logics.  Studia Logica, 65:249–271, 2000.
  * [61] Frank Wolter and Michael Zakharyaschev.  Decidable fragments of first-order modal logics.  The Journal of Symbolic Logic, 66:1415–1438, 2001.