1522 LABEL:LastPageJan. 09, 2019Apr. 11, 2019 Theory of computation $\to$
Modal and temporal logics; Complexity theory and logic;

*This article is an extension of the conference publication [Lüc18b].

# Canonical Models and the
Complexity of Modal Team Logic

Martin Lück  Leibniz Universität Hannover, Institut für Theoretische
Informatik, Appelstraße 4, 30167 Hannover<EMAIL_ADDRESS>
###### Abstract.

We study modal team logic MTL, the team-semantical extension of modal logic ML
closed under Boolean negation. Its fragments, such as modal dependence,
independence, and inclusion logic, are well-understood. However, due to the
unrestricted Boolean negation, the satisfiability problem of full MTL has been
notoriously resistant to a complexity theoretical classification.

In our approach, we introduce the notion of canonical models into the team-
semantical setting. By construction of such a model, we reduce the
satisfiability problem of MTL to simple model checking. Afterwards, we show
that this approach is optimal in the sense that MTL-formulas can efficiently
enforce canonicity.

Furthermore, to capture these results in terms of complexity, we introduce a
non-elementary complexity class, TOWER(poly), and prove that it contains
satisfiability and validity of MTL as complete problems. We also prove that
the fragments of MTL with bounded modal depth are complete for the levels of
the elementary hierarchy (with polynomially many alternations). The respective
hardness results hold for both strict or lax semantics of the modal operators
and the splitting disjunction, and also over the class of reflexive and
transitive frames.

###### Key words and phrases:

team semantics, modal logic, complexity, satisfiability

##  1\. Introduction

It is well-known that non-linear quantifier dependencies, such as $w$
depending only on $z$ in the sentence $\forall x\,\exists y\,\forall
z\,\exists w\,\varphi$, cannot be expressed in first-order logic. To overcome
this restriction, logics of incomplete information such as _independence-
friendly logic_ [HS89] have been studied. Later, Hodges [Hod97] introduced
_team semantics_ to provide these logics with a compositional interpretation.
The fundamental idea is to not consider single assignments to free variables,
but instead whole sets of assignments, called _teams_.

In this vein, Väänänen [Vää07] expressed non-linear quantifier dependencies by
the _dependence atom_ ${=\\!\\!(x_{1},\ldots,x_{n},y)}$, which intuitively
states that the values of $y$ in the team functionally depend on those of
$x_{1},\ldots,x_{n}$. Logics with numerous other non-classical atoms such as
_independence_ $\perp$ [GV13], _inclusion_ $\subseteq$ and _exclusion_ $\mid$
[Gal12] have been studied since, and manifold connections to scientific areas
such as statistics, database theory, physics, cryptography and social choice
theory have emerged (see also Abramsky et al. [AKVV16]).

Team semantics have also been adapted to a range of propositional [YV16,
HKLV16], modal [Vää08], and temporal logics [KMV15, KMVZ18]. Besides
_propositional dependence logic_ $\mathsf{PDL}\xspace$ [YV16] and _modal
dependence logic_ $\mathsf{MDL}\xspace$ [Vää08], also propositional and modal
logics of independence and inclusion have been studied [KMSV17, HKVV15, HS15,
Han17]. Unlike in the first-order setting, the atoms such as the dependence
atom range over flat formulas. For example, the instance
${=\\!\\!(p_{1},\ldots,p_{n},\Diamond\mathsf{unsafe})}$ of a modal dependence
atom may specify that the reachability of an unsafe state is a function of
$p_{1}\cdots p_{n}$, but instead of exhibiting the explicit function, the atom
only stipulates its existence.

Most team logics lack the Boolean negation, and adding it as a connective
${\sim}$ usually increases both the expressive power and the complexity
tremendously. The respective extensions of propositional and modal logic are
called _propositional team logic_ $\mathsf{PTL}\xspace$ [HKLV16, YV17, HKVV18]
and _modal team logic_ $\mathsf{MTL}\xspace$ [Mül14, KMSV15]. With ${\sim}$,
these logics can express all the non-classical atoms mentioned above, and in
fact are expressively complete for their respective class of models [KMSV15,
YV17]. For these reasons, they are both interesting and natural logics.

The expressive power of $\mathsf{MTL}\xspace$ is well-understood [KMSV15], and
a complete axiomatization was presented by the author [Lüc18a]. Yet the
complexity of the satisfiability problem has been an open question [Mül14,
KMSV15, DKV16, HKMV17]. Recently, certain fragments of $\mathsf{MTL}\xspace$
with restricted negation were shown
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$-complete
using the well-known filtration method [Lüc17]. In the same paper, however, it
was shown that no elementary upper bound for full $\mathsf{MTL}\xspace$ can be
established by the same approach, whereas the best known lower bound is
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$-hardness,
inherited from propositional team logic [HKVV18].

Logic | Satisfiability | Validity | References
---|---|---|---
$\mathsf{PDL}\xspace$ | $\mathrm{NP}\xspace$ | $\mathrm{NEXPTIME}\xspace$ | [LV13, Vir17]
$\mathsf{MDL}\xspace$ | $\mathrm{NEXPTIME}\xspace$ | $\mathrm{NEXPTIME}\xspace$ | [Sev09, Han17]
$\mathsf{PIL}\xspace$ | $\mathrm{NP}\xspace$ | $\mathrm{NEXPTIME}\xspace\text{-hard},\text{in }\Uppi^{E}_{2}$ | [HKVV15]
$\mathsf{MIL}\xspace$ | $\mathrm{NEXPTIME}\xspace$ | $\Uppi^{E}_{2}\text{-hard}$ | [KMSV17, Han16]
$\mathsf{PInc}\xspace$ | $\mathrm{EXPTIME}\xspace$ | $\text{co-}\mathrm{NP}\xspace$ | [HKVV15]
$\mathsf{MInc}\xspace$ | $\mathrm{EXPTIME}\xspace$ | $\text{co-}\mathrm{NEXPTIME}\xspace\text{-hard}$ | [HKMV15]
$\mathsf{PTL}\xspace$ | $\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$ | $\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$ | [HKLV16, HKVV18]
$\mathsf{MTL}\xspace_{k}$ | $\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$ | $\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$ | Theorem 31
$\mathsf{MTL}\xspace$ | $\mathrm{TOWER}\xspace(\mathrm{poly})$ | $\mathrm{TOWER}\xspace(\mathrm{poly})$ | Theorem 31

Table 1. Complexity landscape of propositional and modal logics of dependence
($*\mathsf{D}\mathsf{L}$), independence ($*\mathsf{IL}$), inclusion
($*\mathsf{Inc}$) and team logic ($*\mathsf{TL}$). Entries are completeness
results unless stated otherwise.

Contribution. We show that $\mathsf{MTL}\xspace$ is complete for a non-
elementary class we call $\mathrm{TOWER}\xspace(\mathrm{poly})$, which
contains the problems decidable in a runtime that is a tower of nested
exponentials of polynomial height. Likewise, we show that the fragments
$\mathsf{MTL}\xspace_{k}$ of bounded modal depth $k$ are complete for classes
we call
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$
and which corresponds to $(k+1)$-fold exponential runtime and polynomially
many alternations. These results fill a long-standing gap in the active field
of propositional and modal team logics (see Table 1).

In our approach, we consider so-called _canonical models_. Loosely speaking, a
canonical model satisfies every satisfiable formula in some of its submodels,
and such models have been long known for, e.g., many systems of modal logic
[BRV01]. In Section 4, we adapt this notion for modal logics with team
semantics, and prove that such models exist for $\mathsf{MTL}\xspace$. This
enables us to reduce the satisfiability problem to simple model checking,
albeit on models that are of non-elementary size with respect to
${|\nobreak\Phi\nobreak|}+k$, where $\Phi$ are the available propositional
variables and $k$ is a bound on the modal depth.

Nonetheless, this approach is essentially optimal: In Section 5 and 6, we show
that $\mathsf{MTL}\xspace$ can, in a certain sense, _efficiently enforce_
canonical models, that is, with formulas that are of size polynomial in
${|\nobreak\Phi\nobreak|}+k$. In this vein, we then obtain the matching
complexity lower bounds in Section 7 and 8, where we encode computations of
non-elementary length in such large models.

Finally, in Section 9 we extend the preliminary version of this paper [Lüc18b]
and consider restrictions of $\mathsf{MTL}\xspace$ to specific frame classes,
and to so-called _strict_ team-semantical connectives.

##  2\. Preliminaries

The length of (the encoding of) $x$ is denoted by ${|\nobreak x\nobreak|}$. We
assume the reader to be familiar with alternating Turing machines [CKS81] and
basic complexity theory. When a problem is hard or complete for a complexity
class, in this paper we are always referring to logspace reductions.

The class
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$ (also
known as $\mathrm{AEXPTIME}\xspace(\mathrm{poly})$) contains the problems
decidable by an alternating Turing machine in time $2^{p(n)}$ with $p(n)$
alternations, where $p$ is a polynomial. We generalize it to capture the
_elementary hierarchy_ as follows.

Let $\exp_{0}(n)\vcentcolon=n$ and $\exp_{k+1}(n)\vcentcolon=2^{\exp_{k}(n)}$.
A function $f\colon\mathbb{N}\xspace\to\mathbb{N}\xspace$ is _elementary_ if
it is computable in time ${\mathcal{O}(\exp_{k}(n))}$ for some fixed $k$. In
this paper, we consider the elementary hierarchy with polynomially many
alternations:

For $k\geq 0$,
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k},\mathrm{poly})$ is
the class of problems decidable by an alternating Turing machine with at most
$p(n)$ alternations and runtime at most $\exp_{k}(p(n))$, for a polynomial
$p$. Note that setting $k=0$ or $k=1$ yields the classes
$\mathrm{PSPACE}\xspace$ and
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$,
respectively [CKS81]. Schmitz [Sch16] proposed the following non-elementary
class that contains
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k},\mathrm{poly})$ for
all $k$. [[Sch16]] $\mathrm{TOWER}\xspace$ is the class of problems decidable
by a deterministic Turing machine in time (or equivalently, space)
$\exp_{f(n)}(1)$ for an elementary function $f$.

A suitable notion of reduction for this class is the following: An _elementary
reduction_ from $A$ to $B$ is an elementary function $f$ such that $x\in
A\Leftrightarrow f(x)\in B$. $A\leq^{\mathrm{elem}}_{\mathrm{m}}B$ means that
there exists an elementary reduction from $A$ to $B$.

[[Sch16]] $\mathrm{TOWER}\xspace$ is closed under
$\leq^{\mathrm{elem}}_{\mathrm{m}}$.

The next class results from imposing a polynomial bound on the number of
exponentials in the definition of $\mathrm{TOWER}\xspace$, which leads to a
strict subclass. $\mathrm{TOWER}\xspace(\mathrm{poly})$ is the class of
problems that are decided by a deterministic Turing machine in time (or
equivalently, space) $\exp_{p(n)}(1)$ for some polynomial $p$.

The reader may verify that both
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k},\mathrm{poly})$ and
$\mathrm{TOWER}\xspace(\mathrm{poly})$ are closed under
$\leq^{\mathrm{P}}_{\mathrm{m}}$ and $\leq^{\log}_{\mathrm{m}}$. Furthermore,
by the time hierarchy theorem,
$\mathrm{TOWER}\xspace(\mathrm{poly})\subsetneq\mathrm{TOWER}\xspace$.

To the author’s best knowledge, neither has been explicitly considered before.
However, candidates for natural complete problems exist. Although not proved
complete, several problems in $\mathrm{TOWER}\xspace(\mathrm{poly})$ are
provably non-elementary, such as the satisfiability problem of separated
first-order logic [Voi17], the equivalence problem for star-free expressions
[SM73], or the first-order theory of finite trees [CH90], to only name a few.
We refer the reader also to the survey of Meyer [Mey74].

Another example is the two-variable fragment of first-order team logic,
$\mathsf{FO}\xspace^{2}({\sim})$. It is related to $\mathsf{MTL}\xspace$ in
the same fashion as classical two-variable logic $\mathsf{FO}\xspace^{2}$ to
$\mathsf{ML}\xspace$. By reduction from $\mathsf{MTL}\xspace$ to
$\mathsf{FO}\xspace^{2}({\sim})$, the satisfiability problem of
$\mathsf{FO}\xspace^{2}({\sim})$ is
$\mathrm{TOWER}\xspace(\mathrm{poly})$-complete problems as a corollary of our
main result, Theorem 31, while its fragments
$\mathsf{FO}\xspace^{2}_{k}({\sim})$ of bounded quantifier rank $k$ are
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$-hard
[Lüc18c].

Next, we justify why we use only $\leq^{\log}_{\mathrm{m}}$-reductions (or
polynomial time reductions in general) in this paper instead of
$\leq^{\mathrm{elem}}_{\mathrm{m}}$.

######  Proposition 1.

Every problem that is $\leq^{\mathrm{elem}}_{\mathrm{m}}$-complete for
$\mathrm{TOWER}\xspace(\mathrm{poly})$ is also
$\leq^{\mathrm{elem}}_{\mathrm{m}}$-complete for $\mathrm{TOWER}\xspace$.

######  Proof 2.1.

Clearly, $\mathrm{TOWER}\xspace(\mathrm{poly})\subseteq\mathrm{TOWER}\xspace$.
For the lower bound, let $A$ be $\leq^{\mathrm{elem}}_{\mathrm{m}}$-complete
for $\mathrm{TOWER}\xspace(\mathrm{poly})$, and let
$B\in\mathrm{TOWER}\xspace$ be arbitrary. $B$ is decidable in time
$\exp_{r(n)}(1)$ for some elementary $r$. Define the set
$C\vcentcolon=\\{x\\#0^{r({|\nobreak x\nobreak|})}\mid x\in B\\}$. First, we
show that $C\in\mathrm{TOWER}\xspace(\mathrm{poly})$. Consider the algorithm
that first checks if the input $z$ is of the form $x\\#0^{*}$, computes
$r({|\nobreak x\nobreak|})$ in elementary time, checks whether
$z=x\\#0^{r({|\nobreak x\nobreak|})}$, and then whether $x\in B$. The first
two steps clearly take elementary time in $n$, where $n\vcentcolon={|\nobreak
x\\#0^{r({|\nobreak x\nobreak|})}\nobreak|}$, and the final step runs in time
$\exp_{r({|\nobreak x\nobreak|})}(1)\leq\exp_{n}(1)$.

By assumption, $C\leq^{\mathrm{elem}}_{\mathrm{m}}A$ via an elementary
reduction $f$. But clearly also $B\leq^{\mathrm{elem}}_{\mathrm{m}}C$ by the
elementary reduction $g\colon x\mapsto x\\#0^{r({|\nobreak x\nobreak|})}$. As
a consequence, the function $h\vcentcolon=f\circ g$ is a reduction from $B$ to
$A$. $h$ is computable in time
$\exp_{k_{1}}(\exp_{k_{2}}(n))=\exp_{k_{1}+k_{2}}(n)$ for fixed
$k_{1},k_{2}\geq 0$ depending on $f$ and $g$, and hence again elementary.

######  Corollary 2.

$\mathrm{TOWER}\xspace(\mathrm{poly})$ is not closed under
$\leq^{\mathrm{elem}}_{\mathrm{m}}$-reductions.

######  Proof 2.2.

Suppose $\mathrm{TOWER}\xspace(\mathrm{poly})$ is closed under
$\leq^{\mathrm{elem}}_{\mathrm{m}}$-reductions, and let $A$ be any problem
complete for $\mathrm{TOWER}\xspace(\mathrm{poly})$ (such $A$ exists; see also
our main result, Theorem 31). By the previous proposition, then
$\mathrm{TOWER}\xspace\subseteq\mathrm{TOWER}\xspace(\mathrm{poly})$,
contradiction.

##  3\. Modal team logic

We fix a countably infinite set $\mathcal{PS}$ of propositional symbols.
_Modal team logic_ $\mathsf{MTL}\xspace$, introduced by Müller [Mül14],
extends classical modal logic $\mathsf{ML}\xspace$. Formulas of classical
$\mathsf{ML}\xspace$ are built following the grammar

$\displaystyle\alpha$
$\displaystyle\vcentcolon\vcentcolon=\neg\alpha\mid\alpha\land\alpha\mid\alpha\lor\alpha\mid\Box\alpha\mid\Diamond\alpha\mid
p\mid\top\text{,}$

where $p\in\mathcal{PS}$ and $\top$ is constant truth. $\mathsf{MTL}\xspace$
extends $\mathsf{ML}\xspace$ by the grammar

$\displaystyle\varphi$
$\displaystyle\vcentcolon\vcentcolon={\sim}\varphi\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\Box\varphi\mid\Diamond\varphi\mid\alpha\text{,}$

where $\alpha$ denotes an $\mathsf{ML}\xspace$-formula.

The set of propositional variables occurring in a formula
$\varphi\in\mathsf{MTL}\xspace$ is $\mathsf{Prop}(\varphi)$. We use the common
abbreviations $\bot\vcentcolon=\neg\top$,
$\alpha\rightarrow\beta\vcentcolon=\neg\alpha\lor\beta$ and
$\alpha\leftrightarrow\beta\vcentcolon=(\alpha\land\beta)\lor(\neg\alpha\land\neg\beta)$.
For easier distinction, we have classical $\mathsf{ML}\xspace$-formulas
denoted by $\alpha,\beta,\gamma,\ldots$ and reserve
$\varphi,\psi,\vartheta,\ldots$ for general $\mathsf{MTL}\xspace$-formulas.

The _modal depth_ $\mathsf{md}(\varphi)$ of a formula $\varphi$ is recursively
defined:

$\displaystyle\mathsf{md}(p)$ $\displaystyle\vcentcolon=\mathsf{md}(\top)$
$\displaystyle\vcentcolon=0$ $\displaystyle\mathsf{md}({\sim}\varphi)$
$\displaystyle\vcentcolon=\mathsf{md}(\neg\varphi)$
$\displaystyle\vcentcolon=\mathsf{md}(\varphi)$
$\displaystyle\mathsf{md}(\varphi\land\psi)$
$\displaystyle\vcentcolon=\mathsf{md}(\varphi\lor\psi)$
$\displaystyle\vcentcolon=\mathrm{max}\\{\mathsf{md}(\varphi),\mathsf{md}(\psi)\\}$
$\displaystyle\mathsf{md}(\Diamond\varphi)$
$\displaystyle\vcentcolon=\mathsf{md}(\Box\varphi)$
$\displaystyle\vcentcolon=\mathsf{md}(\varphi)+1$

$\mathsf{ML}\xspace_{k}$ and $\mathsf{MTL}\xspace_{k}$ are the fragments of
$\mathsf{ML}\xspace$ and $\mathsf{MTL}\xspace$ with modal depth $\leq k$,
respectively. If the propositions are restricted to a fixed set
$\Phi\subseteq\mathcal{PS}$ as well, then the fragment is denoted by
$\mathsf{ML}\xspace_{k}^{\Phi}$, or $\mathsf{MTL}\xspace^{\Phi}_{k}$,
respectively.

Let $\Phi\subseteq\mathcal{PS}$ be finite. A _Kripke structure_ (over $\Phi$)
is a tuple $\mathcal{K}=(W,R,V)$, where $W$ is a set of _worlds_ or _points_ ,
$(W,R)$ is a directed graph called _frame_ , and
$V\colon\Phi\to\mathfrak{P}(W)$ is the _valuation_ , with $\mathfrak{P}(X)$
being the power set of $X$.

Occasionally, by slight abuse of notation, we use the inverse mapping
$V^{-1}\colon W\to\mathfrak{P}(\Phi)$ defined by
$V^{-1}(w)\vcentcolon=\\{p\in\Phi\mid w\in V(p)\\}$ instead of $V$, i.e., the
set of propositions that are true in a given world. If $w\in W$, then
$(\mathcal{K},w)$ is called _pointed structure_. $\mathsf{ML}\xspace$ is
evaluated on pointed structures in the classical Kripke semantics.

By contrast, $\mathsf{MTL}\xspace$ is evaluated on pairs $(\mathcal{K},T)$
called _structures with teams_ , where $\mathcal{K}=(W,R,V)$ is a Kripke
structure and $T\subseteq W$ is called _team_ (in $\mathcal{K}$). Every team
$T$ has an _image_ $RT\vcentcolon=\\{v\mid w\in T,(w,v)\in R\\}$, and for
$w\in W$, we simply write $Rw$ instead of $R\\{w\\}$. $R^{i}T$ is inductively
defined as $R^{0}T\vcentcolon=T$ and $R^{i+1}T\vcentcolon=RR^{i}T$. An
$R$-_successor team_ (or simply successor team) of $T$ is a team $S$ such that
$S\subseteq RT$ and $T\subseteq R^{-1}S$, where
$R^{-1}\vcentcolon=\\{(v,w)\mid(w,v)\in R\\}$. Intuitively, $S$ is formed by
picking at least one $R$-successor of every world in $T$. The semantics of
$\mathsf{MTL}\xspace$ can now be defined as follows. 111Often, the “atoms” of
$\mathsf{MTL}\xspace$ are restricted to literals $p,\neg p$ instead of
$\mathsf{ML}\xspace$-formulas $\alpha$. However, this implies a restriction to
formulas in negation normal form, and both definitions are equivalent due to
the _flatness_ property of $\mathsf{ML}\xspace$ (cf. [KMSV15, Proposition
2.2]).

$\displaystyle(\mathcal{K},T)\vDash\alpha$
$\displaystyle\Leftrightarrow\;\forall w\in
T\colon(\mathcal{K},w)\vDash\alpha\;\text{ if
}\alpha\in\mathsf{ML}\xspace\text{, and otherwise as}$
$\displaystyle(\mathcal{K},T)\vDash{\sim}\psi$
$\displaystyle\Leftrightarrow\;(\mathcal{K},T)\nvDash\psi\text{,}$
$\displaystyle(\mathcal{K},T)\vDash\psi\land\theta$
$\displaystyle\Leftrightarrow\;(\mathcal{K},T)\vDash\psi\text{ and
}(\mathcal{K},T)\vDash\theta\text{,}$
$\displaystyle(\mathcal{K},T)\vDash\psi\lor\theta$
$\displaystyle\Leftrightarrow\;\exists S,U\subseteq T\text{ such that }T=S\cup
U\text{, }(\mathcal{K},S)\vDash\psi\text{, and
}(\mathcal{K},U)\vDash\theta\text{,}$
$\displaystyle(\mathcal{K},T)\vDash\Diamond\psi$
$\displaystyle\Leftrightarrow\;(\mathcal{K},S)\vDash\psi\text{ for some
successor team }S\text{ of }T\text{,}$
$\displaystyle(\mathcal{K},T)\vDash\Box\psi$
$\displaystyle\Leftrightarrow\;(\mathcal{K},RT)\vDash\psi\text{.}$

We often omit $\mathcal{K}$ and write only $T\vDash\varphi$ (for team
semantics) or $w\vDash\alpha$ (for Kripke semantics).

An $\mathsf{MTL}\xspace$-formula $\varphi$ is _satisfiable_ if it is true in
some structure with team over $\mathsf{Prop}(\varphi)$, which is then called a
_model_ of $\varphi$. Analogously, $\varphi$ is _valid_ if it is true in every
structure with team (over $\mathsf{Prop}(\varphi)$). For a logic
$\mathcal{L}$, the sets of all satisfiable resp. valid formulas of
$\mathcal{L}$ are $\mathsf{SAT}(\mathcal{L})$ and $\mathsf{VAL}(\mathcal{L})$,
respectively.

In the literature on team semantics, the empty team is usually excluded in the
above definition, since most ${\sim}$-free logics with team semantics have the
_empty team property_ , i.e., the empty team satisfies every formula [Vää08,
KMSV17, HS15]. However, this distinction is unnecessary for
$\mathsf{MTL}\xspace$: $\varphi$ is satisfiable iff $\top\lor\varphi$ is
satisfied by some non-empty team222Note that $\top\lor\varphi$ is not a
tautology in general, since $\lor$ is not the Boolean disjunction. Rather,
$\top\lor\varphi$ existentially quantifies a subteam where $\varphi$ holds. In
fact, $\top\lor\varphi$ is a tautology if and only if $\varphi$ holds in the
empty team., and $\varphi$ is satisfied by some non-empty team iff
${\sim}\bot\land\varphi$ is satisfiable.

The modality-free fragment $\mathsf{MTL}\xspace_{0}$ syntactically coincides
with _propositional team logic_ $\mathsf{PTL}\xspace$ [HKLV16, HKVV18, YV17].
The usual interpretations of the latter, i.e., sets of Boolean assignments,
can easily be represented as teams in Kripke structures. For this reason, we
treat $\mathsf{PTL}\xspace$ and $\mathsf{MTL}\xspace_{0}$ as identical in this
article.

Note that the connectives $\lor$, $\rightarrow$ and $\neg$ are not the Boolean
disjunction, implication and negation, except on singleton teams, which
correspond to Kripke semantics. Using $\land$ and ${\sim}$ however, we can
define team-wide Boolean disjunction
$\varphi_{1}\ovee\varphi_{2}\vcentcolon={\sim}({\sim}\varphi_{1}\land{\sim}\varphi_{2})$
and material implication
$\varphi_{1}\rightarrowtriangle\varphi_{2}\vcentcolon={\sim}\varphi_{1}\ovee\varphi_{2}$.

The notation $\Box^{i}\varphi$ is defined via
$\Box^{0}\varphi\vcentcolon=\varphi$ and
$\Box^{i+1}\varphi\vcentcolon=\Box\Box^{i}\varphi$, and analogously for
$\Diamond^{i}\varphi$. To express that at least one element of a team
satisfies $\alpha\in\mathsf{ML}\xspace$, we use
$\mathsf{E}\alpha\vcentcolon={\sim}\neg\alpha$.

$\mathsf{MTL}\xspace$ can express the _(extended) dependence atom_
${=\\!\\!(\alpha_{1},\ldots,\alpha_{n-1},\alpha_{n})}$ of (extended) modal
dependence logic [Vää08, EHM+13], which states that the truth value of
$\alpha_{n}$ is a function of the truth values of
$\alpha_{1},\ldots,\alpha_{n-1}$, where
$\alpha_{1},\ldots,\alpha_{n}\in\mathsf{ML}\xspace$. It is definable in
$\mathsf{MTL}\xspace$ as
${\sim}\left[\top\lor{\sim}\left(\bigwedge_{i=1}^{n-1}{=\\!\\!(\alpha_{i})}\rightarrowtriangle{=\\!\\!(\alpha_{n})}\right)\right]$,
where ${=\\!\\!(\alpha)}\vcentcolon=\alpha\ovee\neg\alpha$ is the _constancy
atom_ , stating that the truth value of $\alpha\in\mathsf{ML}\xspace$ is
constant throughout the team.

The well-known _bisimulation_ relation $\rightleftharpoons^{\Phi}_{k}$
fundamentally characterizes the expressive power of modal logic [BRV01] and
plays a key role in our results.

Let $\Phi\subseteq\mathcal{PS}$ and $k\geq 0$. For $i\in\\{1,2\\}$, let
$(\mathcal{K}_{i},w_{i})$ be a pointed structure, where
$\mathcal{K}_{i}=(W_{i},R_{i},V_{i})$. Then $(\mathcal{K}_{1},w_{1})$ and
$(\mathcal{K}_{2},w_{2})$ are _$(\Phi,k)$ -bisimilar_, in symbols
$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},w_{2})$,
if

  * •

$\forall p\in\Phi\colon w_{1}\in V_{1}(p)\Leftrightarrow w_{2}\in V_{2}(p)$,

  * •

and if $k>0$,

    * –

$\forall v_{1}\in R_{1}w_{1}\colon\exists v_{2}\in
R_{2}w_{2}\colon(\mathcal{K}_{1},v_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},v_{2})$
(_forward_ condition),

    * –

$\forall v_{2}\in R_{2}w_{2}\colon\exists v_{1}\in
R_{1}w_{1}\colon(\mathcal{K}_{1},v_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},v_{2})$
(_backward_ condition).

So-called _characteristic formulas_ or _Hintikka formulas_ capture the essence
of the bisimulation relation in the following sense:

[[GO07, Theorem 32]] Let $\Phi\subseteq\mathcal{PS}$ be finite, $k\geq 0$, and
let $(\mathcal{K},w)$ be a pointed structure. Then there is a formula
$\zeta\in\mathsf{ML}\xspace^{\Phi}_{k}$ such that for all pointed structures
$(\mathcal{K}^{\prime},w^{\prime})$ we have
$(\mathcal{K}^{\prime},w^{\prime})\vDash\zeta$ if and only if
$(\mathcal{K},w)\rightleftharpoons^{\Phi}_{k}(\mathcal{K}^{\prime},w^{\prime})$.

The notion of bisimulation was lifted to team semantics by Hella et al.
[HLSV14, KMSV17, KMSV15]:

Let $\Phi\subseteq\mathcal{PS}$ and $k\geq 0$. For $i\in\\{1,2\\}$, let
$(\mathcal{K}_{i},T_{i})$ be a structure with team. Then
$(\mathcal{K}_{1},T_{1})$ and $(\mathcal{K}_{2},T_{2})$ are _$(\Phi,k)$ -team-
bisimilar_, written
$(\mathcal{K}_{1},T_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},T_{2})$,
if

  * •

$\forall w_{1}\in T_{1}\colon\exists w_{2}\in
T_{2}\colon(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},w_{2})$,

  * •

$\forall w_{2}\in T_{2}\colon\exists w_{1}\in
T_{1}\colon(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},w_{2})$.

If no confusion can arise, we will also refer to teams $T_{1},T_{2}$ that are
$(\Phi,k)$-team-bisimilar simply as $(\Phi,k)$-bisimilar. Throughout the
paper, we will make use of the following characterizations of bisimilarity.

######  Proposition 3.

Let $\Phi\subseteq\mathcal{PS}$ be finite, and $k\geq 0$. For $i\in\\{1,2\\}$,
let $(\mathcal{K}_{i},w_{i})$ be a pointed structure, where
$\mathcal{K}_{i}=(W_{i},R_{i},V_{i})$. The following statements are
equivalent:

  1. (1)

$\forall\alpha\in\mathsf{ML}\xspace^{\Phi}_{k}\colon(\mathcal{K}_{1},w_{1})\vDash\alpha\Leftrightarrow(\mathcal{K}_{2},w_{2})\vDash\alpha$,

  2. (2)

$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},w_{2})$,

  3. (3)

$(\mathcal{K}_{1},\\{w_{1}\\})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},\\{w_{2}\\})$,

and if $k>0$,

  1. (4)

$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{0}(\mathcal{K}_{2},w_{2})$
and
$(\mathcal{K}_{1},R_{1}w_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},R_{2}w_{2})$.

######  Proof 3.1.

(1) $\Leftrightarrow$ (2) is a standard result ([GO07, Theorem 32]). (2)
$\Leftrightarrow$ (3) follows from Definition 3. For $k>0$, we show that (2) +
(3) implies (4). Clearly,
$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{0}(\mathcal{K}_{2},w_{2})$
follows from (2). Due to Hella et al. [HLSV14, Lemma 3.3], (3) implies
$(\mathcal{K}_{1},R_{1}w_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},R_{2}w_{2})$.

Finally, we show (4) $\Rightarrow$ (2). Suppose
$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{0}(\mathcal{K}_{2},w_{2})$
and
$(\mathcal{K}_{1},R_{1}w_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},R_{2}w_{2})$.
Then to show
$(\mathcal{K}_{1},w_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},w_{2})$,
it is sufficient to prove the _forward_ and _backward_ conditions of
Definition 3. Suppose $v_{1}\in R_{1}w_{1}$. Since
$(\mathcal{K}_{1},R_{1}w_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},R_{2}w_{2})$,
by Definition 3 there exists $v_{2}\in R_{2}w_{2}$ such that
$(\mathcal{K}_{1},v_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},v_{2})$,
proving the _forward_ condition. The _backward_ condition is symmetric.

As a consequence, the _forward_ and _backward_ condition from Definition 3 can
be equivalently stated in terms of team-bisimilarity of the respective image
teams. A similar characterization exists for team-bisimilarity:

######  Proposition 4.

Let $\Phi\subseteq\mathcal{PS}$ be finite, and $k\geq 0$. Let
$(\mathcal{K}_{i},T_{i})$ be a structure with team for $i\in\\{1,2\\}$. Then
the following statements are equivalent:

  1. (1)

$\forall\alpha\in\mathsf{ML}\xspace^{\Phi}_{k}\colon(\mathcal{K}_{1},T_{1})\vDash\alpha\Leftrightarrow(\mathcal{K}_{2},T_{2})\vDash\alpha$,

  2. (2)

$\forall\varphi\in\mathsf{MTL}\xspace^{\Phi}_{k}\colon(\mathcal{K}_{1},T_{1})\vDash\varphi\Leftrightarrow(\mathcal{K}_{2},T_{2})\vDash\varphi$,

  3. (3)

$(\mathcal{K}_{1},T_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},T_{2})$.

######  Proof 3.2.

The above statements are all true if $T_{1}=T_{2}=\emptyset$, and they are all
false if exactly one of the teams is empty, since a team $T$ satisfies the
$\mathsf{ML}\xspace$-formula $\bot$ precisely if $T=\emptyset$. For this
reason, we can assume that both $T_{1}$ and $T_{2}$ are non-empty.

By Kontinen et al. [KMSV15, Proposition 3.10], for non-empty $T_{1},T_{2}$
there exists an $\mathsf{MTL}\xspace^{\Phi}_{k}$-formula $\varphi$ that is
true in $(\mathcal{K}_{1},T_{1})$, but holds in $(\mathcal{K}_{2},T_{2})$ if
and only if
$(\mathcal{K}_{1},T_{1})\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},T_{2})$.
This immediately proves (2) $\Rightarrow$ (3). The direction (3) $\Rightarrow$
(2) is due to Kontinen et al. [KMSV15, Proposition 2.8] as well.

Finally, (1) $\Leftrightarrow$ (2) follows from the fact that
$\mathsf{ML}\xspace^{\Phi}_{k}\subseteq\mathsf{MTL}\xspace^{\Phi}_{k}$, and
that conversely every $\mathsf{MTL}\xspace^{\Phi}_{k}$-formula is equivalent
to a formula of the form

$\operatorname*{\scalerel*{\ovee}{\sum}}_{i=1}^{n}\Big{(}\alpha_{i}\land\bigwedge_{j=1}^{m_{i}}\mathsf{E}\beta_{i,j}\Big{)}\text{,}$

where
$\\{\alpha_{1},\ldots,\alpha_{n},\beta_{1,1},\ldots,\beta_{n,m_{n}}\\}\subseteq\mathsf{ML}\xspace^{\Phi}_{k}$
(see [Lüc18a, Theorem 5.2] or [KMSV15, p. 11]).

Note that the analog of condition 4 in Proposition 3 for team bisimulation is
not equivalent: It is possible that
$(\mathcal{K}_{1},T_{1})\rightleftharpoons^{\Phi}_{0}(\mathcal{K}_{2},T_{2})$
and
$(\mathcal{K}_{1},R_{1}T_{1})\rightleftharpoons^{\Phi}_{k-1}(\mathcal{K}_{2},R_{2}T_{2})$,
but
$(\mathcal{K}_{1},T_{1})\not\rightleftharpoons^{\Phi}_{k}(\mathcal{K}_{2},T_{2})$.

##  4\. Types and canonical models

Many modal logics admit a “universal” model, also called _canonical model_.
The defining property of a canonical model is that it simultaneously witnesses
all satisfiable (sets of) formulas in some of its points. These models are a
popular tool for proving the completeness of manifold systems of modal logics;
for the explicit construction of such a model for $\mathsf{ML}\xspace$,
consult, e.g., Blackburn et al. [BRV01, Section 4.2].

Unfortunately, any canonical model for $\mathsf{ML}\xspace$ is necessarily
infinite, and consequently impractical for complexity theoretic
considerations. Instead, we use so-called _$(\Phi,k)$ -canonical models_ for
finite $\Phi\subseteq\mathcal{PS}$ and $k\in\mathbb{N}\xspace$; as the name
suggests they are canonical for the fragment $\mathsf{ML}\xspace^{\Phi}_{k}$.
While these models are finite, by Proposition 3 their size is at least the
number of equivalence classes of $\rightleftharpoons^{\Phi}_{k}$. We call the
equivalence classes of $\rightleftharpoons^{\Phi}_{k}$ _types_.

A first issue arises since types are then proper classes, and in team
semantics, we need to speak about _sets_ of types. For this reason, we begin
this section by defining types on proper set-theoretic grounds, by
indentifying the type of a point with the set of formulas that are true in it,
which is a standard approach in first-order model theory.

###  4.1. Types

A set $\tau\subseteq\mathsf{ML}\xspace^{\Phi}_{k}$ is a _$(\Phi,k)$ -type_ if
it is satisfiable and for all $\alpha\in\mathsf{ML}\xspace^{\Phi}_{k}$
contains either $\alpha$ or $\neg\alpha$. The $(\Phi,k)$-type of a pointed
structure $(\mathcal{K},w)$ is

$\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}\vcentcolon=\big{\\{}\alpha\in\mathsf{ML}\xspace^{\Phi}_{k}\mid(\mathcal{K},w)\vDash\alpha\big{\\}}.$

The set of all $(\Phi,k)$-types is $\Delta^{\Phi}_{k}$. Given a team $T$ in
$\mathcal{K}$, the types in $T$ are

$\llbracket{}\mathcal{K},T\rrbracket{}^{\Phi}_{k}\vcentcolon=\big{\\{}\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}\mid
w\in T\big{\\}}.$

The following assertions ascertain that the above definition of types properly
reflects the bisimulation relation.

######  Proposition 5.

Let $\Phi\subseteq\mathcal{PS}$ and $k\geq 0$. Then

  1. (1)

The unique $(\Phi,k)$-type satisfied by $(\mathcal{K},w)$ is
$\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}$.

  2. (2)

$(\mathcal{K},w)\rightleftharpoons^{\Phi}_{k}(\mathcal{K}^{\prime},w^{\prime})$
if and only if
$\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}=\llbracket{}\mathcal{K}^{\prime},w^{\prime}\rrbracket{}^{\Phi}_{k}$.

  3. (3)

$(\mathcal{K},T)\rightleftharpoons^{\Phi}_{k}(\mathcal{K}^{\prime},T^{\prime})$
if and only if
$\llbracket{}\mathcal{K},T\rrbracket{}^{\Phi}_{k}=\llbracket{}\mathcal{K}^{\prime},T^{\prime}\rrbracket{}^{\Phi}_{k}$.

######  Proof 4.1.

Property (1) is straightforward: two distinct types $\tau,\tau^{\prime}$
satisfied by $(\mathcal{K},w)$ differ in some
$\alpha\in\mathsf{ML}\xspace^{\Phi}_{k}$. But then
$(\mathcal{K},w)\vDash\alpha,\neg\alpha$, contradiction. Property (2)
immediately follows from Proposition 3. For (3), first consider
“$\Rightarrow$”. Due to symmetry, we only show that
$(\mathcal{K},T)\rightleftharpoons^{\Phi}_{k}(\mathcal{K}^{\prime},T^{\prime})$
implies
$\llbracket{}\mathcal{K},T\rrbracket{}^{\Phi}_{k}\subseteq\llbracket{}\mathcal{K}^{\prime},T^{\prime}\rrbracket{}^{\Phi}_{k}$.
Hence suppose $\tau\in\llbracket{}\mathcal{K},T\rrbracket{}^{\Phi}_{k}$. Then
there exists $w\in T$ of type
$\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}=\tau$. By Definition 3,
there is $w^{\prime}\in T^{\prime}$ with
$(\mathcal{K},w)\rightleftharpoons^{\Phi}_{k}(\mathcal{K}^{\prime},w^{\prime})$.
Then
$\llbracket{}\mathcal{K}^{\prime},w^{\prime}\rrbracket{}^{\Phi}_{k}=\tau\in\llbracket{}\mathcal{K}^{\prime},T^{\prime}\rrbracket{}^{\Phi}_{k}$
by property (2). The direction “$\Leftarrow$” of (3) is shown analogously.

It is unsurprising that the type of a point $w$ is determined solely by the
propositions in $w$ and the types in the image $Rw$. In other words, all
pointed structures of type $\tau$ satisfy the same propositions in their
roots, viz. $\tau\cap\Phi$, and have the same types contained in their image
teams. Regarding the latter, we define
$\mathcal{R}\tau\vcentcolon=\big{\\{}\tau^{\prime}\in\Delta^{\Phi}_{k}\mid\\{\alpha\mid\Box\alpha\in\tau\\}\subseteq\tau^{\prime}\big{\\}}$,
given a $(\Phi,k+1)$-type $\tau$. Intuitively, $\mathcal{R}\tau$ is the set of
$(\Phi,k)$-types that occur in the image team of a world of type $\tau$.

The following proposition shows that types are indeed uniquely determined by
the above constituents:

######  Proposition 6.

Let $\Phi\subseteq\mathcal{PS}$ be finite and $k\geq 0$.

  1. (1)

$\llbracket{}w\rrbracket{}^{\Phi}_{k}\cap\Phi=V^{-1}(w)\cap\Phi$ and
$\llbracket{}Rw\rrbracket{}^{\Phi}_{k}=\mathcal{R}\llbracket{}w\rrbracket{}^{\Phi}_{k+1}$,
for all pointed structures $(W,R,V,w)$.

  2. (2)

The mapping $h\colon\tau\mapsto\tau\cap\Phi$ is a bijection from
$\Delta^{\Phi}_{0}$ to $\mathfrak{P}(\Phi)$.

  3. (3)

The mapping $h\colon\tau\mapsto(\tau\cap\Phi,\mathcal{R}\tau)$ is a bijection
from $\Delta^{\Phi}_{k+1}$ to
$\mathfrak{P}(\Phi)\times\mathfrak{P}(\Delta^{\Phi}_{k})$.

######  Proof 4.2.

See the appendix.

######  Lemma 7.

Let $(W,R,V,w)$ be a pointed structure.

  1. (1)

If $\tau\in\Delta^{\Phi}_{0}$, then
$\llbracket{}w\rrbracket{}^{\Phi}_{0}=\tau$ if and only if
$V^{-1}(w)=\tau\cap\Phi$.

  2. (2)

If $\tau\in\Delta^{\Phi}_{k+1}$, then
$\llbracket{}w\rrbracket{}^{\Phi}_{k+1}=\tau$ if and only if
$V^{-1}(w)=\tau\cap\Phi$ and
$\llbracket{}Rw\rrbracket{}^{\Phi}_{k}=\mathcal{R}\tau$.

######  Proof 4.3.

The direction “$\Rightarrow$” of 1. and 2. follows directly from Proposition
6. Moreover, we prove “$\Leftarrow$” only for statement 2., as the proof is
analogous for 1.

Suppose that there are $\tau,\tau^{\prime}\in\Delta^{\Phi}_{k+1}$ such that
$V^{-1}(w)=\tau\cap\Phi$ and
$\llbracket{}Rw\rrbracket{}^{\Phi}_{k}=\mathcal{R}\tau$, but
$\llbracket{}w\rrbracket{}^{\Phi}_{k+1}=\tau^{\prime}$. Then, by
“$\Rightarrow$”, we have $V^{-1}(w)=\tau^{\prime}\cap\Phi$ and
$\llbracket{}Rw\rrbracket{}^{\Phi}_{k}=\mathcal{R}\tau^{\prime}$ as well. In
other words, $\tau\cap\Phi=\tau^{\prime}\cap\Phi$ and
$\mathcal{R}\tau=\mathcal{R}\tau^{\prime}$. However, since the mapping
$h\colon\tau\mapsto(\tau\cap\Phi,\mathcal{R}\tau)$ is bijective according to
Proposition 6, we have
$\tau=\tau^{\prime}=\llbracket{}w\rrbracket{}^{\Phi}_{k+1}$.

We are now ready to state the formal definition of canonicity by the notion of
types:

A structure with team $(\mathcal{K},T)$ is _$(\Phi,k)$ -canonical_ if
$\llbracket{}\mathcal{K},T\rrbracket{}^{\Phi}_{k}=\Delta^{\Phi}_{k}$.

In the following, we often omit $\Phi$ and $\mathcal{K}$ and instead write
$\llbracket{}w\rrbracket{}_{k}$ and $\llbracket{}T\rrbracket{}_{k}$,
respectively, and simply say that $T$ is $(\Phi,k)$-canonical if $\mathcal{K}$
is clear.

###  4.2. Canonical models in team semantics

It is a standard result that for every $\Phi$ and $k\geq 0$ there exists a
$(\Phi,k)$-canonical model [BRV01], or in other words, that the logic
$\mathsf{ML}\xspace^{\Phi}_{k}$ admits canonical models.

We will show that, given a $(\Phi,k)$-canonical model $\mathcal{K}$, every
satisfiable $\mathsf{MTL}\xspace^{\Phi}_{k}$-formula can be satisfied in some
team of $\mathcal{K}$ as well, despite $\mathsf{MTL}\xspace$ being
significantly more expressive than $\mathsf{ML}\xspace$ [KMSV15]. In other
words, the canonical models for $\mathsf{MTL}\xspace^{\Phi}_{k}$ and
$\mathsf{ML}\xspace^{\Phi}_{k}$ coincide:

######  Theorem 8.

Let $(\mathcal{K},T)$ be $(\Phi,k)$-canonical and
$\varphi\in\mathsf{MTL}\xspace^{\Phi}_{k}$. Then $\varphi$ is satisfiable if
and only if $(\mathcal{K},T^{\prime})\vDash\varphi$ for some
$T^{\prime}\subseteq T$.

######  Proof 4.4.

Assume $(\mathcal{K},T)$ and $\varphi$ are as above. As the direction from
right to left is trivial, suppose that $\varphi$ is satisfiable, i.e., has a
model $(\hat{\mathcal{K}},\hat{T})$. As a team in $\mathcal{K}$ that satisfies
$\varphi$, we define

$T^{\prime}\vcentcolon=\Set{w\in
T}{\llbracket{}\mathcal{K},w\rrbracket{}^{\Phi}_{k}\in\llbracket{}\hat{\mathcal{K}},\hat{T}\rrbracket{}^{\Phi}_{k}}\text{.}$

By Proposition 4 and 5, it suffices to prove
$\llbracket{}\hat{\mathcal{K}},\hat{T}\rrbracket{}^{\Phi}_{k}=\llbracket{}\mathcal{K},T^{\prime}\rrbracket{}^{\Phi}_{k}$.
Moreover, the direction “$\supseteq$” is clear by definition. As $T$ is
$(\Phi,k)$-canonical, for every
$\tau\in\llbracket{}\hat{\mathcal{K}},\hat{T}\rrbracket{}^{\Phi}_{k}$ there
exists a world $w\in T$ of type $\tau$. Consequently,
$\llbracket{}\hat{\mathcal{K}},\hat{T}\rrbracket{}^{\Phi}_{k}\subseteq\llbracket{}\mathcal{K},T^{\prime}\rrbracket{}^{\Phi}_{k}$.

How large is a $(\Phi,k)$-canonical model at least? The number of types is
captured by the function $\exp^{*}_{k}$, defined by

$\exp^{*}_{0}(n)\vcentcolon=n\qquad\qquad\exp^{*}_{k+1}(n)\vcentcolon=n\cdot
2^{\exp^{*}_{k}(n)}\text{.}$

######  Proposition 9.

${|\nobreak\Delta^{\Phi}_{k}\nobreak|}=\exp^{*}_{k}\big{(}2^{|\nobreak\Phi\nobreak|}\big{)}$
for all $k\geq 0$ and finite $\Phi\subseteq\mathcal{PS}$.

######  Proof 4.5.

By induction on $k$. For the base case $k=0$, this follows from Proposition 6,
as there is a bijection between $\Delta^{\Phi}_{0}$ and $\mathfrak{P}(\Phi)$
and
$\exp^{*}_{0}\big{(}2^{|\nobreak\Phi\nobreak|}\big{)}=2^{|\nobreak\Phi\nobreak|}={|\nobreak\Delta^{\Phi}_{0}\nobreak|}$.

We proceed with the inductive step, i.e., $k+1$. First note that by induction
hypothesis

$\exp^{*}_{k+1}\big{(}2^{|\nobreak\Phi\nobreak|}\big{)}=2^{|\nobreak\Phi\nobreak|}\cdot
2^{\exp^{*}_{k}(2^{|\nobreak\Phi\nobreak|})}={|\nobreak\mathfrak{P}(\Phi)\times\mathfrak{P}(\Delta^{\Phi}_{k})\nobreak|}\text{.}$

Again, there exists a bijection from $\Delta^{\Phi}_{k+1}$ to
$\mathfrak{P}(\Phi)\times\mathfrak{P}(\Delta^{\Phi}_{k})$ by Proposition 6.

Next, we present an algorithm that solves the satisfiability and validity
problems of $\mathsf{MTL}\xspace_{k}$ by computing a canonical model. Let us
first explicate this construction in a lemma.

######  Lemma 10.

There is an algorithm that, given $\Phi\subseteq\mathcal{PS}$ and $k\geq 0$,
computes a $(\Phi,k)$-canonical model in time polynomial in
${|\nobreak\Delta^{\Phi}_{k}\nobreak|}$.

######  Proof 4.6.

The idea is to construct sets $L_{0}\cup L_{1}\cup\cdots\cup L_{k}$ of worlds
in stage-wise manner such that $L_{i}$ is $(\Phi,i)$-canonical. For $L_{0}$,
we simply add a world $w$ for each $\Phi^{\prime}\in\mathfrak{P}(\Phi)$ such
that $V^{-1}(w)=\Phi^{\prime}$. For $i>0$, we iterate over all
$L^{\prime}\in\mathfrak{P}(L_{i-1})$ and $\Phi^{\prime}\in\mathfrak{P}(\Phi)$
and insert a new world $w$ into $L_{i}$ such that $L^{\prime}$ is the image of
$w$ and such that again $V^{-1}(w)=\Phi^{\prime}$. An inductive argument based
on Proposition 4 and 6 shows that $L_{i}$ is $(\Phi,i)$-canonical for all
$i\in\\{0,\ldots,k\\}$. As $k\leq{|\nobreak\Delta^{\Phi}_{k}\nobreak|}$, and
each $L_{i}$ is constructed in time polynomial in
${|\nobreak\Delta^{\Phi}_{i}\nobreak|}\leq{|\nobreak\Delta^{\Phi}_{k}\nobreak|}$,
the overall runtime is polynomial in ${|\nobreak\Delta^{\Phi}_{k}\nobreak|}$.

With the help of a small lemma, we conclude the upper bound for the
satisfiability and validity problem of $\mathsf{MTL}\xspace$ and its
fragments.

######  Lemma 11.

For every polynomial $p$ there is a polynomial $q$ such that

$p(\exp^{*}_{k}(n))\leq\exp_{k}(q((k+1)\cdot n))$

for all $k\geq 0$ and $n\geq 1$.

######  Proof 4.7.

See the appendix.

######  Theorem 12.

$\mathsf{SAT}(\mathsf{MTL}\xspace_{k})$ and
$\mathsf{VAL}(\mathsf{MTL}\xspace_{k})$ are in
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$.

######  Proof 4.8.

Consider the following algorithm. Let $\varphi\in\mathsf{MTL}\xspace_{k}$ be
the input, $n\vcentcolon={|\nobreak\varphi\nobreak|}$, and
$\Phi\vcentcolon=\mathsf{Prop}(\varphi)$. Construct deterministically, as in
Lemma 10, a $(\Phi,k)$-canonical structure $\mathcal{K}=(W,R,V)$ in time
$p({|\nobreak\Delta^{\Phi}_{k}\nobreak|})$ for a polynomial $p$.

By a result of Müller [Mül14], the model checking problem of
$\mathsf{MTL}\xspace$ is solvable by an alternating Turing machine that has
runtime polynomial in
${|\nobreak\varphi\nobreak|}+{|\nobreak\mathcal{K}\nobreak|}$, and
alternations polynomial in ${|\nobreak\varphi\nobreak|}$. We call this
algorithm as a subroutine: by Theorem 8, $\varphi$ is satisfiable (resp.
valid) if and only if for at least one subteam (resp. all subteams)
$T\subseteq W$ we have $(\mathcal{K},T)\vDash\varphi$. Equivalently, this is
the case if and only if $(\mathcal{K},W)$ satisfies $\top\lor\varphi$ (resp.
${\sim}(\top\lor{\sim}\varphi)$).

Let us turn to the overall runtime. $\mathcal{K}$ is constructed in time
polynomial in
${|\nobreak\Delta^{\Phi}_{k}\nobreak|}=\exp^{*}_{k}(2^{|\nobreak\Phi\nobreak|})\leq\exp^{*}_{k+1}({|\nobreak\Phi\nobreak|})\leq\exp^{*}_{k+1}(n)$.
The subsequent model checking runs in time polynomial in
${|\nobreak\mathcal{K}\nobreak|}+n$, and hence polynomial in
$\exp^{*}_{k+1}(n)$ as well. By Lemma 11, we obtain a total runtime of
$\exp_{k+1}(q((k+2)\cdot n))$ for a polynomial $q$.

The upper bound for $\mathsf{MTL}\xspace$ is proved identically, since
$k\vcentcolon=\mathsf{md}(\varphi)$ is polynomial in
${|\nobreak\varphi\nobreak|}$.

######  Corollary 13.

$\mathsf{SAT}(\mathsf{MTL}\xspace)$ and $\mathsf{VAL}(\mathsf{MTL}\xspace)$
are in $\mathrm{TOWER}\xspace(\mathrm{poly})$.

The usual definition of a canonical model is a structure that has all
(infinite) maximal consistent subsets of a certain class of modal formulas as
worlds (see virtually any textbook on modal logic, e.g., [BRV01]). This indeed
results in a finite number of worlds in the case of, say,
$\mathsf{ML}\xspace^{\Phi}_{k}$ (cf. [Cre83, CH96]). Truly finitary
constructions of canonical models can be traced back to Fine [Fin75], whose
work has been extended towards various other modal systems (e.g., by Moss
[Mos07]). Furthermore, Cresswell and Hughes [CH96] used _mini canonical
models_ , models that are “canonical” only with respect to all subformulas of
a fixed $\mathsf{ML}\xspace$-formula, which allows them to be finite models
with finite sets of formulas as worlds.

All these approaches have in common that they still are non-constructive and
intended for completeness proofs. Even computing a “mini canonical model”
would not be guaranteed to be feasible enough for $\mathsf{MTL}\xspace$: This
would require an explicit translation of a given input
$\mathsf{MTL}\xspace^{\Phi}_{k}$-formula to a Boolean combination of
$\mathsf{ML}\xspace^{\Phi}_{k}$-formulas first (see the proof of Proposition
4), and it is open whether there is an elementary translation for every fixed
$k$ (cf. [Lüc18a]).

In this light, our approach yields a purely constructive definition of a
canonical model (in Lemma 10), which can easily be plugged into the algorithms
used for the above results, and has optimal runtime up to a polynomial.

##  5\. Scopes and Subteam Quantifiers

Kontinen et al. [KMSV15] proved that $\mathsf{MTL}\xspace$ is expressively
complete up to bisimulation: it can define every property of teams that is
$(\Phi,k)$-bisimulation invariant, that is closed under
$\rightleftharpoons^{\Phi}_{k}$, for some finite $\Phi$ and $k$. Two team
properties that fall into this category are in fact $(\Phi,k)$-bisimilarity
itself—in the sense that all worlds in a team have the same $(\Phi,k)$-type—as
well as $(\Phi,k)$-canonicity. Consequently, these properties are definable by
$\mathsf{MTL}\xspace^{\Phi}_{k}$-formulas. However, by a simple counting
argument, formulas defining arbitrary team properties require non-elementary
size w. r. t.$\Phi$ and $k$.

In this section, we consider a special class of structures, and on these,
define $k$-bisimilarity by a formula $\chi_{k}$ of polynomial size in $\Phi$
and $k$. (From now on, we always assume some finite
$\Phi\subseteq\mathcal{PS}$ and omit it in the notation, i.e., we write _$k$
-canonicity_, _$k$ -bisimilarity_, $\rightleftharpoons_{k}$, and so on.)
Afterwards, in Section 6 we devise a formula $\mathsf{canon}_{k}$ of
polynomial size that expresses $k$-canonicity.

###  5.1. Scopes

It is natural to implement $k$-bisimilarity by mutual recursion in the spirit
of Proposition 3: the $(k+1)$-bisimilarity of two points $w,v$ is expressed in
terms of $k$-team-bisimilarity of $Rw$ and $Rv$, and conversely, to verify
$k$-team-bisimilarity of $Rw$ and $Rv$, we proceed analogously to the
_forward_ and _backward_ conditions of Definition 3 and reduce the problem to
checking $k$-bisimilarity of pairs of points in $Rw$ and $Rv$.

$\mathsf{MTL}\xspace$-formulas define team properties, but we want to express
a _relation_ between teams such as $Rw$ and $Rv$. For this reason, we consider
the “marked union” of $Rw$ and $Rv$ as a single team using the following tool.
Formally, if $\alpha\in\mathsf{ML}\xspace$, then the “conditioned” subteam
$T_{\alpha}\subseteq T$ is defined as

$T_{\alpha}\vcentcolon=\Set{w\in T}{w\vDash\alpha}\text{.}$

In the literature, $T_{\alpha}$ is also written $T\upharpoonright\alpha$
[Gal15, Gal16, Gal18]. The corresponding “decoding” operator

$\alpha\hookrightarrow\varphi\vcentcolon=\neg\alpha\lor(\alpha\land\varphi)$

was introduced by Galliani [Gal15, Gal16, Gal18] as well:
$\alpha\hookrightarrow\varphi$ is true in $T$ if and only if
$T_{\alpha}\vDash\varphi$.

Now, instead of defining an $n$-ary relation on teams, a formula $\varphi$ can
define a unary relation—a team property—parameterized by formulas
$\alpha_{1},\ldots,\alpha_{n}\in\mathsf{ML}\xspace$. We emphasize this by
writing $\varphi(\alpha_{1},\ldots,\alpha_{n})$.

It will be useful if the “markers” of the constituent teams are invariant
under traversing edges in the structure. In that case, we call these formulas
_scopes_ :

Let $\mathcal{K}=(W,R,V)$ be a Kripke structure. A formula
$\alpha\in\mathsf{ML}\xspace$ is called a _scope (in $\mathcal{K}$)_ if
$(w,v)\in R$ implies $w\vDash\alpha\Leftrightarrow v\vDash\alpha$. Two scopes
$\alpha,\beta$ are called _disjoint (in $\mathcal{K}$)_ if $W_{\alpha}$ and
$W_{\beta}$ are disjoint.

To avoid interference, we always assume that scopes are formulas in
$\mathsf{ML}\xspace^{\mathcal{PS}\setminus\Phi}_{0}$, i.e., they are always
purely propositional and do not contain propositions from $\Phi$.

$T$$S$$\alpha_{1}$$\alpha_{3}$$\alpha_{2}$$\Rightarrow$$\alpha_{1}$$\alpha_{3}$$\alpha_{2}$$S$$T^{\alpha_{2}}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}S}$
Figure 1. Example of subteam selection in the scope $\alpha_{2}$

It is desirable to be able to speak about subteams in a specific scope. If $S$
is a team, let $T^{\alpha}_{S}\vcentcolon=T_{\neg\alpha}\cup(T_{\alpha}\cap
S)$. For singletons $\\{w\\}$, we simply write $T^{\alpha}_{w}$ instead of
$T^{\alpha}_{\\{w\\}}$. Intuitively, $T^{\alpha}_{S}$ is obtained from $T$ by
“shrinking” the subteam $T_{\alpha}$ down to $S$ without impairing $T\setminus
T_{\alpha}$ (see Figure 1 for an example). Scopes have several desirable
properties:

######  Proposition 14.

Let $\alpha,\beta$ be disjoint scopes and $S,U,T$ teams in a Kripke structure
$\mathcal{K}=(W,R,V)$. Then the following laws hold:

  1. (1)

Distributive laws: ${(T\cap S)}_{\alpha}=T_{\alpha}\cap S=T\cap
S_{\alpha}=T_{\alpha}\cap S_{\alpha}$ and ${(T\cup S)}_{\alpha}=T_{\alpha}\cup
S_{\alpha}$.

  2. (2)

Disjoint selection commutes:
${\big{(}T^{\alpha}_{S}\big{)}}^{\beta}_{U}={\big{(}T^{\beta}_{U}\big{)}}^{\alpha}_{S}$.

  3. (3)

Disjoint selection is independent:
${\big{(}{(T^{\alpha}_{S})}^{\beta}_{U}\big{)}}_{\alpha}=T_{\alpha}\cap S$.

  4. (4)

Image and selection commute:
${(RT)}_{\alpha}={\big{(}R(T_{\alpha})\big{)}}_{\alpha}=R(T_{\alpha})$

  5. (5)

Selection propagates: If $S\subseteq T$, then
$R{\big{(}T^{\alpha}_{S}\big{)}}={(RT)}^{\alpha}_{RS}$.

######  Proof 5.1.

Straightforward; see the appendix.

Accordingly, we write $R^{i}T_{\alpha}$ instead of ${(R^{i}T)}_{\alpha}$ or
$R^{i}(T_{\alpha})$ and $T^{\alpha_{1},\alpha_{2}}_{S_{1},S_{2}}$ for
${(T^{\alpha_{1}}_{S_{1}})}^{\alpha_{2}}_{S_{2}}$.

###  5.2. Subteam quantifiers

We refer to the following abbreviations as _subteam quantifiers_ , where
$\alpha\in\mathsf{ML}\xspace$:

$\displaystyle\exists^{\subseteq}_{\alpha}\;\varphi$
$\displaystyle\vcentcolon=\alpha\lor\varphi$
$\displaystyle\forall^{\subseteq}_{\alpha}\;\varphi$
$\displaystyle\vcentcolon={\sim}\exists^{\subseteq}_{\alpha}{\sim}\varphi$
$\displaystyle\exists^{1}_{\alpha}\;\varphi$
$\displaystyle\vcentcolon=\exists^{\subseteq}_{\alpha}\left[\mathsf{E}\alpha\land\forall^{\subseteq}_{\alpha}(\mathsf{E}\alpha\rightarrowtriangle\varphi)\right]$
$\displaystyle\forall^{1}_{\alpha}\;\varphi$
$\displaystyle\vcentcolon={\sim}\exists^{1}_{\alpha}{\sim}\varphi$

Intuitively, they quantify over subteams $S\subseteq T_{\alpha}$ or worlds
$w\in T_{\alpha}$ such that $T^{\alpha}_{S}$ resp. $T^{\alpha}_{w}$ satisfies
$\varphi$.

######  Proposition 15.

The subteam quantifiers have the following semantics:

$\displaystyle\qquad T\;\vDash\;\;$
$\displaystyle\exists^{\subseteq}_{\alpha}\varphi$
$\displaystyle\;\Leftrightarrow\;\exists S\subseteq T_{\alpha}$
$\displaystyle\colon T^{\alpha}_{S}\vDash\varphi$ $\displaystyle\qquad\qquad
T\;\vDash\;\;$ $\displaystyle\exists^{1}_{\alpha}\varphi$
$\displaystyle\;\Leftrightarrow\;\exists w\in T_{\alpha}$ $\displaystyle\colon
T^{\alpha}_{w}\vDash\varphi$ $\displaystyle\qquad T\;\vDash\;\;$
$\displaystyle\forall^{\subseteq}_{\alpha}\varphi$
$\displaystyle\;\Leftrightarrow\;\forall S\subseteq T_{\alpha}$
$\displaystyle\colon T^{\alpha}_{S}\vDash\varphi$ $\displaystyle\qquad\qquad
T\;\vDash\;\;$ $\displaystyle\forall^{1}_{\alpha}\varphi$
$\displaystyle\;\Leftrightarrow\;\forall w\in T_{\alpha}$ $\displaystyle\colon
T^{\alpha}_{w}\vDash\varphi$

######  Proof 5.2.

We prove the existential cases, as the other ones work dually.

Let us first consider the “$\Rightarrow$” direction for
$\exists^{\subseteq}_{\alpha}$. Accordingly, suppose
$T\vDash\exists^{\subseteq}_{\alpha}\,\varphi$, i.e.,
$T\vDash\alpha\lor\varphi$. Then there exist $S\subseteq T$ and $U\subseteq
T_{\alpha}$ such that $S\vDash\varphi$ and $T=S\cup U$. Since $U\cap
T_{\neg\alpha}=\emptyset$, it holds $T_{\neg\alpha}\subseteq S$. Moreover,
$S=(S\cap T_{\alpha})\cup(S\cap T_{\neg\alpha})=((S\cap T_{\alpha})\cap
T_{\alpha})\cup T_{\neg\alpha}=T^{\alpha}_{S\cap T_{\alpha}}$. Consequently,
$T^{\alpha}_{S\cap T_{\alpha}}\vDash\varphi$ for some set $S\cap
T_{\alpha}\subseteq T_{\alpha}$.

For “$\Leftarrow$”, suppose $T^{\alpha}_{S}\vDash\varphi$ for some $S\subseteq
T_{\alpha}$. Then $T^{\alpha}_{S}$ and $T\setminus T^{\alpha}_{S}$ form a
division of $T$. Since $T\setminus
T^{\alpha}_{S}=T\setminus\left(T_{\neg\alpha}\cup(T_{\alpha}\cap
S)\right)\subseteq T\setminus T_{\neg\alpha}=T_{\alpha}$, it holds $T\setminus
T^{\alpha}_{S}\vDash\alpha$. As a consequence, $T\vDash\alpha\lor\varphi$.

We proceed with $\exists^{1}_{\alpha}$. For “$\Rightarrow$”, suppose that
$T\vDash\exists^{1}_{\alpha}\varphi$. Then there exists $S\subseteq
T_{\alpha}$ such that
$T^{\alpha}_{S}\vDash\mathsf{E}\alpha\land\forall^{\subseteq}_{\alpha}(\mathsf{E}\alpha\rightarrowtriangle\varphi)$.
Since $T^{\alpha}_{S}\vDash\mathsf{E}\alpha$, there exists
$w\in{(T^{\alpha}_{S})}_{\alpha}$. As $\forall^{\subseteq}_{\alpha}$ now
applies to ${(T^{\alpha}_{S})}^{\alpha}_{\\{w\\}}=T^{\alpha}_{w}$ as well, it
follows $T^{\alpha}_{w}\vDash\mathsf{E}\alpha\rightarrowtriangle\varphi$, and
consequently $T^{\alpha}_{w}\vDash\varphi$.

Suppose for “$\Leftarrow$” that $T^{\alpha}_{w}\vDash\varphi$ for some $w\in
T_{\alpha}$. Let $S\subseteq T_{\alpha}$ be arbitrary. If $w\notin S$, then
${(T^{\alpha}_{w})}^{\alpha}_{S}=T^{\alpha}_{\emptyset}\nvDash\mathsf{E}\alpha$,
and if $w\in S$, then
${(T^{\alpha}_{w})}^{\alpha}_{S}=T^{\alpha}_{w}\vDash\varphi$. Therefore, for
any $S\subseteq T_{\alpha}$ it holds
${(T^{\alpha}_{w})}^{\alpha}_{S}\vDash(\mathsf{E}\alpha\rightarrowtriangle\varphi)$,
so
$T^{\alpha}_{w}\vDash\forall^{\subseteq}_{\alpha}(\mathsf{E}\alpha\rightarrowtriangle\varphi)$.
Since also $T^{\alpha}_{w}\vDash\mathsf{E}\alpha$, it follows
$T\vDash\exists^{\subseteq}_{\alpha}\left[\mathsf{E}\alpha\land\forall^{\subseteq}_{\alpha}(\mathsf{E}\alpha\rightarrowtriangle\varphi)\right]$.

###  5.3. Implementing bisimulation

With scopes and subteam quantifiers at our hands, we have all ingredients to
implement $k$-bisimulation.

$\displaystyle\chi_{0}(\alpha,\beta)$
$\displaystyle\vcentcolon=(\alpha\lor\beta)\hookrightarrow\bigwedge_{p\in\Phi}{=\\!\\!(p)}$
$\displaystyle\chi_{k+1}(\alpha,\beta)$
$\displaystyle\vcentcolon=\chi_{0}(\alpha,\beta)\land\Box\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\vcentcolon=(\neg\alpha\land\neg\beta)\ovee\Big{(}\mathsf{E}\alpha\land\mathsf{E}\beta\land{\sim}\big{[}(\alpha\ovee\beta)\lor(\mathsf{E}\alpha\land\mathsf{E}\beta\land{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta))\big{]}\Big{)}$

Note that a literal translation of the forward and backward condition would
rather result in the formula
$\chi^{*}_{k}(\alpha,\beta)\vcentcolon=\forall^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)\land\forall^{1}_{\beta}\exists^{1}_{\alpha}\chi_{k}(\alpha,\beta)$.
The more complicated formula shown above however avoids the exponential size
that would come with two recursive calls.

######  Theorem 16.

Let $k\geq 0$. For all Kripke structures $\mathcal{K}$, teams $T$ and disjoint
scopes $\alpha,\beta$ in $\mathcal{K}$, and points $w\in T_{\alpha}$ and $v\in
T_{\beta}$ it holds:

$\displaystyle T^{\alpha,\beta}_{w,v}$
$\displaystyle\;\vDash\;\chi_{k}(\alpha,\beta)\;$ if and only if
$\displaystyle w\rightleftharpoons_{k}\,$ $\displaystyle v\text{,}$
$\displaystyle T$ $\displaystyle\;\vDash\;\chi^{*}_{k}(\alpha,\beta)\;$ if and
only if $\displaystyle T_{\alpha}\rightleftharpoons_{k}\,$ $\displaystyle
T_{\beta}\text{.}$

Moreover, both $\chi_{k}(\alpha,\beta)$ and $\chi^{*}_{k}(\alpha,\beta)$ are
$\mathsf{MTL}\xspace_{k}$-formulas that are constructible in space
${\mathcal{O}(\log(k+{|\nobreak\Phi\nobreak|}+{|\nobreak\alpha\nobreak|}+{|\nobreak\beta\nobreak|}))}$.

$\alpha$$\beta$$T$$z$$\rightleftharpoons_{0}\\!$$\rightleftharpoons_{0}\\!$$\rightleftharpoons_{0}$$\rightleftharpoons_{1}$?$\Rightarrow$$\rightleftharpoons_{0}$$\rightleftharpoons_{0}$$\rightleftharpoons_{0}$$\Rightarrow$$RT$$z$$z$$RT^{\beta}_{z}$
Figure 2. As $z$ violates the _backward_ condition, shrinking $RT_{\beta}$
leads to a $\rightleftharpoons_{0}$-free subteam, falsifying
$\exists^{1}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\alpha}\exists^{1}_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\beta}\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\chi_{0}(\alpha,\beta)$.

######  Proof 5.3.

The idea is to isolate a single point in $z\in T_{\alpha}\cup T_{\beta}$ that
serves as a _counter-example_ against
$\llbracket{}T_{\alpha}\rrbracket{}_{k}=\llbracket{}T_{\beta}\rrbracket{}_{k}$
by, say,
$\llbracket{}z\rrbracket{}_{k}\in\llbracket{}T_{\beta}\rrbracket{}_{k}\setminus\llbracket{}T_{\alpha}\rrbracket{}_{k}$.
We erase $T_{\beta}\setminus\\{z\\}$ from $T$ using the disjunction $\lor$, as
$T_{\beta}\setminus\\{z\\}\vDash\alpha\ovee\beta$. The remaining team is
exactly $T^{\beta}_{z}$, in which
$\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$ fails (see
Figure 2). The case
$\llbracket{}z\rrbracket{}_{k}\in\llbracket{}T_{\alpha}\rrbracket{}_{k}\setminus\llbracket{}T_{\beta}\rrbracket{}_{k}$
is detected analogously.

We proceed with a formal correctness proof by induction on $k$. Let
$\mathcal{K}=(W,R,V)$ as in the theorem. The base case $k=0$ is
straightforward, as no proposition $p\in\Phi$ occurs in $\alpha$ or $\beta$.
The induction step is split into two parts.

“$\chi_{k}\Rightarrow\chi^{*}_{k}$”: Let $T$ be a team and $\alpha,\beta$
disjoint scopes. Observe that $\chi^{*}_{k}$ is always true if $T_{\alpha}$
and $T_{\beta}$ are both empty (then
$\llbracket{}T_{\alpha}\rrbracket{}_{k}=\llbracket{}T_{\beta}\rrbracket{}_{k}$),
and that it is always false if exactly one of them is empty (then
$\llbracket{}T_{\alpha}\rrbracket{}_{k}\neq\llbracket{}T_{\beta}\rrbracket{}_{k}$).
Therefore, let $T_{\alpha}\neq\emptyset$ and $T_{\beta}\neq\emptyset$. Then
$\chi^{*}_{k}(\alpha,\beta)$ boils down to
${\sim}((\alpha\ovee\beta)\lor\mathsf{E}\alpha\land\mathsf{E}\beta\land{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta))$,
which we prove equivalent to
$\llbracket{}T_{\alpha}\rrbracket{}_{k}=\llbracket{}T_{\beta}\rrbracket{}_{k}$.

The first direction is proved by contradiction. Suppose
$\llbracket{}T_{\alpha}\rrbracket{}_{k}=\llbracket{}T_{\beta}\rrbracket{}_{k}$
but
$T\vDash(\alpha\ovee\beta)\lor\mathsf{E}\alpha\land\mathsf{E}\beta\land{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$.
The disjunction is witnessed by some division $T=S\cup U$, where
w.l.o.g.$S\subseteq T_{\alpha}$ satisfies $\alpha\ovee\beta$, (if $S\subseteq
T_{\beta}$, the proof is symmetric), and
$U\vDash\mathsf{E}\alpha\land\mathsf{E}\beta\land{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$.
Since $T_{\alpha}\cap T_{\beta}=\emptyset$, then $T_{\beta}\subseteq U$, and
clearly $T_{\beta}\subseteq U_{\beta}$. By the formula, some $w\in U_{\alpha}$
exists. By assumption that
$\llbracket{}T_{\alpha}\rrbracket{}_{k}=\llbracket{}T_{\beta}\rrbracket{}_{k}$,
$U_{\beta}$ must contain a world $v$ of type $\llbracket{}w\rrbracket{}_{k}$
as well. But then $U^{\alpha,\beta}_{w,v}\vDash\chi_{k}(\alpha,\beta)$ by
induction hypothesis, contradiction to
$U\vDash{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$.

For the other direction, suppose
$\llbracket{}T_{\alpha}\rrbracket{}_{k}\neq\llbracket{}T_{\beta}\rrbracket{}_{k}$.
W.l.o.g.there exists $w\in T_{\alpha}$ such that
$\llbracket{}w\rrbracket{}_{k}\notin\llbracket{}T_{\beta}\rrbracket{}_{k}$.
(For $w\in T_{\beta}$, the proof is again symmetric.) Consider
$S\vcentcolon=T_{\alpha}\setminus\\{w\\}$ and $U\vcentcolon=T^{\alpha}_{w}$ as
a division of $T$. Then $S\vDash\alpha\ovee\beta$ and
$U\vDash\mathsf{E}\alpha\land\mathsf{E}\beta$. It remains to show
$U\vDash{\sim}\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$.
However, this is easy to see:
$U\vDash\exists^{1}_{\alpha}\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$ if and
only if $U\vDash\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$, but $T_{\beta}$
and hence $U_{\beta}$ contains no world of type
$\llbracket{}w\rrbracket{}_{k}$, so by induction hypothesis $U$ cannot satisfy
$\exists^{1}_{\beta}\chi_{k}(\alpha,\beta)$.

“$\chi^{*}_{k}\Rightarrow\chi_{k+1}$”: We follow Definition 3 and Proposition
3.

$\displaystyle T^{\alpha,\beta}_{w,v}\vDash\chi_{k+1}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\chi_{0}(\alpha,\beta)\land\Box\chi^{*}_{k}(\alpha,\beta)$
(Definition of $\chi_{k+1}$) $\displaystyle\Leftrightarrow\;$ $\displaystyle
w\rightleftharpoons_{0}v\text{ and
}T^{\alpha,\beta}_{w,v}\vDash\Box\chi^{*}_{k}(\alpha,\beta)$ (Induction
hypothesis) $\displaystyle\Leftrightarrow\;$ $\displaystyle
w\rightleftharpoons_{0}v\text{ and
}RT^{\alpha,\beta}_{Rw,Rv}\vDash\chi^{*}_{k}(\alpha,\beta)$ (Proposition 14)
$\displaystyle\Leftrightarrow\;$ $\displaystyle w\rightleftharpoons_{0}v\text{
and }Rw\rightleftharpoons_{k}Rv$ (Induction hypothesis)
$\displaystyle\Leftrightarrow\;$ $\displaystyle
w\rightleftharpoons_{k+1}v\text{.}$ (Proposition 3)

It is routine to check that the formulas are constructible in logarithmic
space from $\alpha$, $\beta$, $\Phi$ and $k$, and that
$\mathsf{md}(\chi_{k})=\mathsf{md}(\chi^{*}_{k})=k$.

Let us stress that $\chi_{k}$ relies on disjoint scopes to be present in the
structure, and it is open whether the property
${|\nobreak\llbracket{}T\rrbracket{}_{k}\nobreak|}\leq 1$ is polynomially
definable without these. Incidentally, the related property
${|\nobreak\llbracket{}Rw\rrbracket{}_{k}\nobreak|}\leq 1$ of points $w$ was
recently studied by Hella and Vilander [HV16], and was proven to be
expressible in $\mathsf{ML}\xspace$, but only by formulas of non-elementary
size. However, they proved that it is definable in exponential size in
_2-dimensional modal logic_ $\mathsf{ML}\xspace^{2}$ (for an introduction to
$\mathsf{ML}\xspace^{2}$, see Marx and Venema [MV97]). Roughly speaking,
$\mathsf{ML}\xspace^{2}$ is evaluated by traversing over _pairs_ of points
independently. The relationship between $\mathsf{ML}\xspace^{2}$ and
$\mathsf{MTL}\xspace$ is unclear: Arguably, pairs of points are a special case
of teams. But on the other hand, the modalities in $\mathsf{MTL}\xspace$ do
not act on the points in a team independently, as in $\mathsf{ML}\xspace^{2}$,
but instead always proceed to a successor team “synchronously”. As a
consequence, it is also open whether $\mathsf{MTL}\xspace$ can define one of
the above properties by a formula of elementary size.

##  6\. Enforcing a canonical model

In this section, we approach the canonical models of $\mathsf{MTL}\xspace$
from a lower bound perspective. Here, we devise an
$\mathsf{MTL}\xspace_{k}$-formula that is satisfiable but permits _only_
$k$-canonical models.

For $k=0$, that is propositional team logic, Hannula et al. [HKVV15] defined
the $\mathsf{PTL}\xspace$-formula

$\displaystyle\mathsf{max}(X)\vcentcolon={\sim}\bigvee_{\mathclap{x\in
X}}{=\\!\\!(x)}$

and proved that $T\vDash\mathsf{max}(\Phi)$ if and only if $T$ is
$0$-canonical, i.e., contains all Boolean assignment over $\Phi$. We
generalize this for all $k$, i.e., construct a satisfiable formula
$\mathsf{canon}_{k}$ that has only $k$-canonical models.

###  6.1. Staircase models

Our approach is to express $k$-canonicity by inductively enforcing
$i$-canonical sets of worlds for $i=0,\ldots,k$ located in different “height”
inside the model. For this purpose, we employ distinct scopes
$\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ (“ _stairs_ ”), and introduce a
specific class of models:

Let $k,i\geq 0$ and let $(\mathcal{K},T)$ be a Kripke structure with team,
$\mathcal{K}=(W,R,V)$. Then $T$ is _$k$ -canonical with offset $i$_ if for
every $\tau\in\Delta_{k}$ there exists $w\in T$ with
$\llbracket{}R^{i}w\rrbracket{}_{k}=\\{\tau\\}$. $(\mathcal{K},T)$ is called
_$k$ -staircase_ if for all $i\in\\{0,\ldots,k\\}$ we have that
$T_{\mathfrak{s}_{i}}$ is $i$-canonical with offset $k-i$.

$\mathfrak{s}_{0}$$\mathfrak{s}_{1}$$\mathfrak{s}_{2}$$\mathfrak{s}_{3}$,
$2^{2^{2^{2^{|\nobreak\Phi\nobreak|}}}}=16={|\nobreak\Delta_{3}\nobreak|}$
elements$\cdots$$\cdots$3-canonical2-canonical1-canonical0-c.OffsetScope:$T$
Figure 3. Visualization of the $3$-staircase for $\Phi=\emptyset$, where the
subteam $T_{\mathfrak{s}_{i}}$ is $i$-canonical with offset $3-i$.

As an example, a $3$-staircase for $\Phi=\emptyset$ is depicted in Figure 3.
Observe that it is a _directed forest_ , i.e., it is acyclic and all worlds
are either _roots_ (i.e., without predecessor) or have exactly one
predecessor. Moreover, it has bounded _height_ , where the height of a
directed forest is the greatest number $h$ such that every path traverses at
most $h$ edges.

######  Proposition 17.

For each $k\geq 0$, there is a finite $k$-staircase $(\mathcal{K},T)$ such
that $\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ are disjoint scopes in
$\mathcal{K}$, and $\mathcal{K}$ is a directed forest with height at most $k$
and its set of roots being exactly $T$.

######  Proof 6.1.

See Figure 3.

Observe that in such a model, $T_{\mathfrak{s}_{k}}$ is $k$-canonical with
offset $0$, which is simply $k$-canonical:

######  Corollary 18 (Finite tree model property of $\mathsf{MTL}\xspace$).

Every satisfiable $\mathsf{MTL}\xspace_{k}$-formula has a finite model
$(\mathcal{K},T)$ such that $\mathcal{K}$ is a directed forest with height at
most $k$ and its set of roots being exactly $T$.

###  6.2. Enforcing canonicity

In the rest of the section, we illustrate how a $k$-staircase can be enforced
in $\mathsf{MTL}\xspace$ inductively.

For $\Phi=\emptyset$, the inductive step—obtaining $(k+1)$-canonicity from
$k$-canonicity—is done by the formula
$\forall^{\subseteq}_{\alpha}\,\exists^{1}_{\beta}\,\Box\chi^{*}_{k}(\alpha,\beta)$.
The idea is that this formula states that for every _subteam_
$T^{\prime}\subseteq T_{\alpha}$ there exists a _point_ $w\in T_{\beta}$ such
that $\llbracket{}RT^{\prime}\rrbracket{}_{k}=\llbracket{}Rw\rrbracket{}_{k}$.
Intuitively, every possible set of types is captured as the image of some
point in $T_{\beta}$. As a consequence, if $T_{\alpha}$ is $k$-canonical with
offset $1$, then $T_{\beta}$ will be $(k+1)$-canonical.

Note that the simpler formula $\Box^{k}\mathsf{max}(\Phi)$ expresses
$0$-canonicity of $R^{k}T$, but not $0$-canonicity of $T$ with offset $k$
(consider, e.g., a singleton $T$). Instead, we use the formula

$\displaystyle\mathsf{max}_{i}\vcentcolon=\;$
$\displaystyle\top\lor(\Diamond^{i}\top\land{\sim}\bigvee_{\mathclap{p\in\Phi}}(\Diamond^{i}p\ovee\Diamond^{i}\neg
p))\text{.}$

It states not only that $R^{i}T$ is $0$-canonical, but also that $R^{i}w$
contains exactly one propositional assignment for each $w\in T$, which
together yields $0$-canonicity with offset $i$.

######  Lemma 19.

$T\vDash\mathsf{max}_{i}$ iff $T$ is $0$-canonical with offset $i$.

######  Proof 6.2.

By the distributive law
$\varphi\lor(\psi_{1}\ovee\psi_{2})\equiv(\varphi\lor\psi_{1})\ovee(\varphi\lor\psi_{2})$,
the duality
${\sim}(\psi_{1}\ovee\psi_{2})\equiv{\sim}\psi_{1}\land{\sim}\psi_{2}$, and
the definition $\mathsf{E}\psi={\sim}\neg\psi$,

${\sim}\bigvee_{\mathclap{p\in\Phi}}(\Diamond^{i}p\ovee\Diamond^{i}\neg
p)\equiv{\sim}\operatorname*{\scalerel*{\ovee}{\sum}}_{P\subseteq\Phi}\Big{(}\bigvee_{p\in
P}\Diamond^{i}p\lor\bigvee_{\mathclap{p\in\Phi\setminus P}}\Diamond^{i}\neg
p\Big{)}\equiv\bigwedge_{P\subseteq\Phi}\\!\\!\mathsf{E}\Big{(}\bigwedge_{p\in
P}\Box^{i}\neg p\land\bigwedge_{\mathclap{p\in\Phi\setminus
P}}\Box^{i}p\Big{)}\text{.}$

The rightmost formula now states that for all types $\tau\in\Delta_{0}$ (each
represented by a subset of $\Phi$, cf. Proposition 6), there exists a world
$w\in T$ such that
$\llbracket{}R^{i}w\rrbracket{}^{\Phi}_{0}\subseteq\\{\tau\\}$. Likewise,
$T\vDash\Diamond^{i}\top$ iff $R^{i}w\neq\emptyset$ for every $w\in T$.

Based on this, $k$-canonicity with offset $i$ is now recursively defined as
$\rho^{i}_{k}$:

$\displaystyle\rho^{i}_{0}(\beta)\,$
$\displaystyle\vcentcolon=\;\beta\hookrightarrow\mathsf{max}_{i}$
$\displaystyle\rho^{i}_{k+1}(\alpha,\beta)$
$\displaystyle\,\vcentcolon=\;\forall^{\subseteq}_{\alpha}\,\exists^{\subseteq}_{\beta}\left(\rho^{i}_{0}(\beta)\land\Box^{i}\forall^{1}_{\beta}\;\Box\chi^{*}_{k}(\alpha,\beta)\right)$
$\displaystyle\mathsf{canon}_{k}\,$
$\displaystyle\vcentcolon=\;\rho^{k}_{0}(\mathfrak{s}_{0})\land\bigwedge_{m=1}^{k}\rho^{k-m}_{m}(\mathfrak{s}_{m-1},\mathfrak{s}_{m})$

######  Theorem 20.

Let $k\geq 0$ and $\mathcal{K}$ be a structure with disjoint scopes
$\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$. Then
$(\mathcal{K},T)\vDash\mathsf{canon}_{k}$ if and only if $(\mathcal{K},T)$ is
a $k$-staircase. Moreover, $\mathsf{canon}_{k}$ is an
$\mathsf{MTL}\xspace_{k}$-formula constructible in space
${\mathcal{O}(\log({|\nobreak\Phi\nobreak|}+k))}$.

######  Proof 6.3.

Similar to Theorem 16, the construction of the above formula in logspace is
straightforward. We proceed with the correctness of the formula. Suppose that
$\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ are disjoint scopes in
$\mathcal{K}$. We show the following by induction on $0\leq i\leq k$: Assuming
that $T_{\alpha}$ is $k$-canonical with offset $i+1$, it holds that
$T_{\beta}$ is $(k+1)$-canonical with offset $i$ if and only if
$T\vDash\rho^{i}_{k+1}(\alpha,\beta)$. With the induction basis done in Lemma
19, the inductive step is proved by the following equivalence:

$\displaystyle T_{\beta}\text{ is }(k+1)\text{-canonical with offset }i$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\tau\in\Delta_{k+1}\colon\exists w\in
T_{\beta}\colon\llbracket{}R^{i}w\rrbracket{}_{k+1}=\\{\tau\\}$ Using the
inverse of the bijection $h\colon\tau\mapsto(\tau\cap\Phi,\mathcal{R}\tau)$
from Proposition 6, we can equivalently quantify over
$\mathfrak{P}(\Delta_{k})$ and $\mathfrak{P}(\Phi)$:
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\Phi^{\prime}\subseteq\Phi\colon\exists
w\in
T_{\beta}\colon\llbracket{}R^{i}w\rrbracket{}_{k+1}=\\{h^{-1}(\Phi^{\prime},\Delta^{\prime})\\}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\Phi^{\prime}\subseteq\Phi\colon\exists
w\in T_{\beta}\colon R^{i}w\neq\emptyset\text{ and }\forall v\in
R^{i}w\colon\llbracket{}v\rrbracket{}_{k+1}=h^{-1}(\Phi^{\prime},\Delta^{\prime})$
By Lemma 7, $V^{-1}(v)=\Phi^{\prime}\text{ and
}\llbracket{}Rv\rrbracket{}_{k}=\Delta^{\prime}$ is equivalent to
$\llbracket{}v\rrbracket{}_{k+1}=h^{-1}(\Phi^{\prime},\Delta^{\prime})$:
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\Phi^{\prime}\subseteq\Phi\colon\exists
w\in T_{\beta}\colon R^{i}w\neq\emptyset$ $\displaystyle\qquad\text{and
}\forall v\in R^{i}w\colon V^{-1}(v)=\Phi^{\prime}\text{ and
}\llbracket{}Rv\rrbracket{}_{k}=\Delta^{\prime}$ Again by Proposition 6,
$h\colon\tau\mapsto\tau\cap\Phi$ is a bijection from $\Delta_{0}$ to
$\mathfrak{P}(\Phi)$: $\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\tau_{0}\in\Delta_{0}\colon\exists
w\in T_{\beta}\colon R^{i}w\neq\emptyset$ $\displaystyle\qquad\text{and
}\forall v\in R^{i}w\colon V^{-1}(v)=\tau_{0}\cap\Phi\text{ and
}\llbracket{}Rv\rrbracket{}_{k}=\Delta^{\prime}$ Once more by Lemma 7:
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\tau_{0}\in\Delta_{0}\colon\exists
w\in T_{\beta}\colon R^{i}w\neq\emptyset$ $\displaystyle\qquad\text{and
}\forall v\in R^{i}w\colon\llbracket{}v\rrbracket{}_{0}=\tau_{0}\text{ and
}\llbracket{}Rv\rrbracket{}_{k}=\Delta^{\prime}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime}\subseteq\Delta_{k}\colon\forall\tau_{0}\in\Delta_{0}\colon\exists
w\in T_{\beta}\colon\llbracket{}R^{i}w\rrbracket{}_{0}=\\{\tau_{0}\\}\text{
and }\forall v\in R^{i}w\colon\llbracket{}Rv\rrbracket{}_{k}=\Delta^{\prime}$
Since $T_{\alpha}$ is assumed $k$-canonical with offset $i+1$, for every
$\tau^{\prime}\in\Delta_{k}$ there exists $u\in T_{\alpha}$ such that
$\llbracket{}R^{i+1}u\rrbracket{}_{k}=\\{\tau^{\prime}\\}$. Accordingly, for
every _set_ $\Delta^{\prime}\subseteq\Delta_{k}$ there exists $S\subseteq
T_{\alpha}$ such that $\llbracket{}R^{i+1}S\rrbracket{}_{k}=\Delta^{\prime}$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\forall\tau_{0}\in\Delta_{0}\colon\exists w\in
T_{\beta}\colon\llbracket{}R^{i}w\rrbracket{}_{0}=\\{\tau_{0}\\}\text{ and
}\forall v\in
R^{i}w\colon\llbracket{}Rv\rrbracket{}_{k}=\llbracket{}R^{i+1}S\rrbracket{}_{k}$
For each $S$, gather the respective $w$ in a team $U\subseteq T_{\beta}$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\exists U\subseteq
T_{\beta}\colon\left(\forall\tau_{0}\in\Delta_{0}\colon\exists w\in
U\colon\llbracket{}R^{i}w\rrbracket{}_{0}=\\{\tau_{0}\\}\right)$
$\displaystyle\qquad\qquad\text{ and }\forall v\in
R^{i}U\colon\llbracket{}Rv\rrbracket{}_{k}=\llbracket{}R^{i+1}S\rrbracket{}_{k}$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}:\exists U\subseteq T_{\beta}\colon U\text{ is $0$-canonical with
offset }i$ $\displaystyle\qquad\qquad\text{ and }\forall v\in
R^{i}U\colon\llbracket{}Rv\rrbracket{}_{k}=\llbracket{}R^{i+1}S\rrbracket{}_{k}$
By the base case $k=0$, and since $U={(T^{\alpha,\beta}_{S,U})}_{\beta}$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\text{ and }\forall v\in
R^{i}U\colon\llbracket{}Rv\rrbracket{}_{k}=\llbracket{}R^{i+1}S\rrbracket{}_{k}$
By Theorem 16: $\displaystyle\Leftrightarrow\;$ $\displaystyle\forall
S\subseteq T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\text{ and }\forall v\in
R^{i}U\colon{(R^{i+1}T)}^{\alpha,\beta}_{R^{i+1}S,Rv}\vDash\chi^{*}_{k}(\alpha,\beta)$
By Proposition 14 (5.): $\displaystyle\Leftrightarrow\;$ $\displaystyle\forall
S\subseteq T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\text{ and }\forall v\in
R^{i}U\colon{(R^{i}T)}^{\alpha,\beta}_{R^{i}S,v}\vDash\Box\chi^{*}_{k}(\alpha,\beta)$
By Proposition 15 applied to ${(R^{i}T)}^{\alpha,\beta}_{R^{i}S,R^{i}U}$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\text{ and
}{(R^{i}T)}^{\alpha,\beta}_{R^{i}S,R^{i}U}\vDash\forall^{1}_{\beta}\Box\chi^{*}_{k}(\alpha,\beta)$
Again by Proposition 14 (5.) and Proposition 15:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\text{ and
}R^{i}\left(T^{\alpha,\beta}_{S,U}\right)\vDash\forall^{1}_{\beta}\Box\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall S\subseteq
T_{\alpha}\colon\exists U\subseteq T_{\beta}\colon
T^{\alpha,\beta}_{S,U}\vDash\rho^{i}_{0}(\beta)\land\Box^{i}\forall^{1}_{\beta}\Box\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\forall^{\subseteq}_{\alpha}\,\exists^{\subseteq}_{\beta}\,(\rho^{i}_{0}(\beta)\land\Box^{i}\forall^{1}_{\beta}\Box\chi^{*}_{k}(\alpha,\beta))$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\rho^{i}_{k+1}(\alpha,\beta)\text{.}$

###  6.3. Enforcing scopes

As the next step, we lift the restriction of the $\mathfrak{s}_{i}$ being
scopes _a priori_. In a sense, this condition is definable in
$\mathsf{MTL}\xspace$ as well. For this, let $\Psi\subseteq\mathcal{PS}$ be
disjoint from $\Phi$. Then the formula below ensures that $\Psi$ is a set of
disjoint scopes “up to height $k$”.

$\displaystyle\mathsf{scopes}_{k}(\Psi)$
$\displaystyle\vcentcolon=\bigwedge_{\begin{subarray}{c}x,y\in\Psi\\\ x\neq
y\end{subarray}}\neg(x\land
y)\land\bigwedge_{i=1}^{k}\Big{(}(x\land\Box^{i}x)\lor(\neg x\land\Box^{i}\neg
x)\Big{)}\text{.}$

The definition up to height $k$ is sufficient for our purposes, which follows
from the next lemma.

######  Lemma 21.

If $\varphi\in\mathsf{MTL}\xspace_{k}$, then $\varphi$ is satisfiable if and
only if $\varphi\land\Box^{k+1}\bot$ is satisfiable.

######  Proof 6.4.

As the direction from right to left is trivial, suppose $\varphi$ is
satisfiable. By Corollary 18, it then has a model $(\mathcal{K},T)$ that is a
directed forest of height at most $k$. But then
$(\mathcal{K},T)\vDash\Box^{k+1}\bot$, since $R^{k+1}T=\emptyset$ and
$(\mathcal{K},\emptyset)$ satisfies all $\mathsf{ML}\xspace$-formulas,
including $\bot$.

######  Theorem 22.

$\mathsf{canon}_{k}\land\mathsf{scopes}_{k}(\\{\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}\\})\land\Box^{k+1}\bot$
is satisfiable, but has only $k$-staircases as models.

######  Proof 6.5.

By combining Proposition 17, Theorem 20 and Lemma 21, the formula is
satisfiable. Since in every model $(\mathcal{K},T)$ the propositions
$\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ must be disjoint scopes due to
$\Box^{k+1}\bot$ and $\mathsf{scopes}_{k}$, we can apply Theorem 20.

As for bisimilarity, it is open whether $(\Phi,k)$-canonicity can be defined
in $\mathsf{MTL}\xspace^{\Phi}_{k}$ _efficiently_ without restricting the
models to those with scopes. Note that the results of this section alone do
not imply that the brute force algorithm given in Theorem 12 is optimal, as
there could possibly be a satisfiability algorithm that does not need to
construct a model. To show proper complexity theoretic hardness, we need to
encode non-elementary computations in such models, to which we will proceed in
the next sections.

##  7\. Defining an order on types

In the previous section, we enforced $k$-canonicity with a formula, i.e., such
that ${|\nobreak\Delta_{k}\nobreak|}$ different types are contained in the
team. In order to encode computations of length
${|\nobreak\Delta_{k}\nobreak|}$, we additionally need to be able to talk
about an ordering of $\Delta_{k}$.

Let us call any finite strict linear ordering simply an _order_. We specify an
order $\prec_{k}$ on $\Delta_{k}$, and analogously to team bisimilarity, an
order $\prec^{*}_{k}$ on $\mathfrak{P}(\Delta_{k})$. To begin with, let us
first agree on some arbitrary order $<$ on $\Phi$, say,
$p_{1}<p_{2}<\cdots<p_{{|\nobreak\Phi\nobreak|}}$. Furthermore, if $\sqsubset$
is some order on $X$, then the _lexicographic order_ $\sqsubset^{*}$ on
$\mathfrak{P}(X)$ is defined by

$\displaystyle X_{1}\sqsubset^{*}X_{2}\text{ iff }\exists x\in X_{2}\setminus
X_{1}\text{ such that }\forall x^{\prime}\in X\colon(x\sqsubset
x^{\prime})\Rightarrow(x^{\prime}\in X_{1}\Leftrightarrow x^{\prime}\in
X_{2})\text{.}$

For example, let $X=\\{0,1\\}$ and $0\sqsubset 1$. Then
$\emptyset\sqsubset^{*}\\{0\\}\sqsubset^{*}\\{1\\}\sqsubset^{*}\\{0,1\\}$. The
order $\prec_{k}$ depends on the propositions true in a world, and otherwise
recursively on the lexicographic order of the image team:

$\displaystyle\tau\prec_{0}\tau^{\prime}\;$
$\displaystyle\Leftrightarrow\;\tau\cap\Phi<^{*}\tau^{\prime}\cap\Phi\text{,}$
$\displaystyle\tau\prec_{k+1}\tau^{\prime}\;$
$\displaystyle\Leftrightarrow\;\tau\cap\Phi<^{*}\tau^{\prime}\cap\Phi\text{ or
}(\tau\cap\Phi=\tau^{\prime}\cap\Phi\text{ and
}\mathcal{R}\tau\;\prec_{k}^{*}\;\mathcal{R}\tau^{\prime})\text{.}$

It is easy to verify by induction that $\prec_{k}$ and $\prec^{*}_{k}$ are
orders on $\Delta_{k}$ and $\mathfrak{P}(\Delta_{k})$, respectively.

The next step is to prove that $\prec_{k}$ and $\prec^{*}_{k}$ are
(efficiently) definable in $\mathsf{MTL}\xspace_{k}$. For this, we pursue the
same approach as for $\chi_{k}$ and $\chi^{*}_{k}$ in Section 5, and show that
$\prec_{k}$ and $\prec^{*}_{k}$ are definable in formulas $\zeta_{k}$ and
$\zeta^{*}_{k}$ in a mutually recursive fashion. Since order is a binary
relation, the formulas below are once more parameterized by two scopes.

$\displaystyle\zeta_{0}(\alpha,\beta)$
$\displaystyle\vcentcolon=\bigvee_{p\in\Phi}\Big{[}(\alpha\hookrightarrow\neg
p)\land(\beta\hookrightarrow p)\land\bigwedge_{\begin{subarray}{c}q\in\Phi\\\
q<p\end{subarray}}(\alpha\lor\beta)\hookrightarrow{=\\!\\!(q)}\Big{]}$
$\displaystyle\zeta_{k+1}(\alpha,\beta)$
$\displaystyle\vcentcolon=\zeta_{0}(\alpha,\beta)\,\ovee\,\chi_{0}(\alpha,\beta)\land\,\Box\zeta^{*}_{k}(\alpha,\beta)$
$\displaystyle\zeta^{*}_{k}(\alpha,\beta)$
$\displaystyle\vcentcolon=\exists^{1}_{\mathfrak{s}_{k}}\left(\exists^{1}_{\beta}\chi_{k}(\mathfrak{s}_{k},\beta)\right)\land\left({\sim}\exists^{1}_{\alpha}\chi_{k}(\mathfrak{s}_{k},\alpha)\right)$
$\displaystyle\qquad\land\Big{(}\big{(}\chi^{*}_{k}(\alpha,\beta)\land(\alpha\lor\beta)\big{)}\,\lor\,\big{(}\forall^{1}_{\alpha\lor\beta}{\sim}\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)\big{)}\Big{)}$

Note that we make use of the scopes $\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$
in the formula, and in the following we restrict ourselves to $k$-staircase
models. Moreover, in the subformula
$\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$, we use the fact that
$\alpha\lor\beta$ is a scope whenever $\alpha,\beta$ are scopes.

We require the next lemma for the correctness of $\zeta_{k}$ and
$\zeta^{*}_{k}$. Intuitively, it states that $\mathsf{MTL}\xspace_{k}$ is
invariant under substitution of “locally equivalent”
$\mathsf{ML}\xspace$-formulas.

######  Lemma 23.

Let $\alpha,\beta\in\mathsf{ML}\xspace$ and
$\varphi\in\mathsf{MTL}\xspace_{k}$. Let $T$ be a team such that
$R^{i}T\vDash\alpha\leftrightarrow\beta$ for all $i\in\\{0,\ldots,k\\}$. Then
$T\vDash\varphi$ if and only if $T\vDash\mathrm{Sub}(\varphi,\alpha,\beta)$,
where $\mathrm{Sub}(\varphi,\alpha,\beta)$ is the formula obtained from
$\varphi$ by substituting every occurrence of $\alpha$ with $\beta$.

######  Proof 7.1.

By straightforward induction; see the appendix.

The following theorem states that in the class of $k$-staircase models (see
the previous section) $\zeta_{k}$ and $\zeta^{*}_{k}$ define the required
orders.

######  Theorem 24.

Let $k\geq 0$, and let $(\mathcal{K},T)$ be a $k$-staircase with disjoint
scopes $\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$. If $w\in
T_{\alpha}$ and $v\in T_{\beta}$, then

$\displaystyle T^{\alpha,\beta}_{w,v}$
$\displaystyle\;\vDash\;\zeta_{k}(\alpha,\beta)\;$ if and only if
$\displaystyle\llbracket{}w\rrbracket{}_{k}$
$\displaystyle\prec_{k}\llbracket{}v\rrbracket{}_{k}\text{,}$ $\displaystyle
T$ $\displaystyle\;\vDash\;\zeta^{*}_{k}(\alpha,\beta)\;$ if and only if
$\displaystyle\llbracket{}T_{\alpha}\rrbracket{}_{k}$
$\displaystyle\prec^{*}_{k}\llbracket{}T_{\beta}\rrbracket{}_{k}\text{.}$

Furthermore, both $\zeta_{k}(\alpha,\beta)$ and $\zeta^{*}_{k}(\alpha,\beta)$
are $\mathsf{MTL}\xspace_{k}$-formulas that are constructible in space
${\mathcal{O}(\log(k+{|\nobreak\Phi\nobreak|}+{|\nobreak\alpha\nobreak|}+{|\nobreak\beta\nobreak|}))}$.

We first give a rough idea of the proof, and after a series of required lemmas
fully prove the theorem. The definition of $\zeta_{k+1}$ simply follows the
definition of $\prec_{k+1}$. Furthermore, the formula $\zeta^{*}_{k}$
implements the lexicographic order $\prec^{*}_{k}$ as follows. As shown in
Figure 4, we first choose some $z\in T_{\mathfrak{s}_{k}}$ that acts as an
_pivot_ to determine if
$\llbracket{}T_{\alpha}\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}T_{\beta}\rrbracket{}$,
in the sense that it is the $\prec_{k}$-maximal type in which $T_{\alpha}$ and
$T_{\beta}$ differ.333Since the pivot is selected from $T_{\mathfrak{s}_{k}}$,
at this point it is crucial that the underlying structure is a $k$-staircase.
The first line of $\zeta^{*}_{k}$ indeed expresses that
$\llbracket{}z\rrbracket{}_{k}\in\llbracket{}T_{\beta}\rrbracket{}_{k}\setminus\llbracket{}T_{\alpha}\rrbracket{}_{k}$.

The disjunction in the second line intuitively states that we then can “split
off” the subteam of $T_{\alpha}\cup T_{\beta}$ consisting of the elements
$\prec_{k}$-greater than $z$ (the solid green area in Figure 4), while
$\chi^{*}_{k}$ ensures that they agree on the contained types (this reflects
the part after the quantifier in the definition of $\sqsubset^{*}$). To
achieve this, the subformula
$\forall^{1}_{\alpha\lor\beta}{\sim}\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$
stipulates that any “remaining” elements from $T_{\alpha}\cup T_{\beta}$
possess only types not $\prec_{k}$-greater than
$\llbracket{}z\rrbracket{}_{k}$ (the dashed green area in the figure).

Here, Lemma 23 is applied, as it ensures that after processing
$\forall^{1}_{\alpha\lor\beta}$ the formula
$\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$ in fact behaves as either
$\zeta_{k}(\mathfrak{s}_{k},\alpha)$ or $\zeta_{k}(\mathfrak{s}_{k},\beta)$;
and hence behaves correctly by induction hypothesis.

$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}T_{\beta}\;\hat{=}\;\mathbf{10\underline{1}}000$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\scriptstyle\succ_{k}$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T_{\alpha}\;\hat{=}\;\mathbf{10\underline{0}}110$$T_{\mathfrak{s}_{k}}$$z$$\prec^{*}_{k}$
?$\succ_{k}$$\rightleftharpoons_{k}\;$$\quad\preceq_{k}$ Figure 4. The pivot
$z\in T_{\mathfrak{s}_{k}}$ determines that
$\llbracket{}T_{\alpha}\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}T_{\beta}\rrbracket{}_{k}$.
The subteam of $T_{\alpha\lor\beta}$ of worlds $\prec_{k}$-greater than $z$
must satisfy $\chi^{*}_{k}(\alpha,\beta)$.

Let $k\geq 0$. Let $\alpha,\beta$ be disjoint scopes and $T$ a team in a
Kripke structure. Then $\alpha$ and $\beta$ are called _$\prec_{k}$
-comparable in $T$_ if for all $w\in T_{\alpha},v\in T_{\beta}$

$\displaystyle T^{\alpha,\beta}_{w,v}$
$\displaystyle\vDash\zeta_{k}(\alpha,\beta)\text{ iff
}\llbracket{}w\rrbracket{}_{k}\prec_{k}\llbracket{}v\rrbracket{}_{k}\text{
and}$ $\displaystyle T^{\alpha,\beta}_{w,v}$
$\displaystyle\vDash\zeta_{k}(\beta,\alpha)\text{ iff
}\llbracket{}v\rrbracket{}_{k}\prec_{k}\llbracket{}w\rrbracket{}_{k}\text{.}$

Likewise, $\alpha$ and $\beta$ are _$\prec^{*}_{k}$ -comparable in $T$_ if

$\displaystyle T$ $\displaystyle\vDash\zeta^{*}_{k}(\alpha,\beta)\text{ iff
}\llbracket{}T_{\alpha}\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}T_{\beta}\rrbracket{}_{k}\text{
and}$ $\displaystyle T$ $\displaystyle\vDash\zeta^{*}_{k}(\beta,\alpha)\text{
iff
}\llbracket{}T_{\beta}\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}T_{\alpha}\rrbracket{}_{k}\text{.}$

The next lemma shows that the correctness of $\prec^{*}_{k}$ follows from that
of $\prec_{k}$.

######  Lemma 25.

Suppose that $(\mathcal{K},T)$ is a $k$-staircase with disjoint scopes
$\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$. If both $\alpha$ and
$\beta$ are $\prec_{k}$-comparable to $\mathfrak{s}_{k}$ in all subteams $S$
of the form $T_{\mathfrak{s}_{0}}\cup\cdots\cup
T_{\mathfrak{s}_{k-1}}\subseteq S\subseteq T$, then $\alpha$ and $\beta$ are
$\prec_{k}^{*}$-comparable in $T$.

######  Proof 7.2.

Assuming $\mathcal{K},T,\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$
as above, the proof is split into the following claims.

######  Claim 26 (a).

The disjoint scopes $\alpha\lor\beta$ and $\mathfrak{s}_{k}$ are
$\prec_{k}$-comparable in any team $S$ that satisfies
$T_{\mathfrak{s}_{0}}\cup\cdots\cup T_{\mathfrak{s}_{k-1}}\subseteq S\subseteq
T$.

######  Proof 7.3 (Proof of claim.).

Let $w\in S_{\alpha\lor\beta}$ and $v\in S_{\mathfrak{s}_{k}}$. W.l.o.g.$w\in
S_{\alpha}$ (the case $w\in S_{\beta}$ works analogously). Then

$\displaystyle
S^{\alpha\lor\beta,\mathfrak{s}_{k}}_{w,v}\vDash\zeta_{k}(\alpha\lor\beta,\mathfrak{s}_{k})$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
S^{\alpha,\beta,\mathfrak{s}_{k}}_{w,\emptyset,v}\vDash\zeta_{k}(\alpha\lor\beta,\mathfrak{s}_{k})$
(Since
$S^{\alpha\lor\beta,\mathfrak{s}_{k}}_{w,v}=S^{\alpha,\beta,\mathfrak{s}_{k}}_{w,\emptyset,v}$)
$\displaystyle\Leftrightarrow\;$ $\displaystyle
S^{\alpha,\beta,\mathfrak{s}_{k}}_{w,\emptyset,v}\vDash\zeta_{k}(\alpha,\mathfrak{s}_{k})$
(By Lemma 23, as
$\bigcup_{i=0}^{k}R^{i}S^{\alpha,\beta,\mathfrak{s}_{k}}_{w,\emptyset,v}\vDash\alpha\leftrightarrow(\alpha\lor\beta)$)
$\displaystyle\Leftrightarrow\;$
$\displaystyle\llbracket{}w\rrbracket{}_{k}\prec_{k}\llbracket{}v\rrbracket{}_{k}\text{.}$
(By assumption of the lemma)

The case $\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$ is symmetric.
$\triangleleft$

For the remaining proof, we omit the subscript $k$ when referring to types and
$\prec$. Furthermore, for all $\tau\in\Delta_{k}$, let
$\llbracket{}T\rrbracket{}^{\tau}$ denote the restriction of
$\llbracket{}T\rrbracket{}$ to types $\tau^{\prime}$ such that
$\tau^{\prime}\succ\tau$. Intuitively, these types are the “more significant
positions” for the lexicographic ordering. In the next claim, we essentially
show that the second line in the definition of $\zeta^{*}_{k}(\alpha,\beta)$
can be expressed as a statement of the form
$\llbracket{}T_{\alpha}\rrbracket{}^{\tau}=\llbracket{}T_{\beta}\rrbracket{}^{\tau}$.

######  Claim 27 (b).

Let $T$ be a team and $\tau\in\Delta_{k}$. Then
$\llbracket{}T_{\alpha}\rrbracket{}^{\tau}=\llbracket{}T_{\beta}\rrbracket{}^{\tau}$
if and only if there exists $S\subseteq T_{\alpha\lor\beta}$ such that
$\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}S_{\beta}\rrbracket{}$ and
$\llbracket{}w\rrbracket{}\nsucc\tau$ for all $w\in
T_{\alpha\lor\beta}\setminus S$.

######  Proof 7.4 (Proof of claim.).

“$\Rightarrow$”: Let $S\vcentcolon=\\{v\in
T_{\alpha\lor\beta}\mid\llbracket{}v\rrbracket{}\succ\tau\\}$. Then
$\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}T_{\alpha}\rrbracket{}^{\tau}=\llbracket{}T_{\beta}\rrbracket{}^{\tau}=\llbracket{}S_{\beta}\rrbracket{}$.
Moreover, for every $w\in T_{\alpha\lor\beta}\setminus S$ clearly
$\llbracket{}w\rrbracket{}\nsucc\tau$ holds.

“$\Leftarrow$”: Assume that $S$ exists as stated in the claim. By symmetry, we
only prove
$\llbracket{}T_{\alpha}\rrbracket{}^{\tau}\subseteq\llbracket{}T_{\beta}\rrbracket{}^{\tau}$.
Consequently, let $w\in T_{\alpha}$ such that
$\llbracket{}w\rrbracket{}\in\llbracket{}T_{\alpha}\rrbracket{}^{\tau}$. Then
$\llbracket{}w\rrbracket{}\succ\tau$ by definition. But then $w\notin
T_{\alpha\lor\beta}\setminus S$. However, we have $w\in T_{\alpha}$, hence
$w\in T_{\alpha\lor\beta}$, which only leaves the possibility $w\in S$.
Combining $w\in S$ and $w\in T_{\alpha}$ yields $w\in S_{\alpha}$, which by
assumption also implies
$\llbracket{}w\rrbracket{}\in\llbracket{}S_{\beta}\rrbracket{}$. As
$\llbracket{}S_{\beta}\rrbracket{}\subseteq\llbracket{}T_{\beta}\rrbracket{}$
and $\llbracket{}w\rrbracket{}\succ\tau$, the membership
$\llbracket{}w\rrbracket{}\in\llbracket{}T_{\beta}\rrbracket{}^{\tau}$
follows. $\triangleleft$

######  Claim 28 (c).

$\alpha$ and $\beta$ are $\prec^{*}_{k}$-comparable in $T$.

######  Proof 7.5 (Proof of claim.).

Due to symmetry, we prove only that $T\vDash\zeta^{*}_{k}(\alpha,\beta)$ iff
$\llbracket{}T_{\alpha}\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}T_{\beta}\rrbracket{}_{k}$.

$\displaystyle\llbracket{}T_{\alpha}\rrbracket{}\prec^{*}\llbracket{}T_{\beta}\rrbracket{}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\tau\in\llbracket{}T_{\beta}\rrbracket{}\setminus\llbracket{}T_{\alpha}\rrbracket{}\colon\forall\tau^{\prime}\in\Delta,\tau\prec\tau^{\prime}\colon\tau^{\prime}\in\llbracket{}T_{\alpha}\rrbracket{}\Leftrightarrow\tau^{\prime}\in\llbracket{}T_{\beta}\rrbracket{}$
(Definition of $\prec^{*}_{k}$) $\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\tau\in\llbracket{}T_{\beta}\rrbracket{}\setminus\llbracket{}T_{\alpha}\rrbracket{}\colon\llbracket{}T_{\alpha}\rrbracket{}^{\tau}=\llbracket{}T_{\beta}\rrbracket{}^{\tau}$
(Definition of $\llbracket{}\cdot\rrbracket{}^{\tau}$) Since
$T_{\mathfrak{s}_{k}}$ is $k$-canonical, for every $\tau\in\Delta$ there
exists $z\in T_{\mathfrak{s}_{k}}$ of type $\tau$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon\llbracket{}T_{\alpha}\rrbracket{}^{\llbracket{}z\rrbracket{}}=\llbracket{}T_{\beta}\rrbracket{}^{\llbracket{}z\rrbracket{}}\text{
and
}\llbracket{}z\rrbracket{}\in\llbracket{}T_{\beta}\rrbracket{}\setminus\llbracket{}T_{\alpha}\rrbracket{}$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon\llbracket{}T_{\alpha}\rrbracket{}^{\llbracket{}z\rrbracket{}}=\llbracket{}T_{\beta}\rrbracket{}^{\llbracket{}z\rrbracket{}}\text{
and }\exists x\in
T_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
T_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}$ As
$\alpha,\beta$ and $\mathfrak{s}_{k}$ are disjoint, we have
$T_{\alpha}=O_{\alpha}$, where $O\vcentcolon=T^{\mathfrak{s}_{k}}_{z}$, and
likewise $T_{\beta}=O_{\beta}$: $\displaystyle\Leftrightarrow\;$
$\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon\llbracket{}O_{\alpha}\rrbracket{}^{\llbracket{}z\rrbracket{}}=\llbracket{}O_{\beta}\rrbracket{}^{\llbracket{}z\rrbracket{}}\text{
and }\exists x\in
O_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
O_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon\exists x\in
O_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
O_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}$
$\displaystyle\text{ and }\exists S\subseteq
O_{\alpha\lor\beta}\colon\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}S_{\beta}\rrbracket{}\text{
and }\forall w\in O_{\alpha\lor\beta}\setminus
S\colon\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$ (by Claim
(b)) Clearly $S$ is a subteam of $O_{\alpha\lor\beta}$ if and only if it is a
subteam of $O$ and satisfies $\alpha\lor\beta$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon\exists x\in
O_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
O_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}$
$\displaystyle\text{ and }\exists S\subseteq
O\colon\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}S_{\beta}\rrbracket{}\text{
and }S\vDash\alpha\lor\beta\text{ and }\forall w\in
O_{\alpha\lor\beta}\setminus
S\colon\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$ Letting
$U=O\setminus S$, we have $O_{\alpha\lor\beta}\setminus
S=U_{\alpha\lor\beta}$: $\displaystyle\Leftrightarrow\;$ $\displaystyle\exists
z\in T_{\mathfrak{s}_{k}}\colon\exists x\in
O_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
O_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}\text{ and
}\exists S\subseteq O\colon$
$\displaystyle\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}S_{\beta}\rrbracket{}\text{
and }S\vDash\alpha\lor\beta\text{ and }\exists U\subseteq O\colon U=O\setminus
S\text{ and }\forall w\in
U_{\alpha\lor\beta}\colon\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$
Clearly, the property $\forall w\in
U_{\alpha\lor\beta}:\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$
is preserved when taking subteams of $U$. Hence, $U=O\setminus S$ satisfies it
if and only if some (not necessarily proper) superteam $U^{\prime}$ of
$O\setminus S$ does: $\displaystyle\Leftrightarrow\;$ $\displaystyle\exists
z\in T_{\mathfrak{s}_{k}}\colon\exists x\in
O_{\beta}\colon\llbracket{}z\rrbracket{}=\llbracket{}x\rrbracket{}\text{ and
}\nexists y\in
O_{\alpha}\colon\llbracket{}z\rrbracket{}=\llbracket{}y\rrbracket{}$
$\displaystyle\text{ and }\exists S\subseteq
O\colon\llbracket{}S_{\alpha}\rrbracket{}=\llbracket{}S_{\beta}\rrbracket{}\text{
and }S\vDash\alpha\lor\beta$ $\displaystyle\qquad\text{ and }\exists
U^{\prime}\subseteq O\colon U^{\prime}\supseteq O\setminus S\text{ and
}\forall w\in
U^{\prime}_{\alpha\lor\beta}\colon\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$
By Theorem 16: $\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon
O\vDash(\exists^{1}_{\beta}\chi_{k}(\mathfrak{s},\beta))\land({\sim}\exists^{1}_{\alpha}\chi_{k}(\mathfrak{s},\alpha))\text{
and }\exists S\subseteq O\colon$ $\displaystyle
S\vDash(\alpha\lor\beta)\land\chi^{*}_{k}(\alpha,\beta)\text{ and }\exists
U^{\prime}\subseteq O\colon U^{\prime}\supseteq O\setminus S\text{ and
}\forall w\in
U^{\prime}_{\alpha\lor\beta}\colon\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$
Note that $T_{\mathfrak{s}_{0}},\ldots,T_{\mathfrak{s}_{k-1}}$ are retained in
$O$. Moreover, $S\subseteq O_{\alpha\lor\beta}$, which implies that they are
still subteams of $O\setminus S$ and hence of $U^{\prime}$. But by Claim (a),
$\alpha\lor\beta$ and $\mathfrak{s}_{k}$ are then $\prec_{k}$-comparable
scopes in $U^{\prime}$ and we can replace
$\llbracket{}z\rrbracket{}\nprec\llbracket{}w\rrbracket{}$:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon
O\vDash(\exists^{1}_{\beta}\chi_{k}(\mathfrak{s},\beta))\land({\sim}\exists^{1}_{\alpha}\chi_{k}(\mathfrak{s},\alpha))$
$\displaystyle\text{ and }\exists S\subseteq O\colon
S\vDash(\alpha\lor\beta)\land\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\qquad\text{ and }\exists U^{\prime}\subseteq O\colon
U^{\prime}\supseteq O\setminus S\text{ and }\forall w\in
U^{\prime}_{\alpha\lor\beta}\colon{(U^{\prime})}^{\alpha\lor\beta}_{w}\vDash{\sim}\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$
Recalling that $O=T^{\mathfrak{s}_{k}}_{z}$, and by Proposition 15, we obtain:
$\displaystyle\Leftrightarrow\;$ $\displaystyle\exists z\in
T_{\mathfrak{s}_{k}}\colon
T^{\mathfrak{s}_{k}}_{z}\vDash(\exists^{1}_{\beta}\chi_{k}(\mathfrak{s},\beta))\land({\sim}\exists^{1}_{\alpha}\chi_{k}(\mathfrak{s},\alpha))$
$\displaystyle\text{ and }\exists S\subseteq T^{\mathfrak{s}_{k}}_{z}\colon
S\vDash(\alpha\lor\beta)\land\chi^{*}_{k}(\alpha,\beta)$
$\displaystyle\qquad\text{ and }\exists U^{\prime}\subseteq
T^{\mathfrak{s}_{k}}_{z}\colon U^{\prime}\supseteq
T^{\mathfrak{s}_{k}}_{z}\setminus S\text{ and
}U^{\prime}\vDash\forall^{1}_{\alpha\lor\beta}{\sim}\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\exists^{1}_{\mathfrak{s}_{k}}(\exists^{1}_{\beta}\chi_{k}(\mathfrak{s},\beta))\land({\sim}\exists^{1}_{\alpha}\chi_{k}(\mathfrak{s},\alpha))$
$\displaystyle\land\big{(}(\alpha\lor\beta)\land\chi^{*}_{k}(\alpha,\beta)\big{)}\lor\big{(}\forall^{1}_{\alpha\lor\beta}{\sim}\zeta_{k}(\mathfrak{s}_{k},\alpha\lor\beta)\big{)}$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\zeta^{*}(\alpha,\beta)\text{.}$ $\triangleleft$∎

In the next lemma, we prove the converse direction of Lemma 25.

######  Lemma 29.

Let $k>0$, and let $(\mathcal{K},T)$ be a $k$-staircase with disjoint scopes
$\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k-1}$. Then $\alpha$ and
$\beta$ are $\prec_{k}$-comparable in every subteam $S$ of $T$ that contains
$T_{\mathfrak{s}_{0}}\cup\cdots\cup T_{\mathfrak{s}_{k-1}}$.

######  Proof 7.6.

The proof is by induction on $k$. Disjoint scopes $\alpha$ and $\beta$ are
always $\prec_{0}$-comparable, which can be easily seen in $\zeta_{0}$. For
the inductive step to $k+1$, assume $(\mathcal{K},T)$ and $S$ as above, and
let $\mathcal{K}=(W,R,V)$. Let $O\vcentcolon=S^{\alpha,\beta}_{w,v}$ with
$w\in S_{\alpha},v\in S_{\beta}$ arbitrary.

######  Claim 30 (a).

$\alpha$ and $\beta$ are $\prec^{*}_{k}$-comparable in $RO$.

######  Proof 7.7 (Proof of claim.).

In the inductive step, now
$\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k},\alpha,\beta$ are disjoint scopes.
Additionally, $(\mathcal{K},RT)$ is a $k$-staircase. In particular, in the
induction step $\alpha$ and $\beta$ are disjoint from $\mathfrak{s}_{k}$. For
this reason, $(\mathcal{K},RO)$ is a $k$-staircase as well, as
${(RO)}_{\mathfrak{s}_{0}\lor\cdots\lor\mathfrak{s}_{k}}={(RT)}_{\mathfrak{s}_{0}\lor\cdots\lor\mathfrak{s}_{k}}$.

Hence, by induction hypothesis, for every team $U$ such that
$RO_{\mathfrak{s}_{0}}\cup\cdots\cup RO_{\mathfrak{s}_{k-1}}\subseteq
U\subseteq RO$, we obtain that $\mathfrak{s}_{k}$ and $\alpha$ are
$\prec_{k}$-comparable in $U$, as well as $\mathfrak{s}_{k}$ and $\beta$.
Consequently, we can apply Lemma 25, which proves the claim. $\triangleleft$

We proceed with the induction step. Again by symmetry, we only show that
$O\vDash\zeta_{k+1}(\alpha,\beta)$ iff
$\llbracket{}w\rrbracket{}_{k+1}\prec_{k+1}\llbracket{}v\rrbracket{}_{k+1}$.
We distinguish three cases w. r. t.$\prec_{0}$:

  * •

If $\llbracket{}w\rrbracket{}_{0}\prec_{0}\llbracket{}v\rrbracket{}_{0}$, then
$O\vDash\zeta_{0}(\alpha,\beta)$ by the induction basis. As the former implies
$\llbracket{}w\rrbracket{}_{k+1}\prec_{k+1}\llbracket{}v\rrbracket{}_{k+1}$
and the latter $O\vDash\zeta_{k+1}(\alpha,\beta)$, the equivalence holds.

  * •

If $\llbracket{}w\rrbracket{}_{0}\succ_{0}\llbracket{}v\rrbracket{}_{0}$, then
$\llbracket{}w\rrbracket{}_{k+1}\nprec_{k+1}\llbracket{}v\rrbracket{}_{k+1}$.
Moreover, $O\nvDash\zeta_{0}(\alpha,\beta)$ by induction basis. Additionally,
$O\nvDash\chi_{0}(\alpha,\beta)$ by Theorem 16. Consequently, both sides of
the equivalence are false.

  * •

If $\llbracket{}w\rrbracket{}_{0}=\llbracket{}v\rrbracket{}_{0}$, then
$O\vDash\chi_{0}(\alpha,\beta)$ by Theorem 16, but
$O\nvDash\zeta_{0}(\alpha,\beta)$ by induction basis. Consequently,
$O\vDash\zeta_{k+1}(\alpha,\beta)$ iff
$O\vDash\Box\zeta^{*}_{k}(\alpha,\beta)$. Also,
$\llbracket{}w\rrbracket{}_{k+1}\prec_{k+1}\llbracket{}v\rrbracket{}_{k+1}$
iff
$\mathcal{R}\llbracket{}w\rrbracket{}_{k+1}\prec^{*}_{k}\mathcal{R}\llbracket{}v\rrbracket{}_{k+1}$.
The following equivalence concludes the proof:

$\displaystyle\mathcal{R}\llbracket{}w\rrbracket{}_{k+1}\prec^{*}_{k}\mathcal{R}\llbracket{}v\rrbracket{}_{k+1}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\llbracket{}Rw\rrbracket{}_{k}\prec^{*}_{k}\llbracket{}Rv\rrbracket{}_{k}$
(By Proposition 6) $\displaystyle\Leftrightarrow\;$ $\displaystyle
RO\vDash\zeta^{*}_{k}(\alpha,\beta)$ (By Claim (a))
$\displaystyle\Leftrightarrow\;$ $\displaystyle
O\vDash\Box\zeta^{*}_{k}(\alpha,\beta)\text{.}$

With the above lemmas we are now in the position to prove Theorem 24:

######  Proof 7.8 (Proof of Theorem 24).

First, it is straightforward to construct $\zeta_{k}$ and $\zeta^{*}_{k}$ in
logarithmic space. For the correctness, let $(\mathcal{K},T)$ be a model with
disjoint scopes $\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ as in
the theorem. By Lemma 29 it immediately follows that $\alpha$ and $\beta$ are
$\prec_{k}$-comparable in $T$. The second part, that $\alpha$ and $\beta$ are
$\prec^{*}_{k}$-comparable in $T$, follows from the combination of Lemma 25
and 29.

##  8\. Encoding non-elementary computations

We combine all the previous sections and extend Theorem 12 and Corollary 13 by
their matching lower bounds:

######  Theorem 31.

  * •

$\mathsf{SAT}(\mathsf{MTL}\xspace)$ and $\mathsf{VAL}(\mathsf{MTL}\xspace)$
are complete for $\mathrm{TOWER}\xspace(\mathrm{poly})$.

  * •

If $k\geq 0$, then $\mathsf{SAT}(\mathsf{MTL}\xspace_{k})$ and
$\mathsf{VAL}(\mathsf{MTL}\xspace_{k})$ are complete for
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$.

The above complexity classes are complement-closed, and additionally
$\mathsf{MTL}\xspace$ and $\mathsf{MTL}\xspace_{k}$ are syntactically closed
under negation. For this reason, it suffices to prove the hardness of
$\mathsf{SAT}(\mathsf{MTL}\xspace)$ and
$\mathsf{SAT}(\mathsf{MTL}\xspace_{k})$, respectively. Moreover, the case
$k=0$ is equivalent to $\mathsf{SAT}(\mathsf{PTL}\xspace)$ being
$\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp,\mathrm{poly})$-hard,
which was proven by Hannula et al. [HKVV18]. Their reduction also works in
logarithmic space. Consequently, the result boils down to the following lemma:

######  Lemma 32.

  * •

If $L\in\mathrm{TOWER}\xspace(\mathrm{poly})$, then
$L\leq^{\log}_{\mathrm{m}}\mathsf{SAT}(\mathsf{MTL}\xspace)$.

  * •

If $k\geq 1$ and
$L\in\mathrm{ATIME}\xspace\text{-}\mathrm{ALT}\xspace(\exp_{k+1},\mathrm{poly})$,
then $L\leq^{\log}_{\mathrm{m}}\mathsf{SAT}(\mathsf{MTL}\xspace_{k})$.

We devise for each $L$ a reduction $x\mapsto\varphi_{x}$ such that
$\varphi_{x}$ is a formula that is satisfiable if and only if $x\in L$. By
assumption, there exists a single-tape alternating Turing machine $M$ that
decides $L$ (for $L\in\mathrm{TOWER}\xspace(\mathrm{poly})$, w.l.o.g.$M$ is
alternating as well).

Let $M$ have states $Q$, which is the disjoint union of $Q_{\exists}$
(_existential states_), $Q_{\forall}$ (_universal states_), $Q_{\text{acc}}$
(_accepting states_) and $Q_{\text{rej}}$ (_rejecting states_). Also, $Q$
contains some initial state $q_{0}$. Let $M$ have a finite tape alphabet
$\Gamma$ with blank symbol $\flat\in\Gamma$, and a transition relation
$\delta$.

We design $\varphi_{x}$ in a fashion that forces its models $(\mathcal{K},T)$
to encode an accepting computation of $M$ on $x$. Let us call any legal
sequence of configurations of $M$ (not necessarily starting with the initial
configuration) a _run_. Then, similarly as in Cook’s theorem [Coo71], we
encode runs as square “grids” with a vertical “time” coordinate and a
horizontal “space” coordinate in the model, i.e., each row of the grid
represents a configuration of $M$.

W.l.o.g.$M$ never leaves the input to the left, and there exists $N$ that is
an upper bound on both the length of a configuration and the runtime of $M$.
Formally, a run of $M$ is then a function
$C\colon{\\{1,\ldots,N\\}}^{2}\to\Gamma\cup(Q\times\Gamma)$, Here, $C(i,j)=c$
for $c\in\Gamma$ means that the $i$-th configuration (i.e., after $M$
performed $i-1$ transitions) contains the symbol $c$ in its $j$-th cell. The
same holds if $C(i,j)=(q,c)$ for $(q,c)\in Q\times\Gamma$, but then
additionally the machine is in the state $q$ with its head visiting the $j$-th
cell in the $i$-th configuration. As an example, for a run $C$ from $M$’s
initial configuration we have $C(1,1)=(q_{0},x_{1})$, $C(1,i)=x_{i}$ for
$2\leq i\leq n$, and $C(1,i)=\flat$ for $n<i\leq N$.

Due to the semantics of $\mathsf{MTL}\xspace$, such a run must be encoded in
$(\mathcal{K},T)$ very carefully. We let the team $T$ contain $N^{2}$ worlds
$w_{i,j}$ in which the respective value of $C(i,j)$ is encoded as a
propositional assignment. However, we cannot simply pursue the standard
approach of assembling a large $N\times N$-grid in the edge relation $R$ in
order to compare successive configurations; by Corollary 18, we cannot force
the model to contain $R$-paths longer than ${|\nobreak\varphi_{x}\nobreak|}$.
Instead, to define grid neighborship, we let $w_{i,j}$ encode $i$ and $j$ in
its _type_. More precisely, we use the linear order $\prec_{k}$ on
$\Delta_{k}$ we defined with the $\mathsf{MTL}\xspace_{k}$-formula $\zeta_{k}$
in the previous section. Then, instead of using $\Box$ and $\Diamond$, we
examine the grid by letting $\zeta_{k}$ judge whether a given pair of worlds
is deemed (horizontally or vertically) adjacent.

###  8.1. Encoding runs in a team

Next, we discuss how runs
$C\colon{\\{1,\ldots,N\\}}^{2}\to\Gamma\cup(Q\times\Gamma)$ are encoded in
$T$. Given a world $w\in T$, we partition the image $Rw$ with two special
propositions $\mathfrak{t}\notin\Phi$ (“timestep”) and
$\mathfrak{p}\notin\Phi$ (“position”). Then we assign to $w$ the pair
$\ell(w)\vcentcolon=(i,j)$ such that
$\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}$ is the $i$-th element,
and $\llbracket{}{(Rw)}_{\mathfrak{p}}\rrbracket{}_{k-1}$ is the $j$-th
element in the order $\prec^{*}_{k-1}$. We call the pair $\ell(w)$ the
_location_ of $w$ (in the grid).

Accordingly, we fix
$N\vcentcolon={|\nobreak\mathfrak{P}(\Delta^{\Phi}_{k-1})\nobreak|}$. For the
case of fixed $k$, $M$ has runtime bounded by $\exp_{k+1}(g(n))$ for a
polynomial $g$. Then taking $\Phi\vcentcolon=\\{p_{1},\ldots,p_{g(n)}\\}$
yields a sufficiently large coordinate space, as

$\displaystyle\exp_{k+1}(g(n))=\exp_{k+1}$
$\displaystyle({|\nobreak\Phi\nobreak|})=2^{\exp_{k-1}\left(2^{|\nobreak\Phi\nobreak|}\right)}\leq
2^{\exp^{*}_{k-1}\left(2^{|\nobreak\Phi\nobreak|}\right)}=2^{{|\nobreak\Delta^{\Phi}_{k-1}\nobreak|}}=N$

by Proposition 9. For runtime $\exp_{g(n)}(1)$ of $M$, we let
$\Phi\vcentcolon=\emptyset$ and precompute $k\vcentcolon=g({|\nobreak
x\nobreak|})+1$, but otherwise proceed identically.

Next, let $\Xi$ be a constant set of propositions disjoint from $\Phi$ that
encodes the range of $C$ via some bijection
$c\colon\Xi\to\Gamma\cup(Q\times\Gamma)$. If a world $w$ satisfies exactly one
proposition $p$ of those in $\Xi$, then by slight abuse of notation we write
$c(w)$ instead of $c(p)$. Intuitively, $c(w)\in\Gamma\cup(Q\times\Gamma)$ is
the content of the grid cell represented by $w$.

Using $\ell$ and $c$, the function $C$ can be encoded into a team $T$ as
follows. First, a team $T$ is called _grid_ if every point in $T$ satisfies
exactly one proposition in $\Xi$, and if every location
$(i,j)\in{\\{1,\ldots,N\\}}^{2}$ occurs as $\ell(w)$ for some point $w\in T$.
Moreover, a grid $T$ is called _pre-tableau_ if for every location $(i,j)$
_and_ every element $p\in\Xi$ there is some world $w\in T$ such that
$\ell(w)=(i,j)$ and $w\vDash p$. Finally, a grid $T$ is a _tableau_ if any two
elements $w,w^{\prime}\in T$ with $\ell(w)=\ell(w^{\prime})$ also agree on
$\Xi$, i.e., $c(w)=c(w^{\prime})$.

Let us motivate the above definitions. Clearly, the definition of a _grid_ $T$
means that $T$ captures the whole domain of $C$, and that $c$ is well-defined
on the level of _points_. If $T$ is additionally a _tableau_ , then $c$ is
also well-defined on the level of _locations_. In other words, a tableau $T$
induces a function
$C_{T}\colon{\\{1,\ldots,N\\}}^{2}\to\Gamma\cup(Q\times\Gamma)$ via
$C_{\alpha}(i,j)\vcentcolon=c(w)$, where $w\in T$ is arbitrary such that
$\ell(w)=(i,j)$.

A _pre-tableau_ can be seen as the union of all possible $C$. In particular,
given any pre-tableau, the definition ensures that arbitrary tableaus can be
obtained from it by the means of subteam quantification $\exists^{\subseteq}$
(cf. p. 5.2).

A tableau $T$ is _legal_ if $C_{T}$ is a run of $M$, i.e., if every row is a
configuration of $M$, and if every pair of two successive rows represents a
valid $\delta$-transition.

The idea of the reduction is now to capture the alternating computation of $M$
by nesting polynomially many quantifications (via $\exists^{\subseteq}$ and
$\forall^{\subseteq}$) of legal tableaus, of which each one is the
continuation of the computation of the previous one.

###  8.2. Accessing two components of locations

An discussed earlier, we choose to represent a location $(i,j)$ in a point $w$
as a pair $(\Delta^{\prime},\Delta^{\prime\prime})$ by stipulating that
$\Delta^{\prime}=\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}$ and
$\Delta^{\prime\prime}=\llbracket{}{(Rw)}_{\mathfrak{p}}\rrbracket{}_{k-1}$.
To access the two components of a encoded location independently, we introduce
the operator

$|^{\alpha}_{\mathfrak{q}}\,\psi\vcentcolon=(\alpha\land\neg\mathfrak{q})\lor((\alpha\hookrightarrow\mathfrak{q})\land\psi)\text{,}$

where $\mathfrak{q}\in\\{\mathfrak{t},\mathfrak{p}\\}$ and
$\alpha\in\mathsf{ML}\xspace$. It is easy to check that
$T\vDash|^{\alpha}_{\mathfrak{q}}\,\psi$ iff
$T^{\alpha}_{T_{\mathfrak{q}}}\vDash\psi$.

In order to _compare_ the locations of grid cells, for each component
$\mathfrak{q}\in\\{\mathfrak{t},\mathfrak{p}\\}$ we define the following
formulas: $\psi^{\mathfrak{q}}_{\prec}(\alpha,\beta)$ tests whether the
location in $T_{\alpha}$ is less than the one in $T_{\beta}$ w. r. t.its
$\mathfrak{q}$-component (assuming singleton teams $T_{\alpha}$ and
$T_{\beta}$). Analogously, $\psi^{\mathfrak{q}}_{\equiv}(\alpha,\beta)$ checks
for equality of the respective component:

$\displaystyle\psi^{\mathfrak{q}}_{\prec}(\alpha,\beta)\vcentcolon=\;$
$\displaystyle\Box\,|^{\alpha}_{\mathfrak{q}}|^{\beta}_{\mathfrak{q}}\zeta_{k-1}^{*}(\alpha,\beta)$
$\displaystyle\psi^{\mathfrak{q}}_{\equiv}(\alpha,\beta)\vcentcolon=\;$
$\displaystyle\Box\,|^{\alpha}_{\mathfrak{q}}|^{\beta}_{\mathfrak{q}}\chi^{*}_{k-1}(\alpha,\beta)$

For this purpose, $\psi^{\mathfrak{q}}_{\prec}$ is built upon the formula
$\zeta^{*}_{k-1}$ from Theorem 24, while $\psi^{\mathfrak{q}}_{\equiv}$ checks
for equality with the help of $\chi^{*}_{k-1}$ from Theorem 16.

######  Claim 33 (a).

Let $\mathcal{K}$ be a structure with a team $T$ and disjoint scopes $\alpha$
and $\beta$. Suppose $w\in T_{\alpha}$ and $v\in T_{\beta}$, where
$\ell(w)=(i_{w},j_{w})$ and $\ell(v)=(i_{v},j_{v})$. Then:

$\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\psi^{\mathfrak{t}}_{\equiv}(\alpha,\beta)$
$\displaystyle\;\Leftrightarrow\;i_{w}=i_{v}$ $\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\psi^{\mathfrak{p}}_{\equiv}(\alpha,\beta)$
$\displaystyle\;\Leftrightarrow\;j_{w}=j_{v}$

Moreover, if $\alpha,\beta,\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k}$ are
disjoint scopes in $\mathcal{K}$ and $(\mathcal{K},T)$ is a $k$-staircase,
then:

$\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\psi^{\mathfrak{t}}_{\prec}(\alpha,\beta)$
$\displaystyle\;\Leftrightarrow\;i_{w}<i_{v}$ $\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\psi^{\mathfrak{p}}_{\prec}(\alpha,\beta)$
$\displaystyle\;\Leftrightarrow\;j_{w}<j_{v}$

######  Proof 8.1 (Proof of claim.).

Let us begin with $\psi^{\mathfrak{t}}_{\equiv}$
($\psi^{\mathfrak{p}}_{\equiv}$ works identically):

$\displaystyle i_{w}=i_{v}\;\Leftrightarrow\;$
$\displaystyle\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}=\llbracket{}{(Rv)}_{\mathfrak{t}}\rrbracket{}_{k-1}$
(By Definition) $\displaystyle\Leftrightarrow\;$ $\displaystyle
RT^{\alpha,\beta}_{{(Rw)}_{\,\mathfrak{t}},{(Rv)}_{\,\mathfrak{t}}}\vDash\chi^{*}_{k-1}(\alpha,\beta)$
(By Theorem 16) $\displaystyle\Leftrightarrow\;$
$\displaystyle{\Big{(}RT^{\alpha,\beta}_{Rw,Rv}\Big{)}}^{\alpha,\beta}_{RT_{\mathfrak{t}},RT_{\mathfrak{t}}}\vDash\chi^{*}_{k-1}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
RT^{\alpha,\beta}_{Rw,Rv}\vDash|^{\alpha}_{\mathfrak{t}}|^{\beta}_{\mathfrak{t}}\chi^{*}_{k-1}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\Box\,|^{\alpha}_{\mathfrak{t}}|^{\beta}_{\mathfrak{t}}\chi^{*}_{k-1}(\alpha,\beta)$
(Proposition 14)

Similarly for $\psi^{\mathfrak{t}}_{\prec}$ ($\psi^{\mathfrak{p}}_{\prec}$
again works identically):

$\displaystyle i_{w}<i_{v}\;\Leftrightarrow\;$
$\displaystyle\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}\prec^{*}_{k-1}\llbracket{}{(Rv)}_{\mathfrak{t}}\rrbracket{}_{k-1}$
(By Definition) $\displaystyle\Leftrightarrow\;$ $\displaystyle
RT^{\alpha,\beta}_{{(Rw)}_{\,\mathfrak{t}},{(Rv)}_{\,\mathfrak{t}}}\vDash\zeta^{*}_{k-1}(\alpha,\beta)$
(By Theorem 24) $\displaystyle\Leftrightarrow\;$
$\displaystyle{\Big{(}RT^{\alpha,\beta}_{Rw,Rv}\Big{)}}^{\alpha,\beta}_{T_{\mathfrak{t}},T_{\mathfrak{t}}}\vDash\zeta^{*}_{k-1}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
RT^{\alpha,\beta}_{Rw,Rv}\vDash|^{\alpha}_{\mathfrak{t}}|^{\beta}_{\mathfrak{t}}\zeta^{*}_{k-1}(\alpha,\beta)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T^{\alpha,\beta}_{w,v}\vDash\Box\,|^{\alpha}_{\mathfrak{t}}|^{\beta}_{\mathfrak{t}}\zeta^{*}_{k-1}(\alpha,\beta)$
(Proposition 14) $\triangleleft$

###  8.3. Defining grids, pre-tableaus, and tableaus

Next, we aim at constructing formulas that check whether a given team is a
grid, pre-tableau, or a tableau, respectively.

First, to check that every location $(i,j)\in{\\{1,\ldots,N\\}}^{2}$ of the
grid occurs as $\ell(w)$ of some $w\in T$, we quantify over all corresponding
pairs
$(\Delta^{\prime},\Delta^{\prime\prime})\in\mathfrak{P}(\Delta_{k-1})^{2}$. To
cover all these sets of types we can quantify, for instance, over the images
of all points of $T_{\mathfrak{s}_{k}}$. However, as subteam quantifiers
$\exists^{\subseteq},\exists^{1},\forall^{\subseteq},\forall^{1}$ cannot pick
_two_ subteams from the same scope, we enforce a $k$-canonical copy
$\mathfrak{s}^{\prime}_{k}$ of $\mathfrak{s}_{k}$ in the spirit of Theorem 20:

$\displaystyle\mathsf{canon}^{\prime}\vcentcolon=\;$
$\displaystyle\rho^{k}_{0}(\mathfrak{s}_{0})\land\bigwedge_{m=1}^{k}\rho^{k-m}_{m}(\mathfrak{s}_{m-1},\mathfrak{s}_{m})\land\rho^{0}_{k}(\mathfrak{s}_{k-1},\mathfrak{s}^{\prime}_{k})$

######  Claim 34 (b).

If $\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}$ are
disjoint scopes in $\mathcal{K}$, then
$(\mathcal{K},T)\vDash\mathsf{canon}^{\prime}$ if and only if
$(\mathcal{K},T)$ is a $k$-staircase and $T_{\mathfrak{s}^{\prime}_{k}}$ is
$k$-canonical. Moreover,
$\mathsf{canon}^{\prime}\land\mathsf{scopes}_{k}(\\{\mathfrak{s}_{0},\ldots,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}\\})\land\Box^{k+1}\bot$
is satisfiable, but is only satisfied by $k$-staircases $(\mathcal{K},T)$ in
which both $T_{\mathfrak{s}_{k}}$ and $T_{\mathfrak{s}^{\prime}_{k}}$ are
$k$-canonical. Furthermore, both formulas are constructible in space
${\mathcal{O}(\log({|\nobreak\Phi\nobreak|}+k))}$.

######  Proof 8.2 (Proof of claim.).

Proven similarly to Theorem 20 and 22. $\triangleleft$

The next formula checks whether a given team is a grid. More precisely, the
subformula $\psi_{\text{pair}}$ compares the $\mathfrak{t}$-component of the
selected location in $\alpha$ to the image of the world quantified in
$\mathfrak{s}_{k}$, and its $\mathfrak{p}$-component to
$\mathfrak{s}^{\prime}_{k}$, respectively. That every world satisfies exactly
one element of $\Xi$ is guaranteed by $\psi_{\text{grid}}$ as well.

$\displaystyle\psi_{\text{grid}}(\alpha)\vcentcolon=\;$
$\displaystyle\Big{(}\alpha\hookrightarrow\bigvee_{e\in\Xi}e\land\bigwedge_{\begin{subarray}{c}e^{\prime}\in\Xi\\\
e^{\prime}\neq e\end{subarray}}\neg
e^{\prime}\Big{)}\land\forall^{1}_{\mathfrak{s}_{k}}\mkern
2.0mu\forall^{1}_{\mathfrak{s}^{\prime}_{k}}\mkern
2.0mu\exists^{1}_{\alpha}\,\psi_{\text{pair}}(\alpha)$
$\displaystyle\psi_{\text{pair}}(\alpha)\vcentcolon=\;$
$\displaystyle\Box\left[\big{(}\,|^{\alpha}_{\mathfrak{t}}\;\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)\big{)}\land\big{(}\,|^{\alpha}_{\mathfrak{p}}\;\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)\big{)}\right]$

In the following and all subsequent claims, we always assume that $T$ is a
team in a Kripke structure $\mathcal{K}$ such that $(\mathcal{K},T)$ satisfies
$\mathsf{canon}^{\prime}\land\Box^{k+1}\bot$. Moreover, all stated scopes are
always assumed pairwise disjoint in $\mathcal{K}$ (as we can enforce this
later in the reduction with $\mathsf{scopes}_{k}(\cdots)$).

######  Claim 35 (c).

$T\vDash\psi_{\text{grid}}(\alpha)$ if and only if $T_{\alpha}$ is a grid.

######  Proof 8.3 (Proof of claim.).

Clearly
$T\vDash\alpha\hookrightarrow\bigvee_{e\in\Xi}e\land\bigwedge_{e^{\prime}\in\Xi,e^{\prime}\neq
e}\neg e^{\prime}$ if and only if every world $w\in T_{\alpha}$ satisfies
exactly one element of $\Xi$. Consequently, for the proof it remains to show
the following equivalence:

$\displaystyle\forall(i,j)\in{\\{1,\ldots,N\\}}^{2}\colon\exists w\in
T_{\alpha}\colon\ell(w)=(i,j)$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\forall\Delta^{\prime},\Delta^{\prime\prime}\subseteq\Delta_{k-1}\colon\exists
w\in
T_{\alpha}:\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}=\Delta^{\prime}\text{
and
}\llbracket{}{(Rw)}_{\mathfrak{p}}\rrbracket{}_{k-1}=\Delta^{\prime\prime}$ By
$k$-canonicity of $\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}$ due to Claim
(b): $\displaystyle\Leftrightarrow\;$ $\displaystyle\forall v\in
T_{\mathfrak{s}_{k}},v^{\prime}\in T_{\mathfrak{s}^{\prime}_{k}}\colon\exists
w\in
T_{\alpha}\colon\llbracket{}{(Rw)}_{\mathfrak{t}}\rrbracket{}_{k-1}=\llbracket{}Rv\rrbracket{}_{k-1}\text{
and
}\llbracket{}{(Rw)}_{\mathfrak{p}}\rrbracket{}_{k-1}=\llbracket{}Rv^{\prime}\rrbracket{}_{k-1}$
By Theorem 16: $\displaystyle\Leftrightarrow\;$ $\displaystyle\forall v\in
T_{\mathfrak{s}_{k}},v^{\prime}\in T_{\mathfrak{s}^{\prime}_{k}}\colon\exists
w\in T_{\alpha}\colon
RT^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{{(Rw)}_{\mathfrak{t}},Rv,Rv^{\prime}}\vDash\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)$
$\displaystyle\qquad\qquad\text{ and
}RT^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{{(Rw)}_{\mathfrak{p}},Rv,Rv^{\prime}}\vDash\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall v\in
T_{\mathfrak{s}_{k}},v^{\prime}\in T_{\mathfrak{s}^{\prime}_{k}}\colon\exists
w\in
T_{\alpha}:{\big{(}RT^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{Rw,Rv,Rv^{\prime}}\big{)}}^{\alpha}_{RT_{\mathfrak{t}}}\vDash\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)$
$\displaystyle\qquad\qquad\text{ and
}{\big{(}RT^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{Rw,Rv,Rv^{\prime}}\big{)}}^{\alpha}_{RT_{\mathfrak{p}}}\vDash\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle\forall v\in
T_{\mathfrak{s}_{k}},v^{\prime}\in T_{\mathfrak{s}^{\prime}_{k}}\colon\exists
w\in T_{\alpha}\colon
RT^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{Rw,Rv,Rv^{\prime}}\vDash\,|^{\alpha}_{\mathfrak{t}}\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)\land\,|^{\alpha}_{\mathfrak{p}}\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)$
By Proposition 14: $\displaystyle\Leftrightarrow\;$ $\displaystyle\forall v\in
T_{\mathfrak{s}_{k}},v^{\prime}\in T_{\mathfrak{s}^{\prime}_{k}}\colon\exists
w\in T_{\alpha}\colon
T^{\alpha,\mathfrak{s}_{k},\mathfrak{s}^{\prime}_{k}}_{w,v,v^{\prime}}\vDash\Box\,|^{\alpha}_{\mathfrak{t}}\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)\land\,|^{\alpha}_{\mathfrak{p}}\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)$
By Proposition 15: $\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\forall^{1}_{\mathfrak{s}_{k}}\forall^{1}_{\mathfrak{s}^{\prime}_{k}}\exists^{1}_{\alpha}\Box\,|^{\alpha}_{\mathfrak{t}}\chi^{*}_{k-1}(\mathfrak{s}_{k},\alpha)\land\,|^{\alpha}_{\mathfrak{p}}\chi^{*}_{k-1}(\mathfrak{s}^{\prime}_{k},\alpha)$
$\displaystyle\Leftrightarrow\;$ $\displaystyle
T\vDash\forall^{1}_{\mathfrak{s}_{k}}\forall^{1}_{\mathfrak{s}^{\prime}_{k}}\exists^{1}_{\alpha}\,\psi_{\text{pair}}(\alpha)$
$\triangleleft$

With slight modifications it is straightforward to define pre-tableaus:

$\displaystyle\psi_{\text{pre-tableau}}(\alpha)\vcentcolon=\;$
$\displaystyle\psi_{\text{grid}}(\alpha)\land\forall^{1}_{\mathfrak{s}_{k}}\mkern
2.0mu\forall^{1}_{\mathfrak{s}^{\prime}_{k}}\mkern
2.0mu\bigwedge_{e\in\Xi}\exists^{1}_{\alpha}\big{(}\psi_{\text{pair}}(\alpha)\land(\alpha\hookrightarrow
e)\big{)}$

######  Claim 36 (d).

$T\vDash\psi_{\text{pre-tableau}}(\alpha)$ if and only if $T_{\alpha}$ is a
pre-tableau.

######  Proof 8.4 (Proof of claim.).

Proven similarly to Claim (c). $\triangleleft$

The other special case of a grid, that is, a _tableau_ , requires a more
elaborate approach to define in $\mathsf{MTL}\xspace$. The difference to a
grid or pre-tableau is that we have to quantify over all _pairs_
$(w,w^{\prime})$ of points in $T$, and check that they agree on $\Xi$ if
$\ell(w)=\ell(w^{\prime})$. However, as discussed before, while $\forall^{1}$
can quantify over all points in a team, it cannot quantify over pairs.

As a workaround, we consider not only a tableau $T_{\alpha}$, but also a
_second_ tableau that acts as a copy of $T_{\alpha}$. Formally, for grids
$T_{\alpha},T_{\beta}$, let $T_{\alpha}\approx T_{\beta}$ denote that for all
pairs $(w,w^{\prime})\in T_{\alpha}\times T_{\beta}$ it holds that
$\ell(w)=\ell(w^{\prime})$ implies $c(w)=c(w^{\prime})$.

As $\approx$ is symmetric and transitive, $T_{\alpha}\approx T_{\beta}$ in
fact implies both $T_{\alpha}\approx T_{\alpha}$ and $T_{\beta}\approx
T_{\beta}$, and hence that both $T_{\alpha}$ and $T_{\beta}$ are tableaus such
that $C_{T_{\alpha}}=C_{T_{\beta}}$, where
$C_{T_{\alpha}},C_{T_{\beta}}\colon{\\{1,\ldots,N\\}}^{2}\to\Gamma\cup(Q\times\Gamma)$
are the induced runs as discussed on p. 8.1.

$\displaystyle\psi_{\text{tableau}}(\alpha)\vcentcolon=\;$
$\displaystyle\psi_{\text{grid}}(\alpha)\land\,\exists^{\subseteq}_{\gamma_{0}}\,\psi_{\text{grid}}(\gamma_{0})\land\psi_{\approx}(\alpha,\gamma_{0})$
$\displaystyle\psi_{\approx}(\alpha,\beta)\vcentcolon=$
$\displaystyle\forall^{1}_{\alpha}\forall^{1}_{\beta}\;\Big{(}\big{(}\psi^{\mathfrak{t}}_{\equiv}(\alpha,\beta)\land\psi^{\mathfrak{p}}_{\equiv}(\alpha,\beta)\big{)}\rightarrowtriangle\operatorname*{\scalerel*{\ovee}{\sum}}_{e\in\Xi}((\alpha\lor\beta)\hookrightarrow
e)\Big{)}$

In the following claim (and in the subsequent ones), we use the scopes
$\gamma_{0},\gamma_{1},\gamma_{2},\ldots$ as “auxiliary pre-tableaus”. Later,
we will also use them as domains to quantify extra locations or rows from.
(The index of $\gamma_{i}$ is incremented whenever necessary to avoid
quantifying from the same scope twice.) For this reason, from now on we always
assume, for sufficiently large $i$, that $T_{\gamma_{i}}$ is a pre-tableau.
This can be later enforced in the reduction with $\psi_{\text{pre-
tableau}}(\gamma_{i})$.

######  Claim 37 (e).

  1. (1)

$T\vDash\psi_{\text{tableau}}(\alpha)$ if and only if $T_{\alpha}$ is a
tableau.

  2. (2)

For grids $T_{\alpha},T_{\beta}$, it holds
$T\vDash\psi_{\approx}(\alpha,\beta)$ if and only if $T_{\alpha}\approx
T_{\beta}$.

######  Proof 8.5 (Proof of claim.).

(2) follows straightforwardly from Claim (a). Let us consider (1). As
$\psi_{\text{tableau}}$ implies $\psi_{\text{grid}}$, and by Claim (c), we can
assume that $T_{\alpha}$ is a grid.

Suppose that the formula is true. Then there exists $S\subseteq
T_{\gamma_{0}}$ such that
$T^{\alpha}_{S}\vDash\psi_{\text{grid}}(\gamma_{0})$. By Claim (c), then $S$
is a grid as well. Moreover, $T_{\alpha}\approx S$ by (2). As argued above,
this implies that $T_{\alpha}$ (and $S$) is a tableau.

For the other direction, suppose that $T_{\alpha}$ is a tableau. Then it
defines a function $C_{T_{\alpha}}$. Since $T_{\gamma_{0}}$ is a pre-tableau,
we can pick a subteam $S$ of it that contains for each
$(i,j)\in{\\{1,\ldots,N\\}}^{2}$ exactly those worlds $w$ with $\ell(w)=(i,j)$
such that $c(w)=C_{T_{\alpha}}(i,j)$. Then $T_{\alpha}\approx S$, and
$\psi_{\text{tableau}}$ is true, with the quantifier
$\exists^{\subseteq}_{\gamma_{0}}$ witnessed by $S$. $\triangleleft$

###  8.4. From tableaus to runs

To ascertain that a tableau contains a run of $M$, we have to check whether
each row indeed is a configuration of $M$—in other words, exactly one cell of
each row contains a pair $(q,a)\in Q\times\Gamma$—and whether consecutive