text:
\section{Introduction}

In the last decades, the work of logicians has unearthed a plethora of decidable fragments of first-order logic $\logic{FO}$.
Many of these cases are restricted quantifier prefixes, such as the BSR-fragment which contains only $\exists^*\forall^*$-sentences \cite{Ramsey1987}.
Others include the guarded fragment $\mathsf{GF}$ \cite{guarded}, the recently introduced separated fragment $\mathsf{SF}$ \cite{separated1,separated2}, or the two-variable fragment $\logic{FO}^2$ \cite{Mortimer75,scott1962decision,fo2}.
See also \citet{BorgerGG1997} for a comprehensive classification of decidable and undecidable cases.

The above fragments all have been subject to intensive research with the purpose of further pushing the boundary of decidability.
One example is the extension of $\logic{FO}^2$ with counting quantifiers, $\logic{FOC}^2$.
For both logics, the satisfiability problem is $\compclass{NEXPTIME}$-complete \cite{foc2,PrattHartmann10}.

\smallskip

Another actively studied extension of first-order logic is \emph{team semantics}, first studied by \citet{hodges_compositional_1997}, which at its core is the simultaneous evaluation of formulas on whole \emph{sets} of assignments, called \emph{teams}.
Based on team semantics, \citet{vaananen_dependence_2007} introduced dependence logic $\logic{D}$, which extends $\logic{FO}$ by atomic formulas $\dep{x_1,\ldots,x_n,y}$ called \emph{dependence atoms}.
Intuitively, these atoms state that the value of the variable $y$ in the team functionally depends on the values of $x_1,\ldots,x_n$.

On the level of expressive power, $\logic{D}$ coincides with existential second-order logic $\logic{SO}(\exists)$, and consequently is undecidable as well \cite{KontinenV09,vaananen_dependence_2007}.
Nonetheless, its two-variable fragment $\logic{D}^2$, as well as its $\exists^*\forall^*$-fragment, were recently proven by \citeauthor{d2nexp} to have a decidable satisfiability problem.
In particular, satisfiability of $\logic{D}^2$ is $\compclass{NEXPTIME}$-complete due to a satisfiability-preserving translation to $\logic{FOC}^2$ \cite{d2nexp}.
Curiously, the corresponding \emph{validity} problem of $\logic{D}^2$ is undecidable~\cite{il2}, which is possible since dependence logic lacks a proper negation operator.
\citet{vaananen_dependence_2007} also considered \emph{team logic} $\logic{TL}$, the extension of $\logic{D}$ by a Boolean negation ${\sim}$.
This logic is equivalent to full second-order logic $\logic{SO}$~\cite{tl-to-so}, and the satisfiability problem is undecidable already for $\logic{TL}^2$.

\smallskip

We study the extension $\logic{FO}({\sim})$ of $\logic{FO}$ with team semantics and negation ${\sim}$, but without dependence atoms.
It was introduced by \citet{abramsky_strongly_2016}, and is incomparable to $\logic{D}$ in terms of expressive power.
Regarding its complexity, however, $\logic{FO}({\sim})$ is much weaker than $\logic{D}$.
In particular, its validity problem is---as for ordinary $\logic{FO}$---complete for $\Upsigma^0_1$ \cite{axiom-fo}, whereas it is non-arithmetical for $\logic{D}$ and $\logic{TL}$~\cite{vaananen_dependence_2007}.

In this paper, we show that its two-variable fragment $\ensuremath{\logic{FO}^2(\negg)}$ is decidable.
More precisely, its satisfiability and validity problem of $\ensuremath{\logic{FO}^2(\negg)}$ are complete for the recently introduced non-elementary complexity class $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$~\cite{mtl_report}.

Our approach for the satisfiability problem is to establish both a finite model property of $\ensuremath{\logic{FO}^2(\negg)}$ and an upper bound for model checking.
In fact, the complexity of the model checking problem has received much less attention in team semantics so far; recent progress focused on the propositional~\cite{hannula_complexity_2018} and modal~\cite{emdl,julian,yang_extensions_2014} variants of team logic and dependence logic.

In the first-order case, \citet{mc-games} proved that model checking for $\logic{D}$ is $\compclass{NEXPTIME}$-complete.
Extending this result, we show that model checking is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete for $\logic{FO}({\sim},\ensuremath{\mathcal{D}})$, where $\ensuremath{\mathcal{D}}$ is any set of $\logic{FO}$-definable dependencies.
Examples for such dependencies are the aforementioned dependence atom ${=\!\!(\cdot,\cdot)}$, but also atoms such as independence $\perp$~\cite{indep} or inclusion $\subseteq$~\cite{galliani_inex}.

\begin{table*}\centering
\begin{tabular}{LCCl}
\toprule
\text{Logic} & \text{Satisfiability} & \text{Validity} & References\\
\midrule
\logic{FO}^2 & \compclass{NEXPTIME} & \text{co-}\compclass{NEXPTIME} & \cite{fo2}\\
\logic{FO}^2({\sim}) & \ensuremath{\compclass{TOWER}(\mathrm{poly})} & \ensuremath{\compclass{TOWER}(\mathrm{poly})} & Theorem~\ref{thm:main-sat} \\
\logic{D}^2 & \compclass{NEXPTIME} & \Upsigma^0_1\text{-hard} & \cite{il2}\\
\logic{TL}^2 & \Uppi^0_1\text{-hard} & \Upsigma^0_1\text{-hard} & \cite{il2}\\
\midrule
& \multicolumn{2}{c}{\text{Model Checking}}  & \\
\midrule
\logic{FO}_k,\logic{FO}^n & \multicolumn{2}{c}{$\in \compclass{PTIME}$} & \cite{fmt}\\[.8mm]
\logic{FO} & \multicolumn{2}{c}{\compclass{PSPACE}} & \cite{fmt}\\
\midrule
\FONKD{}{k}, \FONKD{n}{} & \multicolumn{2}{c}{\compclass{PSPACE}} & Theorem~\ref{thm:mc-completeness}\\[.8mm]
\FONKD{}{} & \multicolumn{2}{c}{\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}} & Theorem~\ref{thm:mc-completeness} \\
\bottomrule
\end{tabular}

\medskip
\caption{Complexity of logics with team semantics. Completeness unless stated otherwise.\label{tab:table-sat}}
\end{table*}

\medskip

\textbf{Organization.}
In Section~\ref{sec:prelim}, we introduce first-order team logic $\logic{FO}({\sim},\ensuremath{\mathcal{D}})$ for arbitrary dependencies $\ensuremath{\mathcal{D}}$, as well as the fragment $\FONKD{n}{k}$ of bounded width $n$ and quantifier rank $k$.
Moreover, we restate the definition of modal team logic $\logic{MTL}$, which is used for several lower bounds.
In Section~\ref{sec:upper}, we prove the upper bounds for model checking by a translation to second-order logic $\logic{SO}$, which admits model checking in $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$.
Afterwards, the upper bound for the satisfiability problem follows in Section~\ref{sec:upper-sat}.
Finally, the lower bounds are proved in Section~\ref{sec:lower}, where we propose a translation from $\logic{MTL}$ to $\ensuremath{\logic{FO}^2(\negg)}$ that extends the well-known \emph{standard translation} from $\logic{ML}$ to $\logic{FO}^2$.

For better readability, some proofs are moved to the appendix and marked with $(\star)$.

\section{Preliminaries}
\label{sec:prelim}

The domain of a function $f$ is $\dom f$.
For $f \colon X \to Y$ and $Z \subseteq X$, $\rest{f}{Z}$ is the restriction of $f$ to the domain $Z$.
The power set of $X$ is $\pow{X}$.

Given a logic $\ensuremath{\mathcal{L}}$, the sets of all satisfiable resp.\ valid formulas of $\ensuremath{\mathcal{L}}$ are denoted by $\ensuremath{\mathsf{SAT}}(\ensuremath{\mathcal{L}})$ and $\ensuremath{\mathsf{VAL}}(\ensuremath{\mathcal{L}})$, respectively.
Likewise, the model checking problem $\ensuremath{\mathsf{MC}}(\ensuremath{\mathcal{L}})$ is the set of all tuples $(A,\varphi)$ such that $\varphi$ is an $\ensuremath{\mathcal{L}}$-formula and $A$ is a model of $\varphi$.
The notation $\size{\varphi}$ means the length of $\varphi$ in a suitable encoding.
$\omega$ is the cardinality of the natural numbers.

\smallskip

We assume the reader to be familiar with alternating Turing machines \cite{alternation}.
When stating that a problem is hard or complete for a complexity class $\ensuremath{\mathcal{C}}$, we refer to $\ensuremath{\leq^\mathrm{log}_\mathrm{m}}$-reductions.
We use the notation $\exp_k$ for the tetration operation, with $\exp_0(n) \dfn n$ and $\exp_{k+1}(n) \dfn 2^{\exp_{k}(n)}$.\label{p:exp}
We simply write $\exp(n)$ instead of $\exp_1(n)$.

\begin{definition}[\cite{mtl_report}]
For $k \geq 0$, $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp}_k,\mathrm{poly})}$ is the class of problems decided by an alternating Turing machine with at most $p(n)$ alternations and runtime at most $\exp_k(p(n))$, for a polynomial $p$.
\end{definition}
\begin{definition}[\cite{mtl_report}]
$\ensuremath{\compclass{TOWER}(\mathrm{poly})}$ is the class of problems that are decided by a deterministic Turing machine in time $\exp_{p(n)}(1)$ for some polynomial $p$.
\end{definition}

The reader may verify that both $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp}_k,\mathrm{poly})}$ and $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$ are closed under polynomial time reductions (and in particular $\ensuremath{\leq^\mathrm{log}_\mathrm{m}}$).

\subsection*{Modal Team Logic}

We fix a set $\Phi$ of propositional symbols.
\emph{Modal team logic} $\logic{MTL}$, introduced by \citet{julian}, extends classical modal logic $\logic{ML}$ via the following grammar, where $\varphi$ denotes an $\logic{MTL}$-formula, $\alpha$ an $\logic{ML}$-formula, and $p$ a propositional variable.
\begin{align*}
\varphi &\ddfn {\sim} \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \Box \varphi \mid \Diamond \varphi \mid \alpha\\
\alpha &\ddfn \neg \alpha \mid \alpha  \land \alpha  \mid \alpha  \lor \alpha \mid \Box\alpha \mid \Diamond\alpha \mid p
\end{align*}

For easier distinction, we usually call classical formulas $\alpha,\beta,\gamma,\ldots$ and reserve $\varphi,\psi,\vartheta,\ldots$ for general formulas.

The \emph{modal depth} $\mathsf{md}(\varphi)$ of formulas $\varphi$ is defined as usual:
\begin{alignat*}{3}
&\mathsf{md}(p) &&\dfn 0 &&\\
&\mathsf{md}({\sim} \varphi) &&\dfn \mathsf{md}(\neg\varphi) &&\dfn \mathsf{md}(\varphi)\\
&\mathsf{md}(\varphi \land \psi) &&\dfn \mathsf{md}(\varphi \lor \psi) &&\dfn \mathrm{max}\{\mathsf{md}(\varphi),\mathsf{md}(\psi)\}\\
&\mathsf{md}(\Diamond \varphi) && \dfn \mathsf{md}(\Box\varphi) &&\dfn \mathsf{md}(\varphi) + 1
\end{alignat*}
The set of propositional variables occurring in $\varphi \in \logic{MTL}$ is denoted by $\mathsf{Prop}(\varphi)$.
$\logic{MTL}_k$ is the fragment of $\logic{MTL}$ with modal depth at most $k$.

\medskip

Let $X \subseteq \Phi$ be a finite set of propositions.
A \emph{Kripke structure} (over $X$) is a tuple $\ensuremath{\mathcal{K}} = (W, R, V)$, where $W$ is a set of \emph{worlds}, $(W,R)$ is a directed graph, and $V \colon X \to \pow{W}$ is the \emph{valuation}.
If $w \in W$, then $(\ensuremath{\mathcal{K}},w)$ is called \emph{pointed Kripke structure}.
$\logic{ML}$ is evaluated on pointed structures in the classical Kripke semantics, whereas
$\logic{MTL}$ is evaluated on pairs $(\ensuremath{\mathcal{K}},T)$, \emph{Kripke structure with teams}, where $T \subseteq W$ is called \emph{team} (in $\ensuremath{\mathcal{K}}$).

The team $RT \dfn \{ v \in W \mid \exists w \in T \colon Rwv \}$ is called \emph{image} of $T$, and we write $Rw$ instead of $R\{w\}$ for brevity.
A \emph{successor team} of $T$ is a team $S$ such that $S \subseteq RT$ and $T \subseteq R^{-1}S$, where $R^{-1} \dfn \{(v,w) \in W^2\mid Rwv\}$.
Intuitively, every $w\in T$ has at least one successor in $S$, and every $v \in S$ has at least one predecessor in $T$.

The semantics of formulas $\varphi \in \logic{MTL}$ is defined as
\begin{alignat*}{3}
&(\ensuremath{\mathcal{K}}, T) \vDash \alpha && \Leftrightarrow\;\forall w \in T \colon (\ensuremath{\mathcal{K}}, w) \vDash \alpha \; \text{ if } \alpha \in \logic{ML}\text{, and otherwise as}\\
&(\ensuremath{\mathcal{K}}, T) \vDash {\sim} \psi &&\Leftrightarrow\;(\ensuremath{\mathcal{K}},T) \nvDash \psi\text{,}\\
&(\ensuremath{\mathcal{K}},T) \vDash \psi \land \theta&&\Leftrightarrow\;(\ensuremath{\mathcal{K}},T) \vDash \psi \text{ and }(\ensuremath{\mathcal{K}},T) \vDash \theta\text{,}\\
&(\ensuremath{\mathcal{K}},T) \vDash \psi \lor \theta&&\Leftrightarrow\;\exists S, U \subseteq T \text{ such that }T = S \cup U\text{, }(\ensuremath{\mathcal{K}},S) \vDash \psi\text{, and }(\ensuremath{\mathcal{K}},U)\vDash \theta\text{,}\\
&(\ensuremath{\mathcal{K}},T)\vDash \Diamond \psi&&\Leftrightarrow\;(\ensuremath{\mathcal{K}}, S)\vDash \psi \text{ for some successor team }S\text{ of }T\text{,}\\
&(\ensuremath{\mathcal{K}},T)\vDash \Box\psi&&\Leftrightarrow\;(\ensuremath{\mathcal{K}},RT) \vDash \psi\text{.}
\end{alignat*}
A formula $\varphi \in \logic{MTL}$ is \emph{satisfiable} if $(\ensuremath{\mathcal{K}},T) \vDash \varphi$ for some Kripke structure $\ensuremath{\mathcal{K}}$ over $X\supseteq \mathsf{Prop}(\varphi)$ and team $T$ in $\ensuremath{\mathcal{K}}$.
Likewise, it is \emph{valid} if it is true in every such pair.

\smallskip

The modality-free fragment $\logic{MTL}_0$ syntactically coincides with \emph{propositional team logic} $\logic{PTL}$ \cite{gandalf,hannula_complexity_2018,YANG20171406}.
The usual interpretations of the latter, i.e.\@\xspace, sets of Boolean assignments, can easily be represented as teams in Kripke structures.
For this reason, we identify $\logic{PTL}$ and $\logic{MTL}_0$ in this paper.

\smallskip

It is easy to check that the following lower bounds due to \citet{hannula_complexity_2018} are logspace reductions.

\begin{theorem}[\cite{hannula_complexity_2018}]
\label{thm:mc-ptl}
$\ensuremath{\mathsf{MC}}(\logic{PTL})$ is $\compclass{PSPACE}$-complete.
\end{theorem}

\begin{theorem}[\cite{hannula_complexity_2018}]
\label{thm:sat-ptl}
$\ensuremath{\mathsf{SAT}}(\logic{PTL})$ and $\ensuremath{\mathsf{VAL}}(\logic{PTL})$ are $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete.
\end{theorem}

For each increment in modal depth, the complexity of the satisfiability problem increases by an exponential, reaching a non-elementary class in the unbounded case:

\begin{theorem}[\cite{mtl_report}]\label{thm:mtl-sat}
$\ensuremath{\mathsf{SAT}}(\logic{MTL})$ and $\ensuremath{\mathsf{VAL}}(\logic{MTL})$ are $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$-complete.
For every finite $k \geq 0$, $\ensuremath{\mathsf{SAT}}(\logic{MTL}_k)$ and $\ensuremath{\mathsf{VAL}}(\logic{MTL}_k)$ are $\KAXX{k+1}$-complete.
\end{theorem}

\subsection*{First-order Team Logic}

A vocabulary is a (possibly infinite) set $\tau$ of function $f$ and predicate symbols $P$, each with arity $\arity{f}$ and $\arity{P}$, respectively.
$\tau$ is called \emph{relational} if it contains no function symbols.
We explicitly state ${=}\in \tau$ if we admit equality.
Moreover, we require that a vocabulary always contains at least one predicate or $=$.

We fix a set $\mathsf{Var} = \{x_1,x_2,\ldots\}$ of first-order variables.
If $\vec{t}$ is a tuple of $\tau$-terms, we let $\mathsf{Var}(\vv{t})$ denote the set of variables occurring in $\vv{t}$.
$\tau$-structures are pairs $\ensuremath{\mathcal{A}} = (A,\tau^\ensuremath{\mathcal{A}})$, where $\dom \ensuremath{\mathcal{A}} \dfn A$ is the domain of $\ensuremath{\mathcal{A}}$.
We sometimes briefly write $\ensuremath{\mathcal{A}}$ instead of $\dom\ensuremath{\mathcal{A}}$ if the meaning is clear.
If $s \colon X \to \ensuremath{\mathcal{A}}$ and $\dom s \supseteq \mathsf{Var}(\vv{t})$, then $\vv{t}\langle s\rangle \in \ensuremath{\mathcal{A}}$ is the evaluation of the terms $\vv{t}$ in $\ensuremath{\mathcal{A}}$ under $s$.

\smallskip

A \emph{team} $T$ (in $\ensuremath{\mathcal{A}}$) is a set of assignments $s\colon X \to \ensuremath{\mathcal{A}}$, where $X$ is the \emph{domain} of $T$.
If $X \supseteq \mathsf{Var}(\vv{t}\,)$ and $\vv{t}$ is a tuple of terms,  $\vv{t}\langle  T \rangle \dfn \{ \vv{t}\langle  s\rangle \mid s \in T \}$.
If $T$ is a team with domain $X \supseteq Y$, then its \emph{restriction} to $Y$ is $\rest{T}{Y}\dfn\{ \rest{s}{Y} \mid s \in T\}$.
In slight abuse of notation, we sometimes identify a tuple $\vv{x}$ with its underlying set, e.g.\@\xspace, write $\rest{T}{\vv{x}}$ instead of $\rest{T}{\{x_1,\ldots,x_{\size{\vv{x}}}\}}$, or $\vv{x} \subseteq \vv{y}$ instead of $\{x_1,\ldots,x_{\size{\vv{x}}}\} \subseteq \{y_1,\ldots,y_{\size{\vv{y}}}\}$.

\begin{proposition}[$\star$]\label{prop:rel}
Let $\ensuremath{\mathcal{A}}$ be a structure, $\vv{t}$ a tuple of terms, $X \supseteq \mathsf{Fr}(\vv{t}\,)$.
For $i \in \{1,2\}$, let $T_i$ be a team in $\ensuremath{\mathcal{A}}$ with domain $X_i \supseteq X$.
Then $\rest{T_1}{X} = \rest{T_2}{X}$ implies $\vv{t}\langle T_1 \rangle = \vv{t}\langle T_2 \rangle$.
Furthermore, for any tuple $\vv{x} \subseteq X$ of variables, $\vval{x}{T_1} = \vval{x}{T_2}$ iff $\rest{T_1}{\vv{x}} = \rest{T_2}{\vv{x}}$.
\end{proposition}

\begin{proposition}[$\star$]\label{prop:iso}
Let $\ensuremath{\mathcal{A}}$ be a structure, $\vv{x}$ a tuple of variables, and $V \dfn \{ s \colon \vv{x} \to \ensuremath{\mathcal{A}} \}$.
Then $\pow{V}$ is the set of all teams in $\ensuremath{\mathcal{A}}$ with domain $\vv{x}$, and the mapping $S \mapsto \vv{x}\langle S\rangle$ is an isomorphism
between the Boolean lattices $(\pow{V},\subseteq)$ and $(\pow{\ensuremath{\mathcal{A}}^{\size{\vv{x}}}},\subseteq)$.
\end{proposition}

If $s \colon X \to \ensuremath{\mathcal{A}}$ and $x \in \mathsf{Var}$, then $s^x_a \colon X \cup \{x\} \to \ensuremath{\mathcal{A}}$ maps $x$ to $a$ and $y \in X \setminus \{x\}$ to $s(y)$.
If $T$ is a team in $\ensuremath{\mathcal{A}}$ with domain $X$, then $f \colon T \to \pow{\ensuremath{\mathcal{A}}}\setminus \{\emptyset\}$ is called a \emph{supplementing function} of $T$.
It extends (or modifies) $T$ to the team $T^x_f \dfn \Set{ s^x_a | s \in T, a \in f(s)}$ with domain $X \cup \{x\}$.
For $f(s) = A$ is constant, we write $T^x_A$ for $T^x_f$.

\smallskip

As an alternative definition of supplementing functions, \citeauthor{galliani_general_2013} used \emph{$x$-variations} \cite{galliani_general_2013}, which are teams that "agree" on all variables but $x$.

\begin{proposition}[$\star$]\label{prop:def-of-supplement}
Let $T$ be a team with domain $X$ and $S$ a team with domain $X \cup \{x\}$ (with possibly $x \in X$), and let $X' \dfn X \setminus \{x\}$.
Then $\rest{S}{X'} = \rest{T}{X'}$ if and only if there is a supplementing function $f$ such that $S = T^x_f$.
\end{proposition}

We are now finally ready to define first-order team logic.
First, the set of ordinary $\tau\text{-}\logic{FO}$-formulas is given by the grammar
\[
\alpha \ddfn P t_1\ldots t_{\arity{P}} \mid \neg \alpha \mid \alpha \land \alpha \mid \alpha \lor \alpha \mid  \exists x\, \alpha \mid \forall x\, \alpha\text{,}
\]
where $P \in \tau$ is a predicate (possibly ${=}$), $x \in \mathsf{Var}$ and $t_1,t_2,\ldots$ are $\tau$-terms.
If $\vv{t} = (t_1,\ldots,t_n)$ and $\vv{u} = (u_1,\ldots,u_n)$ are tuples of terms, then we use the shorthand $\vv{t} = \vv{u}$ for $\bigwedge_{i=1}^n t_i = u_i$.

\begin{definition}[Dependencies]
Let $\tau_P = \{ P\}$, where $P$ is a predicate of arity $k$.
Then $\delta \in \tau_P\text{-}\logic{FO}$ is a \emph{$k$-ary dependency}, and $\mathbf{D}_\delta \dfn \Set{ \tau_P\text{-structure }\ensuremath{\mathcal{A}} \mid \ensuremath{\mathcal{A}} \vDash \delta}$.
\end{definition}

Let $\ensuremath{\mathcal{D}} = \{ \delta_1,\delta_2,\ldots\}$ be a (possibly infinite) set of dependencies.
The logic $\tau$-$\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ then extends $\tau$-$\logic{FO}$ by
\[
\varphi \ddfn \alpha \mid A_i\vv{t} \mid {\sim} \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \exists x\, \varphi \mid \forall x\, \varphi\text{,}
\]
where $\alpha \in \tau\text{-}\logic{FO}$, $\delta_i \in \ensuremath{\mathcal{D}}$ is a $k$-ary dependency, $\vv{t}$ is a $k$-tuple of $\tau$-terms, and $x \in \mathsf{Var}$.
The $A_i\vv{t}$ are called \emph{generalized dependency atoms} or simply \emph{dependency atoms}.

In what follows, we omit $\tau$ if it is not relevant.
The ${\sim}$-free fragment of $\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ is $\ensuremath{\logic{FO}(\ensuremath{\mathcal{D}})}$, and we write $\ensuremath{\logic{FO}(\negg)}$ instead of $\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ if $\ensuremath{\mathcal{D}} = \emptyset$.

\smallskip

\begin{example}
The set $\mathsf{dep} \dfn \{ \delta_1, \delta_2, \ldots \}$ of dependencies is defined by
\[
\delta_n(R) \dfn \forall x_1 \cdots \forall x_{n-1} \forall y \forall z (Rx_1\cdots x_{n-1}y \land Rx_1\cdots x_{n-1}z \rightarrow y = z)\text{.}
\]
$A_n\vv{t}$ is called $n$-ary \emph{dependence atom} and is also written $\dep{t_1,\ldots,t_n}$.
\end{example}

In this notation, Väänänen's dependence logic $\logic{D}$ is $\logic{FO}(\mathsf{dep})$, and team logic $\logic{TL}$ is $\logic{FO}({\sim},\mathsf{dep})$ \cite{vaananen_dependence_2007}.
Other first-order-definable dependencies include the independence atom~\cite{gradel_dependence_2013} as well as the inclusion and exclusion atom \cite{galliani_inex} (see also~\citet{abramsky_expressivity_2016}).

\medskip

If $\varphi$ is a formula, $\mathsf{Fr}(\varphi)$ and $\mathsf{Var}(\varphi)$ denote the set of free resp.\ of all variables in $\varphi$,
defined in the usual manner.
We let $\mathsf{Fr}(A_i\vv{t}\,) \dfn \mathsf{Var}(A_i\vv{t}\,) \dfn \mathsf{Var}(\vv{t})$.
The \emph{width} $\mathsf{w}(\varphi)$ of $\varphi$ is $\size{\mathsf{Var}(\varphi)}$.
The \emph{quantifier rank} $\mathsf{qr}(\varphi)$ of $\varphi$ is
\begin{alignat*}{3}
&\mathsf{qr}(\varphi) &&\dfn 0 && \text{ if $\varphi$ is a first-order atom or a dependency atom,}\\
&\mathsf{qr}({\sim} \varphi) &&\dfn \mathsf{qr}(\neg\varphi) &&\dfn \mathsf{qr}(\varphi)\text{,}\\
&\mathsf{qr}(\varphi \land \psi) &&\dfn \mathsf{qr}(\varphi \lor \psi) &&\dfn \mathrm{max}\{\mathsf{qr}(\varphi),\mathsf{qr}(\psi)\}\text{,}\\
&\mathsf{qr}(\exists x \,\varphi) && \dfn \mathsf{qr}(\forall x\, \varphi) &&\dfn \mathsf{qr}(\varphi) + 1\text{.}
\end{alignat*}

The fragment of $\logic{FO}$ of formulas with width at most $n \leq \omega$ and quantifier rank at most $k \leq \omega$ is denoted by $\logic{FO}^n_k$, with $\FONKD{n}{k}$, $\FONK{n}{k}$ and $\FODK{n}{k}$ defined analogously.
$\tau$-$\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$-formulas $\varphi$ are evaluated on pairs $(\ensuremath{\mathcal{A}},T)$, where $\ensuremath{\mathcal{A}}$ is a $\tau$-structure and $T$ a team $T$ in $\ensuremath{\mathcal{A}}$ with domain $X \supseteq \mathsf{Fr}(\varphi)$:
\begin{alignat*}{3}
&(\ensuremath{\mathcal{A}},T) \vDash \varphi && \Leftrightarrow\;\forall s \in T : (\ensuremath{\mathcal{A}},s) \vDash \varphi \text{ (in Tarski semantics) if }\varphi \in \logic{FO}\text{,}\\
&(\ensuremath{\mathcal{A}},T) \vDash A_i\vv{t} && \Leftrightarrow\;\ensuremath{\mathcal{A}} \vDash \delta_i(\vval{t}{T})\text{,}\\
&(\ensuremath{\mathcal{A}}, T) \vDash {\sim} \psi &&\Leftrightarrow\;(\ensuremath{\mathcal{A}},T) \nvDash \psi\text{,}\\
&(\ensuremath{\mathcal{A}},T) \vDash \psi \land \theta&&\Leftrightarrow\;(\ensuremath{\mathcal{A}},T) \vDash \psi \text{ and }(\ensuremath{\mathcal{A}},T) \vDash \theta\text{,}\\
&(\ensuremath{\mathcal{A}},T) \vDash \psi \lor \theta&&\Leftrightarrow\;\exists S, U \subseteq T \text{ such that }T = S \cup U\text{, }(\ensuremath{\mathcal{A}},S) \vDash \psi\text{, and }(\ensuremath{\mathcal{A}},U)\vDash \theta\text{,}\\
&(\ensuremath{\mathcal{A}},T)\vDash \exists x \, \varphi\;&&\Leftrightarrow\; (\ensuremath{\mathcal{A}},T^x_f) \vDash \varphi \text{ for some }f \colon T \to \pow{\size{\ensuremath{\mathcal{A}}}}  \setminus \{\emptyset\}\text{,}\\
&(\ensuremath{\mathcal{A}},T)\vDash \forall x \, \varphi\;&&\Leftrightarrow\;(\ensuremath{\mathcal{A}},T^x_{\size{\ensuremath{\mathcal{A}}}}) \vDash \varphi\text{.}
\end{alignat*}

A $\tau$-formula $\varphi$ is \emph{satisfiable} if there exists a $\tau$-structure $\ensuremath{\mathcal{A}}$ and team $T$ with domain $X \supseteq \mathsf{Fr}(\varphi)$ in $\ensuremath{\mathcal{A}}$ such that $(\ensuremath{\mathcal{A}},T) \vDash \varphi$.
Likewise, $\varphi$ is \emph{valid} if $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ for all $\tau$-structures $\ensuremath{\mathcal{A}}$ and teams $T$ as above.

\medskip

For $\alpha \in \logic{FO}$ and $\varphi \in \logic{TL}$, define $\alpha \hookrightarrow \varphi \dfn \neg \alpha \lor (\alpha \land \varphi)$, and if $T$ is a team in $\ensuremath{\mathcal{A}}$, let $T_\alpha \dfn \Set{ s \in T \mid (\ensuremath{\mathcal{A}},s) \vDash \alpha }$.
This operator was introduced by \citet{galliani_upwards_2015} and \citet{tl-to-so}.

\begin{proposition}
$(\ensuremath{\mathcal{A}},T) \vDash \alpha \hookrightarrow \varphi$ if and only if $(\ensuremath{\mathcal{A}},T_\alpha) \vDash \varphi$.
\end{proposition}
\begin{proof}
Straightforward.
See also \citeauthor{galliani_upwards_2015} \cite[Lemma 16]{galliani_upwards_2015}.
\end{proof}

\begin{proposition}[Locality]\label{prop:free-vars}
Let $\varphi \in \ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ and $X \supseteq \mathsf{Fr}(\varphi)$.
If $T$ is a team in $\ensuremath{\mathcal{A}}$ with domain $Y \supseteq X$, then $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ if and only if $(\ensuremath{\mathcal{A}},\rest{T}{X})\vDash \varphi$.
\end{proposition}
\begin{proof}
Proven by induction on $\varphi$.
The base case of $\logic{FO}$-formulas and the inductive step for $\land$, $\lor$, $\exists$ and $\forall$ works similarly as \citeauthor{galliani_inex}'s proof for inclusion/exclusion logic \cite[Theorem 4.22]{galliani_inex}, to which the ${\sim}$-case can be added in the obvious manner.

It remains to consider the dependence atoms $A_i\vv{t}$.
As $X \supseteq \mathsf{Fr}(A_i\vv{t}) = \mathsf{Var}(\vv{t})$, clearly $\vv{t}\langle s \rangle = \vec{t}\langle \rest{s}{X} \rangle$ for any $s \in T$, and consequently, $\vv{t}\langle T \rangle = \vv{t}\langle \rest{T}{X} \rangle$.
Hence, $\ensuremath{\mathcal{A}} \vDash \delta_i(\vval{t}{T})$ iff $\ensuremath{\mathcal{A}} \vDash \delta_i(\vval{t}{\rest{T}{X}})$.
\end{proof}

\subsection*{Second-Order Logic}

Second-order logic $\tau$-$\logic{SO}$ (or simply $\logic{SO}$) extends $\tau$-$\logic{FO}$ by an infinite set of function and predicate variables disjoint from $\tau$ and corresponding quantifiers:
\begin{align*}
\hspace{-1.2em}\alpha \ddfn \;&t_1 = t_2 \mid Pt_1\ldots t_n \mid \neg \alpha \mid \alpha \land \alpha \mid \alpha \lor \alpha \mid \exists x\, \alpha\mid \forall x\, \alpha \mid \exists f \, \alpha \mid  \forall f \, \alpha \mid \exists P \, \alpha  \mid \forall P \, \alpha \text{.}
\end{align*}
In second-order logic, $\mathsf{Var}(\alpha)$ resp.\ $\mathsf{Fr}(\alpha)$ refers to the set of all (free) element, function and predicate variables in $\alpha$.
Formulas are evaluated on pairs $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}})$, where $\ensuremath{\mathcal{A}}$ is a structure and $\ensuremath{\mathcal{J}}$ is a \emph{second-order assignment}, i.e.\@\xspace, it maps first-order variables $x\in \mathsf{Fr}(\alpha)$ to elements $\ensuremath{\mathcal{J}}(x) \in \ensuremath{\mathcal{A}}$, function variables $f\in\mathsf{Fr}(\alpha)$ to functions $\ensuremath{\mathcal{J}}(f) \colon \ensuremath{\mathcal{A}}^{\arity{f}} \to \ensuremath{\mathcal{A}}$, and predicate variables $P \in \mathsf{Fr}(\alpha)$ to relations $\ensuremath{\mathcal{J}}(P) \subseteq \ensuremath{\mathcal{A}}^{\arity{P}}$.
The notations $\ensuremath{\mathcal{J}}^x_a$, $\ensuremath{\mathcal{J}}^f_F$ and $\ensuremath{\mathcal{J}}^P_R$ are defined like $s^x_a$ in the first-order setting.
Based on this, the semantics of $\logic{SO}$ are defined in the usual manner.
Instead of $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}) \vDash \alpha(X_1,\ldots,X_n)$ and $\ensuremath{\mathcal{J}}(X_1) = \ensuremath{\mathcal{X}}_1, \ldots, \ensuremath{\mathcal{J}}(X_n) = \ensuremath{\mathcal{X}}_n$, we also write $\ensuremath{\mathcal{A}} \vDash \alpha(\ensuremath{\mathcal{X}}_1,\ldots,\ensuremath{\mathcal{X}}_n)$.

Second-order model checking, $\ensuremath{\mathsf{MC}}(\logic{SO})$, is straightforwardly decidable by evaluating formulas in recursive top-down manner, and using non-deterministic guesses for the quantified elements, functions and relations, which may be of at most exponential size.

\begin{proposition}[$\star$]\label{prop:so-mc}
$\ensuremath{\mathsf{MC}}(\logic{SO})$ is decidable in time $2^{n^\bigO{1}}$ and with $\size{\alpha}$ alternations, where $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}},\alpha)$ is the input.
\end{proposition}

If the arity of quantified functions and relations is bounded a priori, then the interpretation of each quantified function and relation contains $\size{\ensuremath{\mathcal{A}}}^{\bigO{1}}$ tuples.

\begin{corollary}
Let $\tau$-$n$-$\logic{SO}$ be the fragment of $\tau$-$\logic{SO}$ where all quantified functions and relations have arity at most $n$.
Then $\ensuremath{\mathsf{MC}}(\tau\text{-}n\text{-}\logic{SO})$ is $\compclass{PSPACE}$-complete.
\end{corollary}
 \section{From FO(${\sim}$) to SO: Upper bounds for model checking}

\label{sec:upper}

In this section, we present complexity upper bounds for the model checking problem of team logic.
On that account, we assume all first-order structures $\ensuremath{\mathcal{A}}$ and teams $T$ to be finite.

Instead of deciding $\ensuremath{\mathsf{MC}}(\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})})$ directly, we reduce to the corresponding problem of second-order logic, $\ensuremath{\mathsf{MC}}(\logic{SO})$.
For this purpose, we use a result of \citet{vaananen_dependence_2007}, which states that, roughly speaking, $\logic{TL}$-formulas can be translated to $\logic{SO}$.
As a consequence, the upper bounds of $\logic{SO}$ carry over to $\logic{TL}$.

Väänänen's original translation \cite[Theorem 8.12]{vaananen_dependence_2007} from $\logic{TL}$ to $\logic{SO}$ assumes that all variables in a formula are quantified at most once.
However, since we also consider fragments $\FONKD{n}{k}$ of finite width $n$, re-quantification of bound variables may be necessary.
In what follows, we generalize the translation accordingly, and also extend it to include generalized dependence atoms.

\medskip

Suppose $\vv{x} = (x_1,\ldots,x_n)$ is a tuple of variables, $\varphi\in \ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ such that $\mathsf{Fr}(\varphi) \subseteq \vv{x}$, and $R$ is a $n$-ary predicate.
Then we recursively define the $\logic{SO}$-formula $\eta^{\vv{x}}_\varphi(R)$ as shown below.
In order to avoid repetitions in the tuple $\vv{x}$, we define the notation $\vv{x}{;}y$ as
$\vv{x}$ if $y = x_i$ for some $1 \leq i \leq n$, and as $(x_1,\ldots,x_n,y)$ if $y \notin \{x_1,\ldots,x_n\}$.

Next, we state the translation recursively.

\begin{itemize}
\item If $\varphi$ is first-order, then $\eta^{\vec{x}}_\varphi(R) \dfn \forall \vec{x} (R\vec{x} \rightarrow \varphi)$.\smallskip
\item If $\varphi = A_i(\vv{t})$ and $\delta_i \in \ensuremath{\mathcal{D}}$ is $k$-ary, then let $\vv{z} = (z_1,\ldots,z_k)$ be pairwise distinct variables disjoint from $\vv{x}$, and
 $\eta^{\vec{x}}_\varphi(R) \dfn \exists S\,\forall \vv{z} \, (S\vv{z} \leftrightarrow (\exists \vv{x}\, R\vv{x} \land \vv{t} = \vv{z}\,)) \land \delta_i(S)$.\smallskip
\item If $\varphi = {\sim} \psi$, then $\eta^{\vec{x}}_\varphi(R) \dfn \neg \eta^{\vec{x}}_\psi(R)$.\smallskip
\item If $\varphi = \psi \land \theta$, then
$\eta^{\vec{x}}_\varphi(R) \dfn \eta^{\vec{x}}_\psi(R) \land \eta^{\vec{x}}_\theta(R)$.\smallskip
\item If $\varphi = \psi \lor \theta$, then
$\begin{aligned}[t]
\eta^{\vec{x}}_\varphi(R) \dfn \exists S\, \exists U \,&\,  \forall \vec{x} (R\vec{x} \leftrightarrow (S\vec{x} \lor U\vec{x}))\land \eta^{\vec{x}}_\psi(S) \land \eta^{\vec{x}}_\theta(U)\text{.}
\end{aligned}$\smallskip

\item If $\varphi = \exists y \, \psi$
, then
$\begin{aligned}[t]
\eta^{\vec{x}}_\varphi(R) \dfn \exists S\, \forall \vec{x} ((\exists y R\vec{x}) \leftrightarrow (\exists y\, S\vec{x}{;}y))
\land \eta_\psi^{\vec{x}{;}y}(S)\text{.}
\end{aligned}$\smallskip

\item If $\varphi = \forall y \, \psi$, then
$\begin{aligned}[t]
\eta^{\vec{x}}_\varphi(R) \dfn \exists S\, &\forall \vec{x} ((\exists y R\vec{x}) \leftrightarrow (\exists y\, S\vec{x}{;}y))\land \eta_\psi^{\vec{x}{;}y}(S) \\
 \land\,&\forall \vec{x} (R\vec{x} \rightarrow \forall y\, S\vec{x}{;}y) \text{.}
\end{aligned}$
\end{itemize}

\begin{theorem}\label{thm:tl-to-so}
Let $\varphi \in \ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$, let $\vv{x} \supseteq \mathsf{Fr}(\varphi)$ be a tuple of variables, and $T$ be a team in $\ensuremath{\mathcal{A}}$ with domain $Y \supseteq \vv{x}$.
Then $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ if and only if $\ensuremath{\mathcal{A}} \vDash \eta^{\vec{x}}_\varphi(\vval{x}{T})$.
\end{theorem}

In order to prove the $\exists$ and $\forall$ cases, we require the next lemma.
\begin{lemma}[$\star$]\label{lem:supp-as-rest}
Let $T$ have domain $\vv{x}$ and $S$ have domain $\vv{x} \cup \{y\}$ (with possibly $y \in X$), and let $X' \dfn \vv{x} \setminus \{x\}$.
Then $\rest{T}{X'} = \rest{S}{X'}$ if and only if $\ensuremath{\mathcal{A}} \vDash \pi(\vv{x}\langle T\rangle,\vv{x}{;}y\langle S\rangle)$, where $\pi(T,S) \dfn  \forall \vv{x}((\exists y T \vv{x}) \leftrightarrow (\exists y S \vv{x}{;}y))$.
\end{lemma}

\begin{proof}[Proof of Theorem]
Note that $(\ensuremath{\mathcal{A}},T) \vDash \varphi \Leftrightarrow (\ensuremath{\mathcal{A}},\rest{T}{\vv{x}}) \vDash \varphi$ by Proposition~\ref{prop:free-vars}, and $\vval{x}{T} = \vval{x}{\rest{T}{\vv{x}}}$.
For this reason, we can assume that $T$ has domain $\vv{x}$.
The proof is now by induction on $\varphi$.
\begin{itemize}
\item  If $\varphi$ is first-order, clearly $(\ensuremath{\mathcal{A}},T)\vDash \varphi$ iff $\ensuremath{\mathcal{A}} \vDash \varphi(\vv{a})$ for all $\vv{a} \in \vval{x}{T}$ iff $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(\vval{x}{T})$.

\item
If $\varphi = A_i(\vv{t})$ and $\delta_i \in \ensuremath{\mathcal{D}}$ is a $k$-ary dependency, then $(\ensuremath{\mathcal{A}},T) \vDash A_i(\vv{t})$ iff $\ensuremath{\mathcal{A}} \vDash \delta_i(\vval{t}{T})$.
We prove that this is again equivalent to $\ensuremath{\mathcal{A}} \vDash \exists S \,\rho(R,S) \land \delta_i(S)$, where $R = \vval{x}{T}$ and $\rho(R,S) \dfn \forall \vv{z} \, (S\vv{z} \leftrightarrow (\exists \vv{x}\, R\vv{x} \land \vv{t} = \vv{z}\,))$.

It suffices to show that $\ensuremath{\mathcal{A}} \vDash \rho(R,S)$ implies $S = \vval{t}{T}$.
Recall that $\vv{x} \cap \{z_1,\ldots,z_k\} = \emptyset$ and that the $z_i$ are pairwise distinct.
On that account, suppose $\ensuremath{\mathcal{A}} \vDash \rho(R,S)$ and $\vv{a} = (a_1,\ldots,a_k)\in \ensuremath{\mathcal{A}}^k$.
By definition of the formula, $\vv{a} \in S$ iff $\ensuremath{\mathcal{A}} \vDash \exists \vv{x}\, R\vv{x} \land \vv{t} = \vv{a}$.
However, this is the case iff $\vv{t}\langle s \rangle = \vv{a}$ for some $s \in T$, i.e.\@\xspace, $\vv{a} \in \vv{t}\langle T\rangle$.

\item
The cases $\varphi = {\sim} \psi$ and $\varphi = \psi \land \theta$ immediately follow by induction hypothesis.

\item
If $\varphi = \psi \lor \theta$, then by induction hypothesis, $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ iff there are $S,U\subseteq T$ such that $T = S \cup U$ and $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\psi(\vv{x}\langle S \rangle)\land \eta^{\vv{x}}_\theta(\vv{x}\langle U \rangle)$.
Let $R \dfn \vval{x}{T}$.

Then due to Proposition~\ref{prop:iso}, the above is equivalent to the existence of $P,Q \subseteq \ensuremath{\mathcal{A}}^n$ such that $R = P \cup Q$ and $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\psi(P)\land \eta^{\vv{x}}_\theta(Q)$, and consequently to $\ensuremath{\mathcal{A}} \vDash \exists S \, \exists U\, \forall \vv{x}( R\vv{x} \leftrightarrow (S\vv{x} \lor U\vv{x})) \land \eta^{\vv{x}}_\psi(S) \land \eta^{\vv{x}}_\theta(U)$.

\item If $\varphi = \exists y\, \psi$, by Proposition~\ref{prop:def-of-supplement}, then $(\ensuremath{\mathcal{A}},T)\vDash \varphi$ iff $(\ensuremath{\mathcal{A}},S) \vDash \psi$ for some team $S$ with domain $\vv{x}\cup\{y\}$ such that $\rest{T}{X'}=\rest{S}{X'}$.
By Lemma~\ref{lem:supp-as-rest} and by induction hypothesis, this is the case iff $(\ensuremath{\mathcal{A}},\vval{x}{T}) \vDash \exists S\, \forall \vec{x}((\exists y R \vec{x}) \leftrightarrow (\exists y S \vv{x};y)) \land \eta^{\vec{x};y}_\psi(S)$.

\item The case $\varphi = \forall y\, \psi$ is proven analogously to $\exists$.
The additional clause $(R\vec{x} \rightarrow \forall y\, S\vec{x}{;}y)$ ensures that the supplementing function is constant and $f(s) = \dom\ensuremath{\mathcal{A}}$. \qedhere
\end{itemize}
\end{proof}

\begin{definition}
Let $\ensuremath{\mathcal{D}} = \{ \delta_1,\delta_2,\ldots\}$ be a set of dependencies.
$\ensuremath{\mathcal{D}}$ is called \emph{p-uniform} if there is a polynomial time algorithm that for all $i$, when given $A_i\vv{t}$, computes $\delta_i$.
\end{definition}

\begin{corollary}\label{cor:fo-mc}
Let $\ensuremath{\mathcal{D}}$ be a p-uniform set of dependencies.
Then $\ensuremath{\mathsf{MC}}(\ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})})$ is decidable in time $2^{n^{\bigO{1}}}$ and with $\size{\varphi}^\bigO{1}$ alternations, where $(\ensuremath{\mathcal{A}},T,\varphi)$ is the input.
\end{corollary}
\begin{proof}
We compute $\vv{x} \dfn \mathsf{Fr}(\varphi)$, $\eta^{\vv{x}}_\varphi$ and $\vval{x}{T}$ from $\varphi$ and $T$ in polynomial time.
Afterwards, we accept if and only if $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(\vval{x}{T})$.

By Proposition~\ref{prop:so-mc}, the latter can be checked by an algorithm with $\size{\eta^{\vv{x}}_\varphi}$ alternations and time exponential in $(\ensuremath{\mathcal{A}},\vval{x}{T},\eta^{\vv{x}}_\varphi)$.
This corresponds to $\size{\varphi}^{\bigO{1}}$ alternations and runtime exponential in $(\ensuremath{\mathcal{A}},T,\varphi)$.
\end{proof}

\subsection*{Bounded quantifier rank or width}

The complexity of the model checking problem of team logic significantly drops if either the number of variables or the quantifier rank is bounded by an arbitrary constant.
To prove this, we require a special fragment of $\logic{SO}$ that corresponds to such fragments.
We call this fragment \emph{sparse second-order logic}, which uses \emph{sparse quantifiers} $\exists^p$ and $\forall^p$:
\begin{align*}
\!\!\!\!\!\!\!\!\!(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}) \vDash \exists^p P\, \psi &\Leftrightarrow \exists R\subseteq \ensuremath{\mathcal{A}}^{\arity{P}} \text{ such that }\size{R} \leq p(\size{\ensuremath{\mathcal{A}}}) \text{ and }(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}^P_R) \vDash \psi\text{,}\\
\!\!\!\!\!\!\!\!\!(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}) \vDash \forall^p P\, \psi &\Leftrightarrow \forall R \subseteq \ensuremath{\mathcal{A}}^{\arity{P}} \text{ such that }\size{R} \leq p(\size{\ensuremath{\mathcal{A}}}) \text{ it holds }(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}^P_R) \vDash \psi\text{,}
\end{align*}
where $p\colon \ensuremath{\mathbb{N}}\xspace \to \ensuremath{\mathbb{N}}\xspace$ and $\size{\ensuremath{\mathcal{A}}} \dfn \size{\!\dom\ensuremath{\mathcal{A}}} + \sum_{X \in \tau}\size{X^\ensuremath{\mathcal{A}}}$.
In other words, all quantified relations are bounded in their size relative to the underlying $\tau$-structure.
For obvious reason, there are no sparse function quantifiers.

The logic $\logic{SO}[p]$ is now defined as $\logic{SO}$, but with only $\exists^p$ and $\forall^p$ as permitted second-order quantifiers.

Consider the case where $p$ is bounded by a polynomial.
The interpretation of each quantified relation then contains at most $\size{\ensuremath{\mathcal{A}}}^{\bigO{1}}$ tuples.
Consequently, on $\logic{SO}[p]$-formulas, the recursive model checking algorithm from Proposition~\ref{prop:so-mc} then runs in alternating polynomial time instead of exponential time.

\begin{corollary}\label{cor:bounded-so-pspace}
If $p$ is bounded by a polynomial, then
$\ensuremath{\mathsf{MC}}(\logic{SO}[p])$ is decidable in polynomial time with $\size{\alpha}$ alternations, where $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}},\alpha)$ is the input.
\end{corollary}

Remarkably, the translation from team logic with bounded width or quantifier rank to $\logic{SO}$ takes place in this fragment.
For $p \colon \ensuremath{\mathbb{N}}\xspace \to \ensuremath{\mathbb{N}}\xspace$, define the $\logic{SO}[p]$-formula $\zeta^{\vv{x},p}_\varphi$ similarly to $\eta^{\vv{x}}_\varphi$, but with all second-order quantifiers replaced by $\exists^{p}$.

Intuitively, every quantified relation in $\eta^{\vv{x}}_\varphi$ is either dividing or supplementing an existing team resp.\ relation.
For this reason, they grow at most by a factor of $\size{\!\dom\ensuremath{\mathcal{A}}}$ for every quantifier.

\begin{theorem}\label{thm:sparse-translation}
Let $\varphi \in \ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$, let $\vv{x} \supseteq \mathsf{Fr}(\varphi)$ be a tuple of variables, and $T$ be a team in $\ensuremath{\mathcal{A}}$ with domain $Y \supseteq \vv{x}$.
If $p(n) \geq \size{T}\cdot n^{\mathsf{qr}(\varphi)}$ or $p(n) \geq n^{\mathsf{w}(\varphi)}$, then $(\ensuremath{\mathcal{A}},T)\vDash \varphi$ if and only if $\ensuremath{\mathcal{A}} \vDash \zeta^{\vv{x},p}_\varphi(\vval{x}{T})$.
\end{theorem}

We distinguish two cases.

\begin{proof}[Proof for $p(n) \geq \size{T}\cdot n^{\mathsf{qr}(\varphi)}$]

Assume $\ensuremath{\mathcal{A}}$, $T$ as above, let $m \dfn \mathsf{qr}(\varphi)$ and $p(n) \geq n^m$.

The idea of the proof is to show that $\eta^{\vv{x}}_\varphi$ and $\zeta^{\vv{x},p}_\varphi$ agree on $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}})$ for all "sufficiently sparse" $\ensuremath{\mathcal{J}}$ (cf.\ Theorem~\ref{thm:tl-to-so}).

Formally, let $\ell \leq m$ and let $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}})$ be a second-order interpretation such that $\size{\ensuremath{\mathcal{J}}(R)}\leq \size{T}\cdot \size{\ensuremath{\mathcal{A}}}^{\ell}$ for all relations $R \in \dom \ensuremath{\mathcal{J}}$.
Then we prove for all $\varphi \in \ensuremath{\logic{FO}(\negg,\ensuremath{\mathcal{D}})}$ with $\mathsf{qr}(\varphi) \leq m - \ell$ and tuples $\vv{x} \supseteq \mathsf{Fr}(\varphi)$ that it holds $(\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}) \vDash \eta^{\vv{x}}_\varphi \Leftrightarrow (\ensuremath{\mathcal{A}},\ensuremath{\mathcal{J}}) \vDash \zeta^{\vv{x},p}_\varphi$ .

For $\ell = 0$, this yields the theorem, since $\size{\vval{x}{T}} \leq \size{T} \cdot \size{\ensuremath{\mathcal{A}}}^0$.

The proof is by induction on $\varphi$.
We distinguish the following cases.
\begin{itemize}
\item If $\varphi \in \logic{FO}$, then $\eta^{\vv{x}}_\varphi = \zeta^{\vv{x},p}_\varphi$.
\item If $\varphi = {\sim} \psi$ or $\varphi = \psi \land \theta$, then the inductive step is clear.
\item If $\varphi = A_i\vv{t}$ for a $k$-ary dependency $\delta_i \in \ensuremath{\mathcal{D}}$, then
$\zeta^{\vv{x},p}_\varphi(R) = \exists^p S \,\rho(R,S)$ and $\eta^{\vv{x}}_\varphi(R) = \exists S\, \rho(R,S)$, where $\rho(R,S) = \forall \vv{z} \, (S\vv{z} \leftrightarrow (\exists \vv{x}\, R\vv{x} \land \vv{t} = \vv{z}\,)) \land \delta_i(S)$.
We show that $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(R)$ implies $\ensuremath{\mathcal{A}} \vDash \zeta^{\vv{x},p}(R)$.
The other direction is trivial.

On that account, suppose $\ensuremath{\mathcal{A}} \vDash \rho(R,S)$ for some $S \subseteq \ensuremath{\mathcal{A}}^k$.
We construct an injection $f \colon S  \to R$, which implies $\size{S} \leq \size{R}$.
Consequently, $\ensuremath{\mathcal{A}} \vDash \exists^p S\,\rho(R,S)$, as by assumption, $\size{R} \leq \size{T}\cdot \size{\ensuremath{\mathcal{A}}}^\ell \leq \size{T}\cdot \size{\ensuremath{\mathcal{A}}}^m \leq p(\size{\ensuremath{\mathcal{A}}})$.

For every $\vv{a} \in S$, define $f(\vv{a})$ as some $\vv{b} \in R$ such that $\vv{t}\langle\{\vv{x}\mapsto \vv{b}\}\rangle = \vv{a}$.
By $\rho(R,S)$, such $\vv{b}$ must exist.
Clearly, $f$ is injective.
\item If $\varphi = \psi \lor \theta$, then $\zeta^{\vv{x},p}_\varphi(R) = \exists^p S\, \exists^p U \, \rho$ and $\eta^{\vv{x}}_\varphi(R) = \exists S \,\exists U \, \rho'$, where
\begin{align*}
\rho(R,S,U) &= \forall \vec{x} (R\vv{x} \leftrightarrow (S\vv{x} \lor U\vv{x}))\land \zeta^{\vv{x},p}_\psi(S) \land \zeta^{\vv{x},p}_\theta(U)\text{,}\\
\rho'(R,S,U) &= \forall \vec{x} (R\vv{x} \leftrightarrow (S\vv{x} \lor U\vv{x}))\land \eta^{\vv{x}}_\psi(S) \land \eta^{\vv{x}}_\theta(U)\text{.}
\end{align*}
Suppose $\size{R} \leq \size{T}\cdot\size{\ensuremath{\mathcal{A}}}^\ell$ and $\mathsf{qr}(\varphi) \leq m - \ell$.
Clearly $\mathsf{qr}(\psi) = \mathsf{qr}(\theta) = \mathsf{qr}(\varphi)$.

Let $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(R)$, i.e.\@\xspace, $\ensuremath{\mathcal{A}} \vDash \rho'(R,S,U)$ for some $S,U \subseteq \ensuremath{\mathcal{A}}^{\size{\vv{x}}}$.
But $\rho'$ enforces that $\size{S},\size{U} \leq \size{R}$.
Since $\size{R} \leq \size{T}\cdot\size{\ensuremath{\mathcal{A}}}^\ell$ by assumption, we can apply the induction hypothesis to $\eta^{\vv{x}}_\psi(S)$ and $\eta^{\vv{x}}_\theta(U)$ and obtain $\ensuremath{\mathcal{A}} \vDash \rho(R,S,U)$.
Since in particular $\size{S},\size{U} \leq p(\size{\ensuremath{\mathcal{A}}})$, we conclude $\ensuremath{\mathcal{A}} \vDash \exists^p S\, \exists^p U\,\rho$.
The other direction is similar.
\smallskip

\item If $\varphi = \exists y\, \psi$, then $\zeta^{\vv{x},p}_\varphi(R) = \exists^p S\,\rho(R,S)$ and $\eta^{\vv{x}}_\varphi(R) = \exists S \,\rho'(R,S)$, where
\begin{align*}
\rho(R,S) &= \forall \vec{x} ((\exists y R\vec{x}) \leftrightarrow (\exists y\, S\vec{x}{;}y)) \land \zeta_\psi^{\vec{x}{;}y,p}(S)\text{,}\\
\rho'(R,S) &= \forall \vec{x} ((\exists y R\vec{x}) \leftrightarrow (\exists y\, S\vec{x}{;}y)) \land \eta_\psi^{\vec{x}{;}y}(S)\text{.}
\end{align*}
Suppose $\size{R} \leq \size{T}\cdot\size{\ensuremath{\mathcal{A}}}^\ell$ and $\mathsf{qr}(\varphi) \leq m - \ell$.
We show that $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(R)$ implies $\ensuremath{\mathcal{A}} \vDash \zeta^{\vv{x},p}_{\varphi}(R)$.
The other direction is again similar.

Assuming $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(R)$, there exists $S \subseteq \ensuremath{\mathcal{A}}^{\size{\vv{x};y}}$ such that $\ensuremath{\mathcal{A}} \vDash \rho'(R,S)$.
As a first step, we erase unnecessary elements from $S$.
Note that $S$ occurs in $\rho'$ only in atomic formulas $S\vv{x}{;}y$, i.e.\@\xspace, with a fixed argument tuple $\vv{x}{;}y$.
Let $(v_1,\ldots,v_r) \dfn \vv{x}{;}y$.
If now $v_i = v_j$ for some $1 \leq i < j \leq r$, then every tuple $(a_1,\ldots,a_r)$ with $a_i \neq a_j$ can be safely deleted from $S$.
Formally, if $S^* \dfn \vv{x}{;}y\langle V \rangle \cap S$, where $V = \{ s\colon \vv{x}\cup\{y\} \to \ensuremath{\mathcal{A}} \}$, then $\ensuremath{\mathcal{A}} \vDash \rho'(R,S)$ if and only if $\ensuremath{\mathcal{A}} \vDash \rho'(R,S^*)$, which can be showed by straightforward induction.

\smallskip

Note that $\mathsf{qr}(\psi) = \mathsf{qr}(\varphi) - 1 \leq m - (\ell + 1)$.
Consequently, to apply the induction hypothesis, we prove
$\size{S^*} \leq \size{R} \cdot \size{\ensuremath{\mathcal{A}}}\leq \size{T}\cdot \size{\ensuremath{\mathcal{A}}}^{\ell+1}$ by presenting some injective $f \colon S^* \to R \times \ensuremath{\mathcal{A}}$.

If $y \notin \vv{x}$, let $f$ be the identity, as $\rho'$ ensures that $(\vv{a},b)\in S^*$ implies $\vv{a}\in R$.
However, if $y \in \vv{x}$, then we define $f(\vv{a})$ as follows.
By construction, $\vv{a} \in S^*$ equals $\vv{x}\langle s \rangle$ for some $s \colon \vv{x}\to\ensuremath{\mathcal{A}}$.
Again by $\rho'$, there is $\hat{s}\colon \vv{x}\to \ensuremath{\mathcal{A}}$ such that $\vv{x}\langle \hat{s} \rangle \in R$ and $s = \hat{s}^y_{s(y)}$.
Let now $f(\vv{a}) \dfn (\vval{x}{\hat{s}}, s(y))$.
Then $f$ is injective.

Hence, by induction hypothesis, we can replace $\eta^{\vv{x}}_\varphi$ by $\zeta^{\vv{x},p}_\varphi$ and obtain $\ensuremath{\mathcal{A}} \vDash \rho(R,S^*)$.
Since $\size{S^*} \leq \size{\ensuremath{\mathcal{A}}}^{\ell + 1} \leq p(\size{\ensuremath{\mathcal{A}}})$, we obtain $\ensuremath{\mathcal{A}} \vDash \exists^p S\, \rho(R,S)$.
\item The case $\varphi = \forall y\, \psi$ is proven similarly to $\varphi = \exists y\, \psi$.\qedhere
\end{itemize}
\end{proof}

\begin{proof}[Proof for $p(n) \geq n^{\mathsf{w}(\varphi)}$]
We can apply the same argument as in the $\exists$-case of the previous proof.
Suppose $S$ is a second-order variable.
Then $S$ appears in $\eta^{\vv{x}}_\varphi$ only in atomic formulas of the form $S\vv{t}$ for a fixed $\vv{t}$.
Accordingly, it suffices to let $\exists S$ range over subsets of $\vv{t}\langle V \rangle$, where $\vv{y} \dfn \mathsf{Var}(\vv{t})$ and $V \dfn \{ s \colon \vv{y} \to \ensuremath{\mathcal{A}} \}$.

(We consider terms $\vv{t}$ instead of only variables to account for the translations of dependencies, where $S$ can have terms as arguments.)

Since $\vv{y}$ contains at most $\mathsf{w}(\varphi)$ distinct variables, $\size{V} \leq \size{\ensuremath{\mathcal{A}}}^{\mathsf{w}(\varphi)} \leq p(\size{\ensuremath{\mathcal{A}}})$.
Consequently, every second-order quantifier $\exists S$ can be replaced by $\exists^p S$, which implies $\ensuremath{\mathcal{A}} \vDash \eta^{\vv{x}}_\varphi(\vval{x}{T}) \Leftrightarrow \ensuremath{\mathcal{A}} \vDash \zeta^{\vv{x},p}_\varphi(\vval{x}{T})$.
\end{proof}

\begin{corollary}\label{cor:mcfo2-upper1}
Let $\ensuremath{\mathcal{D}}$ be a p-uniform set of dependencies and $m < \omega$.
$\ensuremath{\mathsf{MC}}(\FONKD{m}{\omega})$ and $\ensuremath{\mathsf{MC}}(\FONKD{\omega}{m})$ are then decidable in polynomial time with $\size{\varphi}^\bigO{1}$ alternations, where $(\ensuremath{\mathcal{A}},T,\varphi)$ is the input.
\end{corollary}
\begin{proof}
Analogously to Corollary~\ref{cor:fo-mc}, we reduce to $\ensuremath{\mathsf{MC}}(\logic{SO}[p])$ in polynomial time, where $p(n) \dfn n^{m+1}$.
Accordingly, assume an input $(\ensuremath{\mathcal{A}},T,\varphi)$ and that either $\mathsf{w}(\varphi) \leq m$ or $\mathsf{qr}(\varphi) \leq m$.
Then the input is mapped to $(\ensuremath{\mathcal{A}},\vval{x}{T},\zeta^{p,\vv{x}}_\varphi)$, where $\vv{x} = \mathsf{Fr}(\varphi)$.

Now, if $\mathsf{w}(\varphi) \leq m$, then $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ if and only if $\ensuremath{\mathcal{A}} \vDash \zeta^{p,\vv{x}}_\varphi(\vval{x}{T})$ by Theorem~\ref{thm:sparse-translation}.

Otherwise, $\mathsf{qr}(\varphi) \leq m$.
In that case, w.l.o.g.\@\xspace $\size{T} \leq \size{\ensuremath{\mathcal{A}}}$ (if necessary, pad $\ensuremath{\mathcal{A}}$ with a dummy predicate).
Then $\size{T}\cdot \size{\ensuremath{\mathcal{A}}}^m \leq \size{\ensuremath{\mathcal{A}}}^{m+1} = p(\size{\ensuremath{\mathcal{A}}})$.
As a consequence, we can again apply Theorem~\ref{thm:sparse-translation} and conclude that $(\ensuremath{\mathcal{A}},T) \vDash \varphi$ if and only if $\ensuremath{\mathcal{A}} \vDash \zeta^{p,\vv{x}}_\varphi(\vval{x}{T})$.
\end{proof}

\section{From FO$^2$(${\sim}$) to FO$^2$: Upper bounds for satisfiability}

\label{sec:upper-sat}

In this section, we prove that the satisfiability problem of $\ensuremath{\logic{FO}^2(\negg)}$ is decidable, and in fact, complete for $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$.

Our approach is to establish a finite model property for $\ensuremath{\logic{FO}^2(\negg)}$.
However, instead of attacking $\ensuremath{\logic{FO}^2(\negg)}$ directly, we reduce the logic to $\logic{FO}^2$, which has the exponential model property \cite{fo2}.
As a first step, we expand $\ensuremath{\logic{FO}^2(\negg)}$-formulas into disjunctive normal form with respect to $\land$ and ${\sim}$, using the laws depicted in the next lemma.

We use the abbreviations $\varphi \ovee \psi \dfn {\sim}({\sim} \varphi \land {\sim} \psi)$ (Boolean disjunction) and $\ensuremath\mathsf{E}\beta \dfn {\sim} \neg \beta$ ("at least one assignment in the team satisfies $\beta$").

\begin{lemma}\label{lem:axioms}
The following laws hold for $\ensuremath{\logic{FO}(\negg)}$:
\begin{alignat}{2}
&\alpha \land \bigwedge_{i=1}^n \ensuremath\mathsf{E}\beta_i &&\equiv \bigvee_{i=1}^n(\alpha \land \ensuremath\mathsf{E}\beta_i) \label{eq:flat-dist1} \\
&\bigvee_{i=1}^n(\alpha_i \land \ensuremath\mathsf{E} \beta_i) &&\equiv \Big(\bigvee_{i=1}^n \alpha_i\Big) \land \bigwedge_{i=1}^n \ensuremath\mathsf{E}(\alpha_i\land \beta_i) \label{eq:flat-dist2}\\
&(\vartheta_1 \ovee \vartheta_2) \lor \vartheta_3 &&\equiv (\vartheta_1 \lor \vartheta_3) \ovee (\vartheta_2 \lor \vartheta_3) \label{eq:ovee-lor-dist1}\\
&\vartheta_1 \lor (\vartheta_2 \ovee \vartheta_3) &&\equiv (\vartheta_1 \lor \vartheta_2) \ovee (\vartheta_1 \lor \vartheta_3) \label{eq:ovee-lor-dist2}\\
&\exists x\, (\vartheta_1 \ovee \vartheta_2) &&\equiv (\exists x\,\vartheta_1) \ovee (\exists x\, \vartheta_2) \label{eq:ovee-ex-dist}\\
&\exists x\, (\vartheta_1 \vee \vartheta_2) &&\equiv (\exists x\,\vartheta_1) \vee (\exists x\, \vartheta_2) \label{eq:lor-ex-dist}\\
&\exists x\, (\alpha \land \ensuremath\mathsf{E} \beta) &&\equiv (\exists x\, \alpha) \land \ensuremath\mathsf{E}\,\exists x\,(\alpha \land \beta) \label{eq:land-ex-dist}\\
&\forall x\, (\vartheta_1 \land \vartheta_2) &&\equiv (\forall x \, \vartheta_1) \land (\forall x \, \vartheta_2) \label{eq:land-all-dist}\\
&\forall x \, {\sim} \vartheta &&\equiv {\sim} \forall x \, \vartheta \label{eq:neg-all-dist}
\end{alignat}
\end{lemma}
\begin{proof}
For (\ref{eq:flat-dist1}), (\ref{eq:flat-dist2}) and (\ref{eq:lor-ex-dist}), see \cite[Lemma 4.13, 4.14 and D.1]{axiom-fo}, respectively.
For (\ref{eq:ovee-lor-dist1})--(\ref{eq:ovee-ex-dist}), see \cite[Proposition 5]{abramsky_strongly_2016}.
For (\ref{eq:land-all-dist})--(\ref{eq:neg-all-dist}), see \cite[Chapter 8]{vaananen_dependence_2007}.

For (\ref{eq:land-ex-dist}), the direction "$\vDash$" is clear, as $\alpha\land \ensuremath\mathsf{E}\beta$ implies both $\alpha$ and $\ensuremath\mathsf{E}(\alpha \land \beta)$.
For the converse direction, suppose $(\ensuremath{\mathcal{A}},T) \vDash \exists x \alpha$ and $(\ensuremath{\mathcal{A}},\hat{s}) \vDash \exists x (\alpha \land \beta)$ for some $\hat{s} \in T$.
Then there are $f \colon T \to \pow{\ensuremath{\mathcal{A}}}\setminus \{\emptyset\}$ and $b \in \ensuremath{\mathcal{A}}$ such that $(\ensuremath{\mathcal{A}},T^x_f) \vDash \alpha$ and $(\ensuremath{\mathcal{A}},\hat{s}^x_b) \vDash \alpha \land \beta$.
Define $g(\hat{s}) = f(\hat{s}) \cup \{b\}$ and $g(s) = f(s)$ for $s \in T \setminus \{\hat{s}\}$.
Then $T^x_g = T^x_f \cup \{ s^x_b \}$.
Consequently, $(\ensuremath{\mathcal{A}},T^x_g) \vDash \alpha \land \ensuremath\mathsf{E}\beta$, hence $(\ensuremath{\mathcal{A}},T) \vDash \exists x\, (\alpha \land \ensuremath\mathsf{E} \beta)$.
\end{proof}

\begin{lemma}\label{lem:expansion}
Every $\tau\text{-}\FONK{n}{k}$-formula $\varphi$ is equivalent to a formula of the form
\[
\psi \dfn \bigovee_{i = 1}^n  \left( \alpha_i \land \bigwedge_{j = 1}^{m_i} \ensuremath\mathsf{E} \beta_{i,j}\right)
\]
such that $\{\alpha_1,\ldots,\alpha_n,\beta_{1,1},\ldots,\beta_{n,m_n}\} \subseteq \tau\text{-}\logic{FO}^n_k$ and $\size{\psi} \leq \exp_{\bigO{\size{\varphi}}}(1)$.
\end{lemma}
In the following, \emph{disjunctive normal form} (DNF) refers to formulas in the above form.
\begin{proof}
Proof by induction on $\varphi$.
\begin{itemize}
\item If $\varphi$ is a Boolean combination of $\logic{FO}^n_k$-formulas (over ${\sim}$ and $\land$), then we obtain a DNF of size $\leq \size{\varphi}\cdot 2^{\size{\varphi}}$ similarly as for ordinary propositional logic.
\item If $\varphi = \vartheta_1 \lor \vartheta_2$ for $\vartheta_1$, $\vartheta_2$ in DNF, then
\begin{align*}
\varphi = \;&\bigovee_{i = 1}^n
\left( \alpha_i \land \bigwedge_{j =1}^{m_i} \ensuremath\mathsf{E} \beta_{i,j}\right) \;
\lor
\;\bigovee_{i = 1}^{k} \left( \gamma_i \land \bigwedge_{j = 1}^{\ell_i} \ensuremath\mathsf{E} \delta_{i,j} \right) \\
\equiv \;&\bigovee_{i = 1}^n
\bigvee_{j=1}^{m_i} (\alpha_i \land \ensuremath\mathsf{E} \beta_{i,j}) \;
\lor
\;\bigovee_{i = 1}^{k}  \bigvee_{j=1}^{\ell_i}( \gamma_i \land \ensuremath\mathsf{E} \delta_{i,j} )\tag{Lemma~\ref{lem:axioms}, (\ref{eq:flat-dist1})}\\
\equiv \;& \bigovee_{\substack{1 \leq i_1 \leq n\\1\leq i_2 \leq k}} \;\; \bigvee_{j=1}^{m_{i_1}} (\alpha_{i_1} \land  \ensuremath\mathsf{E} \beta_{i_1,j}) \lor \bigvee_{j=1}^{\ell_{i_2}} (\gamma_{i_2} \land \ensuremath\mathsf{E} \delta_{i_2,j} ) \tag{Lemma~\ref{lem:axioms}, (\ref{eq:ovee-lor-dist1}) and  (\ref{eq:ovee-lor-dist2})}\\
\equiv \;& \bigovee_{i = 1}^{n\cdot k}  \; \bigvee_{j=1}^{o_i} (\mu_{i,j} \land  \ensuremath\mathsf{E} \nu_{i,j}) \tag{where $\mu_{i,j},\nu_{i,j} \in \logic{FO}^n_k$}\\
\equiv \;& \bigovee_{i = 1}^{n\cdot k} \Big(\bigvee_{j=1}^{o_i} \mu_{i,j}\Big) \land \bigwedge_{j = 1}^{o_i} \ensuremath\mathsf{E}(\mu_{i,j} \land \nu_{i,j})\text{,}\tag{Lemma~\ref{lem:axioms}, (\ref{eq:flat-dist2})}
\end{align*}
where the final DNF has size polynomial in $\size{\vartheta_1} + \size{\vartheta_2} \leq \size{\varphi}$.
\item If $\varphi = \exists x \, \vartheta$ for $\vartheta$ in DNF, then
\begin{align*}
\varphi \equiv\;& \exists x \,\bigovee_{i = 1}^n \bigvee_{j=1}^{m_i} (\alpha_i \land  \ensuremath\mathsf{E} \beta_{i,j}) \tag{Lemma~\ref{lem:axioms}, (\ref{eq:flat-dist1})}\\
\equiv\; & \bigovee_{i = 1}^n \bigvee_{j=1}^{m_i} \exists x \,(\alpha_i \land  \ensuremath\mathsf{E} \beta_{i,j}) \tag{Lemma~\ref{lem:axioms}, (\ref{eq:ovee-ex-dist}) and (\ref{eq:lor-ex-dist})}\\
\equiv\; & \bigovee_{i = 1}^n \bigvee_{j=1}^{m_i} \Big( (\exists x \,\alpha_i) \land  \ensuremath\mathsf{E}\exists x \,(\alpha_i \land \beta_{i,j}) \Big) \tag{Lemma~\ref{lem:axioms}, (\ref{eq:land-ex-dist})}\\
\equiv \; & \bigovee_{i = 1}^n \Big(\bigvee_{j=1}^{m_i} \exists x\, \alpha_i \Big) \land \bigwedge_{j=1}^{m_i} \ensuremath\mathsf{E}\exists x\, (\alpha_i\land \beta_{i,j}))\text{,}\tag{Lemma~\ref{lem:axioms}, (\ref{eq:flat-dist2})}
\end{align*}
which is again a DNF of polynomial size.
\item Finally, the $\forall$ case is due to (\ref{eq:land-all-dist}) and (\ref{eq:neg-all-dist}) of Lemma~\ref{lem:axioms}.\qedhere
\end{itemize}
\end{proof}

\begin{theorem}\label{thm:fo2-modelsize}
If $\tau$ is a relational vocabulary, then every satisfiable $\varphi \in \tau\text{-}\ensuremath{\logic{FO}^2(\negg)}$ has a model of size $\exp_{\bigO{\size{\varphi}}}(1)$.
\end{theorem}
\begin{proof}
Let $\varphi \in \tau\text{-}\ensuremath{\logic{FO}^2(\negg)}$ be satisfiable.
By Lemma~\ref{lem:expansion}, $\varphi$ is equivalent to a DNF of size $\exp_{\bigO{\size{\varphi}}}(1)$, which then has at least one satisfiable disjunct
\[
\psi = \alpha \land \bigwedge_{i=1}^m \ensuremath\mathsf{E} \beta_i\text{,}
\]
where $\{\alpha,\beta_1,\ldots,\beta_m\} \subseteq \tau\text{-}\logic{FO}^2$ and w.l.o.g.\@\xspace $\mathsf{Var}(\psi) \subseteq \{x,y\}$.
Let $(\ensuremath{\mathcal{A}}, T)$ be a model of $\psi$.
We show that $\psi$, and hence $\varphi$, has a model $(\ensuremath{\mathcal{B}},T')$ of size $2^{\bigO{\size{\psi}^2}}$.

Observe that $\ensuremath{\mathcal{A}}$ satisfies the classical $\logic{FO}^2$-sentence
\[
\gamma \dfn \bigwedge_{i=1}^m \exists x\,\exists y\, \alpha \land \beta_i\text{,}
\]
since for every $i$, $(\ensuremath{\mathcal{A}},T)\vDash \alpha \land\ensuremath\mathsf{E} \beta_i$, which implies that there is $s \in T$ such that $(\ensuremath{\mathcal{A}},s) \vDash \alpha \land \beta_i$, i.e.\@\xspace, $\ensuremath{\mathcal{A}} \vDash \exists x \exists y \alpha \land \beta_i$.

By \citet{fo2}, if $\delta$ is a satisfiable $\logic{FO}^2$-formula over a relational vocabulary, then $\delta$ has a model of size $2^{\bigO{\size{\delta}}}$ (in Tarski semantics).
Let $\ensuremath{\mathcal{B}}$ the corresponding model of $\gamma$ of size $2^{\bigO{\size{\gamma}}} \subseteq 2^{\bigO{\size{\psi}^2}}$.
Then for every $i$ there exists $\hat{s}_i \colon \{x,y\} \to \ensuremath{\mathcal{B}}$ such that $(\ensuremath{\mathcal{B}},\hat{s}_i) \vDash \alpha \land \beta_i$.
Consequently, $(\ensuremath{\mathcal{B}},\{\hat{s}_1,\ldots,\hat{s}_m\}) \vDash \psi$.
\end{proof}

\begin{corollary}\label{cor:fo2-upperbound}
If $\tau$ is a relational vocabulary, then $\ensuremath{\mathsf{SAT}}(\tau\text{-}\ensuremath{\logic{FO}^2(\negg)})$ and $\ensuremath{\mathsf{VAL}}(\tau\text{-}\ensuremath{\logic{FO}^2(\negg)})$ are in $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$.
\end{corollary}
\begin{proof}
By Corollary~\ref{cor:mcfo2-upper1}, model checking for $\ensuremath{\logic{FO}^2(\negg)}$ is possible in alternating polynomial time, and hence in deterministic exponential time.
In order to obtain a $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$-algorithm for $\ensuremath{\mathsf{SAT}}(\tau\text{-}\ensuremath{\logic{FO}^2(\negg)})$, given a formula $\varphi \in \tau\text{-}\ensuremath{\logic{FO}^2(\negg)}$, we can now iterate over all interpretations $(\ensuremath{\mathcal{A}},T)$ of size $\exp_{\bigO{\size{\varphi}}}(1)$ and perform model checking on $(\ensuremath{\mathcal{A}},T,\varphi)$.
\end{proof}
 \section{From MTL to FO$^2$(${\sim}$): Lower bounds}

\label{sec:lower}

For the lower bounds, we reduce from the model checking and the satisfiability problem of $\logic{MTL}$ and its fragments.
As a part of the reduction, in this section we present a semantics-preserving translation from $\logic{MTL}$ to $\ensuremath{\logic{FO}^2(\negg)}$.

The \emph{standard translation} embeds modal logic $\logic{ML}$ into $\logic{FO}^2$ with the relational vocabulary $\tau_M = (R,P_1,P_2,\ldots)$, where $\arity{R} = 2$ and $\arity{P_i} = 1$.
The standard translation of an $\logic{ML}$-formula is denoted by $\mathsf{st}_x(\varphi)$ resp.\ $\mathsf{st}_y(\varphi)$ and defined recursively:
\begin{align*}
\mathsf{st}_x(p_i)&\dfn P_ix \;\text{ for }p_i \in \ensuremath\mathcal{PS} &
\mathsf{st}_x(\neg \alpha) &\dfn \neg \mathsf{st}_x(\alpha)\\
\mathsf{st}_x(\Box \alpha) & \dfn \forall y \, Rxy \rightarrow \mathsf{st}_y(\alpha) &
\mathsf{st}_x(\alpha \land \beta)& \dfn \mathsf{st}_x(\alpha) \land \mathsf{st}_x(\beta)\\
\mathsf{st}_x(\Diamond \alpha) & \dfn \exists y \, Rxy \land \mathsf{st}_y(\alpha) &
\mathsf{st}_x(\alpha \lor \beta)& \dfn \mathsf{st}_x(\alpha) \lor \mathsf{st}_x(\beta)\text{,}
\end{align*}
with $\mathsf{st}_y(\alpha)$ defined symmetrically via $\mathsf{st}_x(\alpha)$.
The corresponding \emph{first-order interpretation} of a Kripke structure $\ensuremath{\mathcal{K}} = (W,\ensuremath{\mathcal{R}},V)$ is the $\tau_M$-structure $\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}})$ such that $\dom \ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}) = W$, $R^{\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}})} = \ensuremath{\mathcal{R}}$ and $P_i^{\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}})} = V(p_i)$.
For a world $w$, define $w^x \colon \{ x \} \to W$ by $w^x(x) = w$.

The next theorem is standard (see, e.g.\@\xspace, \citet{blackburn_modal_2001}):

\begin{theorem}\label{thm:st-trans-ml}
Let $(\ensuremath{\mathcal{K}},w)$ be a pointed Kripke structure and $\alpha \in \logic{ML}$.
Then
$(\ensuremath{\mathcal{K}},w) \vDash \alpha$ if and only if $(\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),w^x) \vDash \mathsf{st}_x(\alpha)$.
\end{theorem}

In this section, we lift this result to team semantics and translate $\logic{MTL}$ to $\ensuremath{\logic{FO}^2(\negg)}$.
On the model side, the first-order interpretation of a team $T$ in a Kripke structure becomes $T^x \dfn \Set{ w^x | w \in T}$.

The standard translation for $\logic{MTL}$ now extends that of $\logic{ML}$ by the final ${\sim}$-case and also implements the $\Box$-case with  $\hookrightarrow$ instead of $\rightarrow$:
\begin{align*}
\mathsf{st}_x(p_i)&\dfn P_ix \;\text{ for }p_i \in \ensuremath\mathcal{PS} &
\mathsf{st}_x(\neg \varphi) &\dfn \neg \mathsf{st}_x(\varphi)\\
\mathsf{st}_x(\Box \varphi) & \dfn \forall y \, Rxy \hookrightarrow \mathsf{st}_y(\varphi) &
\mathsf{st}_x(\varphi \land \psi)& \dfn \mathsf{st}_x(\varphi) \land \mathsf{st}_x(\psi)\\
\mathsf{st}_x(\Diamond \varphi) & \dfn \exists y \, Rxy \land \mathsf{st}_y(\varphi) &
\mathsf{st}_x(\varphi \lor \psi)& \dfn \mathsf{st}_x(\varphi) \lor \mathsf{st}_x(\psi)\\
\mathsf{st}_x({\sim} \varphi) & \dfn {\sim} \mathsf{st}_x(\varphi)\text{,} & &
\end{align*}
with $\mathsf{st}_y(\varphi)$ again defined symmetrically.
It is easy to see that the "classical" translation of $\Box\varphi$ to $\forall y \, Rxy \to \mathsf{st}_y(\varphi) = \forall y \, (\neg Rxy \lor \mathsf{st}_y(\varphi))$ is unsound under team semantics, and using $\forall y\, Rxy \hookrightarrow \mathsf{st}_y(\varphi) = \forall y\, (\neg Rxy \lor Rxy \land \mathsf{st}_y(\varphi))$ is indeed required.

\begin{theorem}\label{thm:translation}
For all Kripke structures with team $(\ensuremath{\mathcal{K}},T)$, all $\varphi \in \logic{MTL}$ and any first-order variable $x$ it holds $(\ensuremath{\mathcal{K}},T) \vDash \varphi$ if and only if $(\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),T^x)\vDash \mathsf{st}_x(\varphi)$.
\end{theorem}
\begin{proof}
Proof by induction on $\varphi$.
Here, we omit $\ensuremath{\mathcal{K}}$ and $\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}})$ and write, e.g.\@\xspace, $T \vDash \varphi$.

\begin{itemize}
\item $\varphi \in \logic{ML}$: We have $(\ensuremath{\mathcal{K}},T)\vDash \varphi$ iff $\forall w\in T\colon (\ensuremath{\mathcal{K}},w)\vDash \varphi$ by definition of the semantics of $\logic{MTL}$, which by Theorem~\ref{thm:st-trans-ml} is equivalent to $\forall w^x \in T^x\colon (\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),w^x)\vDash \mathsf{st}_x(\varphi)$.
However, as $\mathsf{st}_x(\varphi) \in \logic{FO}$, the latter is equivalent to $(\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),T^x)\vDash \mathsf{st}_x(\varphi)$ by the semantics of $\ensuremath{\logic{FO}(\negg)}$.

\item $\varphi = \psi \land \vartheta$ and $\varphi = {\sim} \psi$ are clear.
\item $\varphi = \psi \lor \theta$:
Suppose $T \vDash  \psi \lor \theta$.
Then $T = S \cup U$ such that $S \vDash \psi$ and $U \vDash \theta$.
By induction hypothesis, $S^x \vDash \mathsf{st}_x(\psi)$ and $U^x \vDash \mathsf{st}_x(\theta)$.
As $S \cup U = T$, clearly $S^x \cup U^x = T^x$.
As a consequence, $T^x \vDash \mathsf{st}_x(\psi) \lor \mathsf{st}_x(\theta) = \mathsf{st}_x(\psi \lor \theta)$.

\smallskip

For the other direction, suppose $T^x \vDash \mathsf{st}_x(\psi\lor\theta) = \mathsf{st}_x(\psi) \lor \mathsf{st}_x(\theta)$ by the means of some subteams $S' \cup U' = T^x$ such that $S' \vDash \mathsf{st}_x(\psi)$ and $U' \vDash \mathsf{st}_x(\theta)$.
Then $S' = S^x$ and $U' = U^x$ for some suitably chosen $S,U \subseteq T$.
By induction hypothesis, $S\vDash \psi$ and $U\vDash \theta$.
In order to prove $T\vDash \psi\lor\theta$, it remains to show $T \subseteq S \cup U$.
For this purpose, let $w \in T$.
As then $w^x \in T^x$, as least one of $w^x \in S'$ or $w^x \in U'$ holds.
But then $w \in S$ or $w \in U$.
\item $\varphi = \Box\psi$:
We define subteams $S$ and $U$ of the duplicating team $(T^x)^y_W$ as follows: $S$ contains all "outgoing edges": $S \dfn \{ s \in (T^x)^y_W \mid s(y) \in Rs(x) \}$.
On the other hand, $U$ contains all "non-edges":
$U \dfn \{ s \in (T^x)^y_W \mid s(y) \notin Rs(x) \}$.
Then clearly $(T^x)^y_W = S \cup U$, $S \vDash Rxy$ and $U \vDash \neg Rxy$.
Moreover, the above division of $(T^x)^y_W$ into $S$ and $U$ is the \emph{only} possible splitting of $(T^x)^y_W$ such that $S \vDash Rxy$ and $U \vDash \neg Rxy$.

By induction hypothesis, clearly $T\vDash \Box\psi \Leftrightarrow (RT)^y \vDash \mathsf{st}_y(\psi)$.
Moreover, by the above argument, $T^x \vDash \mathsf{st}_x(\Box \psi) \Leftrightarrow S \vDash \mathsf{st}_y(\psi)$.
Consequently, it suffices to show that $(RT)^y$ and $S$ agree on $\mathsf{st}_y(\psi)$.
This follows from Proposition~\ref{prop:free-vars}, since
\begin{align*}
(RT)^y &= \{ s\colon \{y\} \to W \mid \exists w \in T : s(y) \in Rw  \}\\
&= \{ \rest{s}{y} \mid s \in (T^x)^y_W \text{ and }s(y) \in Rs(x) \} = \rest{S}{y}\text{.}
\end{align*}
\item $\varphi = \Diamond\psi$:
Suppose $T \vDash \Diamond \psi$, i.e.\@\xspace, $S \vDash \psi$ for some successor team $S$ of $T$.
By induction hypothesis, $S^y \vDash \mathsf{st}_y(\psi)$.
In order to prove $T^x \vDash \exists y \, Rxy \land \mathsf{st}_y(\psi)$, we define a supplementing function $f : T^x \to \pow{W}\setminus \{\emptyset\}$ such that $(T^x)^y_f \vDash Rxy \land \mathsf{st}_y(\psi)$.

Let $f(w^x) \dfn Rw \cap S$.
Then $f(w^x)$ is non-empty for each $w$, as $S$ is a successor team.
Moreover, $(T^x)^y_f \vDash Rxy$.
It remains to show that $(T^x)^y_f\vDash \mathsf{st}_y(\psi)$ follows from $S^y \vDash \mathsf{st}_y(\psi)$.
Here, we combine Proposition~\ref{prop:rel} and \ref{prop:free-vars}, since
\[
y\langle S^y \rangle = S = \bigcup_{w \in T} Rw \cap S = \bigcup_{w^x \in T^x} f(w^x) = \{ s(y) \mid s \in (T^x)^y_f\} = y\langle (T^x)^y_f\rangle\text{.}
\]

For the other direction, suppose $T^x \vDash \exists y\, Rxy \land \mathsf{st}_y(\psi)$ by the means of a supplementing function $f : T^x \to \pow{W}\setminus \{\emptyset\}$ such that $(T^x)^y_f \vDash Rxy \land \mathsf{st}_y(\psi)$.

We define $S \dfn \bigcup_{w \in T} f(w^x)$, and first prove that it is a successor team of $T$, i.e.\@\xspace, that every $v\in S$ has a predecessor in $T$ and that every $w \in T$ has a successor in $S$.

Let $v \in S$.
Then there exists $w \in T$ such that $v \in f(w^x)$.
As a consequence, the assignment $s$ given by $s(x) = w$ and $s(y) = v$ is in $(T^x)^y_f$, and hence satisfies $Rxy$.
In other words, $v$ has a predecessor in $T$.
Conversely, if $w \in T$, then $f(w^x)$ is non-empty, i.e.\@\xspace, contains an element $v$.
As before, $v$ is a successor of $w$.
Since $v \in f(w^x)$, $v \in S$, so $w$ has a successor in $S$.

By a similar argument as above, $y\langle (T^x)^y_f\rangle = S = y\langle S^y\rangle$, hence $S^y \vDash \mathsf{st}_y(\psi)$, and consequently $S \vDash \psi$ by induction hypothesis.
\qedhere
\end{itemize}
\end{proof}

Next, we prove that the standard translation carries several complexity lower bounds into the first-order setting.

\begin{lemma}\label{lem:fo-mc-hardness-nk}
$\ensuremath{\mathsf{MC}}(\tau\text{-}\FONK{1}{0})$ is $\compclass{PSPACE}$-hard if $\tau$ contains infinitely many predicates.
\end{lemma}
\begin{proof}
We reduce from $\ensuremath{\mathsf{MC}}(\logic{PTL})$ (see Theorem~\ref{thm:mc-ptl}) via $(\ensuremath{\mathcal{K}},T,\varphi) \mapsto (\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),T^x,\mathsf{st}_x(\varphi))$.
(W.l.o.g.\@\xspace $\tau$ contains unary predicates $P_0, P_1, \ldots$; otherwise they are easily simulated by predicates of higher arity).

It is easy to see that $\mathsf{st}_x(\varphi)$ is quantifier-free and contains only the variable $x$.
Moreover, by Theorem~\ref{thm:translation}, $(\ensuremath{\mathcal{K}},T) \vDash \varphi\Leftrightarrow (\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}),T^x) \vDash \mathsf{st}_x(\varphi)$.
\end{proof}

\begin{lemma}\label{lem:fo-mc-hardness}
$\ensuremath{\mathsf{MC}}(\tau\text{-}\FONK{\omega}{\omega})$ is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-hard for all vocabularies $\tau$, even on sentences and for a fixed $\tau$-structure $\ensuremath{\mathcal{A}}$ with domain $\{0,1\}$ and a fixed team $\{\emptyset\}$.
\end{lemma}
\begin{proof}
We reduce from $\ensuremath{\mathsf{SAT}}(\logic{PTL})$ (see Theorem~\ref{thm:sat-ptl}).
Given $\varphi \in \logic{PTL}$, suppose $\mathsf{Prop}(\varphi) = \{p_1,\ldots,p_n\}$.
The idea is that a team of worlds, or rather its induced set of Boolean assignments to $p_1,\ldots,p_n$, is simulated by a corresponding team of first-order assignments $s \colon X \to B$, where $X = \{z,x_1,\ldots,x_n\}$ and $B \dfn \{0,1\}$.
Here, the auxiliary variable $z$ plays the role of the constant $1$.
Let $V_b = (\{\emptyset\}^{z}_{\{b\}})^{x_1}_B\cdots^{x_n}_B$ for $b \in B$, i.e.\@\xspace, the team $\{\emptyset\}$ after $n+1$ supplementations with $\{b\}$ resp.\ $B$.

\smallskip

By definition of vocabulary, either ${=} \in \tau$ or $\tau$ contains a predicate.
First, we consider the case ${=} \in \tau$.
We map $\varphi$ to $(\ensuremath{\mathcal{A}},\{\emptyset\},\psi)$, where $\dom \ensuremath{\mathcal{A}} = B$,
$\psi \dfn \exists z\, \forall x_1 \cdots \forall x_n\, \top \lor \varphi^*$, and $\varphi^*$ is obtained from $\varphi$ by replacing each $p_i$ by $x_i = z$.
We prove that the reduction is correct.

To begin with, observe that
\begin{align*}
(\exists U \subseteq V_1 : (\ensuremath{\mathcal{A}},U) \vDash \varphi^*) \Leftrightarrow (\ensuremath{\mathcal{A}},V_1) \vDash \top \lor \varphi^* \Leftrightarrow (\ensuremath{\mathcal{A}},\{\emptyset\})\vDash \psi\text{.}\tag{$\star$}
\end{align*}
Here, "$\Rightarrow$" is clear.
We prove "$\Leftarrow$":
If $(\ensuremath{\mathcal{A}},\{\emptyset\})\vDash \psi$, then $(\ensuremath{\mathcal{A}},U) \vDash \varphi^*$ for some $U \subseteq V_0 \cup V_1$, but for each $s \in U \cap V_0$ we can simply flip all values of $s$.
It is easily proven with Lemma~\ref{lem:expansion} that this does not change the truth of the quantifier-free formula $\varphi^*$.

\smallskip

Next, assume that $\varphi$ is satisfiable, i.e.\@\xspace, $(\ensuremath{\mathcal{K}},T) \vDash \varphi$ for some Kripke structure with team $(\ensuremath{\mathcal{K}},T)$.
For each world $w\in T$, define $s_w \colon X \to B$ by $s_w(z) = 1$ and $s_w(x_i) = 1 \Leftrightarrow (\ensuremath{\mathcal{K}},w) \vDash p_i$.
Then $(\ensuremath{\mathcal{K}},w) \vDash p_i \Leftrightarrow (\ensuremath{\mathcal{A}},s_w) \vDash x_i = z$, and by induction on the syntax of $\varphi$ we obtain $(\ensuremath{\mathcal{A}},U) \vDash \varphi^*$, where $U \dfn \{ s_w  \mid w \in T \}$.
Since $U \subseteq V_1$, $(\star)$ yields $(\ensuremath{\mathcal{A}},\{\emptyset\}) \vDash \psi$.
The other direction is similar.

\smallskip

Next, consider the case where ${=} \notin \tau$; then $\tau$ contains a predicate $P$.
We define $\ensuremath{\mathcal{A}}$ as above, but let $P^\ensuremath{\mathcal{A}} \dfn \{ (1,\ldots,1) \}$.
Furthermore, $\psi \dfn \forall x_1 \cdots \forall x_n\, \top \lor \varphi^*$, and $\varphi^*$ is now $\varphi$ with $p_i$ replaced by $P(x_i,\ldots,x_i)$.
The remaining proof is similar to the previous one.
\end{proof}

Clearly, the standard translation of satisfiable formulas is itself satisfiable.
A converse result holds as well.
Loosely speaking, from a first-order structure (with team) satisfying $\mathsf{st}_x(\varphi)$ we can reconstruct a Kripke model (with team) for $\varphi$.

\begin{lemma}\label{lem:reverse-trans}
If $\varphi \in \logic{MTL}$, then $\varphi$ is satisfiable if and only if $\mathsf{st}_x(\varphi)$ is satisfiable.
\end{lemma}
\begin{proof}
As Theorem~\ref{thm:translation} proves "$\Rightarrow$", we consider "$\Leftarrow$".
Suppose $(\ensuremath{\mathcal{B}},S) \vDash \mathsf{st}_x(\varphi)$.
Then $\ensuremath{\mathcal{B}}$ interprets the binary predicate $R$ and unary predicates $P_1,P_2,\ldots$.
By Proposition~\ref{prop:free-vars}, w.l.o.g.\@\xspace $S$ has domain $\{x\}$, i.e.\@\xspace, $S = (x \langle S \rangle)^x$.

Define now the Kripke structure $\ensuremath{\mathcal{K}} = (\dom \ensuremath{\mathcal{B}}, R^\ensuremath{\mathcal{B}}, V)$ such that $V(p_i) \dfn P_i^\ensuremath{\mathcal{B}}$.
Then clearly $\ensuremath{\mathcal{A}}(\ensuremath{\mathcal{K}}) = \ensuremath{\mathcal{B}}$.
By Theorem~\ref{thm:translation}, $(\ensuremath{\mathcal{K}},x\langle S \rangle) \vDash \varphi$.
\end{proof}

\subsection*{Completeness results}

\begin{theorem}\label{thm:mc-completeness}
Let $\ensuremath{\mathcal{D}}$ be a p-uniform set of dependencies and $\tau$ a vocabulary.
\begin{itemize}
\item $\ensuremath{\mathsf{MC}}(\tau\text{-}\FONKD{\omega}{\omega})$ is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete, with hardness also on sentences and for a fixed $\tau$-structure $\ensuremath{\mathcal{A}}$ with domain $\{0,1\}$ and a fixed team $\{\emptyset\}$.
\item If $\tau$ contains infinitely many relations and at least one of $k \geq 0,n\geq 1$ is finite, then $\ensuremath{\mathsf{MC}}(\tau\text{-}\FONKD{n}{k})$ is $\compclass{PSPACE}$-complete.
\end{itemize}
\end{theorem}
\begin{proof}
The upper bounds are due to Corollary~\ref{cor:fo-mc} and~\ref{cor:mcfo2-upper1}, since alternating polynomial time coincides with $\compclass{PSPACE}$ \cite{alternation}.
The lower bounds are due to Lemma~\ref{lem:fo-mc-hardness-nk} and~\ref{lem:fo-mc-hardness}.
\end{proof}

In particular, the model checking problem for first-order team logic, independence logic, inclusion and exclusion logic with Boolean negation is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete.
Likewise, their two-variable fragments are $\compclass{PSPACE}$-complete.
This implies a straightforward generalization of a result of \citet[Proposition 33]{Lohrey12}:

\begin{corollary}
$\ensuremath{\mathsf{MC}}(\tau\text{-}\logic{SO})$ is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete for all vocabularies $\tau$, with hardness also on sentences and with a fixed $\tau$-interpretation $\ensuremath{\mathcal{A}}$ with $\dom \ensuremath{\mathcal{A}} = \{0,1\}$.
\end{corollary}
\begin{proof}
By Proposition~\ref{prop:so-mc}, and reduction from $\ensuremath{\mathsf{MC}}(\tau\text{-}\logic{FO}({\sim}))$.
Let $R$ be a $0$-ary relation variable.
In the spirit of Corollary~\ref{cor:fo-mc}, we map $(\ensuremath{\mathcal{A}},\{\emptyset\},\varphi)$ to $(\ensuremath{\mathcal{A}},\emptyset,\exists R \; \eta^{\emptyset}_\varphi(R) \land R)$.
\end{proof}

The next theorem states the main result of this paper.

\begin{theorem}\label{thm:main-sat}
Let $\tau$ contain at least one binary predicate, infinitely many unary predicates, and no functions.
\begin{itemize}
\item $\ensuremath{\mathsf{SAT}}(\tau\text{-}\ensuremath{\logic{FO}^2(\negg)})$ and $\ensuremath{\mathsf{VAL}}(\tau\text{-}\ensuremath{\logic{FO}^2(\negg)})$ are $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$-complete.
\item $\ensuremath{\mathsf{SAT}}(\tau\text{-}\FONK{2}{k})$ and $\ensuremath{\mathsf{VAL}}(\tau\text{-}\FONK{2}{k})$ are $\KAXX{k+1}$-hard if $k \geq 0$.
\end{itemize}
\end{theorem}
\begin{proof}
The upper bound for $\tau\text{-}\ensuremath{\logic{FO}^2(\negg)}$ is by Corollary~\ref{cor:fo2-upperbound}.
For the lower bounds, the mapping $\varphi \mapsto \mathsf{st}_x(\varphi)$ is a reduction from $\ensuremath{\mathsf{SAT}}(\logic{MTL})$ resp.\ $\ensuremath{\mathsf{SAT}}(\logic{MTL}_k)$ (see Theorem~\ref{thm:mtl-sat} and Lemma~\ref{lem:reverse-trans}).
The validity case is similar.
\end{proof}

\section{Conclusion}

In this paper, we proved that the logic $\ensuremath{\logic{FO}^2(\negg)}$ is complete for the class $\ensuremath{\compclass{TOWER}(\mathrm{poly})}$ and hence decidable (Theorem~\ref{thm:main-sat}).
In particular, it has the finite model property (Theorem~\ref{thm:fo2-modelsize}), but exhibits non-elementary succinctness compared to classical $\logic{FO}^2$, which enjoys an exponential model property~\cite{fo2}.

Since validity is undecidable for two-variable dependence logic $\logic{D}^2$ \cite{il2} but not for $\ensuremath{\logic{FO}^2(\negg)}$, we conclude that team semantics with the dependence atom ${=\!\!(\cdot,\cdot)}$ leads to undecidability, but with the Boolean negation ${\sim}$ it leads only to non-elementary blowup.

\smallskip

For $\FONKD{n}{k}$, where $n \geq 1$ and $k \geq 0$, we proved a dichotomy regarding its model checking complexity (Theorem~\ref{thm:mc-completeness}):
It is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete if $n = k = \omega$, and otherwise $\compclass{PSPACE}$-complete.
However, both results hold for arbitrary sets of dependence atoms that are (polynomial time uniformly) definable in $\logic{FO}$.

In particular, $\ensuremath{\mathsf{MC}}(\logic{TL})$ is $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete, which naturally extends the result of \citet{mc-games} that $\ensuremath{\mathsf{MC}}(\logic{D})$ is $\compclass{NEXPTIME}$-complete.
However, the former model checking problem stays $\ensuremath{\compclass{ATIME}\text{-}\compclass{ALT}(\mathrm{exp},\mathrm{poly})}$-complete even without the dependence atom, while ordinary $\ensuremath{\mathsf{MC}}(\logic{FO})$ becomes $\compclass{PSPACE}$-complete for both classical and team semantics \cite{mc-games}.

\smallskip

In order to prove some of the lower bounds, we introduced a "standard translation" from $\logic{MTL}$ to $\ensuremath{\logic{FO}^2(\negg)}$ that extends the usual translation from $\logic{ML}$ to $\logic{FO}^2$, and also established $\KAXX{k+1}$-hardness of the satisfiability problem of $\FONK{2}{k}$.
Here, the upper bound is still missing.
In the modal setting, every satisfiable $\logic{MTL}_k$-formula has a $(k+1)$-fold exponential model.
It would be interesting to learn whether $\FONK{2}{k}$ has a similar small model property.
Together with Corollary~\ref{cor:mcfo2-upper1}, a positive answer would immediately yield a matching $\KAXX{k+1}$ upper bound.

\printbibliography

\clearpage

redpajama_set_name: RedPajamaArXiv


Speaker of the House of Representatives, Hon Yakubu Dogara, has commended President Muhammadu Buhari on the release of the female students abducted from their school in Dapchi, Yobe State.
He said the President's efforts to ensure that the girls were freed from captivity has yielded results with the hope of ending years of violent insurgency in the North East.
He, however, called for proactive steps to be taken to forestall a reoccurrence of the incident by security agencies.
"We must remind all those concerned that mass abduction of innocent schoolgirls should never have been allowed to happen in the first place. While we await the outcome of the investigation by the House Ad hoc Committee, the House of Representatives will not accept any further excuses or buck passing between the various security agencies.
Hon Dogara noted that intelligence gathering must be strengthened to prevent attacks before they occur.
While commiserating with the released girls, their parents and families for the ordeal they went through, the speaker gave assurances of the House of Representatives' readiness to continue to promote the security of lives and properties of Nigerians working in concert with the Executive.
He also added that efforts should be intensified to free the remaining Dapchi and Chibok schoolgirls and indeed all those in captivity.


text:
Nanjing railway station () is a major railway station of Nanjing, the capital of Jiangsu province. It is located in the northern part of Nanjing's urban core (just a short walk from the city wall), near Xuanwu Lake.

Services
Until 2010, this was the main railway station of Nanjing, with the great majority of all trains serving Nanjing using this station. Only a  small number of trains, going to the destinations to the southwest of Nanjing, pass through the (old) Nanjing South railway station, which is located south of Nanjing's walled city; service to Nanjing West railway station has been suspended.

After the opening of new Nanjing South railway station in the southern part of greater Nanjing in mid-2010, many of the high-speed trains serving Nanjing have been re-routed to that new station. However, Nanjing station has frequent high-speed service to Shanghai and Shanghai Hongqiao, some services also stopping at Zhenjiang, Changzhou and Suzhou. Some overnight D trains continue on north towards Beijing South railway station, Tianjin West railway station, or Xi'an North railway station.

Nanjing railway station is served by a station of the same name on Line 1 and Line 3 of Nanjing Metro. It is also the terminal for many of the city bus lines.

History
The station opened in September 1968, shortly before the opening of the Nanjing Yangtze River Bridge. The connection with Line 1 of the Nanjing Metro began operations on 3 September 2005 as part of the line's Phase I from  to . The interchange with Nanjing Metro Line 3 opened on 1 April 2015 with the opening of that line.

On 30 September 2016 the metro station served a peak volume of 99,800 passengers.

See also
Zhonghuamen railway station (Nanjing)
Nanjing South railway station
Nanjing West railway station
Nanjing North railway station

References

External links

Nanjing Railway Station
Nanjing Railway Station Timetable

Railway stations in Nanjing
Stations on the Beijing–Shanghai Railway
Stations on the Shanghai–Nanjing Intercity Railway
Stations on the Shanghai–Wuhan–Chengdu high-speed railway
Nanjing Metro stations
Railway stations in China opened in 1968

redpajama_set_name: RedPajamaWikipedia


text:
Q: MvvmCross Android Bindings with dependent assembly Our main android app includes MvxBindingAttributes.xml to provide binding syntax to the android axml.
The issue I've run into, is when writing a plugin (dependent android assembly) which also has xaml definitions (the assembly has it's own MvxBindingAttributes.xml defined as a resource)
Now when compiling the app, compile errors moan that there are duplicate definitions for binding attributes.
Is there guidance on what pattern to follow to allow binding attributes to be used in the main app as well as the referenced android plugin code?

A: So it turns out the same resource cannot be defined in dependent assemblies, so the solution (for me) was to define a shared android assembly that contains common concerns (such as the MvxBindingsResource) which both the android app and android plugin assembly can reference.

redpajama_set_name: RedPajamaStackExchange


On the drive home today there were high clouds, sweeping in, showing the high wind currents. What made them noteworthy was that I could not immediately recognize whether the clouds were the white or grey bands.
There is something invigorating about the return to ever so slightly longer days.
Last week there was a day when I almost turned out the porch light as I left for work. Not quite, but the thought crossed my mind. And we are supposed to be free from rain for at least the next few days. Cold, but not raining (snowing).
I have heard rumors of dumping snow in the midwest.
I have not confirmed whether these will be impacting relatives here and there.
If you are impacted, I hope you are well-provisioned.
We are well provisioned here, and the thought of dinner is starting to penetrate my thoughts.
Smile, originally written by Charlie Chaplin, John Turner & Geoffrey Parsons.
I knew it from Nat King Cole. We just heard it sung by a woman (on the Bob Dylan's Theme Time Radio).
Apparently Chaplin wrote the tune for his film, Modern Times. I seem to remember seeing Modern Times at a theatre in downtown Ann Arbor, on Division or some nearby street (not the State or Michigan). It was a hot, hot summer day and Grandma R was visiting. We went to the theatre to have some fun and get out of the heat. I still vividly remember Charlie walking down the street with two wrenches in his hands, and a woman approaching from the other direction with nut-shaped buttons on her jacket.
Smile, the days are getting longer.
This entry was posted on January 31, 2011 at 7:01 pm and is filed under Uncategorized.	You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.


The Sky's unique design allows it to be easily mounted in an attic where other antennas are simply too large.
The Sky features a tightly integrated low noise state-of-the-art digital amplifier to increase the signal range and improve the quality of the HD broadcast signals. The amplifier is powered via a USB port or with the included power cube.
This Certified Refurbished product is tested & certified by Mohu to look and work like-new. The product includes all original accessories, and is backed by a 1 year warranty.
Weighing in at only 3 pounds, the Sky 60 Attic / Outdoor Antenna is a powerful, amplified antenna solution that was developed from research for the United States military.
The Sky is small, powerful, and unique. With the ability to provide uncompressed HD broadcast to multiple televisions in a home with a range of 60 miles, users will not have to settle with a large, bulky or more expensive rooftop-mounted antenna.
Get Mohu Sky 60 Multidirectional Amplified Indoor/Outdoor HDTV Antenna (Certified Refurbished) at the best price available today.
How would you rate the "Buy Discount Mohu Sky 60 Multidirectional Amplified Indoor/Outdoor HDTV Antenna (Certified Refurbished)"?


you may already be privy to the fact that the Burlington headquarters are located in Vermont.
from the Canadian border, attracting skiiers and snowboarders to its 76 trails from all over.
England. There's more snow, ski, snowboard, and outdoor fun than you'll know what to do with.
suitable for all outdoor enthusiasts.
#7 in TransWorld SNOWboarding magazine for its terrain parks.
Notch also is home to the East's only Triple Black Diamond trail.
challenge. You'll never be bored at Sugarbush Resort.
Vermont ski resorts today, Call Toll-Free, 877-4- SKI-EAST.


BpOlar is son of a jazz musician and as such he was raised from a very young age listening to the jazz masters, and although is approach diverted from this it is part of his background and as such is part of his aproach to the berlin electronic music scene. BpOlar is also a multidisciplinary artist, creating digital drawings and paintings and 3D video clips to document his music and for live usage, or the opposite (makes music to illustrate video). One of these works is presented together with this release.
BpOlar music is strongly focused on creating textures, with a close relation with ambient music. This textures are nonetheless rough and arid, and lead us to alien environments where beats, noises and voices all create suspense moments, where you feel alert all the way through. This release is composed of four tracks and a bonus movie, that complements this particular vision.
If you pay attention to BpOlar work you'll find, in his drawings/paintings, movies and music, traces of this imaginary world, where the central element is the feeling of unsettlement.


Book Cheap Calgary to Ottawa flight tickets at lowest price. Get Upto 20% Cashback to wallet upto Rs. 10,000 using coupon FLYINT on your international flight tickets only on MakeMyTrip. Also Book Ottawa to Calgary Flights. Currently 150 flights flying from Calgary to Ottawa. To save maximum on flight booking click on below Fare Calendar button and choose your dates.
What is the today's cheapest airfare from Calgary to Ottawa?
You can get the best airfare of Rs. 29248.0 when flying from Calgary to Ottawa.
How many flights fly from Calgary to Ottawa everyday?
There are 150 flights flying from Calgary to Ottawa every day.
What is the lowest airfare I can get from Calgary to Ottawa in the coming week ?
The lowest airfare for flying Calgary to Ottawa is Rs. 29248.0 This deal is available only for the next 7 days!