\subsection{Everything about the Projective Characterization Cases}

\bigskip

\probbox{
	\textbf{Problem:} $\mathrm{InProjHomCl}_\mathrm{(fin)}$\\
	\textbf{Input:} $\tau$, $\tau'$ with $\tau\subseteq\tau'$, sentence $\Phi$ over $\tau'$, finite $\tau$-structure $\mathfrak{A}$.\\
	\textbf{Output:} \textsc{yes}, if $\mathfrak{A} \in \homcl{\getffinmodels{\Phi}|_\tau}$, \textsc{no} otherwise.
}

\bigskip

\begin{proposition}
	$\mathrm{InHomCl}$ and $\mathrm{InProjHomCl}$ are \textsc{LogSpace}-interreducible, and so are
	$\mathrm{InHomCl}_\mathrm{fin}$ and $\mathrm{InProjHomCl}_\mathrm{fin}$.
\end{proposition}

\begin{proof}
	$\mathrm{InHomCl}_\mathrm{(fin)} \Rightarrow \mathrm{InProjHomCl}_\mathrm{(fin)}$: special case, pick $\tau=\tau'$.

	$\mathrm{InProjHomCl}_\mathrm{(fin)} \Rightarrow \mathrm{InHomCl}_\mathrm{(fin)}$: let $\sigma = \tau'\setminus \tau$. Then $\mathrm{InProjHomCl}_\mathrm{(fin)}$ holds for $\Phi$ and $\mathfrak{A}$ exactly if $\mathrm{InHomCl}_\mathrm{(fin)}$ holds for $\Phi$ and $\mathfrak{A}\cdot \widehat\sigma$.
\end{proof}

We conclude this section by briefly looking at the projective characterization variant of the homclosedness problem.

\bigskip

\probbox{
	\textbf{Problem:} $\mathrm{ProjHomClosed}_\mathrm{(fin)}$\\
	\textbf{Input:} $\tau$, $\tau'$ with $\tau\subseteq\tau'$, sentence $\Phi$ over $\tau'$.\\
	\textbf{Output:} \textsc{yes}, if $\getffinmodels{\Phi}|_\tau = \homclffin{\getffinmodels{\Phi}|_\tau}$, \textsc{no} otherwise.
}

\bigskip

As it turns out, the situation becomes pretty hopeless there; the problem turns undecidable already for very inexpressive logics,
since they allow for projectively characterizing $\neg(\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \wedge \neg\exists x.\sig{T}{}_\emptyset{}(x))$.

\begin{theorem}[restate=hopeless, name=]
	$\mathrm{ProjHomClosed}_\mathrm{(fin)}$ is undecidable even for
	\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item
		$\mbox{$\bal$}\mathbb{FO}$ with predicate arity $\leq 2$ and three constants,
		\item
		$\FO^\mathbbm{2}$ without constants, and
		\item
		$\mathbb{GFO}$ without constants and with maximum arity $\leq 3$.
	\end{enumerate}
\end{theorem}

\begin{proof}
	\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item
		Take $\neg\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)$, put it in prenex (carefully reusing variables where possible), skolemize leading existential quantifiers into constants. Choose $\tau$ such that the constants are removed.
		\item
		As before but ``paraphrase'' the three constants by unary predicates, axiomatized to be nonempty. Then choose $\tau$ such that the unary predicates are removed.
		\item
		Take  $\neg\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)$, put it in NNF. The obtained sentence is almost guarded, except for the subsentence with prefix $\exists xyz ...$, which we replace by $\exists xyz. \sig{Ter}(x,y,z) \wedge ...$ where $\sig{Ter}$ is a fresh ternary predicate. Then choose $\tau$ such that $\sig{Ter}$ is removed again.\qedhere
	\end{enumerate}
\end{proof}

\subsection{lost and found -- probably not longer needed}

\begin{definition}\label{def:TGDdettiling}
	Given a deterministic domino system
	$\mathcal{D}=(D,B,L,\sig{H}{},\sig{V}{})$, let $$\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} = \forall xyz. \exists v. \Phi_\mathcal{D}$$ where $\Phi_\mathcal{D}$ is the conjunction over the following rules (introducing unary predicates $\sig{T}{}_\emptyset$ and $\sig{T}{}_{\{d\}}$ for all the dominoes $d \in D_\mathcal{D}$):
	%
	\begin{eqnarray}
		& \!\!\!\!\to\!\!\!\! & Eq(x,x) \\
		Eq(x,y) \wedge Eq(y,z)  & \!\!\!\!\to\!\!\!\! & \sig{H}{}(x,v) \\
		\sig{H}{}(x,y) \wedge Eq(y,z)  & \!\!\!\!\to\!\!\!\! & \sig{V}{}(x,v) \\
		\sig{V}{}(x,y) \wedge Eq(y,z)  & \!\!\!\!\to\!\!\!\! & \sig{T}{}_{B \cap L}(v) \\
		%
		\sig{H}{}(x,y) \wedge \sig{V}{}(x,z) & \!\!\!\!\to\!\!\!\! & \sig{H}{}(z,v) \wedge \sig{V}{}(y,v)\\[2ex]
		\sig{T}{}_{\{d\}}(x) \wedge \sig{V}{}(x,y) & \!\!\!\!\to\!\!\!\! & \sig{T}{}_{\sig{V}{}(d)}(y) \\
		%
		\sig{T}{}_{\{d\}}(x) \wedge \sig{H}{}(x,y) & \!\!\!\!\to\!\!\!\! & \sig{T}{}_{\sig{H}{}(d)}(y) \\
		%
		\sig{T}{}_{\{d_1\}}(x) \wedge \sig{H}{}(x,z) \wedge \ \  \nonumber \\[-3pt]
		\sig{T}{}_{\{d_2\}}(y) \wedge \sig{V}{}(y,z) & \!\!\!\!\to\!\!\!\! &
		\sig{T}{}_{\sig{H}{}(d_1)\cap \sig{V}{}(d_2)}(y) \\
		%
		\sig{T}{}_{\{d_1\}}(x) \wedge \sig{T}{}_{\{d_2\}}(x) & \!\!\!\!\to\!\!\!\! &
		\sig{T}{}_{\{d_1\}\cap\{d_2\}}(x)
	\end{eqnarray}
	%
	%

\end{definition}

It is trivial to equivalently rewrite $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ into a \mbox{$\mathbb{TGD}$}{} sentence, so we will consider it as such, whenever convenient.

\begin{lemma}
	\begin{enumerate}
		\item
		$\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ is a $\mbox{$\Al\Al\Al\Ex\FO$}$ formula.
		\item
		Any -- finite or infinite -- model $\mathfrak{A}$ of $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ admits a homomorphism into and a homomorphism from $\mathfrak{A} \uplus \mathfrak{I}$, which is not a model of $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$.
		Moreover $\sig{T}{}_\emptyset{}^\mathfrak{A} = \sig{T}{}_\emptyset{}^{\mathfrak{A}\uplus \mathfrak{I}}$.
		\item
		$\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ has a (finite) model $\mathfrak{A}$ with $\sig{T}{}_\emptyset{}^\mathfrak{A} = \emptyset$
		exactly if there is a (ultimately periodic) $\mathcal{D}$-tiling.
		\item
		$\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ (finitely) entails the \mbox{$\mathbb{CQ}$}{} $\exists x.\sig{T}{}_\emptyset{}(x)$ exactly if there exists no
		(ultimately periodic) $\mathcal{D}$-tiling.
		\item
		The class of (finite) models of the \mbox{$\mathbb{MDTGD}$}{} sentence $\Psi = \Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)$ is closed under (finite-target) homomorphisms exactly if there exists no
		(ultimately periodic) $\mathcal{D}$-tiling. Moreover, $\Psi$ is a \mbox{$\mathbb{MDTGD}$}{} sentence and expressible as a $\mbox{$\Al\Al\Al\Ex\FO$}$ sentence.
	\end{enumerate}
\end{lemma}

\begin{corollary}
	$\mathrm{\sig{H}{}omClosed}_\mathrm{(fin)}$ is undecidable for \mbox{$\mathbb{MDTGD}$}{} (and hence for \mbox{$\mathbb{DTGD}$}{}).
	This even holds for \mbox{$\mathbb{DTGD}$}{} sentences wherein every rule uses only unary and binary predicates as well as $\leq$3 universally and $\leq$1 existentially quantified variables.
\end{corollary}

We will put to use the previously introduced machinery for a few more undecidability results.

\begin{lemma}
	$\neg\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)$
	\begin{enumerate}
		\item
		is equivalent to a \mbox{$\Ex\Ex\Ex\Al\FO$}{} sentence with all predicates of arity $\leq 2$,
		\item
		is (finitely) valid exactly if there is no (ultimately periodic) $\mathcal{D}$-tiling, and
		\item
		has a (finite) model class closed under (finite-target) homomorphisms exactly if it is (finitely) valid.
	\end{enumerate}
\end{lemma}

This directly entails the following theorem establishing undecidability for a $\FO_{=}$ fragment whose satisfiability problem is decidable (and, in fact, even in \textsc{NP}).

\begin{theorem}
	$\mathrm{\sig{H}{}omClosed}_\mathrm{(fin)}$ is undecidable for $\mbox{$\bex$}\Ex\mbox{$\bex$}\mbox{$\bal$}\mathbb{FO}$ even with predicates of arity $\leq 2$ and with no constants.
\end{theorem}

\subsection{Another Lost-and-Found: Open Prefix Classes (mostly fragments, really)}

With the above results established, the remaining prefix classes where decidability of $\mathrm{\sig{H}{}omClosed}_\mathrm{(fin)}$ is still open are $\mbox{$\Al\Ex\Ex\Ex\FO$}$, $\mbox{$\Ex\Al\Al\Al\FO$}$, $\mbox{$\Al\Ex\Ex\FOe$}$, and $\mbox{$\Ex\Al\Al\FOe$}$.

We now turn to $\mbox{$\Al\Ex\Ex\Ex\FO$}$

\begin{definition} Let $\mathcal{D}=(D,D,D,H,V)$ be a classical domino system.
	Let $\Phi^{\forall\exists\exists}_\mathcal{D}$ denote the $\mbox{$\Al\Ex\Ex\Ex\FO$}$ sentence $\forall x \exists yz. Exc(x) \vee (\sig{H}{}(x,y) \wedge \sig{V}{}(x,z))$.
	Let $\Phi^{\forall\forall\forall}_\mathcal{D}$ denote the $\mbox{$\Ex\Al\Al\Al\FO$}$ sentence $\forall xyz. \Psi$ where $\Psi$ is the conjunction over the following formulae:

	\noindent $\sig{H}{}(x,y) \, {\wedge}\,  \sig{V}{}(x,z) \, {\to}\, \sig{H}{}\sig{V}{}(y,z)$ \hfill $\sig{H}{}\sig{V}{}(x,y) \, {\wedge}\,  \sig{V}{}(y,z) \, {\to}\, \sig{H}{}(x,z)$\\
	\noindent $\sig{H}{}(x,y)\, {\to}\, \bigvee_{(d,d')\in \sig{H}{}} \sig{T}{}_{\{d\}}(x) \wedge \sig{T}{}_{\{d'\}}(y)$ \\
	\noindent $\sig{V}{}(x,y)\, {\to}\, \bigvee_{(d,d')\in \sig{V}{}} \sig{T}{}_{\{d\}}(x) \wedge \sig{T}{}_{\{d'\}}(y)$ \\
	\noindent $\sig{T}{}_{\{d\}}(x) \wedge \sig{T}{}_{\{d'\}}(x)\, {\to}\, \sig{T}{}_{\{d\}\cap \{d'\}}(x)$ \\
	\noindent $Exc(x) \to \bot$\\
	\noindent $\neg \sig{T}{}_{\emptyset}(x)$\\

	Moreover, for every $P \in \{\sig{H}{},\sig{V}{},\sig{H}{}\sig{V}{},Exc,\sig{T}{}_S\}$ we add $\neg P(\bold{x}) \leftrightarrow \overline{P}(\bold{x})$ as well as $\overline{P}(\bold{x}) \wedge P(\bold{x}) \to \bot$.

\end{definition}

\newcommand{\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}}{\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}}

\begin{lemma}
	\begin{enumerate}
		\item
		$\Phi^{\forall\exists\exists}_\mathcal{D} \wedge \Phi^{\forall\forall\forall}_\mathcal{D}$ is (finitely) satisfiable exactly if there exists a (ultimately periodic) $\mathcal{D}$-tiling.
		\item
		$\Phi^{\forall\exists\exists}_\mathcal{D}$ (finitely) entails $\neg \Phi^{\forall\forall\forall}_\mathcal{D}$ exactly if there exists no (ultimately periodic) $\mathcal{D}$-tiling.
		\item
		????$\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}$
		is finitely equivalent to $\neg \Phi^{\forall\forall\forall}_\mathcal{D}$ exactly if there exists no (ultimately periodic) $\mathcal{D}$-tiling.
		\item
		A (finite) spoiler of $\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}$ exists exactly if there exists a (ultimately periodic) $\mathcal{D}$-tiling.
	\end{enumerate}
\end{lemma}

\begin{proof}
	...

	Let $\mathfrak{A}\stackrel{h}{\to}\mathfrak{B}$ be a (finite) spoiler for $\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}$. Due to the absence of equality in our logic and thanks to Corollary~\ref{lem:inj-or-ss}, we can without loss of generality assume that $h$ is injective. By definition
	$\mathfrak{A} \in \getffinmodels{\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}}$ but $\mathfrak{B} \not\in \getffinmodels{\Phi^{\forall\exists\exists}_\mathcal{D}\! \wedge \!\!\, \neg \Phi^{\forall\forall\forall}_\mathcal{D}}$.
	In particular this means that $\mathfrak{B} \in \getffinmodels{\neg \Phi^{\forall\exists\exists}_\mathcal{D}}$ or $\mathfrak{B} \in \getffinmodels{\Phi^{\forall\forall\forall}_\mathcal{D}}$.

	We proceed by case distinction: assume $\mathfrak{B} \in \getffinmodels{\neg \Phi^{\forall\exists\exists}_\mathcal{D}}$. Then, there must be some $b \in B$ with
	$b \not\in Ex\sig{c}{}^\mathfrak{B}$ and ...

	Let now $B' = h(A)$ and let $\mathfrak{B}'$ denote the $B'$-induced substructure of $\mathfrak{B}$. Then $h:\mathfrak{A} \to \mathfrak{B}'$ is a surjective homomorphism, hence a bijection (since injectivity was already established above). As surjective homomorphisms preserve positive formulae, it follows that $\mathfrak{B}'\models \Phi^{\forall\exists\exists}_\mathcal{D}$.

	We proceed by case distinction as to whether $\mathfrak{B}'\models \Phi^{\forall\forall\forall}_\mathcal{D}$:

	Assume $\mathfrak{B}'\models \neg\Phi^{\forall\forall\forall}_\mathcal{D}$.
	But then $\mathfrak{B'}\stackrel{id_{B'}}{\to}\mathfrak{B}$ is an embedding spoiler.

	$\mathfrak{B} \in \getffinmodels{\neg \Phi^{\forall\exists\exists}_\mathcal{D}}$:
	This means there must be some

	Since $\Phi^{\forall\forall\forall}_\mathcal{D}$ is purely universal, this implies
	$\mathfrak{B}' \in \getffinmodels{\Phi^{\forall\forall\forall}_\mathcal{D}}$ and $h:\mathfrak{A} \to \mathfrak{B}'$ is a surjective homomorphism, hence a bijection (since injectivity was already established above).

	Moreover it is necessarily strong: the signature contains complement predicates, which are axiomatized such that $P^{\mathfrak{B}'} = B' \setminus \overline{P}^{\mathfrak{B}'}$. Thus assuming

	Surjective homomorphisms preserve positive sentences (i.e. sentences with arbitrary quantifiers but only the connectives $\wedge$ and $\vee$) (CITE SOME MODEL THEORY BOOK?)

\end{proof}

With $\mathrm{HomClosed}_\mathrm{(fin)}$ shown to be undecidable for $\mbox{$\Al\Al\Al\Ex\FO$}$ and $\mbox{$\Ex\Ex\Ex\Al\FO$}$ as well as $\mbox{$\Al\Al\Ex\FOe$}$ and $\mbox{$\Ex\Ex\Al\FOe$}$, the remaining maximal prefix classes (having a decidable satisfiability problem) are $\mbox{$\Ex^*\FOe$}$, $\mbox{$\Al^*\FOe$}$, $\mbox{$\Al\Al\Ex\Ex\FO$}$, $\mbox{$\Ex\Ex\Al\Al\FO$}$, $\mbox{$\Al\Ex\Ex\FOe$}$, and $\mbox{$\Ex\Al\Al\FOe$}$.

\subsection{On the Different Notions of Homclosure}

At the first glance, the different notions $\homcl{\getmodels{\Phi}}$, $\homclfin{\getmodels{\Phi}}$, $\homcl{\getfinmodels{\Phi}}$, and $\homclfin{\getfinmodels{\Phi}}$ might seem abundant and give rise to the question, if some of these may coincide. We show that this is not the case.

From $\getfinmodels{\Phi} \subseteq \getmodels{\Phi}$ and $\homclfin{\mathcal{C}} \subseteq \homcl{\mathcal{C}}$, one can directly infer the following inclusions:
\begin{itemize}
	\item
	$\homclfin{\getfinmodels{\Phi}} \subseteq \homcl{\getfinmodels{\Phi}}$
	\item
	$\homclfin{\getfinmodels{\Phi}} \subseteq \homclfin{\getmodels{\Phi}}$
	\item
	$\homclfin{\getmodels{\Phi}} \subseteq \homcl{\getmodels{\Phi}}$
	\item
	$\homcl{\getfinmodels{\Phi}} \subseteq \homcl{\getmodels{\Phi}}$
	\item
	$\homclfin{\getfinmodels{\Phi}} \subseteq \homcl{\getmodels{\Phi}}$ (by transitivity)
\end{itemize}

We proceed to show that all these inclusions are strict and that
$\homcl{\getfinmodels{\Phi}}$ and $\homclfin{\getmodels{\Phi}}$ are indeed incomparable, even for one fixed $\Phi$.

Let $\Phi$ be the conjunction over the following sentences:

\begin{itemize}
	\item $\forall x.\big( x \not= \sig{b} \Rightarrow \exists y. \sig{P}(x,y) \big)$
	\item $\forall x.\big( x \not= \sig{a} \Leftrightarrow \exists y. \sig{P}(y,x) \big)$
	\item $\forall xyz.\big( \sig{P}(x,y) \wedge \sig{P}(x,z) \Rightarrow y = z \big)$
	\item $\forall xyz.\big( \sig{P}(x,z) \wedge \sig{P}(y,z) \Rightarrow x = y \big)$
\end{itemize}

We now define the following $\{\sig{a},\sig{b},\sig{P}\}$-structures:

\begin{itemize}
	\item
	$\mathfrak{A}_\text{$k$-path} = (\{0,\ldots,k\},0,k,succ)$
	\item
	$\mathfrak{A}_\text{$k$-path$^+$} = (\mathbb{N},0,k,succ)$
	\item
	$\mathfrak{A}_\text{$2$loops} = (\{0,1\},0,1,\{(0,0),(1,1)\})$
	\item
	$\mathfrak{A}_\text{$\infty$-gap} = (\mathbb{Z} \setminus \{0\},1,-1,succ)$
\end{itemize}

We obtain:
$$
\begin{array}{l|llll}
	& \homclfin{\getfinmodels{\Phi}} & \homcl{\getfinmodels{\Phi}} &
	\homclfin{\getmodels{\Phi}} & \homcl{\getmodels{\Phi}} \\\hline
	%
	\mathfrak{A}_\text{$k$-path}     & \in & \in & \in & \in \\
	\mathfrak{A}_\text{$k$-path$^+$} & \not\in & \in & \not\in & \in \\
	\mathfrak{A}_\text{$2$loops}     & \not\in & \not\in & \in & \in \\
	\mathfrak{A}_\text{$\infty$-gap} & \not\in & \not\in & \not\in & \in \\

\end{array}
$$

\subsection{Tilings}

We prove in this section  the undecidability  of the deterministic margin-constraint tiling problems. The proof is a slight modification of the first undecidability proof for origin-constraint tiling problems in \cite{wang1963proceedings} (see also \cite{Wang1990}). We include it here for the convenience of the reader. { The words ``domino'' and ``tile'' are used fully  synonymously in the following, i.e., a tile system  is the same as a domino system and a set of tiles  is the same as a set of dominoes.

}

\gridlemma*

\newcommand{\red}[1]{{\color{red}#1}}

\begin{proof}In order to prove Item 1 we follow the construction of Wang in \cite{Wang1990}.

	 He showed undecidability of the origin-constrained tiling problem by a reduction from the halting problem of deterministic Turing machines. For a given Turing machine, Wang defined a set of tiles such that the $i$th computation step of the machine is completely given by a tiling of the $i$th row of the $\mathbb{N}\times \mathbb{N}$ grid. Therefore, a tiling of the $\mathbb{N}\times \mathbb{N}$ grid can only be found if the Turing machine runs forever.

	 We show in the following how this can be done with a margin-constrained system of dominoes. Our construction relies, in addition to Wang's idea, on two modifications of the classical  set of tiles. First we shift the Turing machine tape content in each new computation step one position to the right. To this end, we define a set of dominoes $\mathcal{D}_1$ of new tiles which occur only in the beginning of each row; their number increases by one from row to row.
	 The second idea is that we store the tape content not once but three times. Each placed tile corresponds to a position on the tape and contains the tape content at this position, but furthermore it also contains the tape content of its left and right neighbors. This idea leads to the definition of the tile system $\mathcal{D}_2$.

	 For a binary relation $R$ on a set $D$  we denote by $R$ also {the} map $R \colon D \rightarrow 2^D$ defined by $R(x)= \{d\in D\mid (x,d)\in R\}$. It will always be clear from the context which of the two objects we mean. Furthermore, if the  set $R(x)$ contains only one element we drop the set brackets, i.e., we write $R(x)=d$ for $d\in D$.

	 Let $\mathcal{M}=\langle\{q_0,\ldots, q_n, q_f\},\{0,1\}, \{0,1\},\delta, q_0, q_f \rangle$ be a deterministic Turing machine where  $\{q_0,\ldots, q_n, q_f\}$ is the set of states, $\{0,1\}$ is the input and tape alphabet, and $\delta$ is a partial transition function  $\{q_0,\ldots, q_n\}\times \{0,1\} \rightarrow \{q_0,\ldots, q_n,q_f\}\times \{0,1\} \times \{L,R\}$.

	 Let $D_1=\{o, l, b ,c,c', d\}$ be a set of dominoes such that $o$ is the origin tile.
	 We define the relations $H_1$ and $V_1$ on  $D_1$ as follows:
	 \begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.7ex, topsep=0ex]
	 	\item $H_1(o)= b$, $V_1(o)= l$,
	 	\item $H_1(b)=b$, $V_1(b)=\{c',d\},$
	 \item $V_1(l)=l$, $H_1(l)=\{c,c'\},$
	 \item $H_1(c)=\{c,c'\}$, $V_1(c)=c,$
	 \item $H_1(c')=d$, $V_1(c')=c,$
	 \item $V_1(d)=c'.$

	 \end{itemize}

	 In the next step we define tiles that contain the information of a Turing machine tape position. Consider the set $T=\{ T^p_i \mid  p\in \{q_0,\ldots, q_n, q_f, e\}, i\in \{0,1\}  \}$.
	 We define the set of tiles $D_2$ as $ (T \uplus \{d\}) \times T \times T$. We denote the three coordinates of a tile $x \in D_2$ with $x_l, x_m$ and $x_r$.
	We want to ensure in the following, that a tile $x\in D_2$ that is placed at the grid corresponds to a tape position of the Turing machine after a certain number of computation steps. The tape content is encoded in the main tape information $x_m=T^p_i$.  The index $i$ tells us which symbol is written on the tape at that certain position. If the head of the machine is at this position we get the state information by the superscript $p$. Otherwise $p=e$, which means the head is somewhere else. The coordinates $x_l$ and $x_r$ give exactly this kind of information for the left and right neighbors of the tape position.

We give now the relation $H_2$ and $V_2$ for a tile $x\in D_2$.

\begin{equation}
H_{2}(x)=\{y\in D_2 \mid x_m=y_l \wedge x_r=y_m   \}
\end{equation}

	 For $V_2$  we make the following case distinction on the different types of the form $x=(T^{u}_{r},T^{v}_{s},T^{w}_{t})\in D_2$.

\newcommand{\eqn}[1]{
\begin{equation}
#1
\end{equation}
}

\begin{enumerate}
	\item $u=q$ for $q\in \{q_1,\ldots,q_n\}$ and $\delta(q,r)=(q',i,R)$:
	\eqn{V_2(x)=\{ (y_l,T^{e}_{i},T^{q'}_{s})\in D_2 \mid y_l  \in T\cup \{d\}\}.}

	\item $v=q$ for $q\in \{q_1,\ldots,q_n\}$ and $\delta(q,s)=(q',i,R)$:
	\eqn{V_2(x)=\{ (y_l,T^{u}_{r}, T^{e}_{i})\in D_2 \mid y_l \in T\cup \{d\}\}.}

	\item $v=q$ for $q\in \{q_1,\ldots,q_n\}$ and $\delta(q,s)=(q',i,L)$:
	\eqn{V_2(x)=\{ (y_l,T^{q'}_{s},T^{e}_{i})\in D_2 \mid  y_l \in T\cup \{d\}\}.}

	\item $w=q$ for $q\in \{q_1,\ldots,q_n\}$ and $\delta(q,s)=(q',i,L)$:
	\eqn{V_{2}(x)=\{ (y_l,x_l,T^{q'}_{s})\in D_2 \mid y_l \in T\cup \{d\}\}.}
	\item In all the remaining cases we define
	\eqn{V_2(x)=\{y\in D_2 \mid  x_m=y_r  \}.}
\end{enumerate}

	 Now consider the set of tiles $D=D_1 \cup D_2$. We define the relations $H_3$ and $V_3$ as follows. For the tiles in $D_2$ that are of the form $ x=(d,T^{v}_{s},T^{w}_{t})$, where $v,w\in \{q_0,\ldots,q_n,e\}$ holds, we set
	 $V_3(x)=\{d\}$. Furthermore we define $H_3(d)=( d\times T^2)$.

	 In the last step of our construction we have to specify the second row of the grid. This row should correspond to the initial tape configuration of the Turing machine. Therefore we define a relation $V_4$ such that
\begin{equation}
V(b)=\{(d, T^{q_0}_0, T^e_0) , ( T^{q_0}_0, T^e_0, T^e_0), ( T^{e}_0, T^e_0, T^e_0) \}.
\end{equation}

	 We claim that the domino system $\mathcal{D}$ on the set $D$ with the relations $B=\{b,o\}$, $L=\{l,o\}$, $H=H_1\cup H_2\cup H_3$ and $V=V_1\cup V_2\cup V_3\cup V_4$ is a deterministic margin constraint domino system which tiles the $\mathbb{N}\times \mathbb{N}$ grid if and only if the Turing machine $\mathcal{M}$ does not halt.

	 In order to prove this we give the following description of the tile system $\mathcal{D}$.

	\underline{Claim 1:} $\mathcal{M}$ runs at least $k$ steps if and only if $\mathcal{D}$ tiles at least the first $k{+1}$ rows. In this case the $i{+1}$th row, with $1\leq i\leq k$ has the following description from left to right:
	\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex, topsep=0ex]
		\item the margin symbol $l$,
		\item $i-1$ times the symbol $c$,
		\item one time the symbol $c'$,
			\item one time the symbol $d$,
			\item an infinite sequence of tiles from $D_2$ that store the Turing machine configuration after computation step $i-1$.
	\end{itemize}

It is clear that this claim holds for $k=1$, by our encoding of the initial machine configuration in the second row (see definition of $V_4$). Now assume the statement holds for $k-1$. It is easy to see from the definition of $H_1$ and $V_1$ that the $c$-block is enlarged by one $c$ from one row to the next.
Note that our definition  of $V_2$ ensures the last item in the claim. The main tape information of a tile gets the left neighbor information of its upper neighbor. This is due to the shifting of the tape. Furthermore one can check  that the state transition and head position change in each computation step are also encoded
in the definition of $V_2$ (see items 1 to 4). Note that this implies  also that a tile where the main information consists of a final state does not have an upper neighbor. This is since there exists no transition in a deterministic Turing machine from a final state to another state.
	 This proves Claim 1.

	 The domino system $\mathcal{D}$ satisfies clearly the items 1 to 3 in \Cref{def:tiling}. Let $d_1$ and $d_2$ be tiles. It is clear that item 4 is satisfied whenever $d_1\in D_1\setminus \{d\}$ or $d_2\in D_1$ holds. Suppose therefore $d_1\in D_2\cup \{d\}$ and $d_2\in D_2$. Note that for a tile $x\in H(d_1)$ the coordinates $x_l$ and $x_m$ are uniquely determined by $d_1$.
	 The coordinate $x_l$ corresponds as a tape position to $(d_2)_m$. The tape information at this position after the next computation step is  determined by its two neighbors $(d_2)_l$ and $(d_2)_r$. The uniqueness of this transition can be checked in the definition of $V_2$.

	 This proves that $\mathcal{D}$ is deterministic. It follows from Claim 1 that this system tiles the grid whenever the machine $\mathcal{M}$ does not halt on the empty input. On the other hand, if the machine halts, then there exists a maximal $k$ such that the first $k$ rows can be tiled. This proves the first item of the lemma.

	\bigskip

Item 2 is also proved by a reduction from the halting problem for Turing machines. We give a reduction such that a Turing machine halts on the empty tape whenever the corresponding tile system admits an ultimately periodic tiling of the grid. On the other hand if the Turing machine runs forever, the defined  set of tiles does not allow for an ultimately periodic tiling.

Note that our reduction from Item 1 satisfies already the second implication. If  the Turing machine $\mathcal{M}$ runs forever the tile system $\mathcal{D}$ tiles the grid by a tiling $t$.  By the definition of $\mathcal{D}$ and Claim 1 above the $i$th row starts with exactly $i-1$ times the symbol $c$ after one $l$. This means that for every $\ell_\mathrm{init},\ell_\mathrm{period}\in \mathbb{N}$ there exists $k\in \mathbb{N}$ such that   $t(k,\ell_\mathrm{init})\not= c$ and $ t(k,\ell_\mathrm{init}+\ell_\mathrm{period})=c$. Therefore the tiling is not ultimately periodic. Moreover, since the used margin-constrained tile systems is deterministic, this is the unique tiling of the grid by this  set of tiles, which proves that $\mathcal{D}$ does not admit an ultimately periodic tiling.

We modify the tiling from Item 1 in the following such that $\mathcal{D}$ tiles the grid ultimately periodically whenever the Turing machine $\mathcal{M}$ halts. If the Turing machine halts it is in the final state. Also, we can assume without loss of generality that the reading head will then be at the leftmost tape position.
Let $f$ and $e$ be new tiles and let $D'$ be the union of the set of dominoes from Item 1 with $\{f,e\}$. We define new relations $V_5$ and $H_4$ as follows.

\begin{enumerate}
	\item Let $x\in D_2$. If  $x$ is of the form $ x=(d,T^{q_f}_{s},T^{w}_{t})$  where $q_f$ is the final state we define	$V_5(x)=f$.
\\Otherwise $V_5(x)=e$ .
	\item $V_5(f)=f$ and  $V_5(e)=e$.
	\item $H_4(c)=f $, $H_4(c')=f$, $H_4(f)=e$ and $H_4(e)=e$.
\end{enumerate}
One can  check that the new tile system $\mathcal{D}'$ on the  set of tiles $D'$ with the relations $B'=B$, $L'=L$, $H'=H\cup H_4$ and $V'=V\cup V_5$ is still a deterministic margin-constrained domino system: Consider tiles $d_1$ and $d_2$ and assume first that $d_1\in D$ and $d_2\in D$ hold, then the only possibilities for $d_1$ that have to be checked are $d_1=c$ and $d_1=c'$. The definition of $V_5$ involves only  old elements from $D_2$ (Item 1 above). Therefore $d_2$ can be assumed to be from $D_2$. It is easy to see that in this cases $|H'(d_1)\cap  V'(d_2)|\leq 1$ holds.
The remaining cases are $d_1\in \{e,f\}$ or $d_2\in \{e,f\}$. In these cases $|H'(d_1)\cap  V'(d_2)|\leq 1$ holds trivially since $e$ and $f$ have unique upper and right neighbors.

We characterize now how a tiling with the system $\mathcal{D}'$ looks like if the Turing machine halts.

		\underline{Claim 2:} If $\mathcal{M}$ runs  $k$ steps and then halts, then $\mathcal{D}$ tiles the grid such that for every $i\geq k+3$ the $i$th row has the following description from left to right
	\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex, topsep=0ex]
		\item The margin symbol $l$,
		\item $k$ times the symbol $c$,
		\item one time the symbol $f$,
		\item an infinite sequence of tiles $e$.
	\end{itemize}

Note that we have by Claim 1 a description of the  $k$th row. Since the Turing machine halts after $k$ steps the first symbol in this row after the symbol $d$ is of the kind $ x=(d,T^{q_f}_{s},T^{w}_{t})$  where $q_f$ is the final state. Therefore the unique tiling of the $k+2$th row is as follows:

		\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex, topsep=0ex]
		\item the margin symbol $l$,
		\item $k$ times the tile $c$,
		\item one time the tile $c'$,
			\item one time the tile $f$, and
		\item an infinite sequence of tiles $e$.
	\end{itemize}
	From this description it is easy to compute the unique tilings of the $k+3$th and $k+4$th row. Since both are identical and by Item 4 in \Cref{def:tiling} it follows that all further rows admit also tilings that are identical to the $k+3$th one.	This proves Claim 2.

{
The tiling described in Claim 2 is ultimately periodic. For the vertical period this follows directly from Claim 2.  For the horizontal period node that a Turing machine can in $k$ computation step reach at most $k+1$ different tape positions. This implies that in the rows $2$ to $k+2$ the tiles right of the $2(k+1)$th column encode the empty tape. Since Claim 2 ensures the horizontal period for the rows greater than $k+1$ the tiling is ultimately periodic.}

  Note also that our modifications to achieve this do not affect the property of a (or the) tiling being not ultimately periodic if the Turing machine runs forever.
	This finishes the proof of the lemma. \end{proof}

\subsection{Proofs of Tools Section}

\translemma*

\begin{proof}

	Note that the negation normal form for a formula $\Phi$ is equivalent to $\Phi$ itself.
	Then, by the definition of  $\mathrm{tr}^n$ it is enough to prove the statement for sentences $\Phi$ in $\mathrm{NNF}$. In order to do this, we prove the
	 following statement. For every $\FO_{=}$ formula $\Phi(\bold{x})$ in $\mathrm{NNF}$, every $n$-labelled constant-sole structure 	$(\mathfrak{A},\lambda)$, and every variable assignment $\beta \colon V\rightarrow \mathfrak{A}^\lambda$ it holds that
\begin{equation}
( \mathfrak{A}^\lambda, \beta) \models \Phi(\bold{x})  \text{~ iff~}
(\mathfrak{A}_\lambda, \beta_1) \models \mathrm{tr}^n_{\beta_2}( \Phi(\bold{x})),
\end{equation}
	where $\beta_1 \colon V \to A$ and $\beta_2 \colon V \to \{1,\ldots,n\}$ are defined such that $\beta(x)=(\beta_1(x),\beta_2(x))$ for all $x \in V$.
	We denote by $\beta_2^+$ the extensions of the assignment $\beta_2$ to all constants $c$ such that $\beta_2^+(c)=1$  (cf. definition of  $\mathrm{tr}^n_\mathit{as}$). Furthermore $\beta_1^+$ is the  extension of $\beta_1$ to all constants $c$ such that $\beta_1^+(c)=c^{\mathfrak{A}_\lambda} $. The map $\beta^+$ is now defined  by $\beta^+ (c)=(\beta^+_1(c),\beta^+_2(c))$. Note that this is compatible with the definition of the constants in the  constant-sole structure $ \mathfrak{A}^\lambda$ since $c^{\mathfrak{A}^\lambda}= (c^{\mathfrak{A}},1)$ holds.

	We prove the statement by structural induction over the set of formulae.
For  literals of the form $\sig{P}(\bold{t})$ or $\neg\sig{P}(\bold{t})$ the statement follows immediately from the definition of $\mathrm{tr}^n_\mathit{as}$ since the projection map from $\mathfrak{A}^\lambda$ to   ${\mathfrak{A}_\lambda}|_\tau$  is a strong surjective homomorphism. Therefore the only cases that we have to check are formulae of the form $t_1=t_2$ and $t_1\not =t_2$ for terms $t_1$ and $t_2$.

	Suppose that $\beta$ is any variable assignment such that  $ (\mathfrak{A}^\lambda, \beta) \models (t_1=t_2)$. Then $\beta_1^+(t_1)=\beta^+_1(t_2)$ and $\beta^+_2(t_1)=\beta^+_2(t_2)$. This implies together with (\ref{eq: 5}) that $(\mathfrak{A}_\lambda, \beta_1) \models \mathrm{tr}^n_{\beta_2}( t_1=t_2)$ holds. For the other direction observe that if $(\mathfrak{A}_\lambda, \beta_1) \models \mathrm{tr}^n_{\beta_2}( t_1=t_2)$  holds, then $\mathrm{tr}^n_{\beta_2}( t_1=t_2)$ is exactly the formula  $t_1=t_2$ and for the assignment $\beta$ it holds that  $\beta^+_2(t_1)=\beta^+_2(t_2)$ by (5).  Furthermore we get in this case that  $\beta^+_1(t_1)=\beta^+_1(t_2)$ must hold and therefore we get $( \mathfrak{A}^\lambda, \beta) \models (t_1=t_2)$.
	This concludes the second direction.

	For the case of  a literal of the form $t_1\not = t_2$ suppose that $\beta$ is a variable assignment such that  $ ( \mathfrak{A}^\lambda, \beta) \models (t_1\not =t_2)$ holds. This implies that $\beta_1^+(t_1)\not=\beta_1^+(t_2)$ or $\beta_2^+(t_1) \not=\beta_2^+(t_2)$ holds.
	For the first possibility it follows by (\ref{eq: 6}) that $(\mathfrak{A}_\lambda, \beta_1) \models \mathrm{tr}^n_{\beta_2}( t_1\not =t_2)$  holds. In the case that  $\beta^+_2(t_1) \not=\beta^+_2(t_2)$ holds, we get by (\ref{eq: 6}) that $\mathrm{tr}^n_{\beta_2}( t_1\not =t_2)$ is precisely $\top$ and therefore again the implication is valid.
	For the other direction assume that  $(\mathfrak{A}_\lambda, \beta_1) \models \mathrm{tr}^n_{\beta_2}( t_1\not =t_2)$  holds. Then either $\mathrm{tr}^n_{\beta_2}( t_1\not =t_2)$ is equal to $\top$ or it is equal to $t_1\not = t_2$ and $\beta^+_1(t_1)\not=\beta^+_1(t_2)$. In both cases at least one of $\beta_i$ satisfies $\beta^+_i(t_1)\not =\beta^+_i(t_2)$ and therefore $\beta^+(t_1)\not =\beta^+(t_2) $ holds. This proves the claim.

	For the inductive step it is straightforward to see that statement holds for all formulae of the form $\Phi(\bold{x}) \wedge \Psi(\bold{x})$ and $\Phi(\bold{x}) \vee \Psi(\bold{x})$
	whenever it holds for $\Phi(\bold{x})$ and $\Psi(\bold{x}) $.

	Therefore it remains to prove the statement for formulae of the form $\exists x .\Phi(x,\bold{y})$ and   $\forall x .\Phi(x,\bold{y})$. Let $\beta$ be an arbitrary variable assignment such that $ ( \mathfrak{A}^\lambda, \beta) \models \exists x .\Phi(x,\bold{y})$ holds. This is true if and only if there exists a variable assignment $\beta'= \beta \cup \{x\mapsto (a,j )\} $, where $(a,i ) $ is a domain element of $\mathfrak{A}^\lambda$ such that $ ( \mathfrak{A}^\lambda, \beta') \models  \Phi(x,\bold{y})$ holds.  By the inductive assumption we get that this is the case if and only if   $(\mathfrak{A}_\lambda, \beta'_1) \models \mathrm{tr}^n_{\beta'_2}(\Phi(x,\bold{y}))$ holds.
	Since $ [\lambda(a) \geq j]$ holds clearly
	in $\mathfrak{A}_\lambda$ this is equivalent to
	the validity of
	$ (\mathfrak{A}_\lambda, \beta'_1) \models  [\lambda(x) \geq j] \wedge \mathrm{tr}^n_{\beta'_2} (\Phi(x,\bold{y}))$ for $\beta'= \beta \cup \{x\mapsto (a,j )\} $.
	Note that such a $\beta$ can be found  if and only if $ (\mathfrak{A}_\lambda, \beta_1) \models  \exists x.[\lambda(x) \geq j] \wedge \mathrm{tr}^n_{\beta'_2} (\Phi(x,\bold{y}))$ holds for some $j$.  By Definition (\ref{eq: 11})  this means that	 $ (\mathfrak{A}_\lambda, \beta_1) \models  \mathrm{tr}^n_{\beta_2}(\exists x .\Phi(x,\bold{y}))$  holds.

	The statement for formulae of the form $\forall x .\Phi(x,\bold{y})$ can be shown by an analogous argument.\end{proof}

\subsection{Proofs of Homclosure Membership Section}

\begin{lemma}\label{lemma:projchar PHIintext}
	Let $\Phi$ be a $\tau$-sentence and let $\mathfrak{A}$ be a finite $\tau$-structure as in \Cref{def:exincol}. Then the following holds:
	\begin{enumerate}
		\item $\Phi^\mathrm{ext}_\mathfrak{A}$ and $\Phi^\mathrm{int}_\mathfrak{A}$ are of polynomial size wrt.\ $|\mathfrak{A}|$ and the size of $\Phi$.
		\item $\Omega_\mathfrak{A}$ projectively characterizes the class of (finite) $\tau$-structures having a homomorphism into $\mathfrak{A}$.
		\item\label{item:projecht} $\Phi^\mathrm{ext}_\mathfrak{A}$ projectively characterizes the class of (finite) models of $\Phi$  having a homomorphism into $\mathfrak{A}$.
	\end{enumerate}
\end{lemma}

\begin{proof}The first statement follows directly from the definitions of  $\Phi^\mathrm{ext}_\mathfrak{A}$ and $\Phi^\mathrm{int}_\mathfrak{A}$.

	For (2), let $\mathfrak{B}$ be a $\tau{\cup}\rho$-structure that satisfies $\Omega_\mathfrak{A}$. Let $\lambda$ be the $n$-labeling of $\mathfrak{B}$ given by the $\rho$-reduct of $\mathfrak{B}$. The map $\lambda$ is a homomorphism from the $\tau$-reduct  $\mathfrak{B}'$ of $\mathfrak{B}$ to $\mathfrak{A}$.
	 To see this assume that $\bold{b}\in  \sig{P}^{\mathfrak{B}'}$ holds for a tuple $\bold{b}$ from $B$. By the definition of $\Omega_\mathfrak{A}$	we get that  $\bold{b} \in (\chi^{\sig{P}}_\mathfrak{A})^\mathfrak{B}$ holds.
	 This implies that $\lambda(\bold{b}) \in  \sig{P}^\mathfrak{A}$ holds and therefore $\lambda$ is a homomorphism.
	For the other inclusion assume the $h\colon\mathfrak{B} \rightarrow \mathfrak{A}$ is a homomorphism. It is easy to check that the implicit representation $\mathfrak{B}_h$ of the $n$-labeled structure $(\mathfrak{B},h)$ satisfies $\Omega_\mathfrak{A}$ and is an expansion of $\mathfrak{B}$. This proves the claim.

	Claim (3) follows immediately from the definition of $\Phi^\mathrm{ext}_\mathfrak{A}$ and the previous claim.\end{proof}

\begin{lemma}\label{lemma:phi int}
Let $\mathfrak{A}$ and $\rho$ as in \Cref{def:exincol} and let $\mathfrak{B}$ be an arbitrary $\tau$-structure such that $h\colon\mathfrak{B}\rightarrow \mathfrak{A}$ is a homomorphism.  Then it holds for every $\tau$-formula $\Phi$ and all assignments $\beta$ that
$$ (\mathfrak{B},\beta) \models   \Phi(\bold{t}) \text{~~if and only if~~} (\mathfrak{B}_h,\beta)\models \Phi^\mathrm{int}_\mathfrak{A}(\bold{t}),$$
where $\mathfrak{B}_h$ is the implicit representation of the $n$-labeled structure $(\mathfrak{B},h)$.\end{lemma}

\begin{proof}We prove the statement by structural induction over the set of formulae.  For the induction beginning let $\Phi(\bold{t})$ be an atomic formula $\sig{P}(\bold{t})$ and let $\beta$ be a term assignment such that $ (\mathfrak{B},\beta) \models   \Phi(\bold{t}) $ holds. Since $h$ is a homomorphism it follows that $(\mathfrak{A},h\circ \beta)\models \sig{P}(\bold{t})$ and therefore also $(\mathfrak{B}_h,\beta)\models \chi^{\sig{P}}_\mathfrak{A}(\bold{t})$ holds. The second direction of the equivalence follows directly from the definition of $\chi^{\sig{P}}_\mathfrak{A}$ and since $\mathfrak{B}_h$ is an expansion of $\mathfrak{B}$.

	For the induction step let $\Phi(\bold{t})$ be of the form $\neg \Psi(\bold{t})$ such that the statement already holds for $\Psi$. Note that then clearly $\Phi^\mathrm{int}_\mathfrak{A}(\bold{t})$ is equal to $\neg \Psi^\mathrm{int}_\mathfrak{A}(\bold{t})$ and we get:
	\begin{align*}
(\mathfrak{B},\beta) \models   \Phi(\bold{t}) &\hspace{4ex}\text{iff} \hspace{-5ex}&& (\mathfrak{B},\beta) \not\models   \Psi(\bold{t}) \\
&\hspace{4ex}\text{iff} \hspace{-5ex}&& (\mathfrak{B}_h,\beta) \not\models   \Psi^\mathrm{int}_\mathfrak{A}(\bold{t})\\
&\hspace{4ex}\text{iff} \hspace{-5ex}&& (\mathfrak{B}_h,\beta)\models \Phi^\mathrm{int}_\mathfrak{A}(\bold{t}).
	\end{align*}
Assume that $\Phi(\bold{t})$ is of the from $\Psi(\bold{t}) \vee \Gamma(\bold{t})$ for formulae $\Psi(\bold{t})$ and $\Gamma(\bold{t})$ for which the statement holds. Since $\Phi^\mathrm{int}_\mathfrak{A}(\bold{t})$ is by its definition of the form $\Psi^\mathrm{int}_\mathfrak{A}(\bold{t}) \vee \Gamma^\mathrm{int}_\mathfrak{A}(\bold{t})$ we get
	\begin{align*}
	(\mathfrak{B},\beta) \models   \Phi(\bold{t}) &&
	\\
	&\hspace{-10ex}\text{iff} \hspace{0ex}&& \hspace{-10ex}(\mathfrak{B},\beta) \models  \Psi(\bold{t}) \vee \Gamma(\bold{t}) \\
&\hspace{-10ex}\text{iff} \hspace{0ex}&& \hspace{-10ex}(\mathfrak{B},\beta) \models   \Psi(\bold{t})  \text{~~or~~}  (\mathfrak{B},\beta) \models \Gamma(\bold{t}) \\
&\hspace{-10ex}\text{iff} \hspace{0ex}&& \hspace{-10ex}(\mathfrak{B}_h,\beta) \models   \Psi^\mathrm{int}_\mathfrak{A}(\bold{t})\text{~~or~~}(\mathfrak{B}_h,\beta) \models \Gamma^\mathrm{int}_\mathfrak{A}(\bold{t}) \\
	&\hspace{-10ex}\text{iff} \hspace{0ex}&& \hspace{-10ex} (\mathfrak{B}_h,\beta)\models \Psi^\mathrm{int}_\mathfrak{A}(\bold{t}) \vee \Gamma^\mathrm{int}_\mathfrak{A}(\bold{t})\\
		&\hspace{-10ex}\text{iff} \hspace{0ex}&& \hspace{-10ex} (\mathfrak{B}_h,\beta)\models \Phi^\mathrm{int}_\mathfrak{A}(\bold{t}) .
\end{align*}
As in the last case assume that $\Phi(\bold{t})$ is of the form $\exists t_1 \Psi(\bold{t})$ for formulae $\Psi(\bold{t})$ for which the statement holds.  Then $\Phi^\mathrm{int}_\mathfrak{A}(\bold{t})$ is by its definition of the form $\exists t_1\Psi^\mathrm{int}_\mathfrak{A}(\bold{t})$.
We get the following:
\begin{align*}
	(\mathfrak{B},\beta) \models   \Phi(\bold{t}) &&&\\
&\hspace{-12ex}\text{iff} \hspace{0ex}&&\hspace{-12ex} \exists b\in B \text{~such that~}  (\mathfrak{B},\beta\cup\{t_1\mapsto b\}) \models   \Psi(\bold{t})\\
&\hspace{-12ex}\text{iff} \hspace{0ex}&&\hspace{-12ex} \exists b\in B \text{~such that~}  (\mathfrak{B}_h,\beta\cup\{t_1\mapsto b\}) \models  \Psi^\mathrm{int}_\mathfrak{A}(\bold{t})\\
	&\hspace{-12ex}\text{iff} \hspace{0ex}&&\hspace{-12ex} (\mathfrak{B}_h,\beta)\models \Phi^\mathrm{int}_\mathfrak{A}(\bold{t}).
\end{align*}
This concludes the proof of the lemma.
\end{proof}

\lemmacoloring*

\begin{proof}
	By \Cref{lemma:projchar PHIintext} Item \ref{item:projecht}, the sentence $\Phi^\mathrm{ext}_\mathfrak{A}$ projectively characterizes the class of (finite) models of $\Phi$  having a homomorphism into $\mathfrak{A}$. Therefore the equivalence of 1) and 3) follows immediately.

The implication from 1) to 2) follows from \Cref{lemma:phi int},
since for every (finite) model $\mathfrak{B}$ of $\Phi$  admitting a homomorphism $h$ into $\mathfrak{A}$, the structure $\mathfrak{B}_\lambda$  with $\lambda=h$ is a (finite) model of $\Phi^\mathrm{int}_\mathfrak{A}$.

For the implication from 2) to 1) assume that $\mathfrak{B}$ is a model of $\Phi^\mathrm{int}_\mathfrak{A}$ and let $\lambda$ be the $n$-labeling of $\mathfrak{B}$ given by the $\rho$-reduct of $\mathfrak{B}$.
Let $\mathfrak{C}$ be the $\tau$-structure
obtained by setting $C=B$, $\sig{c}{}^\mathfrak{C}=\sig{c}{}^\mathfrak{B}$ for all constants, and $\sig{P}{}^\mathfrak{C} = (\chi^{\sig{P}}_\mathfrak{A})^\mathfrak{B}$.
It follows from the definition of  $\chi^{\sig{P}}_\mathfrak{A}(\bold{t})$  that $\lambda$ is a homomorphism from $\mathfrak{C}$ to $\mathfrak{A}$. Furthermore the definition of $\mathfrak{C}$ implies that for all $\sig{P}\in \tau$ and all $\bold{b}$ from $B$ it holds
$$ \bold{b} \in {(\chi^{\sig{P}}_\mathfrak{A})}^{\mathfrak{C}_\lambda}
 \text{~~~if and only if~~~} \bold{b} \in{(\chi^{\sig{P}}_\mathfrak{A})}^\mathfrak{B}. $$
Since $\mathfrak{B}$ satisfies $\Phi^\mathrm{int}_\mathfrak{A}$ it follows that
$\mathfrak{C}_\lambda$ does as well. Now we apply \Cref{lemma:phi int} and get that $\mathfrak{C}$ satisfies $\Phi$ which proves that 1) holds.\end{proof}

\thearbsameasfin*
\begin{proof}
In order to show $\homclfin{\getmodels{\Psi}}\subseteq\homclfin{\getfinmodels{\Psi}}$ let $\mathfrak{B}\in \homclfin{\getmodels{\Psi}}$.  Then
  $\Psi^\mathrm{ext}_\mathfrak{B}$ and  $\Psi^\mathrm{int}_\mathfrak{B}$ have by \Cref{lemma:coloring} models. By the assumption $\mathbb{L}^\mathrm{ext}$ or $\mathbb{L}^\mathrm{int}$ have the FMP which means that $\Phi^\mathrm{ext}_\mathfrak{B}$ or $\Phi^\mathrm{int}_\mathfrak{B}$ are finitely satisfiable. Again by \Cref{lemma:coloring}, we get that $\Phi$ has a  finite model admitting a homomorphism into $\mathfrak{B}$ which shows that
$ \mathfrak{B}\in \homclfin{\getfinmodels{\Psi}}$ holds.
\end{proof}

\firstmain*

\begin{proof}
	First consider \mbox{$\Ex^*\FO^+_{=}$}{}, noting that every such sentence is already homclosed. Thus $\mathrm{InHomCl}_\mathrm{(fin)}$ is equivalent to checking modelhood for the given $\mathfrak{A}$. This can be done in nondeterministic time by guessing an instantiation of the existentially quantified variables and checking satisfaction. \textsc{NP}-hardness follows from a reduction from the graph homomorphism problem (even for disjunction-free sentences).
	We now consider the other fragments. Extrinsic coloring for \mathbb{GNFO}_{=}{} and \mbox{$\mathbb{TGF}$}{}
	and intrinsic coloring for the others establishes a polynomial reduction to the corresponding satisfiability problems via \Cref{lemma:coloring}. Hardness follows by a reduction from satisfiability via \Cref{prop:SatToInHomCl} in all cases (see \Cref{fig:main} for references for the complexity of the satisfiability problem in each case).
\end{proof}

\defgridformula*

\begin{lemma}[restate=gridformula, label=gridformula, name=]
	\begin{enumerate}[itemindent=0ex, leftmargin=4ex, itemsep=-0.5ex]
		\item \label{grid1}
		Every model $\mathfrak{B}$  of  $\Phi_\mathrm{grid}$ is a  $\{\sig{H}{},\sig{V}{}\}$-structures such that for every domain element
		$b \in B$ there is a homomorphism $h: \mathfrak{A}_{\mathbb{N} \times \mathbb{N}} \to \mathfrak{B}$ with $h((0,0))=b$.
		\item \label{grid2}
		Every model of $\Phi_\mathrm{grid}$ has a homomorphism into a structure that is not a model of $\Phi_\mathrm{grid}$.
		\item \label{grid3}
		Every homomorphism from the $\mathbb{N} \times \mathbb{N}$ grid into $\mathfrak{A}_\mathcal{D}$ corresponds to a $\mathcal{D}$-tiling.
		\item \label{grid4}
		Every homomorphism from some model of $\Phi_\mathrm{grid}$ into $\mathfrak{A}_\mathcal{D}$ gives rise to a $\mathcal{D}$-tiling.
		\item \label{grid5}
		Every homomorphism from some finite model of $\Phi_\mathrm{grid}$ into $\mathfrak{A}_\mathcal{D}$ gives rise to an ultimately periodic $\mathcal{D}$-tiling.
		\item \label{grid6}
		Both membership in $\homcl{\getmodels{\Phi_\mathrm{grid}}}$ and $\homcl{\getfinmodels{\Phi_\mathrm{grid}}}$ are undecidable problems.
	\end{enumerate}
\end{lemma}

\begin{proof} For (\ref{grid1}), note that an easy inductive argument under the usage of the extension properties defined in $\Phi_\mathrm{grid}$ proves the claim.

	For (\ref{grid2}), simply choose $\mathfrak{F} \uplus \mathfrak{I}$ as target structure.

	(\ref{grid3}) follows immediately from the definition of a tiling and from the definition of the structure $\mathfrak{A}_\mathcal{D}$ .

	For (\ref{grid4}), let $\mathfrak{B}$ be a model of  $\Phi_\mathrm{grid}$  that has a homomorphism to
	$\mathfrak{A}_\mathcal{D}$. By (\ref{grid1}) we get that  $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}} $ also has a homomorphism to $\mathfrak{B}$ and therefore also to $\mathfrak{A}_\mathcal{D}$. (\ref{grid3}) implies that this gives rise to a  $\mathcal{D}$-tiling.

	For (\ref{grid5}), assume that $\mathfrak{B}$ is a finite model of  $\Phi_\mathrm{grid}$ with a homomorphism $t$ into $\mathfrak{A}_\mathcal{D}$. Let $v\colon B\rightarrow B$ and $h\colon B\rightarrow B$ to functions such that $(x,h(x))\in\sig{H}{}^\mathfrak{B}$ and $(x,v(x))\in\sig{V}{}^\mathfrak{B}$ hold. It is clear that such functions exist since $\mathfrak{B}$ satisfies $\Phi_\mathrm{grid}$.
	We define a map $f$ from $\mathbb{N} \times \mathbb{N} $ to $B$ as follows.   For an arbitrary element $o\in B$ we set $f(0,0)=o$. In the next step we define inductively the map on the  elements $W_0=\{ (x,0) \mid x\in \mathbb{N} \}$. This is done by $f(i+1,0)=h(f(i,0))$. Since $h$ is a  function this is well defined.
	Now we can assume that the map is defined on the elements $W_i=\{ (x,i) \mid x\in \mathbb{N} \}$ and we extend it to $W_{i+1}=\{ (x,i+1) \mid x\in \mathbb{N} \}$ by $f(j,i+1)= v(f(j,i+1))$.
	Note that  by the use of the function $h$ it is clear that after a finite initial sequence of length at most $|B|$, the mapping $f$ is periodic on the first row $W_0$  with respect to the assigned elements from $B$. Since the definition of $f$ at the $n$th column of the grid only depends on the value $f(n,0)$ the columns
	are in the same way periodic as $W_0$ is.
	Furthermore the graph of the map $v$ contains finitely many cycles of finite length. Let $q$ be the greatest common multiple of these lengths. It is clear that for every element $x\in B$ that lies in a cycle applying $q$ times the function $v$ on $x$ results in the element $x$ itself. This shows that $f$ also has a repetition on the rows in the grid in its definition after a possible initial sequence of at most $|B|$ elements.

	What we observed about the function $f$ implies immediately that if $t\circ f$ defines a tiling of the grid by tiles of $\mathcal{D}$ then this tiling is ultimately periodic.

	In order to prove that $t\circ f$  defines a tiling it is enough according to (\ref{grid3}) to show that $f$ is a homomorphism from $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}}$ to $ \mathfrak{B}$.

	Consider the substructure  $\mathfrak{W}_0$ of  $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}}$  induced by $W_0$.

	The map from $\mathfrak{W}_0$ to $\mathfrak{B}$  induced by $f$ is a homomorphism, since
	$(f(i,0),f(i+1,0) )= (f(i,0), h(f(i,0))) \in  \sig{H}{}^{\mathfrak{B}} $ holds for all
	$((i,0),(i+1,0)) \in \sig{H}{}^{\mathfrak{W}_0}$.

	Now we prove by induction that $f$ is a homomorphism on all structure $\mathfrak{W}_{i+1}$ which are induced by the sets $W_{i+1}$. It follows immediately by the choice of $v$ that all tuples of the form $ ((j,i),(j,i+1)) \in \sig{V}{}^{\mathfrak{W}_{i+1}}$ for arbitrary $j\in\mathbb{N}$ are preserved by $f$.
	It remains to show the preservation of tuples of the form $((j,i+1),(j+1,i+1)) \in \sig{H}{}^{\mathfrak{W}_{i+1}}$. Consider the elements $f(j,i+1),f(j+1,i+1), f(j,i)$ and $f(j+1,j)$
	in $B$. By the induction hypothesis and the observation from before we get that $\sig{H}(f(j,i), f(j+1,i)) $,  $\sig{V}(f(j,i), f(j,i+1)   )$ and $\sig{V}(f(j+1,i), f(j+1,i+1))$ hold in $\mathfrak{B}$. Since $\mathfrak{B}$ satisfies the sentence $\Phi_\mathrm{grid}$ it follows that also $\sig{H}(f(j,i+1),f(j+1,i+1))$ holds in $\mathfrak{B}$. This implies that $f$ induces a homomorphism from $\mathfrak{W}_{i+1}$ to $\mathfrak{B}$ and therefore concludes the proof that $f$ is a homomorphism.

	For (\ref{grid6}), we prove the statements by reductions from the  tiling problem and the ultimately periodic tiling problem.
    The undecidability of  these problems was shown in \cite{berger1966undecidability} and in	\cite{remarksonberger}, respectively.

	The reductions map an instance of the tiling problem, that is a  set of tiles $\mathcal{D}$ to the structure $\mathfrak{A}_\mathcal{D}$.

	To see that this is a correct reduction to the membership problem of $\homcl{\getmodels{\Phi_\mathrm{grid}}}$ note that $\mathcal{D}$ tiles by (\ref{grid3}) the grid if and only if   $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}} $ has a homomorphism to $\mathfrak{A}_\mathcal{D}$. By (\ref{grid1})  and since  $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}} $ is a model of  $\Phi_\mathrm{grid}$ this holds if and only if $\mathfrak{A}_\mathcal{D} \in \homcl{\getmodels{\Phi_\mathrm{grid}}}$. This proves the undecidability of the membership problem for $ \homcl{\getmodels{\Phi_\mathrm{grid}}}$.

	For the undecidability of the membership problem for $\homcl{\getfinmodels{\Phi_\mathrm{grid}}}$ we use the same mapping from  sets of tiles to structures.
	Assume that a set of tiles $\mathcal{D}$ admits an ultimately periodic tiling  $t$ of the grid. Let
	$k_\mathrm{init},k_\mathrm{period},\ell_\mathrm{init},\ell_\mathrm{period}$ from the definition of ultimately periodic tiling. Let $\mathfrak{D}'$ be the finite substructure of $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}} $ that is induced by elements of the from $(x,y)$ where $x\leq  k_\mathrm{init}+k_\mathrm{period}$ and $y\leq  l_\mathrm{init}+l_\mathrm{period}$ hold.
	We add new tuples to the relations $\sig{H}{}^{\mathfrak{D}'}$ and $\sig{V}{}^{\mathfrak{D}'}$  from $\mathfrak{D}'$ and define in this way a new structure $\mathfrak{D}$.
	For all elements of the form $(k_\mathrm{init}+k_\mathrm{period},y)  $ we add the tuple
	$((k_\mathrm{init}+k_\mathrm{period},y)  ,(k_\mathrm{init}+1,y))$ to the relation $\sig{H}{}^{\mathfrak{D}'}$.
	Analogous we add for all elements of the form $(x,l_\mathrm{init}+l_\mathrm{period})  $ the tuple
	$((x,l_\mathrm{init}+l_\mathrm{period})  ,(x,l_\mathrm{init}+1))$ to the relation $\sig{V}{}^{\mathfrak{D}'}$.
	It is easy to see that the so defined structure $\mathfrak{D}$ satisfies $\Phi_\mathrm{grid}$. Since the tiling $t$ was ultimately periodic the restriction of the tiling to the elements of $\mathfrak{D}$ defines a homomorphism from $\mathfrak{D}$ to $\mathfrak{A}_\mathcal{D} $. Since $\mathfrak{D}$ is clearly finite this implies that the structure $\mathfrak{A}_\mathcal{D}$ is in $\homcl{\getfinmodels{\Phi_\mathrm{grid}}}$ .

	For the other direction of the reduction proof assume that $\mathfrak{A}_\mathcal{D}$ is in $\homcl{\getfinmodels{\Phi_\mathrm{grid}}}$ . This implies by (\ref{grid5}) immediately that $\mathcal{D}$ admits an ultimately periodic tiling of the grid. \end{proof}

\undecTGD*

\begin{proof}
Immediate from Item~\ref{grid6} of \Cref{gridformula}.
\end{proof}

\subsection{Proofs of Homclosedness Section}

\SattToHomClosed*

\begin{proof}
	We $\textsc{C}'$-reduce (finite) unsatisfiability in $\mathbb{L}'$ to $\mathrm{HomClosed}_\mathrm{(fin)}$ for $\mathbb{L}$ as follows: given $\Phi$, compute $f(\Phi)$.

If the set of (finite) models of $f(\Phi)$ is closed under (finite-target) homomorphisms then
$\getffinmodels{f(\Phi)}|_{\tau \cup \{\sig{U}{}\}}$ is closed under (finite-target) homomorphisms
and therefore an empty set. This implies that $\Phi$ is (finitely) unsatisfiable.
On the other hand if  $\Phi$ is (finitely) unsatisfiable then $\getffinmodels{f(\Phi)}|_{\tau \cup \{\sig{U}{}\}}$  as well as $\getffinmodels{f(\Phi)}$ are closed under (finite-target) homomorphisms since they are empty.\end{proof}

\SattToHomClosedCompanion*

\begin{proof}
	We $\textsc{C}'$-reduce (finite) unsatisfiability in $\mathbb{L}'$ to $\mathrm{HomClosed}_\mathrm{(fin)}$ for $\mathbb{L}$ as follows: given $\Phi$, compute $f(\Phi)$.

If $\Phi$ is (finitely) unsatisfiable, then $f(\Phi)$ is (finitely) valid and therefore its (finite) models are closed under (finite target) homomorphisms.

If $\Phi$ is (finitely) satisfiable witnessed by some (finite) model $\mathfrak{A}$, this means that $(\mathfrak{A},A)$ is not a model of $f(\Phi)$. Let now $\mathfrak{B}= \mathfrak{A} \cdot \{\widecheck{\sig{U}{}}\}$, which clearly is a (finite) model of $f(\Phi)$. Moreover, the identity function is a homomorphism from $\mathfrak{B}$ to $(\mathfrak{A},A)$, which shows that $f(\Phi)$ is not (finitely) homomorphism closed.

It follows that checking (finite) homomorphism-closedness of $f(\Phi)$ is equivalent to checking (finite) unsatisfiability of $\Phi$.
\end{proof}

\HomSeparation*

\begin{proof}
	Given $\mathfrak{A}$, $\mathfrak{B}$, and $h$, we obtain $\mathfrak{C}$, $h_1$, and $h_2$ as follows:
	\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item $C = A \uplus B$
		\item $h_1\colon A \mathrel{{\hookrightarrow}} C$ is set to $id_A$
		\item $h_2\colon C \mathrel{{\str[0.6ex]{\surhom}}} B$ is obtained via $h_2 = h \uplus id_B$

		\item $\sig{c}{}^\mathfrak{C} = \sig{c}{}^\mathfrak{A}$ for every constant $\sig{c}{} \in \tau$
		\item $\sig{P}{}^\mathfrak{C} = \{(c_1,\ldots,c_k) \mid (h_2(c_1),\ldots,h_2(c_k)) \in \sig{P}{}^\mathfrak{B}\}$ for every $k$-ary predicate $\sig{P}\in\tau$.\qedhere
	\end{itemize}
\end{proof}

\InjFormula*

\begin{proof}
	Let $\Phi$ be some $\tau$-sentence and let $\tau'$ consist of copies $\sig{P}'$ for each predicate $\sig{P}\in\tau$.

	For the first direction, assume that $\Phi^{\scaleobj{0.8}{\text{\faBolt}}}_\cl{\mathrel{{\hookrightarrow}}}$ is (finitely) satisfiable. Then there is a (finite) model $\mathfrak{D} \vDash \Phi^{\scaleobj{0.8}{\text{\faBolt}}}_\cl{\mathrel{{\hookrightarrow}}}$ over the signature $\tau\uplus\tau'\uplus \{ \sig{U} \}$. We now define two $\tau$-structures, $\mathfrak{B}$ as $\mathfrak{D}|_{\tau}$ and $\mathfrak{A}$ as the following one:
	\begin{itemize}
		\item The domain of $\mathfrak{A}$ is $\sig{U}^{\mathfrak{D}}$.
	 	\item For each constant $\sig{c}{}\in\tau$ we put $\sig{c}^{\mathfrak{A}} = \sig{c}^{\mathfrak{D}}$. Note that, by definition of the relativization of a formula, $\sig{c}^{\mathfrak{D}}\in\sig{U}^{\mathfrak{D}}$ for all constant symbols $\sig{c}$. So this is well defined.
	 	\item For each predicate $\sig{P}\in\tau$ let $\sig{P}^{\mathfrak{A}} = (\sig{U}^{\mathfrak{D}})^{\mathrm{ar}(\sig{P})} \cap \sig{P}^{\mathfrak{D}}\cap\sig{P}'^{\mathfrak{D}}$. Note that the first conjunct $(\sig{U}^{\mathfrak{D}})^{\mathrm{ar}(\sig{P})}$ ensures well definedness.
	\end{itemize}
	Define $s\colon\mathfrak{A}\to\mathfrak{B}, a\mapsto a$. $s$ is an injective homomorphism. As the injectivity is plain to see, we just verify that $s$ is a homomorphism. For each constant $\sig{c}\in\tau$ we have $s(\sig{c}^{\mathfrak{A}}) = \sig{c}^{\mathfrak{D}}$. Since $\sig{c}^{\mathfrak{D}} = \sig{c}^{\mathfrak{B}}$ for $\sig{c}\in\tau$ by means of $\mathfrak{B} = \mathfrak{D}|_{\tau}$ the map $s$ preserves constants. Now let $\bold{a}\in\sig{P}^{\mathfrak{A}}$ for some predicate $\sig{P}\in\tau$, which additionally means that $\bold{a}$ is a tuple from $\mathfrak{A}$ by the $(\sig{U}^{\mathfrak{D}})^{\mathrm{ar}(\sig{P})}$ part of the definition. By construction $\bold{a}\in\sig{P}^{\mathfrak{D}}$. Since $\sig{P} \in\tau$ it holds that $\sig{P}^{\mathfrak{D}}  =\sig{P}^{\mathfrak{B}}$. Thus we obtain by componentwise application $s(\bold{a}) \in\sig{P}^{\mathfrak{B}}$. Hence we conclude that $s$ is a homomorphism.
	\newline
	Now we show that $\mathfrak{A}\stackrel{s}{\mathrel{{\hookrightarrow}}}\mathfrak{B}$ constitutes a (finite) injective spoiler, of which $\mathfrak{D}$ is a witness. For showing the spoiler property (as we already established that $s$ is an injective homomorphism this is the only thing left to prove) we note that by construction $\mathfrak{A}\vDash\Phi$ as $\mathfrak{D}\vDash(\Phi^-)^{\mathrm{rel}(\sig{U}{})}$ and the universe of $\mathfrak{A}$ is $\sig{U}^{\mathfrak{D}}$. Furthermore, as $\mathfrak{B}=\mathfrak{D}|_{\tau}$ we obtain $\mathfrak{B}\vDash\lnot\Phi$ since $\mathfrak{D}\vDash\lnot\Phi$ and $\Phi$ is a $\tau$-sentence.
	\newline
	Finally, we constructed $\mathfrak{A}$ and $\mathfrak{B}$ such that $\mathfrak{D}|_{\tau}=\mathfrak{B}$, $\sig{U}^{\mathfrak{D}}=s(A)$, and $\sig{P}^{\mathfrak{D}}\cap\sig{P}'^{\mathfrak{D}}=\sig{P}^{\mathfrak{A}}$ for every predicate $\sig{P}\in\tau$. By definition of $s$ this establishes that $\mathfrak{D}$ is a witness of the (finite) injective spoiler $\mathfrak{A}\stackrel{s}{\mathrel{{\hookrightarrow}}}\mathfrak{B}$.

	For the other direction, let $\mathfrak{A}\stackrel{s}{\mathrel{{\hookrightarrow}}}\mathfrak{B}$ be a (finite) injective spoiler for the $\tau$-sentence $\Phi$. We define $\mathfrak{D}$ as follows:
	\begin{itemize}
		\item The domain of $\mathfrak{D}$ is $B$.
		\item For each constant $\sig{c}\in\tau$ we put $\sig{c}^{\mathfrak{D}} = \sig{c}^{\mathfrak{B}}$.
		\item For each predicate $\sig{P}\in\tau$ we put $\sig{P}^{\mathfrak{D}} = \sig{P}^{\mathfrak{B}}$.
		\item For each predicate $\sig{P}\in\tau$ we put \newline $\sig{P}'^{\mathfrak{D}}=\{(s(a_1),\ldots,s(a_k)) \mid   (a_1,\ldots,a_k) \in \sig{P}{}^\mathfrak{A}\}$.
		\item $\sig{U}^{\mathfrak{D}}=s(A)$.
	\end{itemize}
	It is obvious that $\mathfrak{D}|_{\tau}=\mathfrak{B}$, $\sig{U}^{\mathfrak{D}}=s(A)$ and $\sig{P}{}^\mathfrak{D} {\cap}\,{\sig{P}{}'}^\mathfrak{D}\! = \{(s(a_1),\ldots,s(a_k)) \mid   (a_1,\ldots,a_k) \in \sig{P}{}^\mathfrak{A}\}$ for every predicate $\sig{P}$ from $\tau$. Hence $\mathfrak{D}$ is a (finite) witness of the injective spoiler $\mathfrak{A}\stackrel{s}{\mathrel{{\hookrightarrow}}}\mathfrak{B}$. By $\mathfrak{A}\stackrel{s}{\mathrel{{\hookrightarrow}}}\mathfrak{B}$ being a spoiler we obtain that $\mathfrak{D}\vDash \lnot\Phi$ as $\Phi$ is a $\tau$-sentence and $\mathfrak{D}|_{\tau}=\mathfrak{B}$. Furthermore, as $\mathfrak{A}\vDash \Phi$ and $s$ being injective, $\mathfrak{D}\vDash (\Phi^{-})^{\mathrm{rel}(\sig{U}{})}$ also holds. Hence we obtain $\mathfrak{D}\vDash \Phi^{\scaleobj{0.8}{\text{\faBolt}}}_\cl{\mathrel{{\hookrightarrow}}}$.
\end{proof}

\squeeze*

\begin{proof}
	Let $\lambda$ be defined by $a \mapsto \min(n,|h^{-1}(a)|)$ where $h^{-1}(a)$, as usual, denotes the set $\{b \in B \mid h(b)= a\}$.
	Now define $\hslash \colon B \rightarrow A^\lambda $ such that the elements of $h^{-1}(a)$ are mapped to $\{(a,1), \ldots, (a,\lambda(a))\}$ in a surjective way, which is possible by construction.
	By definition of $\mathfrak{A}^\lambda$, the map $\hslash$ is  a strong surjective homomorphism and clearly satisfies $h = \pi \circ \hslash$.
	The equivalence of $\mathfrak{B}$ and $\mathfrak{A}^\lambda$ regarding $\FO_{=}$ sentences of quantifier rank $n$ can be shown as usual via an $n$-step Ehrenfeucht-Fra\"{i}ssé game, where, upon spoiler picking $e$, duplicator picks a fresh element from

{$h^{-1}(\pi(e))$ or $\pi^{-1}(h(e))$}, respectively.
\end{proof}

\mainsecond*

\begin{proof}
	For all cases, membership can be shown for the finite cases directly via \Cref{FinHomClFormula} by a polynomial reduction to a fragment with the appropriate unsatisfiability problem.

	The general cases can be reduced to the finite ones via \Cref{thm:FSP}.

	Hardness follows for \mathbb{GNFO}_{=}, \mbox{$\mathbb{TGF}$}, $\mbox{$\FO_{=}^\mathbbm{2}$}{}$, and \mbox{$\Al^*\FOe$}{} as well as \mbox{$\Al\Al\Ex\Ex\FO$}{} via \Cref{prop:SattToHomClosed} from the corresponding known unsatisfiability complexities.
	For $\mbox{$\Ex^*\FOe$}$ and $\mbox{$\Ex\Ex\Al\Al\FO$}$, it follows via \Cref{prop:SattToHomClosedCompanion} from the unsatisfiability complexities of  \mbox{$\Al^*\FOe$}{} and \mbox{$\Al\Al\Ex\Ex\FO$}{}, respectively.
\end{proof}

\TGDNPtheorem*

\begin{proof}
	For \textsc{NP}-hardness, we reduce the 3-colorability problem to $\mathrm{HomClosed}_\mathrm{(fin)}$ as follows: given a finite graph expressed as $\{E\}$-structure $\mathfrak{G}$, three-colorability of $\mathfrak{G}$ is equivalent to the existence of a homomorphism from $\mathfrak{G}$ to $\mathfrak{K_3}$ (the complete but loop-free 3-element graph). However, this is the case exactly if the \mbox{$\mathbb{TGD}$}{} sentence $\Phi \ = \ \cq{\mathfrak{K_3}} \Rightarrow \cq{\mathfrak{G}}$ is a tautology. This, in turn coincides with $\getmodels{\Phi}$ being closed under homomorphisms (as, for the negative case, we find that $\mathfrak{K_3} \notin \getmodels{\Phi}$ receives a homomorphism from $\mathfrak{I} \in \getmodels{\Phi}$).

	In order to show \textsc{NP} membership, we provide a corresponding nondeterministic polytime algorithm that answers the question. From now on, we consider a \mbox{$\mathbb{TGD}$}{} sentence $\Phi$ as the finite set of conjuncts, each representing a single TGD (simply called ``rule'' in the following). We first apply a \textsc{PTime} preprocessing as follows: One by one, go through all the rules $\forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y}.\psi(\bold{x},\bold{y})$ of $\Phi$ and do the following:
	Let $\sim$ be the smallest equivalence relation over all the atoms from $\psi$ such that $\alpha \sim \alpha'$ whenever $\alpha$ and $\alpha'$ share an $\exists$-quantified variable from $\bold{y}$. For every $\sim$-equivalence class, form the conjunction over its atoms and $\exists$-quantify over all variables from $\boldsymbol{y}$ occurring therein. Let $\exists\bold{y_1}.\psi_1,\ldots, \exists\bold{y_n}.\psi_n$ be the formulae thus obtained. Now, replace $\forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y}.\psi(\bold{x},\bold{y})$
	by the rules $\forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y_1}.\psi_1(\bold{x},\bold{y_1}), \ldots, \forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y_n}.\psi_n(\bold{x},\bold{y_n})$. Finally, the new rule set is deterministically partitioned into two sets: those where all variables present in $\psi$'s atoms are $\exists$-quantified will be called \emph{disconnected}, all other rules will be called \emph{connected}. Obviously all this preprocessing can be done in deterministic polynomial time and produces a partitioned rule set of polynomial size in the original one. Moreover, the obtained rule set is semantically equivalent to the original one.

	We proceed to describe a polysize certificate witnessing homomorphism-closedness of a preprocessed rule set.
	Our certificate contains the following:
	\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex, topsep=0ex]
	\item a \emph{relevance partitioning} of the rule set into \emph{self-redundant} and \emph{self-irredundant} rules, where all connected rules (but possibly also some disconnected ones) are categorized as self-redundant. It is straight forward to check validity of such a partition in \textsc{PTime}.
    \item a \emph{redundancy witness} for each of the self-redundant rules: a substitution $h\colon \bold{y} \rightarrow \bold{x}$ sending every atom inside $\psi$ to an atom inside $\varphi$. Obviously redundancy witnesses can be verified in \textsc{PTime}.
	\item a \emph{universal model derivation}: a forward-chaining derivation sequence starting from $\mathfrak{I}$ using only self-irredundant rules and applying each rule at most once,  including the homomorphisms used for the rule applications. Let $\mathfrak{M}$ denote the universal model constructed in this derivation.  Again such a guess is of polynomial size and allows for \textsc{PTime} verification.
 \item a \emph{discharge witness} for each self-irredundant rule: a mapping $h\colon \bold{y} \rightarrow M$ sending every atom $\sig{R}(y_1,\ldots,y_n)$ inside $\psi$ to a ``semantic atom'' inside $\mathfrak{M}$, i.e., $(h(y_1),\ldots, h(y_n))  \in \sig{R}^\mathfrak{M}$.
 Discharge witnesses can be verified in \textsc{PTime}.
	\end{itemize}

	Summing up, the algorithm's guess consists of one relevance partitioning, one redundancy witness for every self-redundant rule, one universal model derivation, and one discharge witness per self-irredundant rule. Verification for each can be done in \textsc{PTime}.

	We now argue that the algorithm is correct (i.e., that the existence of a certificate as above coincides with the TGD set's homomorphism-closedness):

	\begin{enumerate}[label={\roman*}), itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item First, consider the case where one of the connected rules is not self-redundant (i.e., no appropriate witness can be provided). For such a rule $\forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y}.\psi(\bold{x},\bold{y})$, let $\mathfrak{A}_\varphi$ be such that $\cq{\mathfrak{A}_\varphi} = \exists \bold{x}.\varphi(\bold{x})$.
		Then, $\mathfrak{F}$ is a model, but $\mathfrak{F} \uplus \mathfrak{A}_\varphi$ is not -- due to the special form of $\psi$ that we achieved in the preprocessing. This is despite the existence of a homomorphism from $\mathfrak{F}$. Thus the rule set is not homclosed, as required. In the following, we consider the case where all connected rules are indeed (self-)redundant.

		\item Obviously, self-redundant rules are tautologies and hence have no influence on the set of models, so the question if the rule set is homomorphism-closed reduces to the question if its subset of self-irredundant rules is. By now we know that, in the considered rule set, every such rule $\forall \bold{x}.\varphi(\bold{x}) {\Rightarrow} \exists\bold{y}.\psi(\bold{x},\bold{y})$
		must be disconnected, i.e., be such that no variables from $\bold{x}$ occur in $\psi$, therefore any such rule can be written as $(\exists \bold{x}.\varphi(\bold{x})) \Rightarrow (\exists\bold{y}.\psi(\bold{y}))$. Henceforth, we assume our considered rule set contains the self-irredundant in this syntactic form. From the structure of the rules follows that there exists a finite universal model (i.e. one which has a homomorphism into every other model) $\mathfrak{M}$ which can be obtained in a forward-chaining derivation where every rule is applied at most once. This information is provided by the certificate's universal model derivation.

		\item We proceed to consider two cases.

		\begin{enumerate}
			\item Assume the non-existence of a discharge witness of $(\exists \bold{x}.\varphi(\bold{x})) \Rightarrow (\exists\bold{y}.\psi(\bold{y}))$.
			This means that among the remaining rules, there is one $(\exists \bold{x}.\varphi(\bold{x})) \Rightarrow (\exists\bold{y}.\psi(\bold{y}))$ for which $\mathfrak{M} \not\models \exists\bold{y}.\psi(\bold{y})$. Yet in that case $\mathfrak{M} \uplus \mathfrak{A}_\varphi$ is not a model (mark that the rule is not self-redundant by assumption), despite the existence of the trivial homomorphism from $\mathfrak{M}$ -- consequently the rule set is not homclosed.
			\item The existence of all discharge witnesses proves that each remaining rule's head is satisfied in $\mathfrak{M}$. Then, the same holds for every structure $\mathfrak{M}'$ into which a homomorphism from $\mathfrak{M}$ exists, which trivially entails that all remaining rules are satisfied in any such $\mathfrak{M}'$ and hence the rule set is homclosed. \qedhere
		\end{enumerate}

	\end{enumerate}
\end{proof}

\subsection{Proofs of Characterizing Homclosures Section}

\notFO*

\begin{proof}
	We note that $\mathfrak{A} \in \homcl{\getmodels{\Phi_{\infty}}}$ exactly if $\mathfrak{A}$ contains an infinite $\sig{P}{}$-path.
	Hence, if $\mathfrak{A}$ is finite, $\mathfrak{A} \in \homcl{\getmodels{\Phi_{\infty}}}$ exactly if $\mathfrak{A}$ contains a directed $\sig{P}{}$-cycle.
	Checking for the existence of directed cycles is \textsc{NLogSpace}-complete \cite{DBLP:journals/jcss/Jones75} whereas
	$\FO_{=}$ sentences can only describe problems in \textsc{AC}$^0$ \cite{DBLP:books/daglib/0095988}, which is strictly weaker than \textsc{NLogSpace}~\cite{FurstSS84}.
\end{proof}

\ExCharHomA*

\begin{proof}
	We show the claim by a reduction from (finite) satisfiability.
	Let $\Psi$ be an arbitrary $\FO_{=}$ formula.

	Consider $\Psi'$ defined as
	$\Psi^{\mathrm{rel}(\sig{U}{})} \wedge \Phi_{\text{grid}}$ chosen in a way that the signature $\tau_1 \uplus \{\sig{U}{}\}$ of $\Psi^{\mathrm{rel}(\sig{U}{})}$ and the signature $\tau_2$ of $\Phi_{\text{grid}}$ are disjoint.
	If $\Psi$ is (finitely) unsatisfiable, then so is $\Psi'$. In that case $\homclffin{\getffinmodels{\Psi'}}$ is empty and can be characterized by $\Phi_\bold{false}$.

	If $\Psi$ is (finitely) satisfiable, then any sentence $\tilde\Psi$ (finitely) characterizing $\homclffin{\getffinmodels{\Psi'}}$ can be turned into a procedure for deciding if for a domino system $\mathcal{D}$ a(n ultimately periodic) $\mathcal{D}$-tiling exists: this is the case exactly if the structure $\mathfrak{A}_\mathcal{D} \cdot\widehat{\tau_1} \cdot \widehat{\{\sig{U}{}\}}$ is a model of $\tilde\Psi$.

	It follows that the (finite) homomorphism closure of $\getffinmodels{\Psi'}$ is characterizable (in any non-degenerate logic $\mathbb{L}$) exactly if $\Psi$ is unsatisfiable. Checking the latter is undecidable.
\end{proof}

\ExCharHomB*

\begin{proof}
	We show the claim by a reduction from the existence of a(n ultimately periodic) tilling by the deterministic domino set $\mathcal{D}$.

Let the TGD sentence $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ with signature $\tau$ be defined as in \Cref{def:TGDdettiling}. Let
\begin{equation}
\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}} = \Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \wedge \Big( \big(\exists x.  \sig{T}{}_\emptyset(x) \big) \Rightarrow \cq{\mathfrak{F}} \Big).
\end{equation}
	If no (ultimately periodic) $\mathcal{D}$-tiling exists, then $\cq{\mathfrak{F}}$ characterizes $\homclffin{\getffinmodels{\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}}}}$.

	If, on the other hand, some (ultimately periodic) $\mathcal{D}$-tiling exists, then any sentence $\Psi$ (finitely) characterizing $\homclffin{\getffinmodels{\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}}}}$ can be turned into a procedure for deciding if for some other domino system $\mathcal{D}'$ a(n ultimately periodic) $\mathcal{D}'$-tiling exists: this is the case exactly if the structure $\mathfrak{A}_{\mathcal{D}'} \cdot\widehat{\sigma}$ with $\sigma=\tau \setminus \{\sig{H}{},\sig{V}{}\}$  is a model of $\Psi$.
This holds since all $\{\sig{H},\sig{V}\}$-reducts of models of  $\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}}$ satisfy  $\Phi_{\text{grid}}$ and furthermore if an ultimately periodic $\mathcal{D}'$-tiling exists we can find a  model of  $\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}}$ such that the period of the grid induced by its $\{\sig{H},\sig{V}\}$-reduct is a multiple of the period of the $\mathcal{D}'$-tiling. This is possible since a domino set that tiles the grid with an ultimately periodic tiling with period length $k$  also tiles it with an ultimately periodic tiling with period length $k\cdot s$  for all $s\in \mathbb{N}$.

	It follows that the (finite) homomorphism closure of $\getffinmodels{\Phi'_{\mathcal{D}\text{-}\mathrm{tiling}}}$ is characterizable (in any decent logic $\mathbb{L}$ in the above sense) exactly if some (ultimately periodic) $\mathcal{D}$-tiling exists. Checking the latter is undecidable.
\end{proof}

\EAFOinEPO*

\begin{proof}
	Assume $\Phi$ is over the signature $\tau$.
	Let $\Phi^\mathrm{sk}$ be the $\mbox{$\Al^*\FOe$}$ sentence obtained from $\Phi$ via skolemization of all the existentially quantified variables into constants. Clearly then  $\getffinmodels{\Phi} = \getffinmodels{\Phi^\mathrm{sk}}|_\tau$. Since $\Phi^\mathrm{sk}$ is a $\mbox{$\Al^*\FOe$}$ sentence, any model $\mathfrak{A}$ gives rise to a ``small'' submodel by taking the substructure $\mathfrak{A}'$ induced by the set $A' \subseteq A$ containing all elements denoted by constants (if the signature has no constants, pick one arbitrary element). Moreover, the identity on $A'$ is a homomorphism from $\mathfrak{A}'$ to $\mathfrak{A}$. Let $\mathcal{A}$ be the set of small submodels thus obtained, for which therefore holds $\homcl{\mathcal{A}}=\homcl{\getmodels{\Phi^\mathrm{sk}}}$ and hence also $\homcl{\mathcal{A}|_\tau}=\homcl{\getmodels{\Phi}}$. Due to the bound on the domain size (number of constants), $\mathcal{A}$ (and thus $\mathcal{A}|_\tau$) can contain only finitely many different structures (up to isomorphism) and is effectively computable via enumeration and model checking. Hence $\homcl{\mathcal{A}|_\tau}$ can be characterized by the  $\mbox{$\Ex^*\FOe$}$ sentence $\Psi = \bigvee_{\mathfrak{A} \in \mathcal{A}|_\tau} \cq{\mathfrak{A}}$.
\end{proof}

\allhomcaptures*

We split the proof into separate statements and prove them individually:
\begin{itemize}
\item \Cref{prop:charFOte} deals with homcapturing of $\mbox{$\FO_{=}^\mathbbm{2}$}$
\item \Cref{prop:charGFO} deals with homcapturing of $\mbox{$\mathbb{GFO}_{=}$}$
\item \Cref{prop:charGNFO} deals with homcapturing of $\mathbb{GNFO}_{=}$
\item \Cref{prop:charTGF} deals with homcapturing of $\mbox{$\mathbb{TGF}$}$
\item \Cref{prop:charEAAE} deals with homcapturing of $\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$
\end{itemize}

Before, however, we will show a useful result, which allows us to -- without loss of generality -- restrict our attention to (projective) normal forms of the considered logics (as they are typically used in results related to satisfiability).

\begin{lemma}[projective normal form sufficiency]\label{lem:normalformOK}
For some $\tau \subseteq \tau' \subseteq \tau''$, let
\begin{itemize}[itemindent=0ex, leftmargin=3ex, itemsep=-0.7ex, topsep=-0.5ex]
\item
$\Phi$ be a $\tau$-sentence,
\item
$\Phi'$ be a $\tau'$-sentence projectively characterizing $\Phi$, i.e., $\getmodels{\Phi'}|_\tau = \getmodels{\Phi}$,
\item
$\Psi$ be a $\tau''$-sentence projectively characterizing the homclosure of $\Phi'$, i.e., $\homcl{\getmodels{\Phi'}} = \getmodels{\Psi}|_{\tau'}$.
\end{itemize}
Then $\Psi$ also projectively characterizes the homclosure of $\Phi$, i.e., $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_{\tau}$ holds.
\end{lemma}

\begin{proof}
Since $\tau \subseteq \tau'$, we obtain
\begin{equation}
\getmodels{\Psi}|_\tau = \getmodels{\Psi}|_{\tau'}|_\tau = \homcl{\getmodels{\Phi'}}|_\tau \stackrel{*}{=} \homcl{\getmodels{\Phi'}|_\tau} = \homcl{\getmodels{\Phi}}.
\end{equation}
For the equality denoted by $\stackrel{*}{=}$, we show the two inclusions separately:

``$\subseteq$'': Let $\mathfrak{B} \in \homcl{\getmodels{\Phi'}}|_\tau$. Then there exists a $\tau'$-structure $\mathfrak{B}' \in \homcl{\getmodels{\Phi'}}$ with $\mathfrak{B}'|_\tau = \mathfrak{B}$. Hence there exist a $\tau'$-structure $\mathfrak{A}' \in \getmodels{\Phi'}$ and a homomorphism $h \colon \mathfrak{A}' \to \mathfrak{B}'$. But then $h$ also serves as a homomorphism from $\mathfrak{A} = \mathfrak{A}'|_\tau$ to $\mathfrak{B}'|_\tau = \mathfrak{B}$. By $\mathfrak{A} \in  \getmodels{\Phi'}|_\tau$ we then obtain $\mathfrak{B} \in \homcl{\getmodels{\Phi'}|_\tau}$.

``$\supseteq$'': Let $\mathfrak{B} \in \homcl{\getmodels{\Phi'}|_\tau}$. Then there exist a $\tau'$-structure $\mathfrak{A}' \in \getmodels{\Phi'}$ and a homomorphism $h \colon \mathfrak{A}'|_{\tau} \to \mathfrak{B}$. Let now $\mathfrak{B}' =  \mathfrak{B} \cdot {\raisebox{1pt}{$\widehat{\ \ \ \ \ \ }$} \hspace{-4.5ex}  { \tau' {\setminus} \tau}}$. Clearly,
then $h$ serves as homomorphism from $\mathfrak{A}'$ to $\mathfrak{B}'$, thus $\mathfrak{B}' \in \homcl{\getmodels{\Phi'}}$. Yet, since $\mathfrak{B}'|_\tau = \mathfrak{B}$, we obtain $\mathfrak{B} \in \homcl{\getmodels{\Phi'}}|_\tau$.
\end{proof}

As the next three results (namely \Cref{prop:charFOte}, \Cref{prop:charGFO}, and \Cref{prop:charTGF}) will make use of some essentially equal parts in the homcapturing sentence we introduce these ``generic'' parts beforehand.

\begin{definition}
	Let $\Phi$ be a $\mathbb{FO}{}$ sentence over some fixed signature $\tau$ and let $C$ denote the set of all constant symbols from $\tau$. Additionally, we fix some map $\mathrm{width}$ mapping each $\tau$-formula to some natural number, its so-called \emph{width}. We specify this map when the need arises.

	A \emph{type $\mathfrak{t}$} is a maximal consistent set of $\tau$-literals (i.e., negated and unnegated atoms where the relation symbol is from $\tau$) over terms from $\bold{v} \cup C$, where $\bold{v}$ is a dedicated, finite, linearly ordered set of \emph{type variables} of cardinality $\geq \mathrm{width}(\Phi)$. When necessary we might explicitly mention the signature at consideration, i.e. we say \emph{$\tau$-type}.
	To each type $\mathfrak{t}$ we associate a $\bold{v}$-subsequence $\bold{v}_{\mathfrak{t}}$ enumerating the variables of $\mathfrak{t}$.
	We say $\mathfrak{t}$ is an \emph{$n$-type}, or equivalently is a type of \emph{order $n$}, if $\bold{v}_{\mathfrak{t}}$ is a sequence of exactly $n$ variables. We define $\mathrm{order}$ to be a map from the set of types to the natural numbers, associating to each type its order, i.e., an $n$-type $\mathfrak{t}$ has $\mathrm{order}(\mathfrak{t}) = n$.
	For a structure $\mathfrak{A}$ we say that an $n$-type $\mathfrak{t}$ is \emph{realized} by an $n$-tuple $\bold{a} = (a_{1}, \ldots, a_{n}) \in A^{n}$, if for the componentwise evaluation map $\nu \colon \bold{v}_{t} \mapsto \bold{a}, (\bold{v}_{\mathfrak{t}})_{i} \mapsto a_{i}$ the relation $(\mathfrak{A}, \nu) \vDash \mathfrak{t}$ holds.
	We say a type $\mathfrak{t}$ of order $n$ is \emph{realized} ($k$ times) in $\mathfrak{A}$ if it is realized by ($k$ distinct) $n$-tuples from $\mathfrak{A}$.

	Given an atom $\delta$ using exactly the variables from $\bold{x}$ (and possibly additional constants), we say a type $\mathfrak{t}$ is \emph{guarded by $\delta$} if there exists a variable substitution $\nu\colon \bold{x} \to \bold{v}_{\mathfrak{t}}\cup C$ with $\bold{v}_{\mathfrak{t}} \subseteq \{\nu(x) \mid x \in \bold{x}\}$ such that $\nu(\delta) \in \mathfrak{t}$, where the application of a substitution $\nu$ to an expression replaces all occurrences of every variable $x$ in $\nu$'s domain by $\nu(x)$. Then $\nu$ will be called \emph{guard witness}.
	A type $\mathfrak{t}$ is \emph{guarded}, if it is guarded by some atom.
	A type $\mathfrak{t}$ is called \emph{rigid} if it does not contain literals of the form $v=v'$ (for distinct variables $v,v'$ from $\bold{v}_{\mathfrak{t}}$) or $\sig{c} = v$ or $v = \sig{c}$ for $\sig{c}\in C$.
	For $\bold{v}' \subseteq \bold{v}_{\mathfrak{t}}$, we obtain the $\bold{v}'$-\emph{subtype} of $\mathfrak{t}$, denoted $\mathfrak{t}|_{\bold{v}'}$, by removing from $\mathfrak{t}$ all literals mentioning any variable from $\bold{v}_\mathfrak{t} \setminus \bold{v}'$.

	By $\mathcal{E}$ we will denote a fixed finite set of rigid types and call it the set of \emph{eligible types}. For a $\tau$-structure $\mathfrak{A}$ we denote by $\mathcal{E}(\mathfrak{A})$ its \emph{type summary}, which is a pair $(\mathcal{E}_{+}, \mathcal{E}_{!})$ of subsets of $\mathcal{E}$ such that $\mathcal{E}_{+}$ ($\mathcal{E}_{!}$) contains every type realized (exactly once) in $\mathfrak{A}$. Furthermore, the \emph{model summary} $\getsummary{\Phi}$ of a sentence $\Phi$ is defined by $\{ \mathcal{E}(\mathfrak{A}) \ | \ \mathfrak{A}\in \getmodels{\Phi} \}$

	For a set $\mathcal{E}$ of eligible types we extend the signature $\tau$ by a set $\sigma$ of \emph{type predicates}: $\sigma$ contains a new $n$-ary predicate $\sig{Tp}_{\mathfrak{t}}$ for every eligible $n$-type $\mathfrak{t}\in\mathcal{E}$.
	Let $\mathfrak{A}$ be a $\tau$-structure. The \emph{$\mathcal{E}$-adornment} of $\mathfrak{A}$, denoted by $\mathfrak{A}\cdot\mathcal{E}$ is the $\tau\uplus\sigma$-structure expanding $\mathfrak{A}$ such that $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}} = \{ \bold{a} \ | \ \bold{a} \text{ realizes } \mathfrak{t} \text{ in } \mathfrak{A} \}$.

	If $\mathfrak{A}, \mathfrak{B}$ are $\tau$-structures such that there is a homomorphism $h \colon \mathfrak{A}\to\mathfrak{B}$ and we have a set of eligible types $\mathcal{E}$, then we denote by $\mathfrak{B}\cdot h(\mathfrak{A}\cdot\mathcal{E}|_{\sigma})$ the $\tau\uplus\sigma$-structure $\mathfrak{B}'$ expanding $\mathfrak{B}$ with $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'} = \{ h(\bold{a}) \ | \ \bold{a} \in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}} \}$.

	We define
	\begin{equation}
		\Psi_\mathrm{hom} = \!\bigwedge_{\mathfrak{t} \in \mathcal{E}} \!\forall \bold{v}_{\mathfrak{t}}.\big( \sig{Tp}_\mathfrak{t}(\bold{v}_{\mathfrak{t}}) \Rightarrow \smallbigwedge \{\alpha \tight{\in} \mathfrak{t} \mid \alpha \text{ positive lit.}\} \big).
	\end{equation}

	For every $(\mathcal{E}_{+}, \mathcal{E}_{!}) \in \getsummary{\Phi}$ let $\Psi_{\mathrm{gen}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$ be the conjunction of the following formulae:

	\newcommand{\hspace{-1.5ex}}{\hspace{-1.5ex}}
	\noindent
	\begin{eqnarray}
		\hspace{-1.5ex}\exists \bold{v}_\mathfrak{t}. \sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& & \hspace{-1.5ex} \hspace{25ex}\mbox{for } \mathfrak{t} \in \mathcal{E}_{+}  \label{eq: gen 1}\\
		\hspace{-1.5ex}\forall \bold{v}_\mathfrak{t}. \sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \bot \hspace{20ex}\mbox{for } \mathfrak{t} \in \mathcal{E}\setminus \mathcal{E}_{+}  \label{eq: gen 2}\\
		\hspace{-1.5ex}\forall \bold{v}_\mathfrak{t}. \sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} 	\sig{Tp}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'}) \hspace{5.25ex}\mbox{for } \mathfrak{t},\mathfrak{t}' \in \mathcal{E}_{+}, \mathfrak{t}'=\mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}  \label{eq: gen 3} \\
		\hspace{-1.5ex}\forall \bold{x}. \sig{Tp}_\mathfrak{t} (\bold{x}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} 	\sig{Tp}_{\kappa\mathfrak{t}}( \eta^{\kappa\bold{v}_\mathfrak{t}}_\bold{v} (\bold{x}) ) \hspace{1.75ex}\mbox{for } \mathfrak{t} \in \mathcal{E}, \kappa \colon \bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}} \bold{v} \label{eq: gen 3plus}
	\end{eqnarray}
	\let\hspace{-1.5ex}\undefined
	where
	\begin{itemize}
		\item
		the permutation $\kappa$ on the set $\bold{v}$ is extended to variable tuples in the usual way and also used as substitution on logical expressions,
		\item for a (repetition-free) tuple $\bold{v}'$ of variables from $\bold{v}$, we let $\eta^{\bold{v}'}_\bold{v}$ denote the sorting function rearranging the entries of $|\bold{v}'|$-tuples in a way that $\eta^{\bold{v}'}_\bold{v}(\bold{v}')$ becomes a subsequence of $\bold{v}$.
	\end{itemize}
\end{definition}
Several remarks to this definition:
\begin{enumerate}
	\item Note that each signature $\tau$ is finite (hence also the set of constant symbols $C$ from $\tau$) and the set of dedicated type variables $\bold{v}$ is finite as well. Hence there are only finitely many distinct literals with terms from $\bold{v}\cup C$. This implies the finiteness of every type $\mathfrak{t}$. For convenience we may identify $\mathfrak{t}$ (which is a set of literals) with the conjunction over all the literals contained in it, i.e. $\bigwedge \mathfrak{t}$ (which then is a formula).
	\item Given a $\tau$-structure $\mathfrak{A}$ and a tuple $\bold{a} = (a_{1}, \ldots, a_{n})$ (such that $\mathrm{length}(\bold{a}) \le \mathrm{length}(\bold{v})$), $\bold{a}$ realizes one, up to permutation of type variables, unique type $\mathfrak{t}$ characterizing the induced substructure of $\mathfrak{A}$ by the elements from $\bold{a}$ and the interpretations of every constant symbol. To be more precise, let $\bold{v}_{\mathfrak{t}} = (v_{1}, \ldots, v_{n})$ be the initial segment of $\bold{v}$ of length $\mathrm{length}(\bold{a})$ and $\mu \colon \bold{v}_{\mathfrak{t}}\to\bold{a}, v_i\mapsto a_i$ the componentwise evaluation of $\bold{v}_{\mathfrak{t}}$ by $\bold{a}$. We extend $\mu$ to $\bold{v}_{\mathfrak{t}}\cup C$ by defining $\mu(\sig{c}) = \sig{c}^{\mathfrak{A}}$ for every $\sig{c}\in C$. For each $\sig{R}$ and $\bold{t} = (t_{1}, \ldots, t_{\mathrm{ar}(\sig{R})})\subseteq \bold{v}_{\mathfrak{t}}\cup C$ the literal
	\begin{itemize}
		\item $\sig{R}(\bold{t})$ is in $\mathfrak{t}$, iff $\mu(\bold{t}) \in \sig{R}^{\mathfrak{A}}$ and
		\item $\lnot\sig{R}(\bold{t})$ is in $\mathfrak{t}$, iff $\mu(\bold{t}) \notin \sig{R}^{\mathfrak{A}}$.
	\end{itemize}
	This set is consistent as (by $\mathfrak{A}$ being a structure) for $\bold{t}$ we cannot have $\mu(\bold{t})\in \sig{R}^{\mathfrak{A}}$ and $\mu(\bold{t})\notin \sig{R}^{\mathfrak{A}}$ simultaneously. Furthermore it is maximal since either $\mu(\bold{t})\in \sig{R}^{\mathfrak{A}}$ or $\mu(\bold{t})\notin \sig{R}^{\mathfrak{A}}$. To show uniqueness (up to variable permutations), assume there were a second type $\mathfrak{t}^{\ast}$ also realized by $\bold{a}$ such that for all $\kappa \colon \bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}}\bold{v}$ the inequality $\kappa\mathfrak{t}^{\ast}\neq\mathfrak{t}$ holds. Without loss of generality we may assume that $\bold{v}_{\mathfrak{t}} = \bold{v}_{\mathfrak{t}^{\ast}} = (v_{1}, \ldots, v_{n})$ and $\kappa$ mapping each $v\in\bold{v}_{\mathfrak{t}}$ to itself (and hence $\kappa\mathfrak{t}^{\ast}=\mathfrak{t}^{\ast}$). As $\mathfrak{t} \neq \mathfrak{t}^{\ast}$ there is some $\sig{R} \in \tau$ and $\bold{t}(t_{1}, \ldots, t_{\mathrm{ar}(\sig{R})})\subseteq \bold{v_{\mathfrak{t}}} \cup C$ such that $\sig{R}(\bold{t})\in \mathfrak{t}$ and $\sig{R}(\bold{t})\notin\mathfrak{t}^{\ast}$. By maximal consistency of types this means $\lnot\sig{R}(\bold{t})\in \mathfrak{t}^{\ast}$. But as $\bold{a}$ realizes both types we obtain $\mu(\bold{t})\in\sig{R}^{\mathfrak{A}}$ and $\mu(\bold{t})\notin\sig{R}^{\mathfrak{A}}$, a contradiction.
	\item A note on eligible types: Depending on the logical fragment under scrutiny, we will make the notion of eligibility more specific. In fact, for $\Phi$ a sentence from some fragment of $\mathbb{FO}{}$, the finiteness will be ensured by considering just types whose order is bounded by $\mathrm{width}(\Phi)$.
	\item As a corollary to sets $\mathcal{E}$ being finite, we immediately obtain that for an $\mathbb{FO}{}$ sentence $\Phi$ (and a set of eligible types $\mathcal{E}$) its model summary $\getsummary{\Phi}$ is finite.
\end{enumerate}
\begin{lemma}\label{lem:eligclosure}
	Let $\tau$ be a signature and $\Phi$ a $\mathbb{FO}{}$ $\tau$-sentence. Let $\mathcal{E}$ be a finite set of rigid types.
	\begin{enumerate}
		\item\label{item eligclosure:1} For every $\mathfrak{t}, \mathfrak{t}' \in \mathcal{E}$ and every $\mathfrak{A}\in\getmodels{\Phi}$ with $\mathcal{E}(\mathfrak{A}) = (\mathcal{E}_{+}, \mathcal{E}_{!}) \in \getsummary{\Phi}$ with $\mathfrak{t}' = \mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}$ and $\mathfrak{t}\in \mathcal{E}_{+}$, then also $\mathfrak{t}' \in \mathcal{E}_{+}$. More specifically: Every componentwise assignment $\mu\colon\bold{v}_{\mathfrak{t}}\to\bold{a}$ of the variables from $\mathfrak{t}$ to a tuple $\bold{a}$ from $\mathfrak{A}$ of length $\mathrm{order}(\mathfrak{t})$ witnessing the realization of $\mathfrak{t}$ by $\bold{a}$ in $\mathfrak{A}$ gives rise to a subtuple $\bold{a}'$ of $\bold{a}$, namely $\mu(\bold{v}_{\mathfrak{t}'})$, such that $\bold{a}' = \mu|_{\bold{v}_{\mathfrak{t}'}}$ witnesses the realization of $\mathfrak{t}'$ by $\bold{a}'$ in $\mathfrak{A}$.
		\item\label{item eligclosure:2} If $\mathcal{E}$ is closed under taking variable permutations, i.e., for every $\mathfrak{t} \in \mathcal{E}$ and $\kappa\colon \bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}}\bold{v}$ also $\kappa\mathfrak{t} \in \mathcal{E}$,
		then so is $\mathcal{E}_{+}$ for every $(\mathcal{E}_{+}, \mathcal{E}_{!})\in\getsummary{\Phi}$.
	\end{enumerate}
\end{lemma}
Note that Item \ref{item eligclosure:1} essentially asserts for every $(\mathcal{E}_{+}, \mathcal{E}_{!}) \in \getsummary{\Phi}$ a kind of limited closure under taking subtypes in $\mathcal{E}_{+}$ .

\begin{proof}
	Let $\Phi$ be a $\mathbb{FO}{}$ $\tau$-sentence and $\mathcal{E}$ a set of eligible types.

		We first show Item \ref{item eligclosure:1}. Let $\mathfrak{t}, \mathfrak{t}'\in \mathcal{E}$ with $\mathfrak{t}'=\mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}$, $\mathfrak{A}\in\getmodels{\Phi}$, $\mathcal{E}(\mathfrak{A})=(\mathcal{E}_{+}, \mathcal{E}_{!})\in\getsummary{\Phi}$, and $\mathfrak{t} \in\mathcal{E}_{+}$. Hence $\mathfrak{t}$ is realized in $\mathfrak{A}$ by some tuple $\bold{a} = (a_{1}, \ldots, a_{n})\in A^{n}$ where $n = \mathrm{order}(\mathfrak{t})$. Let $\mu\colon \bold{v}_{\mathfrak{t}} \to \bold{a}$ be the componentwise variable evaluation witnessing this realization, i.e. $(\mathfrak{A}, \mu) \vDash \mathfrak{t}$. Now we set $\iota\colon \bold{v}_{\mathfrak{t}'}\to\bold{v}_{\mathfrak{t}}, v \mapsto v$. Then the map $\mu\circ\iota$ witnesses the realization of $\mathfrak{t}' = \mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}$ in $\mathfrak{A}$ by the subtuple $\mu(\bold{v}_{\mathfrak{t}'})$ (obtained by componentwise application of $\mu$) of $\bold{a}$. As $\mathfrak{t}' \in \mathcal{E}$ we conclude $\mathfrak{t}'\in \mathcal{E}_{+}$.

	Now take $\mathcal{E}$ to be closed under taking permutations of variables, let $\mathfrak{A}\in\getmodels{\Phi}$, and $\mathcal{E}(\mathfrak{A}) = (\mathcal{E}_{+}, \mathcal{E}_{!})\in\getsummary{\Phi}$. Furthermore take some type $\mathfrak{t}\in \mathcal{E}_{+}$ and some permutation $\kappa\colon\bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}}\bold{v}$. Since $\mathfrak{t}\in\mathcal{E}_{+}$, it is realized by some tuple $\bold{a}=(a_{1}, \ldots, a_{n})\in A^{n}$ where $n = \mathrm{order}(\mathfrak{t})$. We denote by $\mu \colon \bold{v}_{\mathfrak{t}}\to \bold{a}$ the componentwise variable assignment witnessing the realization of $\mathfrak{t}$ by $\bold{a}$ in $\mathfrak{A}$, i.e. $(\mathfrak{A}, \mu)\vDash \mathfrak{t}$. Then the tuple $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a})$ realizes $\kappa\mathfrak{t}$, witnessed by $\mu' \colon \kappa\bold{v}_{\mathfrak{t}}\to \eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a}), (\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{v}_{\mathfrak{t}}))_{i}\mapsto (\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a}))_{i}$. As $\mathcal{E}$ is closed under taking permutations of variables, we conclude that $\kappa\mathfrak{t}\in\mathcal{E}_{+}$. This establishes Item \ref{item eligclosure:2}.
\end{proof}
\begin{lemma}\label{lem:PsiGen}
	Let $\Phi$ be a $\mathbb{FO}{}$ $\tau$-sentence, $\mathcal{E}$ be a set of eligible types (i.e., a finite set of rigid type) closed under variable permutations, and $\sigma$ be the set of fresh type predicates $\sig{Tp}_{\mathfrak{t}}$ for all $\mathfrak{t}\in \mathcal{E}$. Then for $\mathfrak{A} \in\getmodels{\Phi}$ the $\mathcal{E}$-adornment $\mathfrak{A}\cdot \mathcal{E}$ satisfies $\Psi_{\mathrm{gen}, \mathcal{E}(\mathfrak{A})}$. Furthermore, for every $\mathfrak{B}$ being a homomorphic codomain of $\mathfrak{A}$ via a homomorphism $h \colon \mathfrak{A}\to\mathfrak{B}$ the $\tau\uplus\sigma$-structure $\mathfrak{B} \cdot h(\mathfrak{A}\cdot \mathcal{E}|_{\sigma})$ equally satisfies $\Psi_{\mathrm{gen}, \mathcal{E}(\mathfrak{A})}$.
\end{lemma}
\begin{proof}
	Let $\Phi$ be a $\mathbb{FO}{}$ $\tau$-sentence,  $\mathfrak{A}\in\getmodels{\Phi}$ and let $\mathcal{E}$ be the set of eligible types and $\mathcal{E}(\mathfrak{A}) = (\mathcal{E}_{+}, \mathcal{E}_{!})$ denote the type summary of $\mathfrak{A}$.
	We show that the $\mathcal{E}$-adornment $\mathfrak{A}\cdot\mathcal{E}$ of $\mathfrak{A}$ satisfies $\Psi_{\mathrm{gen}, \mathcal{E}(\mathfrak{A})}$. More specifically:
	\newline
	For all $\mathfrak{t} \in \mathcal{E}$ the interpretation $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot \mathcal{E}}$ contains by definition some tuple $\bold{a}$ from $\mathfrak{A}\cdot\mathcal{E}$ if and only if $\bold{a}$ realizes the associated type $\mathfrak{t}$ in $\mathfrak{A}$. As every $\mathfrak{t} \in \mathcal{E}_{+}$ is realized in $\mathfrak{A}$ we conclude that $\mathfrak{A}\cdot\mathcal{E}$ satisfies Formulae \ref{eq: gen 1}. As none of the types $\mathfrak{t} \in \mathcal{E}\setminus \mathcal{E}_{+}$ is being realized in $\mathfrak{A}$, we see by the same token that the interpretations $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ have to be empty. Hence we immediately obtain that $\mathfrak{A}\cdot \mathcal{E}$ satisfies Formulae \ref{eq: gen 2}.
	\newline
	Now take $\mathfrak{t}, \mathfrak{t}' \in \mathcal{E}$ such that $\mathfrak{t}' = \mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}$ and let $\bold{a}$ be some tuple from $\mathfrak{A}\cdot\mathcal{E}$ such that $\bold{a}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$. By definition $\bold{a}$ realizes $\mathfrak{t}$ in $\mathfrak{A}$, let $\mu\colon \bold{v}_{\mathfrak{t}} \to\bold{a}$ be the componentwise evaluation witnessing this.
	By \Cref{lem:eligclosure} $\mathfrak{t}'$ is realized in $\mathfrak{A}$ (i.e. $\mathfrak{t}' \in\mathcal{E}_{+}$) by the subtuple $\mu(\bold{v}_{\mathfrak{t}'})$ ($\mu$ applied componentwise) of $\bold{a}$ realizing $\mathfrak{t}'$. Hence it is in $\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{A}\cdot\mathcal{E}}$ by definition. Finally, observing that $\mu$ assigns the tuple $\bold{a}$ componentwise to $\bold{v}_{\mathfrak{t}}$, yields the satisfaction of Formulae \ref{eq: gen 3} by $\mathfrak{A}\cdot\mathcal{E}$.
	\newline
	To show the satisfaction of the last kind of Formulae (i.e. Formulae \ref{eq: gen 3plus}), let $\mathfrak{t} \in \mathcal{E}$, $\kappa \colon \bold{v} \mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}} \bold{v}$ a permutation of the variables and $\bold{a}$ a tuple from $\mathfrak{A}\cdot\mathcal{E}$ such that $\bold{a}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$. Note that, since $\mathcal{E}$ is closed under taking permutations of (type) variables, $\kappa\mathfrak{t}\in\mathcal{E}$. As for every $\mathfrak{t} \in\mathcal{E}\setminus\mathcal{E}_{+}$ the interpretation $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ is empty, it suffices to discuss the case when $\mathfrak{t}\in \mathcal{E}_{+}$. Hence $\bold{a}$ realizes $\mathfrak{t}$ in $\mathfrak{A}$. It is plain that $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a})$ realizes $\kappa\mathfrak{t}$ in $\mathfrak{A}$, hence $\kappa\mathfrak{t}\in\mathcal{E}_{+}$. Thus we obtain $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a}) \in \sig{Tp}_{\kappa\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$, showing that $\mathfrak{A}\cdot\mathcal{E}$ satisfies Formulae \ref{eq: gen 3plus}.

	We now turn to the second part of the lemma. Let $\mathfrak{B}$ be a $\tau$-structure such that there is a homomorphism $h\colon \mathfrak{A} \to \mathfrak{B}$. We show that the structure $\mathfrak{B}\cdot h(\mathfrak{A}\cdot\mathcal{E}|_{\sigma})$ (which we will denote by $\mathfrak{B}'$) also satisfies $\Psi_{\mathrm{gen}, \mathcal{E}(\mathfrak{A})}$. Additionally, $h\colon \mathfrak{A}\to\mathfrak{B}$ is also a homomorphism if lifted to $h' \colon \mathfrak{A}\cdot\mathcal{E} \to \mathfrak{B}'$. As $h$ is already a homomorphism from $\mathfrak{A}$ to $\mathfrak{B}$ we only have to check whether for every $\sig{Tp}_{\mathfrak{t}} \in\sigma$ and $\bold{a}\in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ the image of $\bold{a}$ under $h'$ satisfies $h'(\bold{a})\in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$. But by definition of $\mathfrak{B}'$ the interpretation of these type predicates is already defined to be the homomorphic image of the respective interpretations in $\mathfrak{A}\cdot\mathcal{E}$. Hence $h'(\bold{a})\in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$ yielding that $h'$ is also a homomorphism.
	\newline
	Applying this knowledge we immediately obtain that $\mathfrak{B}'$ satisfies Formulae \ref{eq: gen 1}: As $\mathfrak{A}\cdot\mathcal{E}$ satisfies \ref{eq: gen 1} we find for every $\mathfrak{t} \in \mathcal{E}_{+}$ a tuple $\bold{a}$ such that $\bold{a}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$. As $h'$ is a homomorphism we get $h'(\bold{a}) \in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$.
	To show satisfaction of Formulae \ref{eq: gen 2} we note first, that by definition of $\mathfrak{B}'$ we interpreted the type predicates exactly as the homomorphic image of their interpretation in $\mathfrak{A}\cdot\mathcal{E}$. Hence for every $\mathfrak{t}\in \mathcal{E}\setminus\mathcal{E}_{+}$ we obtain $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'} = \emptyset$ as $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ was already empty. This yields Formulae \ref{eq: gen 2}.
	\newline
	Now let $\mathfrak{t}, \mathfrak{t}' \in \mathcal{E}$ such that $\mathfrak{t}' = \mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}$ and let $\bold{b}$ be a tuple from $\mathfrak{B}'$ such that $\bold{b}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$. As $\bold{b}$ is in $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$ we know by definition of $\mathfrak{B}'$ that $\bold{b}$ is the homomorphic image of some tuple from $\mathfrak{A}\cdot\mathcal{E}$, more specifically we find a tuple $\bold{a}$ in $\mathfrak{A}\cdot\mathcal{E}$ such that $\bold{a}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ and $h'(\bold{a}) = \bold{b}$. Let $\mu\colon \bold{v}_{\mathfrak{t}} \to\bold{a}$ be the componentwise evaluation witnessing the satisfaction of $\sig{Tp}_{\mathfrak{t}}$ by $\bold{a}$ in $\mathfrak{A}\cdot\mathcal{E}$. By \Cref{lem:eligclosure} the subtuple $\bold{a}^{\ast} = \mu(\bold{v}_{\mathfrak{t}'})$ (where $\mu$ is applied componentwise) of $\bold{a}$ satisfies $\sig{Tp}_{\mathfrak{t}'}$ in $\mathfrak{A}\cdot\mathcal{E}$. By applying $h'$ to $\bold{a}^{\ast}$ we obtain a subtuple $\bold{b}^{\ast} = h'(\bold{a}^{\ast})$ of $\bold{b}$ which satisfies $\bold{b}^{\ast}\in \sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}'}$. This ensures the satisfaction of Formulae \ref{eq: gen 3} by $\mathfrak{B}'$.
	\newline
	Finally, let $\mathfrak{t} \in \mathcal{E}$, $\kappa \colon \bold{v} \mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}} \bold{v}$ a permutation of the variables and $\bold{b}$ a tuple from $\mathfrak{B}'$ such that $\bold{b}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$. Since by definition of $\mathfrak{B}'$ the interpretation $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$ is non-empty if and only if $\mathfrak{t} \in \mathcal{E}_{+}$ it 	suffices to assume just that. From $\bold{b}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$ we obtain via the definition of $\mathfrak{B}'$ that there is a tuple $\bold{a}$ in $\mathfrak{A}\cdot\mathcal{E}$ such that $\bold{a}\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$ and $h'(\bold{a}) = \bold{b}$. As Formulae \ref{eq: gen 3plus} hold in $\mathfrak{A}\cdot\mathcal{E}$ we can conclude that $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a})\in \sig{Tp}_{\kappa\mathfrak{t}}^{\mathfrak{A}\cdot\mathcal{E}}$. As the application of maps that are defined on elements	extends to tuples componentwise, $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}$ and $h'$ commute, hence
	\begin{equation}
		h'(\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{a})) = \eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(h'(\bold{a})) = \eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{b})
	\end{equation}
	and since $h'$ is a homomorphism we obtain immediately $\eta_{\bold{v}}^{\kappa\bold{v}_{\mathfrak{t}}}(\bold{b})\in \sig{Tp}_{\kappa\mathfrak{t}}^{\mathfrak{B}'}$. This proves that $\mathfrak{B}'$ satisfies Formulae \ref{eq: gen 3plus} and concludes the whole proof of the lemma.
\end{proof}

\begin{proposition}[restate=FOTEinESO, name=]\label{prop:charFOte}
	For every \mbox{$\FO_{=}^\mathbbm{2}$}{} $\tau$-sentence $\Phi$,
	there exists
	a \mbox{$\FO_{=}^\mathbbm{2}$}{}
	sen\-tence $\Psi$
	such that $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$.
\end{proposition}

\begin{proof}
Thanks to \Cref{lem:normalformOK}, we can w.l.o.g. assume $\Phi$ to be in Scott's normal form, i.e.
\begin{equation}
\Phi = \forall xy. \varphi(x,y) \wedge \bigwedge_i \forall x \exists y.\psi_i(x,y),
\end{equation}
 where $\varphi$ and all $\psi_i$ are quantifier-free $\mbox{$\FO_{=}^\mathbbm{2}$}$ $\tau$-formulae.

Let $\bold{v} = \{ v_{1}, v_{2} \}$ be the set of dedicated type variables we will use in this proof.
We now define the set $\mathcal{E}$ of eligible types as all rigid $1$-types and $2$-types (using variables from $\bold{v}$) wrt. $\tau$. Note that $\mathcal{E}$ is closed under variable permutations.

	As there are only two permutations on $\{ v_{1}, v_{2} \}$ (the identity and the permutation $\kappa$ mapping $v_1$ to $v_2$ and $v_2$ to $v_1$) we will denote for every $\mathfrak{t}\in\mathcal{E}$ by $\mathfrak{t}^-$ its flipped version $\kappa\mathfrak{t}$. Note that this leaves constants untouched.

Let now
\begin{equation}
\Psi = \Psi_\mathrm{hom}\ \wedge \hspace{-2ex}\bigvee_{(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-2ex} \Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)},
\end{equation}
where $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ is obtained as the conjunction over $\Psi_{\mathrm{gen}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$ and the following sentences (letting $\mathcal{E}_{\text{+},1}$ and $\mathcal{E}_{\text{+},2}$ denote the $1$- and $2$-types in $\mathcal{E}_{\text{+}}$, respectively, and letting $\mathcal{E}_{!,1}$ denote the $1$-types in $\mathcal{E}_{!}$):
	%
	\noindent
	\begin{align}

		\!\!\!\!\!\forall xy. \sig{Tp}_\mathfrak{t}(x) \wedge \sig{Tp}_\mathfrak{t}(y) & \Rightarrow x=y & & \hspace{-1ex}\mbox{for }\mathfrak{t} \in \mathcal{E}_{\text{!},1} \label{proj0}\\

		\!\!\!\!\forall xy. \sig{Tp}_{\mathfrak{t}'} (x) \wedge \sig{Tp}_{\mathfrak{t}''} (y) & \Rightarrow \hspace{-8.5ex} \bigvee_{{\scriptstyle \mathfrak{t} \in \mathcal{E}_{\text{+},2}} \atop {\scriptstyle \quad\quad\quad\  \mathfrak{t}|_{v_1} = \mathfrak{t}',\,  \mathfrak{t}|_{v_2} = \mathfrak{t}''}} \hspace{-8.5ex} \sig{Tp}_{\mathfrak{t}} (x,y) & &\hspace{-1ex}\mbox{for } \mathfrak{t}'\!,\!\mathfrak{t}''\! \in\hspace{-1pt} \mathcal{E}_{\text{+},1}\hspace{-2ex} \label{proj5}\\
		\forall x \exists y. \Big(\hspace{-2.2ex}\bigvee_{\scriptstyle\quad\mathfrak{t} \in \mathcal{E}_{\text{+},1}} \hspace{-2ex} \sig{Tp}_\mathfrak{t} (x) & \Rightarrow \hspace{-7.5ex} \bigvee_{{\scriptstyle\quad\mathfrak{t}' \in \mathcal{E}_{\text{+},2}}\atop{\scriptstyle\quad\quad\quad \mathfrak{t}' \models \psi_i(v_1,v_2)}} \hspace{-7.2ex} \sig{Tp}_{\mathfrak{t}'} (x,y)\Big) & &\hspace{-1ex}\hspace{0.5ex} \psi_i \mbox{ from } \Phi \label{proj6}
	\end{align}

	Clearly, $\Psi$ is a \mbox{$\FO_{=}^\mathbbm{2}$}{} $\tau{\uplus}\sigma$-sentence.
	Moreover, we obtain $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$:

	``$\subseteq$'': Let $\mathfrak{A} \in \getmodels{\Phi}$ and let $h\colon\mathfrak{A} \to \mathfrak{B}$. Obtain $\mathfrak{A}'=\mathfrak{A}\cdot\mathcal{E}$ and $\mathfrak{B}'=\mathfrak{B}\cdot h(\mathfrak{A}\cdot\mathcal{E}|_\sigma)$ as described before. Pick $(\mathcal{E}_\text{+},\mathcal{E}_!) = \mathcal{E}(\mathfrak{A})$. Then
	$\mathfrak{A}' \models \Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ because of $\Phi$-modelhood and $\mathfrak{A}' \models \Psi_\mathrm{hom}$ by construction.
	Furthermore, by applying \Cref{lem:PsiGen} $\mathfrak{A}'$ as well as $\mathfrak{B}'$ satisfy $\Psi_{\mathrm{gen}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$.
	Next, Formulae \ref{proj0} holds by definition of $\mathfrak{A}'$ and the fact that $\mathcal{E}_{!, 1}$ contains the $1$-types realized exactly once. Hence every type predicate associated to such a $1$-type can only be satisfied by exactly one element from $\mathfrak{A}'$. By definition of $\mathfrak{B}'$ Formulae \ref{proj0} also hold there: Since every type predicate from $\sigma$ is interpreted in $\mathfrak{B}'$ as the homomorphic image of the interpretation of the very same type predicate in $\mathfrak{A}'$, and those are singleton sets, we obtain the claimed satisfaction.
	Now let $b_{1} , b_{2}$ be elements from $\mathfrak{B}'$ such that there are types $\mathfrak{t}', \mathfrak{t}'' \in\mathcal{E}_{+,1}$ with $b_{1} \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}'}$ and $b_{1} \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}'}$. By definition there are $a_{1}$ and $a_{2}$ in $\mathfrak{A}'$ with $a_1 \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{A}'}$ and $a_1 \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{A}'}$ such that $h(a_1) = b_1$ and $h(a_2) = b_2$.  Without loss of generality we now assume $\bold{v}_{\mathfrak{t}'} = \{v_1 \}$ and $\bold{v}_{\mathfrak{t}''} = \{ v_2 \}$. If this were not the case, using the closure under variable permutation we could enforce this condition. Note that it will be only important for the next step in a technical way, to extract a $2$-type that is rigid. Because now we obtain by definition of $\mathfrak{A}'$ (and the uniqueness of the realized types of elements/tuples) that $a_1$ realizes $\mathfrak{t}'$, $a_2$ realizes $\mathfrak{t}''$ and $(a_{1}, a_{2})$ realizes some type $\mathfrak{t}$ that naturally satisfies $\mathfrak{t}|_{v_1} = \mathfrak{t}'$ and $\mathfrak{t}|_{v_2} = \mathfrak{t}''$. Hence $(a_1, a_2) \in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}'}$ and applying $h$ we obtain $(b_1, b_2) = h(a_1, a_2) \in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$.
	This argument yields \ref{proj5}.
	Finally we discuss that $\mathfrak{B}'$ satisfies \ref{proj6}. Suppose $b$ be in $\mathfrak{B}'$ and let $\mathfrak{t}\in\mathcal{E}_{+, 1}$ be some type such that $b \in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}'}$. Hence there is $a$ in $\mathfrak{A}'$ such that $h(a)=b_1$ and $a \in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}'}$. As $\mathfrak{A}'$ as an expansion has the same domain as $\mathfrak{A}$ and $\mathfrak{A}\vDash \Phi$ we obtain an element $a_{i}$ such that $(a, a_i)$ satisfies $\psi_{i}(x,y)$ for all $\forall\exists$-conjuncts in $\Phi$. The type $\mathfrak{t}(v_1,v_2)$ realized by $(a,a_i)$ is in $\mathcal{E}_{+, 2}$ and we have $\mathfrak{t}'\vDash\psi_{i}(v_1, v_2)$. Hence $(a,a_i) \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{A}'}$. Applying $h$ we first obtain a $b_i = h(a_i)$ such that also $(b,b_i) \in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}'}$ holds. By this argument \ref{proj6} holds in $\mathfrak{B}'$.

	Consequently $\mathfrak{B}'$ must be a model of $\Psi$, hence $\mathfrak{B} \in \getmodels{\Psi}|_\tau$.

	``$\supseteq$'': 	Let $\mathfrak{B}'$ be a model of $\Psi$ and let $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ be the disjunct made true in the rear part of $\Psi$.
		The crucial observation about the structure $\mathfrak{B}' $ is that in general, elements $a$ or a tuple $(a,b)$ from $B'$ may satisfy more than one type predicate. Note that if this would not be the case, we'd easily find a weak substructure $ \mathfrak{A}'$ of $\mathfrak{B}$ which is projectively in $ \getmodels{\Phi}$. This holds since the type predicates inherit the satisfiability of $\Phi$. In order to overcome this difficulty of ``ambiguity of types'' we
	construct a structure $\mathfrak{A} \in \getmodels{\Phi}$ and a homomorphism $\mathfrak{A} \to \mathfrak{B}'|_\tau$ as follows: first construct the $\sigma$-structure $\mathfrak{A}'$ by letting
	\begin{equation}
	A' = \{ (b,\mathfrak{t}) \mid b\in B, b\in \sig{Tp}_\mathfrak{t}^\mathfrak{B}, \mathfrak{t}\in \mathcal{E}_{\text{+},1}\}.\label{projdef1}
    \end{equation}
	For the unary type predicates, let
	$\sig{Tp}_\mathfrak{t}^{\mathfrak{A}'} = A' \cap (B \times \{\mathfrak{t}\})$
	and for binary type predicates, let
	%
	\begin{align*}
		& \sig{Tp}_{\mathfrak{t}}^\mathfrak{A'} = \Big\{ \big((b,\mathfrak{t}'),\!(b'\!,\mathfrak{t}'')\big)\ \Big|\
		\mathfrak{t}|_{v_1}{=}\mathfrak{t}', \mathfrak{t}|_{v_2}{=}\mathfrak{t}'', (b,b') \in \sig{Tp}_{\mathfrak{t}}^\mathfrak{B} \Big\} \label{eq75}
	\end{align*}
	In a next step, we define $\mathfrak{A}$ from $\mathfrak{A}'$ as follows: let $k$ be the maximum number of distinct $\mathfrak{t}'' \in \mathcal{E}_{\text{+},2}$ with $(a,a') \in \sig{Tp}_{\mathfrak{t}''}^\mathfrak{A'}$ across all pairs $(a,a')$ from $A'$. Define a function
	$\mathfrak{t}^{?\!} \colon A' \times A' \times \{0,\ldots,k-1\} \to \mathcal{E}_{\text{+},2}$ such that for every $a,a' \in A'$, the set $\{ \mathfrak{t}^{?\!}(a,a',i) \mid 0\leq i < k \}$ contains all and only the  distinct $\mathfrak{t}''$ with $(a,a') \in \sig{Tp}_{\mathfrak{t}''}^\mathfrak{A'}$ (with possible repetitions) and $\mathfrak{t}^{?\!}(a,a',i) = \mathfrak{t}^{?\!}(a',a,i)^-$. Note that the last identity is possible by (\ref{eq: gen 3plus}).
	Now, let
	\begin{equation}
	A_! = \{(b,\mathfrak{t}) \in A' \mid \mathfrak{t} \in \mathcal{E}_{\text{!},1} \}
	\end{equation}

	and let
	\begin{equation}
	A = A_! \times \{0\} \cup (A' \setminus A_!) \times \{0,\ldots, k-1\}.
	\end{equation}

Note that $A_!$ contains for every $\mathfrak{t} \in \mathcal{E}_{\text{!},1}$ exactly one element of the form $(b,\mathfrak{t}) $ since $\mathfrak{B}$ satisfies (\ref{proj0}).
	We assign relations to the type predicates as follows (for all $\mathfrak{t} \in \mathcal{E}_{\text{+},1}$ and $\mathfrak{t}'' \in \mathcal{E}_{\text{+},2}$):
\begin{eqnarray}
	\sig{Tp}_\mathfrak{t}^\mathfrak{A} & \hspace{-2ex} = \hspace{-2ex} & \{ (a,i) \mid a \in \sig{Tp}_\mathfrak{t}^\mathfrak{A'} \} \text{ for } \mathfrak{t} \in \mathcal{E}_{\text{+},1} \label{projdef2}\\
    \sig{Tp}_{\mathfrak{t}''}^\mathfrak{A} & \hspace{-2ex} = \hspace{-2ex} & \{ ((a,i),(a',j)) \mid \mathfrak{t}^{?\!}(a,a',i\,{+}\,j\!\! \mod k) = \mathfrak{t}''\}. \quad\quad
\end{eqnarray}

It follows from our construction that the structure $\mathfrak{A}$ satisfies formulae (\ref{eq: gen 1}), (\ref{eq: gen 2}), and (\ref{proj0}). To see that (\ref{eq: gen 3}) is satisfied consider $((a,i),(a',j))\in A^2$ such that  $((a,i),(a',j)) \in \sig{Tp}_\mathfrak{t}^\mathfrak{A}$ holds. By the definition of $\sig{Tp}_\mathfrak{t}^\mathfrak{A}$ we get $\mathfrak{t}^{?\!}(a,a',i\,{+}\,j\!\! \mod k) = \mathfrak{t}$.
	Let

	 $(a,a')=((b,\mathfrak{t}^a),(b',\mathfrak{t}^{a'})   )$.
	Since $(a,a')\in \sig{Tp}_{\mathfrak{t}}^{{\mathfrak{A}'}}$ holds  by definition of $\mathfrak{t}^{?\!}$ we get by the definition of  $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}'}$ that $\mathfrak{t}|_{v_1}=\mathfrak{t}^a$ holds.

	By the definition of  $\sig{Tp}_{\mathfrak{t}}^{\mathfrak{A}'}$ and since $\mathfrak{B}$ satisfies (\ref{eq: gen 3}) we have that $(b,\mathfrak{t}^a)$ is in $\sig{Tp}_{\mathfrak{t}^a}^{\mathfrak{A}'}$.
	This implies that $((b,\mathfrak{t}^a),i)$ is in $\sig{Tp}_{\mathfrak{t}^a}^{\mathfrak{A}}$. Since  $\mathfrak{t}|_{v_1}=\mathfrak{t}^a$ holds and the same argument works for $v_{2}$ and $\mathfrak{t}^{a'}$, we showed that (\ref{eq: gen 3}) is satisfied in $\mathfrak{A}$.

Formulae (\ref{eq: gen 3plus})  clearly hold in $\mathfrak{A}$. In consequence, $\Psi_{(\mathcal{E}_{+}, \mathcal{E}_{!})}$ as well as (\ref{proj0}) holds in $\mathfrak{A}$.

	For signature elements from $\tau$, choose $\cdot^\mathfrak{A}$ such that all (pairs of) domain elements realize exactly the types as indicated by the type predicates. This is possible since, by construction, there is exactly one $2$-type-predicate holding for every pair of domain elements.
   Furthermore, every domain element has been assigned exactly two $1$-type-predicates (whose associated types only differ in the used variable name but are otherwise identical by (\ref{eq: gen 3plus})) by the definitions (\ref{projdef1}) and  (\ref{projdef2}).
		The $1$-type-predicates  also fit with all the two-type predicates
	by what we have shown before.

	We now claim that $\mathfrak{A}|_\tau$ is a model of $\Phi$. To see this, consider an arbitrary element $a=((b,\mathfrak{t}),i)\in A$. Since $\mathfrak{B}$ satisfies (\ref{proj6}), there exists a $b'\in B$ such that that the inner implication in (\ref{proj6}) is satisfied (for $x=b$ and $y=b'$).
	By the construction of $\mathfrak{A}$, we know  that $b\in \sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}}$ holds and therefore the premise of the implication is satisfied. This implies the existence of a type $\mathfrak{t}'$ such that $(b,b')\in \sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}}$ and
	$	\mathfrak{t}' \models \psi_i(v_1,v_2)$ hold.
	By the definition of $\mathfrak{t}^{?\!}$, we can find a $j$ such that $\mathfrak{t}^{?\!}( (b,\mathfrak{t}),(b',\mathfrak{t}'|_{v_2}),i\,{+}\,j\!\! \mod k) = \mathfrak{t}'$. Therefore, we get for $a'=((b',\mathfrak{t}'|_{v_2}),j) $ that $(a,a') \in \sig{Tp}_{\mathfrak{t}'}^{\mathfrak{A}} $ holds. By the definition of the $\tau$-relations from $\mathfrak{A}$, it follows that $\psi_{j}(a,a')$ holds in $\mathfrak{A}$.
		The proof for the conjunct $\forall xy. \varphi(x,y) $ is by an analogous (but easier, since ``type-internal'') use of formula (\ref{proj5}).
		Consider arbitrary elements $a=((b, \mathfrak{t}),i)\in A$ and $a'=((b', \mathfrak{t}'), i')\in A$. By construction of $\mathfrak{A}$ we know that $b\in\sig{Tp}_{\mathfrak{t}}^{\mathfrak{B}}$ and $b'\in\sig{Tp}_{\mathfrak{t}'}^{\mathfrak{B}}$. By \ref{proj5} there is a at least one $\mathfrak{t}''\in\mathcal{E}_{+, 2}$ with $\mathfrak{t}''|_{v_1}=\mathfrak{t}$ and $\mathfrak{t}''|_{v_2}=\mathfrak{t}'$ such that $(b,b')\in\sig{Tp}_{\mathfrak{t}''}^{\mathfrak{B}}$. Hence by definition of $\mathfrak{t}^{?\!}$ one of those types $\mathfrak{t}''$ satisfies $\mathfrak{t}^{?\!}((b, \mathfrak{t}), (b', \mathfrak{t}'), i\,{+}\,i'\!\! \mod k) = \mathfrak{t}''$. Consequently $(a,a')\in\sig{Tp}_{\mathfrak{t}''}^{\mathfrak{A}}$ by construction. By the definition of the $\tau$-relations from $\mathfrak{A}$ we immediately obtain that $(a,a')$ realizes $\mathfrak{t}''$. Now note that, as $\mathfrak{t}''\in\mathcal{E}_{+,2}$, $\mathfrak{t}''\vDash\varphi(v_1,v_2)$ since $\mathcal{E}_{+}$ collects all eligible types realized by some $\mathfrak{A}^{\ast}\in\getmodels{\Phi}$. Hence $(a,a')$ satisfies $\varphi$ in $\mathfrak{A}$. Thus the conjunct $\forall xy. \varphi(x,y)$ holds for $\mathfrak{A}$.

By our construction, $h\colon \mathfrak{A}|_\tau \to \mathfrak{B}|_\tau$ with $((b,\mathfrak{t}),i) \mapsto b$ is a homomorphism, which proves the statement.
\end{proof}

\input{characterizability}

\begin{lemma}[restate=GNFOredGFO, label=GNFOredGFO, name=]
For every \mathbb{GNFO}_{=}{} $\tau$-sentence $\Phi$, there exists some
\mbox{$\mathbb{GFO}_{=}$}{}
sentence $\Phi^*$ with
$\homcl{\getmodels{\Phi}} = \homcl{\getmodels{\Phi^*}|_\tau}$.
\end{lemma}

\begin{proof}By \cite[Proposition 3.2]{GuardedNegation}, there exist a \mbox{$\mathbb{GFO}_{=}$}{} sentence $\Phi'$ and an \mbox{$\Ex^*\FO^+_{=}$}{} sentence (more precisely: a union of conjunctive queries) $\Phi''$ such that $\getmodels{\Phi} = \getmodels{\Phi' \wedge \neg \Phi''}|_{\tau}$ ($\dag$).

	Then, by \cite[Lemma 2.4]{BaranyGO13} and the corresponding proof, there exists a \mbox{$\mathbb{GFO}_{=}$}{} sentence $\Phi'''$ such that
	(i) $\getmodels{\Phi' \wedge \neg \Phi''} \subseteq \getmodels{\Phi' \wedge \neg \Phi'''}$ and (ii) for every model $\mathfrak{A}$ of $\Phi' \wedge \neg \Phi'''$ there is
	a model  $\mathfrak{B}$ of $\Phi' \wedge \neg \Phi''$ such that a homomorphism $\mathfrak{B} \to \mathfrak{A}$ exists.
	Therefore, $\homcl{\getmodels{\Phi' \wedge \neg \Phi''}} = \homcl{\getmodels{\Phi' \wedge \neg \Phi'''}}$ ($\ddag$).

So we obtain:
\begin{eqnarray}
	\homcl{\getmodels{\Phi}} & \stackrel{\dag}{=} & \homcl{\getmodels{\Phi' \wedge \neg \Phi''}|_{\tau}} \\
	& \stackrel{*}{=} & \homcl{\getmodels{\Phi' \wedge \neg \Phi''}}|_{\tau} \\
	& \stackrel{\ddag}{=} & \homcl{\getmodels{\Phi' \wedge \neg \Phi'''}}|_{\tau} \\
	& \stackrel{*}{=} & \homcl{\getmodels{\Phi' \wedge \neg \Phi'''}|_{\tau}}.
\end{eqnarray}
The equivalent transformation used in the steps denoted by $\stackrel{*}{=}$ has been justified in the proof of \Cref{lem:normalformOK}.
Note that $\Phi' \wedge \neg \Phi''' \in \mbox{$\mathbb{GFO}_{=}$}$ and let $\Phi^* = \Phi' \wedge \neg \Phi'''$.
\end{proof}

\begin{proposition}\label{prop:charGNFO}
For every \mathbb{GNFO}_{=}{} $\tau$-sentence $\Phi$,
there exists
a \mbox{$\mathbb{GFO}_{=}$}{}
sen\-tence $\Psi$
such that $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$.
\end{proposition}

\begin{proof}
Given $\Phi$, we apply \Cref{GNFOredGFO} to obtain a \mbox{$\mathbb{GFO}_{=}$}{} $\tau'$-sentence $\Phi^*$ for some $\tau' \supseteq \tau$ satisfying $\homcl{\getmodels{\Phi}} = \homcl{\getmodels{\Phi^*}|_\tau}$.
Applying \Cref{prop:charGFO} to $\Phi^*$, we obtain a \mbox{$\mathbb{GFO}_{=}$}{} $\tau''$-sentence $\Psi$ for some $\tau'' \supseteq \tau'$ satisfying $\homcl{\getmodels{\Phi^*}} = \getmodels{\Psi}|_{\tau'}$. Yet, since $\tau \subseteq \tau'$, we also obtain $$\getmodels{\Psi}|_\tau = \getmodels{\Psi}|_{\tau'}|_\tau = \homcl{\getmodels{\Phi^*}}|_\tau \stackrel{*}{=} \homcl{\getmodels{\Phi^*}|_\tau} = \homcl{\getmodels{\Phi}}$$ (the equality denoted by $\stackrel{*}{=}$ has been shown in the proof of \Cref{lem:normalformOK}), therefore $\Psi$ serves the desired purpose.
\end{proof}

\begin{proposition}[restate=TGFinESO, name=]\label{prop:charTGF}
For every \mbox{$\mathbb{TGF}$}{} $\tau$-sentence $\Phi$,
there exists
a \mbox{$\mathbb{TGF}$}{}
sen\-tence $\Psi$
such that $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$.
\end{proposition}

\begin{proof}
	Let $\Phi$ be a \mbox{$\mathbb{TGF}$}{} $\tau$-sentence which we assume to be in normal form (see \Cref{lem:TGFNF}), i.e. with $\sig{Univ}\in\tau$
	\begin{equation}
		\Phi = \Phi_{\sig{Univ}}\land \Phi_{\forall} \land \Phi_{\forall\exists}
	\end{equation}
	where
	\begin{eqnarray}
		\Phi_{\sig{Univ}} & = & \forall xy. \sig{Univ}(x,y),	\label{eq: prop52 Univ}\\[2ex]
		\Phi_{\forall} & = & \bigwedge_{i}\forall\bold{x}. (\alpha_{i}(\bold{x}) \Rightarrow \vartheta_{i}[\bold{x}]), \text{ and} \label{eq: prop52 A}\\
		\Phi_{\forall\exists} & = & \bigwedge_{j}\forall\bold{z}. (\beta_{j}(\bold{z}) \Rightarrow \exists\bold{y}.\gamma_{j}(\bold{y}\bold{z})), \label{eq: prop52 AE}
	\end{eqnarray}
	with $\alpha_{i}$, $\beta_{j}$ guard atoms, $\gamma_{j}$ just atoms, and $\vartheta_{i}$ being a disjunction of literals.
	We define the \emph{width} of $\Phi$ (denoted by $\mathrm{width}(\Phi)$) to be the maximal arity of a relation symbol appearing in $\Phi$. We denote by $C$ the set of all constant symbols from $\tau$.

	Let the set $\mathcal{E}$ of eligible types consist of all rigid guarded types of order $\le\mathrm{width}(\Phi)$.

	Let $\sigma$ contain for each $\mathfrak{t} \in \mathcal{E}$ a fresh relational symbols $\sig{Tp}_{\mathfrak{t}}$. Then we define the $\tau \uplus\sigma$-sentence
	\begin{equation}
		\Psi = \Psi_{\mathrm{hom}} \land\bigvee_{(\mathcal{E}_{+}, \mathcal{E}_{!}) \in\getsummary{\Phi}} \Psi_{(\mathcal{E}_{+}, \mathcal{E}_{!})} ,
	\end{equation}
	where $\Psi_{(\mathcal{E}_{+}, \mathcal{E}_{!})}$ is the sentence:
	\begin{equation}
		\Psi_{(\mathcal{E}_{+}, \mathcal{E}_{!})} = \Psi_{\mathrm{gen}, (\mathcal{E}_{+}, \mathcal{E}_{!})}\land \Psi_{\mathrm{guard}, (\mathcal{E}_{+}, \mathcal{E}_{!})}\land \Psi_{\text{\mbox{$\mathbb{TGF}$}{}}, (\mathcal{E}_{+}, \mathcal{E}_{!})}.
	\end{equation}
		We now show $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$ by proving the two inclusions separately:

	``$\subseteq$'': Let $\mathfrak{A} \in \getmodels{\Phi}$ and let $h\colon\mathfrak{A} \to \mathfrak{B}$. Take $\mathcal{E}$ to be the set of all eligible types for $\Phi$ and $\sigma$ the set of fresh relation symbols $\sig{Tp}_{\mathfrak{t}}$ associated to each $\mathfrak{t} \in \mathcal{E}$ with the appropriate arity. Then the $\mathcal{E}$-adornment of $\mathfrak{A}$, $\mathfrak{A}\cdot\mathcal{E}$, is a $\tau\uplus\sigma$-structure which we will denote by $\mathfrak{A}^{\ast}$. Furthermore, let $\mathfrak{B}\cdot h(\mathfrak{A}^{\ast} |_{\sigma})$ be the $\tau \uplus\sigma$-structure described before, which we denote by $\mathfrak{B}^{\ast}$. Obviously $\mathfrak{B}^{\ast}|_{\tau} = \mathfrak{B}$ holds.

	By \Cref{lem:PsiGen} $\mathfrak{B}^{\ast}$ satisfies $\Psi_{\mathrm{gen}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$. Additionally, after applying \Cref{lem:PsiGuardTGF} $\mathfrak{B}^{\ast}$ satisfies $\Psi_{\mathrm{guard}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$, $\Psi_{\mathrm{hom}}$, and $\Psi_{\text{\mbox{$\mathbb{TGF}$}{}}, (\mathcal{E}_{+}, \mathcal{E}_{!})}$. Consequently $\mathfrak{B}^{\ast}\vDash \Psi$.

	``$\supseteq$'': Let $\mathfrak{B}$ be a model of $\Psi$. Application of \Cref{lem:ConstrA} yields a $\tau\uplus\sigma$ structure $\mathfrak{A}$ satisfying $\Phi$ and a homomorphism $h\colon\mathfrak{A}\to\mathfrak{B}$. Restricting both $\mathfrak{A}$ and $\mathfrak{B}$ to $\tau$ yields the claim.
	%
	%
	%
	%
	%
	%
	%
	%
	%
	%
\end{proof}

We can ``piggyback'' on this result to obtain the comparable statement for $\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$.

\begin{proposition}[restate=EAAEinESO, name=]\label{prop:charEAAE}
For every \mbox{$\Ex^*\Al\Al\Ex^*\FO$}{} $\tau$-sentence $\Phi$,
there exists
a \mbox{$\mathbb{TGF}$}{}
sen\-tence $\Psi$
such that $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$.
\end{proposition}
\begin{proof}
	$\Phi$ can be projectively characterized by a \mbox{$\mathbb{TGF}$}{} sentence $\Phi'$ obtained as follows: skolemize the outer existential quantifiers into extra constants and add an atom using a fresh predicate of adequate arity as a guard following every inner existential quantifier. Clearly, $\Phi'$ is in \mbox{$\mathbb{TGF}$}{} and it projectively characterizes $\Phi$, so the former can be seen as the ``$\mbox{$\mathbb{TGF}$}$ normal form'' of the latter.
	Let now $\Psi$ be obtained from $\Phi'$ following \Cref{prop:charTGF}. We then obtain $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_{\tau}$ thanks to \Cref{lem:normalformOK}.
\end{proof}

\phithreesat*

\begin{lemma}\label{lem:NPhardnesFO2}
	\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item $\Phi_\mathrm{3SAT}$ is contained in constant-free, equality-free $\FO^\mathbbm{2}$ (and therefore in $\mbox{$\FO_{=}^\mathbbm{2}$}$ and \mbox{$\mathbb{TGF}$}).
\item There exists a sentence $\Psi$  in constant-free, equality-free $\mbox{$\bal$}\Al\mbox{$\bex$}\Ex\mathbb{FO}$ (and therefore in
$\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$) such that $ \homcl{\getffinmodels{\Psi}}|_\tau\subseteq \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$.
		\item The size of $\mathfrak{A}_\mathcal{S}$ is polynomial in the size of $\mathcal{S}$.
		\item $\bigwedge_{\{\ell,\ell',\ell''\}\in \mathcal{S}} \ell \vee \ell' \vee \ell''$ is satisfiable exactly if $\mathfrak{A}_\mathcal{S} \in \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$.
		\item Checking membership in $\homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$ is \textsc{NP}-hard in the size of the structure.
		\item Checking membership in $\homcl{\getffinmodels{\Psi}}$ is \textsc{NP}-hard in the size of the structure.

	\end{enumerate}
\end{lemma}

\begin{proof}
	Item 1 follows immediately from the definition of $\Phi_\mathrm{3SAT}$.

	For Item 2: We let $\Psi = \forall x y \exists z v.\psi$ where $\psi$ is the conjunction over
\begin{eqnarray}
	& & \sig{First}(z) \\
	& & \sig{Eq}(x,x) \\
		\sig{First}(x) & {\!\!\!\!\Rightarrow\!\!\!\!} &  \sig{CLst}(x) \\
	\sig{CLst}(x) \wedge \sig{Eq}(x,y) & {\!\!\!\!\Rightarrow\!\!\!\!} &  \sig{Lit}(x,v) \wedge \sig{Sel}(v)\\
	\sig{CLst}(x) \wedge \sig{Lit}(x,y) & {\!\!\!\!\Rightarrow\!\!\!\!} &  \sig{Next}(x,v) \ \ \ \ \ \nonumber\\[-0.6ex]
	&  &  \ \wedge\, \big(\sig{CLst}(v) \vee \sig{Nil}(v)\big)\ \ \ \ \ \\
	\sig{Sel}(x) \wedge \sig{Sel}(y) & {\!\!\!\!\Rightarrow\!\!\!\!} & \sig{Cmp}(x,y).
\end{eqnarray}

The containment $ \getffinmodels{\Psi}|_\tau \subseteq \getffinmodels{\Phi_\mathrm{3SAT}}$ follows immediately and therefore also $ \homcl{\getffinmodels{\Psi}}|_\tau\subseteq \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$ holds.

	Item 3 follows directly from the definition of  $\mathfrak{A}_\mathcal{S}$.

	For Item 4:  Let $V=\{p_1,\ldots,p_m\}$ be the variable set of the propositional formula $\varphi =\bigwedge_{\{\ell,\ell',\ell''\}\in \mathcal{S}} \ell \vee \ell' \vee \ell''$.

	Assume that there exists an assignment $\alpha\colon V\rightarrow \{\top,\bot\} $ that witnesses the satisfiability of $\varphi$.
	Let $\tau$ be the signature of   $\mathfrak{A}_\mathcal{S}$ and let $\mathfrak{B}'$ be the $\tau {\setminus} \{\sig{Sel}\}$-reduct of   $\mathfrak{A}_\mathcal{S}$.
	The $\tau$-structure $\mathfrak{B}$ is the expansion of   $\mathfrak{B}'$ where the relation $\sig{Sel}^\mathfrak{B}$ is defined as follows:

\begin{enumerate}
	\item $\sig{Sel}^\mathfrak{B}\subset \{b_i,b_i'\mid 1\leq i\leq m\}$,
	\item 	$b_i \in \sig{Sel}^\mathfrak{B}$  if and only $\alpha(p_i)=\top$,
		\item 	$b_i' \in \sig{Sel}^\mathfrak{B}$  if and only $\alpha(p_i)=\bot$.
\end{enumerate}
One can easily check that $\mathfrak{B}$ satisfies $\Phi_\mathrm{3SAT}$. Furthermore, the identity map from  $\mathfrak{B}$  to $\mathfrak{A}_\mathcal{S}$  is a homomorphism which proves that $\mathfrak{A}_\mathcal{S} \in \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$ holds.

For the opposite direction suppose that there exists a structure $\mathfrak{B}$ from $\getffinmodels{\Phi_\mathrm{3SAT}}$ that has a homomorphism $h$ to  $\mathfrak{A}_\mathcal{S} $. Note that Equation \ref{Def14: 1} of \Cref{def: 3SAT} ensures that the structure $\mathfrak{B}$ contains an element $x_f$ such that $x_f\in \sig{First}^\mathfrak{B}$ holds. Since $h$ is a homomorphism $h(x_f)=a_1$ holds. For every element $x$ in $\sig{CLst}^\mathfrak{B}$ exists by Equation \ref{Def14: 3} an element $y$ such that $(x,y)\in \sig{Next}^\mathfrak{B}$ holds. In the structure $\mathfrak{A}_\mathcal{S}$ the same holds but with unique elements $y$. This implies that there exists a set $W\subseteq \sig{CLst}^\mathfrak{B}$ with $x_f\in W$ such that $h$ restricted to $W$ is a bijection from $W$ to $\{a_i \mid 1\leq i\leq n+1\}$. We denote this restricted map by $h'$.
Let $f\colon W\rightarrow \sig{Sel}^\mathfrak{B}$ be a map such that $(x,f(x))\in \sig{Lit}^\mathfrak{B}$  holds for all $x\in W$. Such a map exists by Equation \ref{Def14: 4}.
Observe that $h(f(W)) \subset \{b_i,b_i' \mid 1\leq i\leq m\}$ holds. Moreover since we have $f(W)\subset \sig{Sel}^\mathfrak{B}$ by defintion, all pairs of distinct elements in $f(W)$ are in the relation $\sig{Cmp}^\mathfrak{B}$ by Equation \ref{Def14: 5}. This implies that for all $i\in \{1,\ldots,m\}$ at most one of $b_i$ and $b_i'$ is in  $h(f(W))$. We define a variable assignment $\alpha\colon V\rightarrow \{\top,\bot\} $ as follows:

\begin{enumerate}
	\item $\alpha(p_i) =\top$ if $b_i\in h(f(W))$,
		\item $\alpha(p_i) =\bot$ if $b_i'\in h(f(W))$,
		\item $\alpha(p_i) =\top$ if $b_i$ and $b_i'$ are not in $ h(f(W))$.

\end{enumerate}
This is a well defined map by what we saw before. Furthermore, to see that the clause $C_j$ is satisfied, consider the element $y =h'^{-1}(a_j) \in Q$. By the definition of $f$ we have that $(y,f(y))\in \sig{Lit}^\mathfrak{B} $  and therefore $(h(y),h(f(y)))\in \sig{Lit}^{\mathfrak{A}_\mathcal{S}} $  holds. Assume without loss of generality that $h(f(y)) =b_l$ for some $l\in \{1,\ldots,m\}$. Then we have $(a_j,b_l)\in \sig{Lit}^{\mathfrak{A}_\mathcal{S}} $ which means by the definition of $\mathfrak{A}_\mathcal{S}$ that $p_l$ is a literal of $C_j$. By the definition of $\alpha$ we have $\alpha(p_l)=\top$ which proves that $C_j$ is satisfied.

For Item 5: The 3SAT problem is a well known \textsc{NP}-hard problem \cite{Karp1972}. We have a reduction from the 3SAT problem to the membership problem for $\homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$ by mapping a 3SAT instance $\mathcal{S}$ to the structure $\mathfrak{A}_\mathcal{S} $.
This is indeed a  reduction by Item 4 and it is polynomial time computable by Item 3.

For Item 6: We reduce the 3SAT problem to the membership problem of $\homcl{\getffinmodels{\Psi}}$. We map an instance $\mathcal{S}$ to the structure $\mathfrak{A}^*_\mathcal{S}$ that is the expansion of $\mathfrak{A}_\mathcal{S}$ by the relation $\sig{Eq}^{\mathfrak{A}^*_\mathcal{S}}=\{(x,x) \mid x\in A_\mathcal{S}\}$.

Assume that $\mathcal{S}$ is satisfiable. Let $\mathfrak{B}$ be the structure from the first direction of 5). It is easy to see that its expansion $\mathfrak{B}^*$  satisfies $\Psi$ and therefore
$\mathfrak{A}^*_\mathcal{S}$ is in  $\homcl{\getffinmodels{\Psi}}$.

For the other direction assume that $\mathfrak{A}^*_\mathcal{S}\in \homcl{\getffinmodels{\Psi}}$ holds. By 2) we get that  then also $\mathfrak{A}_\mathcal{S} \in \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$ holds which implies by 4) that $\mathcal{S}$ is satisfiable.\end{proof}

\NPhardFOprop*

\begin{proof} The proposition follows from Item~1, Item~2, Item~5 and Item~6 of \Cref{lem:NPhardnesFO2}.
\end{proof}

\GNFOinLFP*

\begin{proof}
Given a $\mathbb{GNFO}_{=}$ $\tau$-sentence $\Phi$, bring it in $\mbox{$\mathbb{GFO}_{=}$}$ ``homclosure normal form'' according to \Cref{GNFOredGFO},
		 obtaining a $\mbox{$\mathbb{GFO}_{=}$}$ $\tau'$-sentence $\Phi'$. From $\Phi'$ compute $\Psi$ as in \Cref{prop:charGFO}, adjusting the definition of $\Psi_\mathrm{hom}$ as follows:
\begin{equation}
\bigwedge_{\mathfrak{t} \in \mathcal{E}} \!\forall \bold{v}_\mathfrak{t}.\big( \sig{Tp}_\mathfrak{t}(\bold{v}_\mathfrak{t}) \Rightarrow \smallbigwedge \mathfrak{t}|_\tau^+ \big),
\end{equation}
where
\begin{equation}
\mathfrak{t}|_\tau^+ = \{\alpha \tight{\in} \mathfrak{t} \mid \alpha = \sig{P}(\bold{t}) \text{ with }\sig{P}\in\tau\}
\end{equation}
so, compared to the original $\Psi_\mathrm{hom}$, the new one disregards auxiliary symbols from $\tau'\setminus \tau$. Clearly, we still obtain $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_\tau$ and hence also $\homcl{\getmodels{\Phi}} = \getmodels{\exists \sigma.\Psi}$ where
\newcommand{\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}}{\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}}
\begin{align}
	\exists \sigma.\Psi & = \exists \sigma . \Big(\Psi_\mathrm{hom} \wedge \hspace{-1ex} \bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!)}\Big) \\
	& \equiv \hspace{-1ex} \bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \exists \sigma . \big(\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!)} \wedge \Psi_\mathrm{hom} \big)\\
	& =: \hspace{-1ex} \bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \exists \sigma . \big(\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}\big),
\end{align}
with $\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}$ being the conjunction over
\noindent
\newcommand{\hspace{-1.5ex}}{\hspace{-1.5ex}}
\newcommand{\hspace{-1.5ex}}{\hspace{-1.5ex}}
\begin{eqnarray}
	\exists \bold{v}_\mathfrak{t}. \big(\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t})\big) \hspace{-1.5ex}\less\ & & \hspace{-1.5ex} \hspace{27ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E}_{+}\quad\quad\ \\
	\forall \bold{v}_\mathfrak{t}. \big(\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \bot \big)\hspace{21ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E}\setminus\mathcal{E}_{+}  \\
	\forall \bold{v}_\mathfrak{t}. \big(\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \sig{Tp}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big) \hspace{7ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t},\mathfrak{t}' \in \mathcal{E}_{+}, \mathfrak{t}'=\mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}  \\
	\forall \bold{v}_\mathfrak{t}. \big(\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \sig{Tp}_{\kappa\mathfrak{t}}( \eta^{\kappa\bold{v}_\mathfrak{t}}_\bold{v} (\bold{v}_\mathfrak{t}) )\big) \hspace{1.3ex}\mbox{for } \mathfrak{t} \in \mathcal{E}, \kappa : \bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}} \bold{v} \\
	\forall \bold{v}_\mathfrak{t}. \big(\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \hspace{-7ex} \bigvee_{\quad\quad(\mathfrak{t},\nu) \Subset_j^\bold{z} (\mathfrak{t}',\nu')} \hspace{-6ex} \exists \bold{v}_{\mathfrak{t}'}{\!\setminus}\nu(\bold{z}) .\sig{Tp}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big) \hspace{3ex}\hspace{-1.5ex}\mbox{for } (\mathfrak{t},\nu)\! \in \!B_{j}\\
    \forall \bold{v}_\mathfrak{t}.\big( \sig{Tp}_\mathfrak{t}(\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Rightarrow &\hspace{-1.5ex} \smallbigwedge \mathfrak{t}|_\tau^+ \big) \hspace{22ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E}
\end{eqnarray}
where $j$ ranges over the number of conjuncts in $\Phi_{\forall\exists}$ (cf. the proof of \Cref{prop:charGFO}).

In a next step, we equivalently rewrite  all constituents of $\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}$ as follows (all side conditions remain untouched):
\begin{eqnarray}
	\exists \bold{v}_\mathfrak{t}. \neg\big(\neg\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t})\big) \hspace{-1.5ex}\less\ & &  \\
	\forall \bold{v}_\mathfrak{t}. \big(\neg\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \top\big) \\
	\forall \bold{v}_\mathfrak{t}. \big(\neg\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \neg \sig{Tp}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big) \\
	\forall \bold{v}_\mathfrak{t}. \big(\neg\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \neg\sig{Tp}_{\kappa\mathfrak{t}}( \eta^{\kappa\bold{v}_\mathfrak{t}}_\bold{v} (\bold{v}_\mathfrak{t}) )\big) \\
	\forall \bold{v}_\mathfrak{t}. \big(\neg\sig{Tp}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \hspace{-6ex} \bigwedge_{\quad\quad(\mathfrak{t},\nu) \Subset_j^\bold{z} (\mathfrak{t}',\nu')} \hspace{-6ex} \forall \bold{v}_{\mathfrak{t}'}{\!\setminus}\nu(\bold{z}) .\neg\sig{Tp}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big) \\
	\forall \bold{v}_\mathfrak{t}.\big(\neg\sig{Tp}_\mathfrak{t}(\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \neg\smallbigwedge \mathfrak{t}|_\tau^+ \big)
\end{eqnarray}

We next let for $\overline{\sigma} = \{ \overline{\sig{Tp}}_\mathfrak{t} \mid {\sig{Tp}}_\mathfrak{t} \in \sigma\}$ be a set of ``complement predicates'', with the intention that $\overline{\sig{Tp}}_\mathfrak{t}$ is meant to denote the complement relation of ${\sig{Tp}}_\mathfrak{t}$. With this in mind, we rewrite the above sentences in the straightforward way, obtaining
\newcommand{\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}}{\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}}
$\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}$
as the conjunction over the following $\tau\uplus\overline{\sigma}$-sentences:
\begin{eqnarray}
	\exists \bold{v}_\mathfrak{t}. \neg\big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t})\big) \ \!\hspace{-1.5ex}\less\hspace{-1.5ex}& &  \hspace{-1.5ex} \hspace{27ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E}_{+}\quad\quad\ \\
	\forall \bold{v}_\mathfrak{t}. \big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \top \big)
    \hspace{21ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E}\setminus \mathcal{E}_{+} \label{fp0}\\
	\forall \bold{v}_\mathfrak{t}. \big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \overline{\sig{Tp}}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big)
	    \hspace{7ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t},\mathfrak{t}' \in \mathcal{E}_{+}, \mathfrak{t}'=\mathfrak{t}|_{\bold{v}_{\mathfrak{t}'}}  \label{fp1}\\
\forall \bold{v}_\mathfrak{t}. \big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \overline{\sig{Tp}}_{\kappa\mathfrak{t}}( \eta^{\kappa\bold{v}_\mathfrak{t}}_\bold{v} (\bold{v}_\mathfrak{t}) )\big) \hspace{1.3ex}\mbox{for } \mathfrak{t} \in \mathcal{E}, \kappa : \bold{v}\mathrel{{\hookrightarrow\hspace{-0.8ex}\!\!\!\to}} \bold{v} \\
	\forall \bold{v}_\mathfrak{t}. \big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \hspace{-7.5ex} \bigwedge_{\quad\quad\quad(\mathfrak{t},\nu) \Subset_j^\bold{z} (\mathfrak{t}',\nu')} \hspace{-8ex} \forall \bold{v}_{\mathfrak{t}'}{\!\setminus}\nu(\bold{z}) .\overline{\sig{Tp}}_{\mathfrak{t}'}(\bold{v}_{\mathfrak{t}'})\big)
	    \hspace{2.5ex}\hspace{-1.5ex}\mbox{for } (\mathfrak{t},\nu) \in B_{j} \label{fp2}\\
	\forall \bold{v}_\mathfrak{t}.\big(\overline{\sig{Tp}}_\mathfrak{t}(\bold{v}_\mathfrak{t}) \hspace{-1.5ex}& \Leftarrow &\hspace{-1.5ex} \neg\smallbigwedge \mathfrak{t}|_\tau^+ \big)  \hspace{20ex}\hspace{-1.5ex}\mbox{for } \mathfrak{t} \in \mathcal{E} \label{fp3}
\end{eqnarray}

Note that, for the mentioned reasons,
\begin{equation}
\exists \overline{\sigma} . \big(\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}} \big) \equiv \exists \sigma . \big(\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}} \big).
\end{equation}
Also note that the set of sentences of the forms (\ref{fp1}), (\ref{fp2}), and (\ref{fp3}) can be grouped such that, for every $\overline{\sig{Tp}}_\mathfrak{t} \in \overline{\sigma}$, there exists precisely one sentence of the form
\begin{equation}
\forall \bold{v}_\mathfrak{t}. \big(\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t}) \Leftarrow \xi_{\overline{\sig{Tp}}_\mathfrak{t}}[\bold{v}_\mathfrak{t}] \big),
\end{equation}
where $\xi_{\overline{\sig{Tp}}_\mathfrak{t}}[\bold{v}_\mathfrak{t}]$ is a $\FO_{=}$ sentence with only positive occurrences of $\overline{\sigma}$-atoms (obtain $\xi_{\overline{\sig{Tp}}_\mathfrak{t}}[\bold{v}_\mathfrak{t}]$ as the disjunction of all the bodys of those implications whose head is $\overline{\sig{Tp}}_\mathfrak{t} (\bold{v}_\mathfrak{t})$). Therefore, the obtained set of sentences gives rise to a monotonic operator over $\tau \uplus \overline{\sigma}$-structures simultaneously inflating all $\overline{\sig{Tp}}_\mathfrak{t}$ relations. Hence, $\exists \overline{\sigma} . \big(\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}} \big)$ is equivalent to the simultaneous inductive $\FO_{=}$ least fixed-point expression $\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}^\mathbf{sim\text{-}lfp}$ defined by
\begin{equation}
\bigwedge_{\mathfrak{t} \in \mathcal{E}_\text{+}} \exists \bold{x}.\neg\Big[\textbf{lfp}_{\overline{\sig{Tp}}_\mathfrak{t}} \big\{\, \overline{\sig{Tp}}_{\mathfrak{t}'}(\bold{v}_\mathfrak{t}) \leftarrow \xi_{\overline{\sig{Tp}}_{\mathfrak{t}'}}[\bold{v}_\mathfrak{t}] \,\, \big|\,  \mathfrak{t}' \tight{\in} \mathcal{E}\,\big\}\Big](\bold{x}).
\end{equation}
As simultaneous induction can be expressed using plain least-fixed-point logic \cite{GurevichS86}, there exists some plain $\FO_{=}^\mathbf{lfp}$ sentence $\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}^\mathbf{lfp}$ equivalent to $\hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}^\mathbf{sim\text{-}lfp}$. By defining
\begin{equation}
\Psi^\mathbf{lfp}=\bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \hspace{-0pt}\smash{\overline{\Psi}}\hspace{-7pt}\phantom{\Psi}_{\!(\mathcal{E}_\text{+},\mathcal{E}_!),\mathrm{hom}}^\mathbf{lfp},
\end{equation}
we obtain $\exists \sigma. \Psi \equiv \Psi^\mathbf{lfp}$
and therefore $\getmodels{\Psi^\mathbf{lfp}} = \homcl{\getmodels{\Phi}}$ as desired.
Using the fact that evaluating $\FO_{=}^\mathbf{lfp}$ sentences over structures can be done in polynomial time \cite{Immerman82,Vardi82}, we obtain polytime data complexity of homclosure membership.
\end{proof}

\subsection{Characterizing Finite-Model Homclosures}

\cornercaseone*

\begin{proof}
	$\homcl{\getfinmodels{\Phi_\infty}}$ contains precisely all -- finite or infinite -- $\{\sig{P}\}$-structures that have a directed $\sig{P}$-cycle. Toward a contradiction, let us assume that there were an \mbox{$\mbox{$\bex$}{}\SO$}{} formula $\Psi$ characterizing $\homcl{\getfinmodels{\Phi_\infty}}$. This means the first-order part of $\Psi$, denoted $\Psi'$, projectively characterizes $\homcl{\getfinmodels{\Phi_\infty}}$. Now, for a given number $k$, let $\Gamma^{\not\circlearrowright}_k$ be the $\mathbb{FO}$ sentence disallowing directed $\sig{P}$-cycles of length $k$ defined by
\begin{equation}
\Gamma^{\not\circlearrowright}_k \ \ = \ \ \forall x_1\ldots x_k . \neg \sig{P}(x_k,x_1) \vee \bigvee_{i=1}^{k-1} \neg \sig{P}(x_i,x_{i+1}).
\end{equation}
	Now define the infinite $\mathbb{FO}$ theory $\Xi = \{\Psi'\}\cup\{ \Gamma^{\not\circlearrowright}_k \mid k > 0 \}$.
	Obviously any finite subset of $\Xi$ is satisfiable, while $\Xi$ is not. However this contradicts the compactness theorem of $\FO_{=}$ and therefore the presumed existence of $\Psi$ is refuted.
\end{proof}

\cornercasetwo*

\begin{proof}
	``$\subseteq$'': let $\mathfrak{B} \in \homcl{\getfinmodels{\Phi}}$. Then, by definition, there exists some finite $\mathfrak{A} \in  \getfinmodels{\Phi}$ and a homomorphism $h:\mathfrak{A} \mathrel{{\to}} \mathfrak{B}$. Let $\mathfrak{C}$ be the finite substructure of $\mathfrak{B}$ induced by $h(A)$. Then $h$ also serves as a homomorphism from $\mathfrak{A}$ to $\mathfrak{C}$ and therefore $\mathfrak{C} \in \homclfin{\getfinmodels{\Phi}}$ and, by assumption, $\mathfrak{C} \in \getfinmodels{\Psi}$. We now obtain $\mathfrak{D}$ from $\mathfrak{B}$ by adding $\sig{U}$ to its signature and letting $\sig{U}^\mathfrak{D} = h(A)$. Then, obviously, $\mathfrak{C} = [\mathfrak{D}]_\sig{U}$ and, thanks to  $\mathfrak{C} \in \getfinmodels{\Psi}$ we obtain $\mathfrak{D} \in \getmodels{\Psi^{\mathrm{rel}(\sig{U})}}$ by the remarks from \Cref{sec:tools}.

	By construction, $\sig{U}^\mathfrak{D}$ is finite, therefore $\mathfrak{B} \in \getmodels{\exists^{\scaleobj{0.8}{<}\omega} \sig{U}. \Psi^{\mathrm{rel}(\sig{U})}}$ as desired.

	``$\supseteq$'': let $\mathfrak{B} \in \getmodels{\exists^{\scaleobj{0.8}{<}\omega} \sig{U}. \Psi^{\mathrm{rel}(\sig{U})}}$. Then there must be a structure $\mathfrak{D} \in \getmodels{\Psi^{\mathrm{rel}(\sig{U})}}$ expanding $\mathfrak{B}$ by interpreting an additional signature element $\sig{U}$ such that $\sig{U}^\mathfrak{D}$ is finite. Let $\mathfrak{C} = [\mathfrak{D}]_\sig{U}$, which is finite by construction and an induced substructure of $\mathfrak{B}$. Then by the properties of relativization follows $\mathfrak{C} \in \getmodels{\Psi}$ and due to finiteness of $\mathfrak{C}$ even $\mathfrak{C} \in \getfinmodels{\Psi}$, therefore, by assumption $\mathfrak{C} \in \homclfin{\getfinmodels{\Phi}}$, meaning there exists some $\mathfrak{A} \in \getfinmodels{\Phi}$ and a  homomorphism $h:\mathfrak{A} \to \mathfrak{C}$. But then $id_{C} \circ h$ is a homomorphism from $\mathfrak{A}$ to $\mathfrak{B}$, witnessing $\mathfrak{B} \in \homcl{\getfinmodels{\Phi}}$ as desired.
\end{proof}

\subsection{Proofs for Normal Form Section}

\boundedex*

\begin{proof}
	Assume $\Phi \in \mbox{$\exists\hspace{-4.5pt}\exists$}^n\mbox{$\forall\hspace{-4.5pt}\forall$}^*\FO_{=}$ is over the signature $\tau {\uplus} \sigma$ with predicates $\tau$ and constants $\sigma$. Let $\sigma^\mathrm{sk}$ be a set of $n$ Skolem constants.
	Let $\Phi^\mathrm{sk}$ be the $\mbox{$\Al^*\FOe$}$ $\tau {\uplus} \sigma {\uplus} \sigma^\mathrm{sk}$-sentence obtained from $\Phi$ via skolemization of all the existentially quantified variables into (additional) constants. Clearly then  $\getffinmodels{\Phi} = \getffinmodels{\Phi^\mathrm{sk}}|_\tau$. Since $\Phi^\mathrm{sk}$ is a $\mbox{$\Al^*\FOe$}$ sentence, any model $\mathfrak{A}$ gives rise to a small submodel by taking the substructure $\mathfrak{A}'$ induced by the set $A' \subseteq A$ containing all elements denoted by constants. The identity on $A'$ is a homomorphism from $\mathfrak{A}'$ to $\mathfrak{A}$. Let $\mathcal{A}$ be the set of small submodels thus obtained, for which therefore holds $\homcl{\mathcal{A}}=\homcl{\getmodels{\Phi^\mathrm{sk}}}$ and hence also $\homcl{\mathcal{A}|_\tau}=\homcl{\getmodels{\Phi}} = \getmodels{\Phi}$.
	Now let us obtain $\Psi = \exists \sigma^\mathrm{sk}.\bigvee_{\mathfrak{A}\in \mathcal{A}} \mathrm{cq}'(\mathfrak{A})$ where
\begin{equation}
\mathrm{cq}'(\mathfrak{A}) \ = \ \hspace{-2ex} \bigwedge_{{\sig{c},\sig{c}'\in \sigma \cup \sigma^\mathrm{sk}}\atop{\mathfrak{A}\models \sig{c}{=}\sig{c}'}}\hspace{-2.5ex}
\sig{c} \,{=}\, \sig{c}' \quad \wedge \quad  \hspace{-3ex} \bigwedge_{{\sig{P} \in \tau,\, k=\text{ar}(\sig{P})}\atop{{\mathfrak{A}\models \sig{P}{} (\sig{c}_1,\ldots,\sig{c}_k) }}} \hspace{-3.5ex}
\sig{P}{} (\sig{c}_1,\ldots,\sig{c}_k).
\end{equation}

	Then we get $\getmodels{\Psi} = \homcl{\mathcal{A}|_\tau} = \getmodels{\Phi}$.
	Moreover $\Psi \in \mbox{$\exists\hspace{-4.5pt}\exists$}^n\FO_{=}^+$.
\end{proof}

\classnormalform*

\begin{proof}
	1) and 2) follow immediately since ``being superstructure'' and ``having surjective homomorphisms'' are transitive relations on structures.

	For 3) note that a class is closed under (finite) homomorphism if and only if it is closed under (finite) superstructures and (finite) surjective homomorphisms. By 1) we get that $\supclffin{(\homsucl{\mathcal{C}})}$  is closed under  (finite) superstructures.
	Therefore it remains to show the closure under (finite) surjective homomorphisms.

	Let $\mathfrak{A}\in \supclffin{(\homsucl{\mathcal{C}})}$ and suppose that there exists a (finite) surjective homomorphism $h\colon \mathfrak{A}\rightarrow  \mathfrak{B}$ where $\mathfrak{B}$ is a $\tau$-structure.
	By definition of $\supclffin{(\homsucl{\mathcal{C}})}$ there exists a substructure $\mathfrak{A}_0$ of $\mathfrak{A}$ such that $\mathfrak{A}_0 \in \homsucl{\mathcal{C}}$.
	Let $\mathfrak{B}_0$ be the substructure of $\mathfrak{B}$ that is induced by $h(A_0)$. The structure $\mathfrak{A}_0$ has clearly a (finite) surjective homomorphism to $\mathfrak{B}_0$ and since $\homsucl{\mathcal{C}}$ is by 2) closed under (finite) surjective homomorphisms it follows that $\mathfrak{B}_0\in \homsucl{\mathcal{C}}$.
	Since $\mathfrak{B}_0$ is a substructure of $\mathfrak{B}$ it follows by the definition of  $\supclffin{(\homsucl{\mathcal{C}})}$ that $\mathfrak{B}\in  \supclffin{(\homsucl{\mathcal{C}})}$ holds.\end{proof}

\supstructure*

\begin{proof}
	Let $\mathfrak{A} \in \supclffin{\getffinmodels{\Psi}}$ and let $\mathfrak{B}$ a substructure of $\mathfrak{A}$ such that $\mathfrak{B}\in \getffinmodels{\Psi}$. Such a substructure exists by the definition of  $\supclffin{\getffinmodels{\Psi}}$. We can therefore choose $B\subseteq A$ as a witness for the set variable $\dot{\sig{U}}$ in $\exists \dot{\sig{U}}. \Psi^{\mathrm{rel}(\dot{\sig{U}})}$ and get that $\mathfrak{A} \in \getffinmodels{\Psi^{\mathrm{sup}}}$.
	For the other direction suppose that $\mathfrak{A} \in \getffinmodels{\Psi^{\mathrm{sup}}}$ holds. This means by definition that there exists a subset $B$ of $A$ such that $\Psi^{\mathrm{rel}(B)}$ holds on $\mathfrak{A}$. Therefore the structure $\mathfrak{B}$ that is induced by  $\mathfrak{A}$ on $B$ satisfies $\Psi$ and we get $\mathfrak{A} \in \supclffin{\getffinmodels{\Psi}}$.
\end{proof}

\surjhom*

\begin{proof}
	Let $\mathfrak{A} \in \homsucl{\getffinmodels{\Psi}}$ and let $\mathfrak{A}'$ be a $\tau{\uplus} \tau' {\uplus} \{\sig{U}\}$-expansion of $\mathfrak{A}$ that satisfies $\Theta_\sig{U}^{\tau'} \wedge\bigwedge_ {\sig{P}'\in \tau'} \forall \bold{x}.\big(\sig{P}(\bold{x}) \,{\Rightarrow}\, \sig{P}'(\bold{x})\big)$. Let $\mathfrak{B}_1$ be the substructure of $\mathfrak{A}'$  that is induced by $\sig{U}^{\mathfrak{A}'}$. Let $\mathfrak{B}_2$ be the $\tau'$-reduct of   $\mathfrak{B}_1$. We define $\mathfrak{B}$ as the $\tau$-structure that arises from the signature substitution $\tau' \mapsto \tau$ in the structure $\mathfrak{B}_2$.
	We claim that there exists a surjective homomorphism $ h\colon \mathfrak{A}\mathrel{{\to\hspace{-0.8ex}\!\!\!\to}} \mathfrak{B}$ with the following definition: The map is the identity on $\sig{U}^{\mathfrak{A}'}$. Each element $x\not \in \sig{U}^{\mathfrak{A}'}$ is mapped to some element $y \in \sig{U}^{\mathfrak{A}'}$ such that $\eta^{\tau'}(x,y)$ holds. Such a mapping exists (but is not unique) according to the sentence $\Theta_\sig{U}^{\tau'}$.
	Since $\sig{P}^{\mathfrak{A}'}\subseteq {\sig{P}'}^{\mathfrak{A}'}$ holds and by the formula  $\eta^{\tau'}(x,y)$ it follows that $h$ is a homomorphism. Note that $h$ is surjective since it is the identity on $\sig{U}^{\mathfrak{A}'}$, which is the domain of $\mathfrak{B}$. By our assumption that $\mathfrak{A}$ is from $ \homsucl{\getffinmodels{\Psi}}$ it follows that $\mathfrak{B}\in  \getffinmodels{\Psi}$ holds. This is nothing else than saying that $\mathfrak{A} \models \Psi_{\tau \mapsto \tau'}^{\mathrm{rel}(\sig{U}) }$ holds, which proves the first inclusion.

	For the second inclusion, assume $\mathfrak{A}\in \getffinmodels{\Psi^{\mathrm{shom}}}$ and that there exists a surjective homomorphism $h\colon \mathfrak{A} \mathrel{{\to\hspace{-0.8ex}\!\!\!\to}}\mathfrak{B}$. Define the $\tau{\uplus} \tau' {\uplus} \{\sig{U}\}$-expansion $\mathfrak{A}'$ of $\mathfrak{A}$  as follows. For all $\sig{P}\in \tau$ we define the relation ${\sig{P}'}^{\mathfrak{A}'}$ as the preimage of $\sig{P}^\mathfrak{A}$ under $h$. The set $\sig{U}^{\mathfrak{A}'}$ is defined as some set of representatives of the kernel classes of $h$. It is clear that $\mathfrak{A}'$ satisfies $\Theta_\sig{U}^{\tau'} \wedge\bigwedge_ {\sig{P}'\in \tau'} \forall \bold{x}.\big(\sig{P}(\bold{x}) \,{\Rightarrow}\, \sig{P}'(\bold{x})\big)$ and therefore it satisfies
	$\Psi_{\tau \mapsto \tau'}^{\mathrm{rel}(\sig{U}) }$ as well.
	Let $\mathfrak{A}_1$ be the structure that is induced  by $\mathfrak{A}'$ on $\sig{U}^{\mathfrak{A}'}$.
	By the definition of $\mathfrak{A}'$ the $\tau'$-reduct of $\mathfrak{A}_1$ is isomorphic to $\mathfrak{B}$ after the signature substitution $\tau' \mapsto \tau$. This implies that $\mathfrak{B}$ satisfies $\Psi$. Since the surjective homomorphism $h$ and the structure  $\mathfrak{B}$ were arbitrary, we get $\mathfrak{A} \in \homsucl{\getffinmodels{\Psi}}$. \end{proof}

\section{Characterizing Homomorphism Closures Logically}\label{sec:CharHomCl}

\bigskip

\probbox{
	\textbf{Problem:} $\mathrm{CharHomCl}_{\mathrm{(fin)}}$\\
	\textbf{Input:} $\tau$, sentences $\Phi$ and $\Psi$ over $\tau$.\\
	\textbf{Output:} Yes, if $\getffinmodels{\Psi} = \homclffin{\getffinmodels{\Phi}}$, no otherwise.
}

\bigskip

\begin{proposition}\label{prop:SatToHomCl}
	$\mathrm{HomClosed}_\mathrm{(fin)}$ can be \textsc{LogSpace}-reduced to $\mathrm{CharHomCl}_\mathrm{(fin)}$.
\end{proposition}

\begin{proof} Pick $\Phi = \Psi$. \end{proof}

Thus, $\mathrm{CharHomCl}_\mathrm{(fin)}$ is undecidable whenever $\mathrm{HomClosed}_\mathrm{(fin)}$ is.

\color{thomas} {\bf Thomas' from here.}

Plan for suitable decidable fragments of FOL:

1. Check $\Phi \models \Psi$. Easy if $\Phi \wedge \neg\Psi$ is guaranteed to be in the same (or another) satisfiability-decidable fragment. Complexity: co-class of the corresponding satisfiability problem.

2. Check $\mathrm{HomClosed}$ of $\Psi$. We know how to do this (last section). Again: complexity is co-class of the corresponding satisfiability problem.

3. Check that every model of $\Psi$ has a model of $\Phi$ as ``homomorphic origin''
Trick: given that $\Psi$'s models are homomorphism-closed we know that there is an equivalent positive existential formula with quantifier rank not higher than $\Psi$'s.
This can be converted into a UCQ where every disjunct is a CQ using only linearly many variables in the size of $\Psi$. That means, the set of models of $\Psi$ can be described as the finite union $\bigcup_{\mathfrak{A} \in \mathcal{A}} \homcl{\{\mathfrak{A}\}}$ of the element-wise homomorphism closures of a set of $\tau$-structures with domain size linearly bounded by $\Psi$ (and thus has an exponentially bounded description, thus there are at most doubly exponentially many different such structures). Clearly, then, if one of the models $\Psi$ does not have a homomorphic "origin" among the models of
$\Phi$, there must even be one structure $\mathfrak{A} \in \mathcal{A}$ with $\mathfrak{A} \not\in \homcl{\getmodels{\Phi}}$. Hence, we can proceed as follows:
for every (of the doubly exponentially many) size-bounded $\tau$-structure $\mathfrak{A}$ check if $\mathfrak{A} \in \getmodels{\Psi}$ (``easy'', in EXPTIME since time complexity of FO model checking is $O(n^k)$ where n is the size of the structure and k the size of the formula) and, if that is the case, check $\mathfrak{A} \in \homcl{\getmodels{\Phi}}$ (in the co-class of satisfiability, here we need better bounds assuring that the results hold for any polynomial $|A|$ even if $\mathfrak{A}$ is exponential).
We cannot test all 2Exp possibilities

So we can test $\mathrm{CharHomCl}$ by executing 3 checks not harder than unsatisfiability.

\color{black}

\begin{theorem}
	$\mathrm{CharHomCl}_{\mathrm{(fin)}}$ for
	\begin{enumerate}
		\item
		\mathbb{GNFO}_{=}{} is \textsc{2ExpTime}-complete,
		\item
		\mbox{$\mathbb{TGF}$}{} is \textsc{coN2ExpTime}-complete,
		\item
		\mbox{$\mathbb{C}_{=}^\mathbbm{2}$}{} is \textsc{coNExpTime}-complete,
		\item
		\mbox{$\Al^*\FOe$}{} is \textsc{coNExpTime}-complete,
		\item
		\mbox{$\Ex^*\FOe$}{} is \textsc{coNExpTime}-complete,
		\item
        \mbox{$\Ex^*\FO^+_{=}$}{} is \textsc{coNP}$^\textsc{NP}$-complete.
	\end{enumerate}
\end{theorem}

\begin{proof}
For \mbox{$\Ex^*\FO^+_{=}$}{}, homomorphism-closedness is guaranteed to hold, therefore, the task coincides with checking equivalence of two \mbox{$\Ex^*\FO^+_{=}$}{} sentences, which is known to be \textsc{coNP}$^\textsc{NP}$-complete (CITE HUBIE CHEN).
For the other fragments, membership can be uniformly established via TO BE FILLED IN BY THOMAS ...
while hardness follows from the corresponding results for $\mathrm{HomClosed}_{\mathrm{(fin)}}$
in the light of Proposition~\ref{prop:SatToHomCl}.
\end{proof}

\begin{theorem}
$\mathrm{CharHomCl}_{\mathrm{(fin)}}$ is undecidable for \mbox{$\mathbb{TGD}$}{}.
\end{theorem}

\begin{proof}
We show that the undecidable problem of checking whether a boolean conjunctive query Q is entailed from a \mbox{$\mathbb{TGD}$}{} sentence $\Phi$ can be \textsc{LogSpace}-reduced to $\mathrm{CharHomCl}_{\mathrm{(fin)}}$. We define $\Phi_Q$ as $\Phi\wedge (Q \to CQ(\mathfrak{F}))$. Then $\Phi \models Q$ exactly if
$ \homclffin{\getffinmodels{\Phi_Q}} = \getffinmodels{CQ(\mathfrak{F})} $
\end{proof}

\section{Checking Homclosedness}\label{sec:homclosedness}

The next problem we investigate is the
problem of
 determining whether a given sentence is homclosed (that is, the class of its models is closed under homomorphisms).

\bigskip

\probbox{
	\textbf{Problem:} $\mathrm{HomClosed}$\\
	\textbf{Input:} $\tau$, $\tau$-sentence $\Phi$.\\
	\textbf{Output:} \textsc{yes}, if $\getmodels{\Phi} = \homcl{\getmodels{\Phi}}$, \textsc{no} otherwise.
}

\bigskip

For the finite-model version of this problem, note that any structure has a homomorphism into some infinite structure. Thus, any non-empty class $\mathcal{C}$ of finite structures cannot be homomorphism-closed (whence the question if $\getfinmodels{\Phi} = \homcl{\getfinmodels{\Phi}}$ trivializes to the question if $\getfinmodels{\Phi} = \emptyset$). This motivates the subsequent definition, focusing on finite target structures.

\bigskip

\probbox{
	\textbf{Problem:} $\mathrm{HomClosed}_\mathrm{fin}$\\
	\textbf{Input:} $\tau$, $\tau$-sentence $\Phi$.\\
	\textbf{Output:} \textsc{yes}, if $\getfinmodels{\Phi} = \homclfin{\getfinmodels{\Phi}}$, \textsc{no} otherwise.
}

\medskip

To begin with, obviously, both problems are trivial (i.e., the answer is always \textsc{yes}) for fragments where every sentence's model class is homomorphism-closed, such as $\mbox{$\Ex^*\FO^+_{=}$}$.

Next, we will see that under very mild assumptions, (finite) satisfiability within the considered logic can be reduced to $\mathrm{HomClosed}_\mathrm{(fin)}$, yielding lower bounds for the latter in many cases. To this end, we state the following technical result.

\newcommand{\vspace{-4pt}}{\vspace{-4pt}}

\begin{lemma}[restate=SattToHomClosed, label=prop:SattToHomClosed, name=]
Let $\mathbb{L},\mathbb{L}' \subseteq \mbox{$\mathbb{SO}$}$ and $f \colon \mathbb{L}'\to \mathbb{L}$ such that
\vspace{-4pt}
\begin{itemize}[itemindent=0ex, leftmargin=1.8ex, itemsep=-0.6ex, labelsep=0.7ex, topsep=0ex]
\item (finite) unsatisfiability in $\mathbb{L}'$ is $\textsc{C}$-hard and
\item $f$ is $\textsc{C}'$-computable  and maps $\tau$-sen\-ten\-ces to $\tau\cup\{\sig{U}\}\cup \tau'$-sen\-ten\-ces with  {$\getffinmodels{f(\Phi)}|_{\tau \cup \{\sig{U}{}\}}  = \{(\mathfrak{A}, \emptyset) \mid \mathfrak{A}\in \llbracket \Phi\rrbracket_{(<\omega)}    \}$.}
\end{itemize}
Then $\mathrm{HomClosed}_\mathrm{(fin)}$ for $\mathbb{L}$ is $\textsc{C}$-hard under $\textsc{C}'$-reductions.
\end{lemma}
\vspace{-4pt}

In particular, \Cref{prop:SattToHomClosed} shows that for any logic allowing for extending any sentence $\Phi$ into $\Phi \wedge \forall x.\neg \sig{U}(x)$, (finite) hom\-closed\-ness
must be as hard as (finite) unsatisfiability. As a direct consequence of this lemma, we also obtain un\-de\-cida\-bi\-li\-ty for all logics containing $\mathbb{FO}$, but also for all undecidable $\FO_{=}$ prefix classes featuring a universal quantifier (such as $\mbox{$\Al\Al\Al\Ex\FO$}$ or $\mbox{$\Al\Al\Ex\FOe$}$), even if the signature does not contain constants. As in the previous section, this justifies focusing our attention to logics with a decidable satisfiability problem. However, it turns out that even for many of those,  $\mathrm{HomClosed}_\mathrm{(fin)}$ is undecidable, as we will show now. To this end, we establish a companion result to \Cref{prop:SattToHomClosed}.

\begin{lemma}[restate=SattToHomClosedCompanion, label=prop:SattToHomClosedCompanion, name=]
	Let $\mathbb{L},\mathbb{L}' \subseteq \mbox{$\mathbb{SO}$}$ and $f \colon \mathbb{L}'\to \mathbb{L}$ such that
\vspace{-4pt}
	\begin{itemize}[itemindent=0ex, leftmargin=1.8ex, itemsep=-0.6ex, labelsep=0.7ex, topsep=0ex]
		\item (finite) unsatisfiability in $\mathbb{L}'$ is $\textsc{C}$-hard and
		\item $f$ is $\textsc{C}'$-computable and maps $\tau$-sen\-ten\-ces to $\tau\cup\{\sig{U}\}$-sen\-ten\-ces with  $\getffinmodels{f(\Phi)} = \{(\mathfrak{A},\tilde{A}) \mid \mathfrak{A} \,{\in}\, \getffinmodels{\neg\Phi} \mbox{ or } \tilde{A} \,{\not=}\, A\}$.
	\end{itemize}
	Then $\mathrm{HomClosed}_\mathrm{(fin)}$ for $\mathbb{L}$ is $\textsc{C}$-hard under $\textsc{C}'$-reductions.
\end{lemma}
\vspace{-4pt}

In particular, this result shows that for any logics $\mathbb{L}$ and $\mathbb{L}'$ where one can easily find for any $\mathbb{L}'$ sentence $\Phi$ an $\mathbb{L}$ sentence equivalent to $\neg\Phi \vee \exists x.\neg \sig{U}{}(x)$,
$\mathrm{HomClosed}_\mathrm{(fin)}$ for $\mathbb{L}$ is at least as hard as unsatisfiability for $\mathbb{L}'$. Picking $\mbox{$\Al\Al\Al\Ex\FO$}$ and $\mbox{$\Al\Al\Ex\FOe$}$ for $\mathbb{L}'$, this immediately entails undecidability of $\mathrm{HomClosed}_\mathrm{(fin)}$ for the prefix classes $\mbox{$\Ex\Ex\Ex\Al\FO$}$ and $\mbox{$\Ex\Ex\Al\FOe$}$, despite decidability of satisfiability. Again, this even holds when constants are absent from the signature.
Of course, this also entails undecidability of $\mathrm{HomClosed}_\mathrm{(fin)}$ for the decidable prefix classes \mbox{$\Ex^*\Al\Al\Ex^*\FO$}{} (the Gödel class)
and \mbox{$\Ex^*\Al^*\FOe$}{} (the Bernays-Schönfinkel class).

\input{thomas-on-splitting-homs}

Finally, we turn to \mbox{$\mathbb{TGD}$}, for which the above machinery fails to work (despite the trivial (un)satisfiability problem) as \mbox{$\mathbb{TGD}$}{} is not closed under negation. We start with a positive result.

\begin{theorem}[restate=TGDNPtheorem, name=]
$\mathrm{HomClosed}_\mathrm{(fin)}$ for \mbox{$\mathbb{TGD}$}{} is \textsc{NP}-complete.
\end{theorem}

Intuitively, this result is facilitated by the fact that homclosed \mbox{$\mathbb{TGD}$}{} sentences must have very small universal models, against which  homclosedness violations can be checked on a per-rule basis. However, all is lost as soon as just a tad of disjunction is introduced.

\newcommand{\tight}[1]{\hspace{1pt}{#1}\hspace{1pt}}
\newcommand{\hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex}}{\hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex}}

\begin{definition}\label{def:TGDdettiling}
	Given a deterministic domino system
	$\mathcal{D}=(D,B,L,H,V)$, we define the \mbox{$\mathbb{TGD}$}{} sentence
	\begin{equation}
	\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} = \Phi_\mathrm{grid} \wedge \Phi_\mathcal{D},
	\end{equation}
	where $\Phi_\mathcal{D}$ is the conjunction over the following rules (with unary predicates $\sig{T}{}_\emptyset$ and $\sig{T}{}_{\{d\}}$ for all the dominoes $d \in D_\mathcal{D}$):
	%
	\begin{eqnarray}
		  &  & \hspace{-7ex}\exists v.\sig{T}{}_{B \cap L}(v) \\[3pt]
		%

		\forall xy.\big(\sig{T}{}_{\{d\}}(x) \tight{\wedge} \sig{V}{}(x,y) \hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex} \sig{T}{}_{V(d)}(y) \big)
		\hspace{10.7ex}{d \tight{\in} L}\hspace{4.5ex}\\[3pt]
		%

		\forall xy.\big(\sig{T}{}_{\{d\}}(x) \tight{\wedge} \sig{H}{}(x,y) \hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex} \sig{T}{}_{H(d)}(y) \big)
		\hspace{10.5ex}{d \tight{\in} B}\\[3pt]
		%

		\forall xyz.\big( \sig{T}{}_{\{d\}}(x) \tight{\wedge} \sig{H}{}(x,z) \tight{\wedge} \sig{T}{}_{\{d'\}}(y) \tight{\wedge} \sig{V}{}(y,z) \hspace{-18.7ex} \nonumber \\[-1pt]
		 \hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex}
		\sig{T}{}_{H(d)\cap V(d')}(z) \big)
		\hspace{2.5ex} {d,\!d' \tight{\in} D}\\[3pt]
		%

		\forall x.\big(\sig{T}{}_{\{d\}}(x) \tight{\wedge} \sig{T}{}_{\{d'\}}(x) \hspace{-1.7ex} & \Rightarrow & \hspace{-1.7ex}
		\sig{T}{}_{\emptyset}(x) \big)
		\hspace{5ex} {d,\!d' \tight{\in} D, d \tight{\neq} d'}
	\end{eqnarray}
\end{definition}
Note that a(n ultimately periodic) $\mathcal{D}$-tiling exists exactly if
$\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ has a (finite) model $\mathfrak{A}$ with $\sig{T}{}_\emptyset{}^\mathfrak{A} = \emptyset$.
This is the case exactly if	$\getffinmodels{\exists x.\sig{T}{}_\emptyset{}(x)} \neq\getffinmodels{\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)}$. Yet, note that any -- finite or infinite -- model $\mathfrak{A}$ of $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$ with $\sig{T}{}_\emptyset{}^\mathfrak{A} = \emptyset$ admits a homomorphism into $\mathfrak{A} \uplus \mathfrak{I}$, for which $\sig{T}{}_\emptyset{}^{\mathfrak{A}\uplus \mathfrak{I}} = \emptyset$ and it is not a model of $\Phi_{\mathcal{D}\text{-}\mathrm{tiling}}$, thus $\mathfrak{A}\uplus \mathfrak{I} \notin \getffinmodels{\Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)}$. Therefore, the class of (finite) models of the \mbox{$\mathbb{MDTGD}$}{} sentence $\Psi = \Phi_{\mathcal{D}\text{-}\mathrm{tiling}} \vee \exists x.\sig{T}{}_\emptyset{}(x)$ is closed under (finite-target) homomorphisms exactly if there exists no (ultimately periodic) $\mathcal{D}$-tiling. We get the following.

\begin{theorem}
	$\mathrm{HomClosed}_\mathrm{(fin)}$ is undecidable for \mbox{$\mathbb{MDTGD}$}{} (and hence for \mbox{$\mathbb{DTGD}$}{}).
	This even holds for \mbox{$\mathbb{DTGD}$}{} sentences with $\leq\! 4$ universally and $\leq\! 1$ existentially quantified variables and predicates of arity $\leq\! 2$.
\end{theorem}

\section{Conclusion}

Inspired by the homomorphism preservation theorem and motivated by routinely encountering -- clearly fundamental yet seemingly largely neglected -- questions
regarding homclosures of logically characterized model classes, we undertook a principled analysis of four basic questions related to that matter and clarified them for a wide range of theoretically and practically relevant logical formalisms, both in the finite-model setting and the arbitrary-model one. \Cref{fig:main} summarizes the results obtained.

Next to several newly introduced generic techniques, which might prove useful well beyond the specific formalisms considered here, our most noteworthy achievements are probably the establishment of a computationally well-behaved normal form for homclosed $\mbox{$\mathbb{SO}$}$ sentences, and the insight that checking homclosure membership for the very expressive guarded negation fragment of first-order logic ($\mathbb{GNFO}_{=}$) has only polynomial-time data complexity.

Plenty of open problems remain.
Obviously other, different logical formalisms could be investigated regarding the considered questions.
Not all of the established techniques immediately lend themselves to coping with ``counting logics'', such as two-variable logic with counting quantifiers.
More generally, logics without the finite model property might turn out to be harder to handle.

The investigation into the prefix classes has not yet resulted in a complete characterization of decidability and complexity of the homclosedness problem. A first inspection seems to indicate that corresponding results would hinge on a more fine-grained analysis of fragments defined by the conjunction over sentences from different prefix classes.

As far as normal forms are concerned, for first-order prefix classes with bounded number of existential quantifiers, preceded by universal quantification, the question remains generically unsolved. For \mbox{$\mathbb{TGF}$}{} and \mbox{$\FO_{=}^\mathbbm{2}$}{}, normal forms have been shown to exist, but recognizing them is costly and more syntactic solutions would be preferred.

An interesting open problem is whether there exists a syntactic fragment of \emph{existential second-order logic} such that the classes of finite structures that are expressible in the fragment are precisely the homomorphism-closed classes in \textsc{NP}. Similarly, we ask whether there exists a logic (in the sense of Gurevich~\cite{GroheLogicforP}) that captures precisely the homclosed classes of finite structures that are in the complexity class \textsc{P}.

Another interesting avenue arises from the area of constraint satisfaction problems (CSPs). It seems advisable to systematically explore which (complements of)
CSPs can be described as the homclosure of sentences in
one of the well-behaved logics $\mbox{$\mathbb{GFO}_{=}$}$ and $\mathbb{GNFO}_{=}$ -- guaranteeing solvability in \textsc{P}, by Theorem~\ref{sorpresa}.
For a start, note that \Cref{thm:allhomcaptures} implies that the homclosures of $\mathbb{GNFO}_{=}{}$ and $\mbox{$\mathbb{GFO}_{=}$}{}$
sentences are expressible in guarded existential second-order logic;
this even holds projectively. Yet, by a recent result of a subset of
the authors~\cite{BKR}, if the complement of a CSP can be expressed in
this form, then the CSP is of the form CSP$({\mathfrak B})$ for an
$\omega$-categorical structure ${\mathfrak B}$. This implies that the
so-called universal-algebraic approach can be used to study complexity
and expressivity questions CSPs of said type \cite{Book}.

\section{Introduction}
The
\emph{homomorphism preservation theorem} states that, for any first-order sentence $\Phi$, the property of being a model of~$\Phi$~is preserved under homomorphisms\footnote{Henceforth, we will simply call such a $\Phi$ (and its model class)  \emph{homclosed{}}.} if and only if $\Phi$ is equivalent to an existential positive sentence.
For arbitrary models, this correspondence goes back to \L{}os, Tarski, and Lyndon in the 1950s, whereas Rossman showed only rather recently that it also holds when considering \emph{finite} models only \cite{Rossman08}.

Classes of homclosed first- or second-order sentences are ubiq\-ui\-tous in computer science. In databases, they often serve as intuitive \emph{query languages} and check for the presence of a certain ``pattern'' in a given database \cite{DBLP:conf/pods/RudolphK13}. In particular, existential positive sentences, which can be expressed as so-called \emph{unions of conjunctive queries}, are encountered very frequently in practice. Homclosed classes of finite structures  also appear naturally in other areas of computer science; for example, the complement of any constraint satisfaction problem, viewed as a class of finite structures, is homclosed.

This paper poses and comprehensively answers the following four fundamental questions concerning homclosures:

\begin{enumerate}[itemindent=0ex, leftmargin=3ex]
\item \textbf{Homclosure membership.}
Given a sentence $\Phi$ from some logic and a finite structure $\mathfrak{A}$,
we want to decide whether $\mathfrak{A}$ belongs to the homclosure of $\Phi$. How difficult is this problem computationally?
We are interested both in the \emph{combined complexity} (where both $\mathfrak{A}$ and $\Phi$ are given) and in the \emph{data complexity} (where $\mathfrak{A}$ is given and $\Phi$ is fixed).
\item \textbf{Homclosedness.}
Given a sentence $\Phi$ from some logic, we want to decide whether $\Phi$ is homclosed. How difficult is this problem computationally?
\item \textbf{Homclosure characterizability.}
Given a sentence $\Phi$ from some logic,
does there exist a sentence $\Psi$ (from the same or a different logic) such that
the class of $\Psi$'s models is precisely the homclosure of the class of $\Phi$'s models?
\item \textbf{Homclosed normal forms.}
For which logics
exists a \emph{`syntactic normal form'}, i.e., a subset of easily recognizable sentences such that an arbitrary sentence from that logic is equivalent to a sentence in normal form if and only if the former is homclosed?
\end{enumerate}
\vspace{-2ex}
This paper provides answers to these questions for (fragments of) first- and se\-cond-or\-der logic of varying expressivity, with a particular emphasis on very expressive but decidable formalisms (including the two-variable fragment, the guarded (negation) fragment, and the triguarded fragment), popular formalisms in database theory (such as existential positive sentences and tuple-generating dependencies), and diverse prefix classes.
We next summarize our findings and methods. Our results hold both for the finite- and the arbitrary-model case, so we will not make this distinction here, even if distinct proofs are sometimes required.

As for Question 1), \Cref{sec:InHomCl} presents results regarding decidability and combined complexity. We show that the homclosure membership problem is generically interreducible with the considered logic's satisfiability problem in a wide variety of cases, thus tightly tying decidability and complexity of homclosure membership to satisfiability; the reduction from the former to the latter is shown by logically encoding model \emph{colorings}, inspired by similar ideas from constraint satisfaction. As notable exception, we find that for tuple-generating dependencies, the problem is undecidable despite satisfiability being trivial. Regarding the data complexity of homclosure membership, we find that question intimately related to Question 3), since in the presence of a logical characterization of a sentence's homclosure, checking homclosure membership boils down to model checking against the characterizing sentence. Along those lines, \Cref{sec:characterizability} provides a variety of results, the most striking of which is probably \Cref{sorpresa}, asserting polynomial time data complexity of checking membership in the homclosure of sentences in the guarded (negation) fragment of first-order logic.

Regarding Question 2) addressed in \Cref{sec:homclosedness}, we find that under fairly weak assumptions, the satisfiability problem for the logic under consideration can be reduced to its homclosedness problem. Yet, a similar reduction can be found from satisfiability in the ``dual'' logic, identifying several prefix classes where homclosedness is undecidable, despite satisfiability being decidable. For the remaining cases, we propose a generic reduction from homclosedness to unsatisfiability,
based on the notion of \emph{spoiler} -- a homomorphism from a model to a non-model, i.e., a witness for non-homclosedness -- and a way of creating spoiler-detecting sentences. Again, tuple-generating dependencies need to be coped with differently; we find that for the plain version, homclosedness is \textsc{NP}-complete, while adding disjunction turns the problem undecidable.

For Question 3), which we focus on in \Cref{sec:characterizability}, it is important to note that already for very basic first-order sentences (including tuple-generating dependencies), their homclosure is not expressible in first-order logic, and even the question whether a given first-order sentence is expressible in any logic with a decidable model checking problem is undecidable. On the other hand, we show that the homclosure of any sentence from the Bernays-Schönfinkel class can even be characterized in existential positive first-order logic. Using elaborate model-theoretic characterizations based on \emph{types}, we are able to show that the two-variable fragment, the triguarded fragment and the Gödel class allow for homclosure-characterization in second-order logic (in fact, even in decidable fragments thereof), while sentences in the guarded and the guarded negation fragment can be homclosure-characterized even in first-order logic with least fixed points. Employing arguments from descriptive complexity we show that these characterizability results are optimal in a certain sense.

Question 4) is dealt with in \Cref{sec:normalforms}. For fragments of first-order logics, we exploit the homomorphism-preservation theorem to settle the case for all fragments fully encompassing existential positive first-order logic. We can also give a syntactic normal form for Bernays-Schönfinkel subclasses with a bounded number of quantifiers. For fragments with a decidable homclosedness problem, we can resort to this (usually costly) check to identify normal form sentences. A few cases, however, remain open.
Finally, turning to full second-order logic, we are indeed able to establish a normal form for sentences whose models are closed under homomorphisms, too. As opposed to first-order logic, however, this normal form can be even computed from the given second-order sentence in polynomial time.

Detailed proofs can be found in the appendix.

\section*{Acknowledgments}
We are indebted to the as meticulous as benevolent anonymous reviewers for their appreciation and numerous valuable suggestions for improvement. We are particularly grateful to Bartosz Bednarczyk for his diligent help in polishing the final version (pun intended).

Manuel Bodirsky has received funding from the European Research Council through the ERC Consolidator Grant 681988 (CSP-Infinity).
Thomas Feller and Sebastian Rudolph are supported by the European Research Council through the ERC Consolidator Grant 771779 (DeciGUT).
Simon Knäuer is supported by DFG Graduiertenkolleg 1763 (QuantLA).

\bibliographystyle{abbrv}

\section{Checking Homclosure Membership}\label{sec:InHomCl}

The first problem we address is determining whether a given finite structure is contained in the homclosure of the set of models (or finite models) of a given sentence $\Phi$.

\bigskip

\probbox{
\textbf{Problem:} $\mathrm{InHomCl}_\mathrm{(fin)}$\\
\textbf{Input:} $\tau$, $\tau$-sentence $\Phi$, finite $\tau$-structure $\mathfrak{A}$.\\
\textbf{Output:} \textsc{yes}, if $\mathfrak{A} \in \homcl{\getffinmodels{\Phi}}$, \textsc{no} otherwise.
}

\bigskip

The fact that $\Phi$ is (finitely) satisfiable iff $\mathfrak{F}_\tau \in \homcl{\getffinmodels{\Phi}}$, already yields some lower bounds for this problem's difficulty.

\begin{proposition}\label{prop:SatToInHomCl}
(Finite) satisfiability can be \textsc{LogSpace}-reduced to $\mathrm{InHomCl}_\mathrm{(fin)}$.
\end{proposition}

This shows that $\mathrm{InHomCl}_\mathrm{(fin)}$ is undecidable for any logic with an undecidable (finite) satisfiability problem, such as $\mathbb{FO}$ and every logic containing it, but also all $\mathbb{FO}$ reduction classes.

Toward some decidable cases and corresponding optimal upper bounds, we employ and formalize the straightforward idea of ``coloring'' a model with elements of the target structure.

\begin{definition}[extrinsic/intrinsic $\mathfrak{A}$-coloring]\label{def:exincol}
Let $\mathfrak{A}$ be a finite $\tau$-structure over the domain $A=\{1,\ldots,n\}$.
As before, we use a signature $\rho =\{ \sig{Bit}^\lambda_1,\ldots,\sig{Bit}^\lambda_\ell \}$ of unary predicates with $\ell = \lceil \log_2 n \rceil$ to represent $n$-labeled structures.

Given a predicate $\sig{P} \in \tau$ of arity $k$ and a $k$-tuple of terms
$\bold{t}=(t_1,\ldots,t_k)$, we let $\chi^{\sig{P}}_\mathfrak{A}(\bold{t})$ denote the formula
\begin{equation}
	\sig\sig{P}(\boldsymbol{t}) \wedge \bigvee_{{(m_1,\ldots,m_k)}\in \sig{P}{}^\mathfrak{A}\ } \bigwedge_{i=1}^k [\lambda(t_i)=m_i].
\end{equation}
We denote by $\Omega_\mathfrak{A}$ the following $\tau{\uplus}\rho$-sentence:
\begin{equation}
\bigwedge_{{\sig{P}\in \tau}\atop{k=\text{ar}(\sig{P})}} \forall x_1\ldots x_k. \sig\sig{P}(x_1,\ldots,x_k)
\Rightarrow \chi^{\sig{P}}_\mathfrak{A}(x_1,\ldots, x_k).
\end{equation}
Given a $\tau$-sentence $\Phi$ and a finite $\tau$-structure $\mathfrak{A}$, we define the \emph{extrinsic \mbox{$\mathfrak{A}$-coloring}} of $\Phi$ by
$\Phi^\mathrm{ext}_\mathfrak{A} = \Phi \wedge \Omega_\mathfrak{A}$. The \emph{intrinsic \mbox{$\mathfrak{A}$-coloring}} of $\Phi$, denoted $\Phi^\mathrm{int}_\mathfrak{A}$ is obtained from $\Phi$ by replacing, for all predicates $\sig{P} \in \tau$, any occurrence of $\sig\sig{P}(\bold{t})$ by $\chi^{\sig{P}}_\mathfrak{A}(\bold{t})$.
\end{definition}

Note that both $\Phi^\mathrm{ext}_\mathfrak{A}$ and $\Phi^\mathrm{int}_\mathfrak{A}$ are of polynomial size wrt.\ $|\mathfrak{A}|$ and the size of $\Phi$.
The sentence $\Omega_\mathfrak{A}$ projectively characterizes the class of $\tau$-structures having a homomorphism into $\mathfrak{A}$, thus $\Phi^\mathrm{ext}_\mathfrak{A}$ projectively characterizes the class of (finite) models of $\Phi$  having a homomorphism into $\mathfrak{A}$.
Also, every model of $\Phi$ having a homomorphism into $\mathfrak{A}$ can be extended to a model of $\Phi^\mathrm{int}_\mathfrak{A}$, and conversely, for every model $\mathfrak{B}$ of $\Phi^\mathrm{int}_\mathfrak{A}$, the structure $\mathfrak{C}$ obtained by setting $C:=B$, $\sig{c}{}^\mathfrak{C}:=\sig{c}{}^\mathfrak{B}$ for all constants, and $\sig{P}{}^\mathfrak{C} := (\chi^{\sig{P}}_\mathfrak{A})^\mathfrak{B}$ is a model of $\Phi$ with a homomorphism into $\mathfrak{A}$. Hence we obtain the following lemma.

\begin{lemma}[restate=lemmacoloring, label=, name=]\label{lemma:coloring}
	Let $\Phi$ be an arbitrary $\tau$-sentence and let $\mathfrak{A}$ be a finite $\tau$-struc\-ture.
The following are equivalent:
\begin{enumerate}[itemindent=0ex, leftmargin=1.8ex, itemsep=-0.5ex, labelsep=0.7ex, topsep=0ex
	\item
	$\Phi$ has a (finite) model admitting a homomorphism into $\mathfrak{A}$.
	\item
	$\Phi^\mathrm{int}_\mathfrak{A}$ is (finitely) satisfiable.
	\item
	$\Phi^\mathrm{ext}_\mathfrak{A}$ is (finitely) satisfiable.
\end{enumerate}
\end{lemma}

As a direct consequence, arbitrary and finite homclosure membership coincide for a wide range of fragments.

\begin{theorem}[restate=thearbsameasfin, label=thm:first-main, name=]\label{the:arb-sameas-fin}
Let $\mathbb{L} \,{\subseteq}\, \mbox{$\mathbb{SO}$}$ and $\mathbb{L}^\mathrm{ext}:=\{\Phi^\mathrm{ext}_\mathfrak{A}\mid \Phi \in \mathbb{L}, \mathfrak{A} \mbox{ finite}\}$
as well as $\mathbb{L}^\mathrm{int}:=\{\Phi^\mathrm{int}_\mathfrak{A}\mid \Phi \in \mathbb{L}, \mathfrak{A} \mbox{ finite}\}$.
If $\mathbb{L}^\mathrm{ext}$ or $\mathbb{L}^\mathrm{int}$ has the FMP, then $\homclfin{\getmodels{\Psi}}=\homclfin{\getfinmodels{\Psi}}$ for every $\Psi \in \mathbb{L}$.
\end{theorem}
This theorem applies to various fragments, including any (sublogic) of \mbox{$\mathbb{DTGD}$}{}, \mathbb{GNFO}_{=}{}, \mbox{$\mathbb{TGF}$}{}, \mbox{$\FO_{=}^\mathbbm{2}$}{}, \mbox{$\Ex^*\Al\Al\Ex^*\FO$}{}, or \mbox{$\Ex^*\Al^*\FOe$}{}. We obtain the following complexity results.

\begin{theorem}[restate=firstmain, label=thm:first-main, name=]
$\mathrm{InHomCl}_\mathrm{(fin)}$ is complete for
\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
\item
\textsc{2ExpTime} for \mathbb{GNFO}_{=}{},
\item
\textsc{N2ExpTime} for \mbox{$\mathbb{TGF}$}{},
\item
\textsc{NExpTime} for
\mbox{$\FO_{=}^\mathbbm{2}$}{},
\mbox{$\Ex^*\Al\Al\Ex^*\FO$}{},
\mbox{$\Ex^*\Al^*\FOe$}{},
\mbox{$\Al^*\FOe$}{},
\item
\textsc{NP} for \mbox{$\Ex^*\FOe$}{} and
\mbox{$\Ex^*\FO^+_{=}$}{}.
\end{enumerate}

\end{theorem}

Next to the combined complexity addressed in the previous theorem, one might also ask for the complexity if the sentence is fixed and only the structure of interest varies. We will come back to this question in the course of \Cref{sec:characterizability}.

We conclude with a case where the difficulty of $\mathrm{InHomCl}_\mathrm{(fin)}$ does not coincide with that of satisfiability (in the most egregious way). We recap that \mbox{$\mathbb{TGD}$}{} (just like \mbox{$\mathbb{MDTGD}$}{} and \mbox{$\mathbb{DTGD}$}{}) has a trivial satisfiability problem (in that every \mbox{$\mathbb{TGD}$}{} sentence is satisfiable and finitely satisfiable, with $\mathfrak{F}$ uniformly serving as a model), yet we present a fixed \mbox{$\mathbb{TGD}$}{} sentence $\Phi_\mathrm{grid}$ for which $\mathrm{InHomCl}_\mathrm{(fin)}$ is undecidable.

\begin{definition}[restate=defgridformula, name=]
We let $\mathfrak{A}_{\mathbb{N} \times \mathbb{N}}$ denote the $\mathbb{N} \times \mathbb{N}$ grid, i.e., the $\{\sig{H}{},\sig{V}{}\}$-structure with domain $A_{\mathbb{N} \times \mathbb{N}} = \mathbb{N} \times \mathbb{N}$ that satisfies
$\sig{H}{}^{\mathfrak{A}_{\mathbb{N} \times \mathbb{N}}} = \{((k,\ell),(k+1,\ell)) \mid k,\ell \in \mathbb{N}\}$ as well as
$\sig{V}{}^{\mathfrak{A}_{\mathbb{N} \times \mathbb{N}}} = \{((k,\ell),(k,\ell+1)) \mid k,\ell \in \mathbb{N}\}$.

Let $\Phi_\mathrm{grid}$ denote the \mbox{$\mathbb{TGD}$}{} sentence
\begin{equation}
\begin{array}{l}
\Big( \forall x \exists y. \sig{H}{}(x,y) \Big) \wedge
\Big( \forall x \exists y. \sig{V}{}(x,y) \Big) \wedge \\
\hspace{4ex}\Big( \forall xyzv. \sig{H}{}(x,y) \wedge \sig{V}{}(x,z) \wedge \sig{V}{}(y,v) \Rightarrow \sig{H}{}(z,v) \Big).
\end{array}
\end{equation}
For a given domino system $\mathcal{D}=(D,D,D,H,V)$, we define the finite $\{\sig{H}{},\sig{V}{}\}$-structure $\mathfrak{A}_\mathcal{D}$ as follows: $A_\mathcal{D} = D$ as well as $\sig{H}{}^{\mathfrak{A}_\mathcal{D}}=H$ and $\sig{V}{}^{\mathfrak{A}_\mathcal{D}}=V$.
\end{definition}

Noting that every model $\mathfrak{B}$ of $\Phi_\mathrm{grid}$ allows for a homomorphism $h \colon \mathfrak{A}_{\mathbb{N} \times \mathbb{N}} \to \mathfrak{B}$,
it follows that every homomorphism from some (finite) model of $\Phi_\mathrm{grid}$ into $\mathfrak{A}_\mathcal{D}$ gives rise to a(n ultimately periodic) $\mathcal{D}$-tiling.
Thus, by \Cref{gridlemma}, both membership in $\homcl{\getmodels{\Phi_\mathrm{grid}}}$ and $\homcl{\getfinmodels{\Phi_\mathrm{grid}}}$ are undecidable problems.

\begin{theorem}[restate=undecTGD, label=corr:undecTGD, name=]
$\mathrm{InHomCl}_\mathrm{(fin)}$ is undecidable for \mbox{$\mathbb{TGD}$}{} (and hence for \mbox{$\mathbb{MDTGD}$}{} and \mbox{$\mathbb{DTGD}$}{}).
\end{theorem}

\section{Normal Forms for Homclosed Fragments}\label{sec:normalforms}

This section is devoted to identifying ``homclosed normal forms'' of certain logics.
Given a logic $\mathbb{L}$, a homclosed normal form $\mathbb{H}\mathbb{L}$ of $\mathbb{L}$ is a fragment which satisfies
\begin{itemize}[itemindent=0ex, leftmargin=3ex, topsep=0ex]
\item $\mathbb{H}\mathbb{L} \subseteq \mathbb{L}$,
\item every $\Phi \in \mathbb{H}\mathbb{L}$ is homclosed,
\item for each homclosed $\Phi \in \mathbb{L}$ exists a $\Phi' \in \mathbb{H}\mathbb{L}$ with $\Phi \equiv \Phi'$,
\item membership in $\mathbb{H}\mathbb{L}$ is decidable.
\end{itemize}

It is, of course, desirable to strengthen the last requirement to say that membership can be decided ``easily'', e.g., in polytime.
Likewise, we might require the existence of a (preferably computationally inexpensive) algorithm to compute $\Phi'$ from a given $\Phi$, or of a (not too high) upper bound regarding the size of $\Phi'$ with respect to $\Phi$.

\noindent\textbf{Normal Forms for $\FO_{=}$ and Fragments.}\quad
The homomorphism preservation theorem provides a normal form for full $\FO_{=}$, namely $\mbox{$\Ex^*\FO^+_{=}$}$; the equivalent $\mbox{$\Ex^*\FO^+_{=}$}$ sentences may even be chosen to have equal quantifier rank.
Rossman's theorem shows that the same normal form can be used if we consider finite models only;
more recently, Rossman even established that any homclosed first-order formula of quantifier rank $k$ is equivalent to an existential positive formula of quantifier rank $k^{O(1)}$~\cite{Rossman17}.
Note that computing the normal form can be quite costly: there is a potentially non-elementary blow-up for the length of a shortest equivalent existential positive formula \cite[Theorem 6.1]{Rossman08}.

Obviously, this characterization of a normal form for $\FO_{=}$ carries over to any $\FO_{=}$ fragment that fully encompasses $\mbox{$\Ex^*\FO^+_{=}$}$. For Bernays-Schönfinkel fragments with bounded number of existential quantifiers, we state the following observation.

\begin{proposition}[restate=boundedex, name=]
For every homclosed $\mbox{$\exists\hspace{-4.5pt}\exists$}^n\mbox{$\forall\hspace{-4.5pt}\forall$}^*\FO_{=}$ sentence there exists an equivalent $\mbox{$\exists\hspace{-4.5pt}\exists$}^n\FO_{=}^+$ sentence.
\end{proposition}

For other fragments, the case is less immediate. Whenever $\mathrm{HomClosed}$ is decidable for $\mathbb{L}$, we can use this (usually expensive) test to directly define $\mathbb{H}\mathbb{L}$, thus obtaining $\mathbb{H}\mbox{$\mathbb{TGF}$}$, $\mathbb{H}\mbox{$\FO_{=}^\mathbbm{2}$}$, and $\mathbb{H}\mbox{$\Al\Al\Ex\Ex\FO$}$. For $\FO_{=}$ fragments not covered by these cases (such as \mbox{$\Al\Al\Al\Ex\FO$}), the question remains open.

\newcommand{\supclffin}[1]{#1^{\cl{\str{\mathrel{{\hookrightarrow}}}}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}}}
\newcommand{\homsucl}[1]{#1^{\mathrm{sH}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}}}

\input{bigtable}

\noindent\textbf{Normal Form for Homclosed $\mbox{$\mathbb{SO}$}$.}\quad
We next provide a syntactic normal form for $\mbox{$\mathbb{SO}$}$ sentences whose class of models is homclosed. This normal form arises as a combination of a normal form for superstructure-closed classes and a normal form for classes closed under surjective homomorphisms. Our proof relies  on the interplay of syntactic manipulations of $\mbox{$\mathbb{SO}$}$ sentences on the one hand and ``operators'' on classes of structures on the other. We focus on the following two operations that can be applied to classes $\mathcal{C}$ of $\tau$-structures:

\vspace{-2.5ex}
\begin{eqnarray}
\supclffin{\mathcal{C}} \hspace{-1.5ex} & = & \hspace{-1.5ex} \{\mathfrak{A} \text{~(finite)}\mid \mathfrak{B}\, {\str{\mathrel{{\hookrightarrow}}}}\, \mathfrak{A} \text{ for some }\mathfrak{B}\in \mathcal{C}\}, \\
\homsucl{\mathcal{C}} \hspace{-1.5ex} & = & \hspace{-1.5ex} \{\mathfrak{A} \text{~(finite)}\mid
\{\mathfrak{A}\}^\cl{\mathrel{{\to\hspace{-0.8ex}\!\!\!\to}}} \subseteq \mathcal{C})
\}.
\end{eqnarray}
\vspace{-2.5ex}

With these notions, we can establish the following characterizations of classes of $\tau$-structures.

\begin{lemma}[restate=classnormalform, label=lem:classnormalform, name=]
	For any class $\mathcal{C}$  of (finite) $\tau$-structures holds:
	\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
		\item $\supclffin{\mathcal{C}}$ is closed under (finite) superstructures. Moreover, if $\mathcal{C}$  is closed under  (finite) superstructures, then $\supclffin{\mathcal{C}}=\mathcal{C}$.
		\item $\homsucl{\mathcal{C}}$ is closed under (finite) surjective homomorphisms. Moreover, if $\mathcal{C}$  is closed  under (finite) surjective homomorphisms, then $\homsucl{\mathcal{C}}=\mathcal{C}$.
		\item $\supclffin{(\homsucl{\mathcal{C}})}$ is (finitely) homclosed. Moreover, every (finitely) homclosed $\mathcal{C}$ satisfies $\supclffin{(\homsucl{\mathcal{C}})}=\mathcal{C}$.
	\end{enumerate}
\end{lemma}

Based on this, we can introduce a normal form for super\-struc\-ture-closed $\mbox{$\mathbb{SO}$}$.

\begin{definition}
	Let $\tau$ be a signature and let $\Psi$ be an~$\mbox{$\mathbb{SO}$}$ $\tau$-sentence.
	Then the~$\mbox{$\mathbb{SO}$}$ $\tau$-sentence $\Psi^{\mathrm{sup}}$ is defined as
	$\exists \dot{\sig{U}}. \Psi^{\mathrm{rel}(\dot{\sig{U}})}$,
	where $\dot{\sig{U}}$ is a fresh unary predicate.
\end{definition}

\begin{proposition}[restate=supstructure, label=prop:supstructure, name=]
	Let $\Psi$ be an~$\mbox{$\mathbb{SO}$}$ $\tau$-sentence. Then
	\begin{equation}
	\supclffin{\getffinmodels{\Psi}}= \getffinmodels{\Psi^{\mathrm{sup}}}.
	\end{equation}
\end{proposition}

\Cref{prop:supstructure} and \Cref{lem:classnormalform} give rise to the normal form for superstructure-closed $\mbox{$\mathbb{SO}$}$.

\begin{corollary}\label{cor:supstr}For any~$\mbox{$\mathbb{SO}$}$ $\tau$-sentence $\Psi$, $\getffinmodels{\Psi^{\mathrm{sup}}} $ is closed under (finite)  superstructures.
	Moreover, if $\getffinmodels{\Psi}$ is closed under (finite) superstructures, then $\getffinmodels{\Psi^{\mathrm{sup}}}=\getffinmodels{\Psi}$.
\end{corollary}

We proceed by establishing a normal form for $\mbox{$\mathbb{SO}$}$ sentences closed under surjective homomorphisms.
For a signature $\tau$ and variables $z,z'$, we let $\eta^{\tau}(z,z')$ denote the formula
\begin{equation}
	\bigwedge_{{\sig{P} \in \tau}\atop{k=\text{ar}(\sig{P})}} \hspace{-6.5ex}
	\bigwedge_{{1\leq i \leq k}\atop{{\hspace{6.5ex} \bold{x}=(x_1,\ldots,x_{i-1})}\atop{\hspace{6.5ex}\bold{y}=(x_{i+1},\ldots,x_k)}}}
	\hspace{-6.0ex}
	\forall \bold{x}\bold{y}. \sig{P}(\bold{x},z,\bold{y}) \Leftrightarrow \sig{P}(\bold{x},z',\bold{y}),
\end{equation}
and, for a unary $\sig{U} \notin \tau$, we define the $\tau{\uplus}\{\sig{U}\}$-sentence $\Theta_\sig{U}^\tau$ by
\begin{equation}
\forall x \exists y. (\sig{U}(y)\wedge \eta^{\tau}(x,y)).
\end{equation}

\begin{definition}
	Let $\tau$  and $\tau'$ be  disjoint signatures such that $\tau'$ consists of copies $\sig{P}'$ of all predicates $\sig{P} \in \tau$. Let $\Psi$ be an $\mbox{$\mathbb{SO}$}$ $\tau$-sentence.
	Then the $\mbox{$\mathbb{SO}$}$ $\tau$-sentence  $\Psi^{\mathrm{shom}}$ is defined by

\vspace{-3ex}
\begin{equation}
\forall \sig{U} \, \forall \tau'\! . \bigg(\Big( \Theta_\sig{U}^{\tau'} \wedge \! \bigwedge_ {\sig{P}'\in \tau'} \! \forall \bold{x}.\big(\sig{P}(\bold{x}) \,{\Rightarrow}\, \sig{P}'(\bold{x})\big)\Big) \Rightarrow \Psi_{\tau \mapsto \tau'}^{\mathrm{rel}(\sig{U}) } \bigg),
\end{equation}
\vspace{-2.5ex}

\noindent where $\sig{U}$ is a fresh unary predicate and $\Psi_{\tau \mapsto \tau'}^{\mathrm{rel}(\sig{U})}$ denotes $\Psi^{\mathrm{rel}(\sig{U})}$ with every $\sig{P} \in \tau$ replaced by its copy $\sig{P}' \in \tau'$.
\end{definition}

\begin{proposition}[restate=surjhom, label=prop:surjhom, name=]
Let $\Psi$ be an \mbox{$\mathbb{SO}$}{} $\tau$-sentence. Then
\begin{equation}
\homsucl{\getffinmodels{\Psi}}= \getffinmodels{\Psi^{\mathrm{shom}}}.
\end{equation}
\end{proposition}

This result, together with \Cref{prop:supstructure} and \Cref{lem:classnormalform}, yields the normal form for surjective-homomorphism-closed $\mbox{$\mathbb{SO}$}$.

\begin{corollary}\label{cor:suhom}For any $\mbox{$\mathbb{SO}$}$ $\tau$-sentence $\Psi$, $\getffinmodels{\Psi^{\mathrm{shom}}}$ is closed under  surjective (finite) homomorphisms.
	Moreover, if $\getffinmodels{\Psi}$ is closed under  surjective (finite) homomorphisms, then $\getffinmodels{\Psi^{\mathrm{shom}}}=\getffinmodels{\Psi}$.
\end{corollary}

We are now ready to combine the established results toward the desired normal form for homclosed $\mbox{$\mathbb{SO}$}$.
Invoking \Cref{cor:supstr}, \Cref{cor:suhom}, and \Cref{lem:classnormalform}, we obtain the following statement, motivating the subsequent definition.

\begin{theorem}\label{thm:normalformSO}An $\mbox{$\mathbb{SO}$}$-definable class of (finite) $\tau$-structures is of the form
\vspace{-1.5ex}
\begin{equation}
\getffinmodels{(\Psi^{\mathrm{shom} }) ^{\mathrm{sup}}}
\end{equation}
for an $\mbox{$\mathbb{SO}$}$ $\tau$-sentence $\Psi$  if and only if it is closed under (finite) homomorphisms.
\end{theorem}

\begin{definition}
	We define  $\mathbb{HSO}$ as the set of  $\mbox{$\mathbb{SO}$}$ sentences of the form  $(\Psi^{\mathrm{shom} }) ^{\mathrm{sup}}$ for any $\mbox{$\mathbb{SO}$}$ sentence $\Psi$.
\end{definition}

It is clear that membership in $\mathbb{HSO}$ is decidable. We can now formulate the main result of this section, as a direct consequence from \Cref{thm:normalformSO} and the fact that $(\Psi^{\mathrm{shom} }) ^{\mathrm{sup}}$ is polytime-computable from $\Psi$.

\begin{corollary} Every (finitely) homclosed $\mbox{$\mathbb{SO}$}$ sentence $\Phi$ is equivalent (on finite structures) to a $\mathbb{HSO}$ sentence $\Psi$ which can be computed from $\Phi$ in polynomial time.
\end{corollary}

\section{Characterizability of Homclosures}\label{sec:characterizability}

In case a sentence $\Phi$ under consideration is not homclosed, one might still be interested in the (finite) homclosure $\homclffin{\getffinmodels{\Phi}}$ of its (finite) models. In particular one might want to (finitely) characterize it logically, that is, find some sentence $\Psi$
whose set of (finite) models is precisely $\Phi$'s (finite) homclosure.

We start with the observation that even for very basic $\FO_{=}$ sentences contained in very restricted fragments, it might be impossible to characterize their homclosure within $\FO_{=}$.

\newcommand{\vspace{-6.2pt}}{\vspace{-6.2pt}}

\begin{definition}\label{infpath}
Let $\Phi_{\infty}$ denote the $\{\sig{P}\}$-sentence
$
\forall x \exists y. \sig\sig{P}(x,y).
$
\end{definition}
\vspace{-6.2pt}

We note that $\Phi_{\infty}$ is simultaneously contained in $\mbox{$\mathbb{GFO}_{=}$}$, $\FO^\mathbbm{2}$, $\mbox{$\forall\hspace{-4.5pt}\forall$}\mbox{$\exists\hspace{-4.5pt}\exists$}\mathbb{FO}$ and $\mbox{$\mathbb{TGD}$}$.
$\homcl{\getmodels{\Phi_{\infty}}}$ consists of all structures containing an infinite $\sig{P}{}$-path.
In the finite, this condition is equivalent to containing a directed $\sig{P}{}$-cycle. Identifying such structures is \textsc{NLogSpace}-complete, hence not expressible in $\FO_{=}$~\cite{FurstSS84}.

\begin{proposition}[restate=notFO, name=]\label{notfo}
$\homcl{\getmodels{\Phi_{\infty}}}$ cannot be characterized within $\FO_{=}$.
\end{proposition}
\vspace{-6.2pt}

Given that homclosures are not guaranteed to be characterizable in $\FO_{=}$ even for very inexpressive $\FO_{=}$ fragments, we might ask whether one can at least tell sentences that have a $\FO_{=}$-characterizable homclosure from those that do not.

$\left.\right.$\\[-1.5ex]
\probbox{
	\textbf{Problem:} $\mathrm{ExCharHomCl}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}^\mathbb{L}$\\
	\textbf{Input:} $\tau$, $\tau$-sentence $\Phi$.\\
	\textbf{Output:} \textsc{yes}, if $\getffinmodels{\Psi} = \homclffin{\getffinmodels{\Phi}}$ for some $\mathbb{L}$-sen\-tence $\Psi$, \textsc{no} otherwise.
}
\\

It turns out the answer is no. Also, there is no stronger logic capable of characterizing the homclosures of all $\FO_{=}$ sentences, nor one that would facilitate $\mathrm{ExCharHomCl}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}$.

\begin{theorem}[restate=ExCharHomA, name=]
$\mathrm{ExCharHomCl}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}^\mathbb{L}$ is undecidable for $\FO_{=}$ sentences whenever $\mathbb{L}$ is a non-degenerate logic with a decidable model checking problem.
\end{theorem}

\begin{theorem}[restate=ExCharHomB, name=]
	$\mathrm{ExCharHomCl}_{\scaleobj{0.8}(\!\,\fin\,\!\scaleobj{0.8})}^\mathbb{L}$ is undecidable for $\mbox{$\mathbb{TGD}$}$ sentences whenever $\mathbb{L}$ is a logic able to express $\cq{\mathfrak{F}}$ and having a decidable model checking problem.
\end{theorem}
\vspace{-6.2pt}

After establishing these negative results, we turn to the other end of the spectrum to identify cases where the homomorphism closure is guaranteed to be characterizable in $\mbox{$\FO_{=}^\mathbbm{2}$}$ and thus -- as a consequence of the homomorphism preservation theorems -- even in $\mbox{$\Ex^*\FO^+_{=}$}$. For $\mbox{$\Ex^*\Al^*\FOe$}$, the Bernays-Schönfinkel class, this is an easy consequence of the existence of ``small'' induced submodels.

\begin{proposition}[restate=EAFOinEPO, name=]
	Every $\mbox{$\Ex^*\Al^*\FOe$}$ sentence $\Phi$ satisfies $\homcl{\getmodels{\Phi}} = \homcl{\getfinmodels{\Phi}}$ and one can effectively compute a $\mbox{$\Ex^*\FO^+_{=}$}$ sentence $\Psi$ with $\homcl{\getmodels{\Phi}}=\getmodels{\Psi}$.
\end{proposition}
\vspace{-6.2pt}

Using descriptive complexity theory \cite{DBLP:books/daglib/0095988}, this implies a very low data complexity of checking hom\-closure membership.

\begin{corollary}
	For any fixed $\mbox{$\Ex^*\Al^*\FOe$}$ sentence $\Phi$, checking membership in $\homcl{\getffinmodels{\Phi}}$ is in \textsc{AC}$^0$ in the size of the structure.
\end{corollary}
\vspace{-6.2pt}

Now, after establishing the extremal cases (of characterizability failing altogether vs. it succeeding already within $\mbox{$\Ex^*\FO^+_{=}$}$) we investigate the middle ground in between: the fragments \mbox{$\Ex^*\Al\Al\Ex^*\FO$}{}, \mbox{$\FO_{=}^\mathbbm{2}$}{}, \mbox{$\mathbb{TGF}$}{}, \mbox{$\mathbb{GFO}_{=}$}{}, and \mathbb{GNFO}_{=}{}. By \Cref{the:arb-sameas-fin}, we know that $\homclfin{\getmodels{\Phi}}=\homclfin{\getfinmodels{\Phi}}$ for every sentence $\Phi$ in any of these logics. Therefore, any sentence characterizing $\homcl{\getmodels{\Phi}}$ will also finitely characterize $\homclfin{\getfinmodels{\Phi}}$. Hence, we will next describe how to characterize $\homcl{\getmodels{\Phi}}$ for the considered fragments. The task of characterizing $\homcl{\getfinmodels{\Psi}}$ is slightly different and will be discussed thereafter.

It is helpful to study projective homclosure characterizations.

\begin{definition}
	For logics $\mathbb{L}, \mathbb{L}' \subseteq \mbox{$\mathbb{SO}$}$, we say $\mathbb{L}'$ \emph{homcaptures} $\mathbb{L}$ if for every $\tau$ and $\mathbb{L}$ $\tau$-sentence $\Phi$ there exist some $\sigma$ and a $\mathbb{L}'$ $\tau{\uplus}\sigma$-sentence $\Psi$ such that  $\homcl{\getmodels{\Phi}} = \getmodels{\Psi}|_{\tau}$.
\end{definition}
\vspace{-6.2pt}

Note that whenever a logic $\mathbb{L}'$ homcaptures a logic $\mathbb{L}$, it follows that for any $\mathbb{L}$ sentence $\Phi$, we find an $\mbox{$\mbox{$\bex$}{}\SO$}(\mathbb{L}')$ sentence characterizing $\Phi$'s homclosure, where $\mbox{$\mbox{$\bex$}{}\SO$}(\mathbb{L}')$ describes the fragment of $\mbox{$\mathbb{SO}$}$ sentences led by second-order existential quantifiers followed by an $\mathbb{L}'$ sentence.

We will next give a description of a generic type-based approach toward homcapturing results, which will be applicable to all mentioned logics with slight variations in the details.

Fixing a finite signature $\tau$, we let \emph{$n$-types} denote maximal consistent sets $\mathfrak{t}$ of literals (i.e., negated and un\-ne\-ga\-ted atoms) using all constants from $\tau$ and a finite collection of variables $v_1,\ldots,v_n$ (denoted $\bold{v}$) disjoint from the variables used in the considered sentence.
For convenience, we identify the (necessarily finite) set $\mathfrak{t}$ with $\bigwedge \! \mathfrak{t}$.
We say an $n$-type $\mathfrak{t}$ is \emph{realized} by an $n$-tuple $\bold{a} = (a_1,\ldots,a_n) \in A^n$ of domain elements of a $\tau$-structure $\mathfrak{A}$, if $(\mathfrak{A},\{v_i \mapsto a_i\}) \models \mathfrak{t}$. We say $\mathfrak{t}$ is \emph{realized} ($k$ times) in $\mathfrak{A}$ if it is realized by ($k$ distinct) tuples of $\mathfrak{A}$. Note that every tuple $\bold{a}$ realizes one unique type, which entirely characterizes the substructure of $\mathfrak{A}$ induced by all the elements of $\bold{a}$ together with all elements denoted by constants.
Our approach makes use of the fact that for several logics, many questions regarding a structure can be answered, if one knows what types of a certain kind are realized therein. On a generic level, we assume there is a function that, given a $\tau$-sentence $\Phi$ yields a finite set $\mathcal{E}$ of \emph{eligible types} (possibly containing $n$-types of varying $n$), which are sufficient for our purposes. Then, given a $\tau$-structure $\mathfrak{A}$, we let its \emph{type summary} $\mathcal{E}(\mathfrak{A})$ denote the pair $(\mathcal{E}_\text{+},\mathcal{E}_!)$ where $\mathcal{E}_\text{+}$ ($\mathcal{E}_!$) consists of those types from $\mathcal{E}$ realized (exactly once) in $\mathfrak{A}$.\footnote{In fact, $\mathcal{E}_!$ is only needed for the $\mbox{$\FO_{=}^\mathbbm{2}$}$ case in order to deal with the phenomenon of so-called ``kings'', i.e., $1$-types forced to be unique in models. For the other logics considered, $\mathcal{E}_\text{+}$ suffices.}
Furthermore, the \emph{model summary} $\getsummary{\Phi}$ of a sentence $\Phi$ is defined by $\{\mathcal{E}(\mathfrak{A}) \mid \mathfrak{A} \in \getmodels{\Phi}\}$, which is a finite set by assumption.

We will extend our signature by a set $\sigma$ of \emph{type predicates}, containing an $n$-ary predicate symbol $\sig{Tp}_\mathfrak{t}$ for every eligible $n$-type $\mathfrak{t} \in \mathcal{E}$.
Given a $\tau$-structure $\mathfrak{A}$ and a set $\mathcal{E}$ of eligible types over $\tau$, the \emph{$\mathcal{E}$-adornment} of $\mathfrak{A}$, denoted $\mathfrak{A}\cdot\mathcal{E}$ is the $\tau\uplus\sigma$-structure expanding $\mathfrak{A}$ such that
$\sig{Tp}_\mathfrak{t}^{\mathfrak{A}\cdot\mathcal{E}} = \{ \bold{a} \mid \bold{a} \text{ realizes } \mathfrak{t} \text{ in } \mathfrak{A} \}$. In a way, $\mathcal{E}$-adornments materialize the information regarding relevant types in a model. While this information is obviously redundant in the model itself, we will make good use of it when characterizing a model's homomorphic targets.

Given a $\tau$-sentence $\Phi$ (which we presume to be in some normal form with bounded quantifier alternation), we will construct a $\tau\uplus\sigma$-sentence $\Psi$ that (projectively) identifies those $\mathfrak{B}$ into which some model $\mathfrak{A}$ of $\Phi$ has a homomorphism $h\colon\mathfrak{A} \mathrel{{\to}} \mathfrak{B}$, using the following idea: assuming such an $h$ exists, then it will also serve as homomorphism from $\mathfrak{A}\cdot\mathcal{E}$ to $\mathfrak{B}\cdot h(\mathfrak{A}\cdot\mathcal{E}|_\sigma)$ denoting the structure $\mathfrak{B}'$ expanding $\mathfrak{B}$ by letting $\sig{Tp}_\mathfrak{t}^{\mathfrak{B}'} = \{ (h(a_1),\ldots,h(a_n)) \mid (a_1,\ldots,a_n) \in \sig{Tp}_\mathfrak{t}^{\mathfrak{A}\cdot\mathcal{E}} \}$, that is, where all type information materialized in $\mathfrak{A}$ is transferred to $\mathfrak{B}$ along $h$. In fact, $\Psi$ is then built in a way that its models are precisely such $\mathfrak{B}'$.
Thereby, one integral part of $\Psi$ is a conjunct $\Psi_\mathrm{hom}$ ensuring that types are mapped to $\mathfrak{B}$ in a way compatible with the homomorphism condition, i.e., that at least all positive literals postulated by the type are indeed present:
\begin{equation}
\Psi_\mathrm{hom} = \!\bigwedge_{\mathfrak{t} \in \mathcal{E}} \!\forall \bold{v}.\big( \sig{Tp}_\mathfrak{t}(\bold{v}) \Rightarrow \smallbigwedge \{\alpha \tight{\in} \mathfrak{t} \mid \alpha \text{ positive lit.}\} \big)
\end{equation}
Moreover, we require that the collection of ``transferred type atoms'' found in $\mathfrak{B}'$ corresponds to the type summary of some model. To this end, we include in $\Psi$ the case distinction
\begin{equation}
\bigvee_{(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)},
\end{equation}
where each $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ details existence and relationships between the mapped types. Some of the conditions specified in $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ are generically derived from $(\mathcal{E}_\text{+},\mathcal{E}_!)$, others are obtained by translating constraints from $\Phi$ into ``type language'', expressed by type atoms.
By construction, the sentence $\Psi$ thus obtained holds in some type-adorned structure $\mathfrak{A}\cdot\mathcal{E}$ if and only if $\mathfrak{A} \in \getmodels{\Phi}$. Also, its satisfaction is preserved under ``type-faithful'' homomorphisms  $h\colon\mathfrak{A}\cdot\mathcal{E} \mathrel{{\to}} \mathfrak{B}'$ as described above, thus ensuring $\homcl{\getmodels{\Phi}} \subseteq \getmodels{\Psi}|_{\tau}$.
The other direction $\homcl{\getmodels{\Phi}} \supseteq \getmodels{\Psi}|_{\tau}$ is shown by taking a model $\mathfrak{B}' \in \getmodels{\Psi}$, removing all information about $\tau$, and ``unfolding'' or  ``unraveling'' it such that, in the resulting structure $\mathfrak{A}'$, the diverse $\sig{Tp}_\mathfrak{t}$ instances do not provide contradicting information about the $\tau$-connections between their arguments. This allows for reconstructing the interpretations of the original signature elements $\tau$ from the $\sig{Tp}_\mathfrak{t}$ instances. After forgetting the latter, we have arrived at our wanted $\mathfrak{A} \in \getmodels{\Phi}$.

Applying the described strategy yields the following theorem.

\begin{theorem}[restate=allhomcaptures, label=thm:allhomcaptures, name=]\label{thm:homcapture}
	\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.3ex]
		\item $\mbox{$\FO_{=}^\mathbbm{2}$}$ homcaptures itself.
		\item $\mbox{$\mathbb{TGF}$}$ homcaptures itself and $\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$.
		\item $\mbox{$\mathbb{GFO}_{=}$}$ homcaptures itself and $\mathbb{GNFO}_{=}$.
	\end{enumerate}
\end{theorem}

As an example for all these logics, note that the hom\-clo\-sure of $\Phi_\infty$ from \Cref{infpath},
is projectively characterized by
\begin{equation}
\exists x.\big(\hspace{1pt}\sig{Lv}(x)\hspace{1pt}\big) \wedge \forall x.\big(\, \sig{Lv}(x) \Rightarrow \exists y. (\hspace{1pt}\sig{P}(x,y) \wedge \sig{Lv}(y)\hspace{1pt})\,\big).
\end{equation}

In view of our earlier discussion, this ensures that all these logics admit homclosure characterization in $\mbox{$\mbox{$\bex$}{}\SO$}$, and that the data complexity of homclosure membership is in \textsc{NP} \cite{fagingeneralized}.

\begin{corollary}
	For any fixed \mbox{$\FO_{=}^\mathbbm{2}$}, \mbox{$\mathbb{TGF}$}{}, \mbox{$\Ex^*\Al\Al\Ex^*\FO$}, \mbox{$\mathbb{GFO}_{=}$}{} or \mathbb{GNFO}_{=}{} sentence $\Phi$, checking $\mathfrak{A} \in \homcl{\getmodels{\Phi}}$

	is in \textsc{NP}.
\end{corollary}

We next complement these $\textsc{NP}$-membership results by providing matching lower bounds even for much weaker logics.

\newcommand{ \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\! }{ \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\! }
\newcommand{\,{\wedge}\,}{\,{\wedge}\,}
\newcommand{\,{\vee}\,}{\,{\vee}\,}

\begin{definition}[restate=phithreesat, name=]\label{def: 3SAT}
	Given an instance of 3SAT $\mathcal{S} = \{C_1, \ldots, C_n\}$ consisting of $n$ clauses each containing 3 literals over propositional variables $p_1,\ldots,p_m$, we define the structure $\mathfrak{A}_{\mathcal{S}}$ by
	%
	\begin{eqnarray}
		A_\mathcal{S} & {\!\!\!\!=\!\!\!\!} & \{a_i \mid 1\leq i\leq n\tight{+}1\} \cup \{b_i, b'_i \mid 1\leq i\leq m\}\ \ \ \ \ \ \ \\
		\sig{First}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{a_1\}\\
		\sig{CLst}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{a_i \mid 1\leq i\leq n\}\\
		\sig{Nil}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{a_{n+1}\}\\
		\sig{Next}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{(a_i,a_{i+1}) \mid 1\leq i\leq n\}\\
		\sig{Lit}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{(a_i,b_j) \mid p_j \in C_i\} \cup \{(a_i,b'_j) \mid \neg p_j \in C_i\}\\
		\sig{Sel}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{b_i, b'_i \mid 1\leq i\leq m\}\\
		\sig{Cmp}^{\mathfrak{A}_{\mathcal{S}}} & {\!\!\!\!=\!\!\!\!} & \{(b_i,b_j),(b'_i,b'_j),(b_i,b'_k),(b'_i,b_k) \mid i\not= k\}
	\end{eqnarray}
	We let $\Phi_\mathrm{3SAT}$ be the sentence containing the conjunction of the following sentences (leading universal quantifier omitted):
\begin{eqnarray}
	& & \!\!  \exists x. \sig{First}(x)  	\label{Def14: 1}\\
	%
	\sig{First}(x)
	 \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\!
	\sig{CLst}(x)\ \ \ \ \ \label{Def14: 2} \\
	%
	\sig{CLst}(x)
	 \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\!
	\exists y. \sig{Next}(x,y) \,{\wedge}\, \big(\sig{CLst}(y) \,{\vee}\, \sig{Nil}(y)\big)\ \ \ \ \   \label{Def14: 3} \\

	\sig{CLst}(x)
	 \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\!
	\exists y. \sig{Lit}(x,y)  \wedge \sig{Sel}(y)   \label{Def14: 4}
	\\
	%
	\sig{Sel}(x) \,{\wedge}\, \sig{Sel}(y)
	 \!\! & {\!\!\!\!\!\!{\Rightarrow}\!\!\!\!\!\!} &  \!\!
	\sig{Cmp}(x,y).   \label{Def14: 5}
\end{eqnarray}
\end{definition}
Obviously, $\Phi_\mathrm{3SAT}$ is contained in constant-free, equality-free $\FO^\mathbbm{2}$ (and therefore in $\mbox{$\FO_{=}^\mathbbm{2}$}$ and \mbox{$\mathbb{TGF}$}). It can be
rewritten into constant-free, equality-free $\mbox{$\bal$}\Al\mbox{$\bex$}\Ex\mathbb{FO}$ (and therefore into
$\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$). Moreover, for any set $\mathcal{S}$ of $3$-clauses, satisfiability of the 3SAT instance $\bigwedge_{\{\ell_1,\ell_2,\ell_3\}\in \mathcal{S}} \ell_1 \vee \ell_2 \vee \ell_3$  coincides with $\mathfrak{A}_\mathcal{S} \in \homcl{\getffinmodels{\Phi_\mathrm{3SAT}}}$. Hence we obtain the following statement, providing matching lower bounds.

\begin{proposition}[restate=NPhardFOprop, name=]
	Checking homclosure membership is \textsc{NP}-hard for constant-free, equality-free $\FO^\mathbbm{2}$ and $\mbox{$\bal$}\Al\mbox{$\bex$}\Ex\mathbb{FO}$ with predicate arity $\leq 2$.
\end{proposition}

Note that this settles the case of the data complexity of homclosure membership for any logic between $\FO^\mathbbm{2}$ / $\mbox{$\bal$}\Al\mbox{$\bex$}\Ex\mathbb{FO}$ on the lower and  $\mbox{$\FO_{=}^\mathbbm{2}$}$ / $\mbox{$\mathbb{TGF}$}{}$ / $\mbox{$\Ex^*\Al\Al\Ex^*\FO$}$ on the upper end, showing that one cannot hope for characterizability in a logic having a lower data complexity of model checking. It does not provide a lower bound for $\mbox{$\mathbb{GFO}_{=}$}$ or $\mathbb{GNFO}_{=}$, though. As it turns out, we can in fact do better for these\textellipsis

Given a $\mathbb{GNFO}_{=}$ sentence $\Phi$, let $\Psi$ be the $\mbox{$\mathbb{GFO}_{=}$}$ sentence projectively characterizing $\homcl{\getmodels{\Phi}}$ constructed as described before.
Then we obtain $\homcl{\getmodels{\Phi}} = \getmodels{\exists \sigma.\Psi}$ and also observe
\begin{align}
	\exists \sigma.\Psi & = \exists \sigma . \Big(\Psi_\mathrm{hom} \wedge \hspace{-1ex} \bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!)}\Big) \\
	 & \equiv \hspace{-1ex} \bigvee_{\scriptscriptstyle(\mathcal{E}_\text{+},\mathcal{E}_!)\in \getsummary{\Phi}} \hspace{-1ex} \exists \sigma . \big(\Psi_{\!(\mathcal{E}_\text{+},\mathcal{E}_!)} \wedge \Psi_\mathrm{hom} \big).
\end{align}
Thoroughly inspecting $\exists \sigma.(\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)} \wedge \Psi_\mathrm{hom})$, we find that it can be equi\-valently rewritten into the following $\FO_{=}$ sentence with least fixed points over simultaneous inductive definitions for ``complement predicates'' $\overline{\sig{Tp}}_\mathfrak{t}$ from a signature $\overline{\sigma}$:
\begin{equation}
\bigwedge_{\mathfrak{t}\, \in \,\mathcal{E}_\text{+}} \!\exists \bold{x}.\neg\Big[\textbf{lfp}_{\overline{\sig{Tp}}_\mathfrak{t}} \big\{\, \overline{\sig{Tp}}_{\mathfrak{t}'}(\bold{y}) \leftarrow \xi_{\overline{\sig{Tp}}_{\mathfrak{t}'}}[\bold{y}] \,\, \big|\,  \mathfrak{t}' \tight{\in} \mathcal{E}\,\big\}\Big](\bold{x}),
\end{equation}
where the $\xi_{\overline{\sig{Tp}}_\mathfrak{t}'}$ are $\FO_{=}$ $\tau\uplus\overline{\sigma}$-formulae with only positive occurrences of type atoms, obtained from aggregating the bodies of the contrapositions of the implications in $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$.\footnote{Conceptually, this equivalent transformation can be explained as follows: for any two models $\mathfrak{B}_1$, $\mathfrak{B}_2$ of $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$ with $\mathfrak{B}_1|_\tau = \mathfrak{B}_2|_\tau$, the struc\-ture $\mathfrak{B}_1 {\cdot} \mathfrak{B}_2$ obtained as the $\sigma$-expansion of $\mathfrak{B}_1|_\tau$ by $\sig{Tp}_\mathfrak{t}^{\mathfrak{B}_1 {\cdot} \mathfrak{B}_2} = \sig{Tp}_\mathfrak{t}^{\mathfrak{B}_1} {\cup} \sig{Tp}_\mathfrak{t}^{\mathfrak{B}_2}$ for all eligible $\mathfrak{t}$ is also a model. Hence, for every $(\mathcal{E}_\text{+},\mathcal{E}_!)$-compatible $\tau$-structure $\mathfrak{B}$, there is a ``maximal $\sigma$-expansion'' $\mathfrak{B}^*$ satisfying $\Psi_{(\mathcal{E}_\text{+},\mathcal{E}_!)}$, which can be deterministically obtained in a type-elimination like process, via a least fixed-point computation over predicates $\overline{\sig{Tp}}_{\mathfrak{t}}$ that express exactly the absence of ${\sig{Tp}}_{\mathfrak{t}}$. This spares us the ``guessing'' of type relations via $\exists \sigma$.}
Simultaneous induction can in turn be expressed using plain least-fixed-point logic \cite{GurevichS86}, therefore $\Psi$ as a whole can be expressed in first-order least-fixed-point logic denoted $\FO_{=}^\mathbf{lfp}$ (sometimes also referred to as LFP or FO+LFP). Using the fact that evaluating $\FO_{=}^\mathbf{lfp}$ sentences over structures can be done in polynomial time \cite{Immerman82,Vardi82}, we obtain an improved result regarding the data complexity of homclosure membership.

\begin{theorem}[restate=GNFOinLFP, name=]\label{sorpresa}
Homclosures of $\mathbb{GNFO}_{=}$ and $\mbox{$\mathbb{GFO}_{=}$}$ sentences can be characterized in $\FO_{=}^\mathbf{lfp}$. Thus, for a fixed $\mathbb{GNFO}_{=}$ or $\mbox{$\mathbb{GFO}_{=}$}$ sentence $\Phi$, checking $\mathfrak{A} \in \homcl{\getmodels{\Phi}}$ is \textsc{P}-complete.
\end{theorem}

As a minimalistic example, consider the $\mbox{$\mathbb{GFO}_{=}$}{}$ sentence $\Phi_\infty$ from \Cref{infpath}, whose homclosure cannot be characterized in $\FO_{=}$ (see \Cref{notfo}),
but by the $\FO_{=}^\mathbf{lfp}$ sentence
\begin{equation}
\exists x.\neg\Big[\textbf{lfp}_{\sig{Cds}} \big\{ \sig{Cds}(y) \leftarrow  \forall z. \big(\sig{P} (y,z) \Rightarrow \sig{Cds}(z)\big) \big\}\Big](x),
\end{equation}
where the fixed point predicate $\sig{Cds}$ identifies ``cul-de-sac'' elements in the given $\{\sig{P}\}$-structure.

\section{Preliminaries}

We assume the reader to be familiar with standard notions regarding model theory, first- and second-order logic, decidability, and complexity theory.

\noindent\textbf{Structures and Homomorphisms.}\quad
We let capital Fraktur letters denote structures and the corresponding capital Roman letters their domains; i.e., $A$ denotes the domain of ${\mathfrak A}$.
We assume that structures have non-empty domains. A structure is called finite
if its domain is finit
. We work with signatures $\tau$ that consist of finitely many constant and predicate symbols (written in typewriter font, often simply called \textsl{constants} and \textsl{predicates} for brevity), and let $\text{ar}(\sig{P})$ denote the arity of a predicate $\sig{P} \in \tau$.
For convenience, we assume that our signatures contain at least one constant symbol; this is not a severe restriction since we may always add a new constant symbol to the signature without affecting our results. The \emph{size} $|{\mathfrak A}|$ of a finite $\tau$-structure ${\mathfrak A}$ is the number of bits needed to represent ${\mathfrak A}$ up to isomorphism, and bounded by
$(|\tau|+1)(|A|+1)^{m+1}$ where $m$ is the maximal arity of the predicates in $\tau$.

A \emph{homomorphism} $h \colon {\mathfrak A} \to {\mathfrak B}$ from a \mbox{$\tau$-structure} ${\mathfrak A}$ to a \mbox{$\tau$-structure} ${\mathfrak B}$ is a function $h \colon A \to B$
where

\vspace{-1ex}
\begin{itemize}[itemindent=0ex, leftmargin=2ex, partopsep=0ex]
\item for every predicate symbol $\sig{P} \in \tau$,
$(a_1,\dots,a_{\text{ar}(\sig{P})}) \in \sig{P}^{{\mathfrak A}}$ implies $\big (h(a_1),\dots,h(a_{\text{ar}(\sig{P})}) \big) \in \sig{P}^{{\mathfrak B}}$, and
\item for every constant symbol $\sig{c} \in \tau$, we have
$h(\sig{c}^{{\mathfrak A}}) = \sig{c}^{{\mathfrak B}}$.
\end{itemize}
\vspace{-1ex}

A homomorphism $h \colon {\mathfrak A} \to {\mathfrak B}$ is called \emph{strong} if for every predicate symbol $\sig{P} \in \tau$ we have
$(a_1,\dots,a_{\text{ar}(\sig{P})}) \in \sig{P}^{{\mathfrak A}}$ \emph{exactly if}
$\big (h(a_1),\dots,h(a_{\text{ar}(\sig{P})}) \big) \in \sig{P}^{{\mathfrak B}}$.
We use the common symbols $\mathrel{{\hookrightarrow}}$ and $\mathrel{{\to\hspace{-0.8ex}\!\!\!\to}}$ for injective and surjective homomorphisms, respectively, and add a horizontal stroke ($\str\mathrel{{\to}}$, $\mathrel{{\str{\injhom}}}$, $\mathrel{{\str[0.6ex]{\surhom}}}$) when they are strong.
Injective strong homomorphisms are also called \emph{embeddings}.

Given a class $\mathcal{C}$ of $\tau$-structures, let $\homcl{\mathcal{C}}$ denote the \emph{homomorphism closure of $\mathcal{C}$}, i.e., the class of all $\tau$-structures into which some structure $\mathfrak{A} \in \mathcal{C}$ has a homomorphism. We use $\mathcal{C}^{\cl{\str{\mathrel{{\hookrightarrow}}}}}$ and $\mathcal{C}^{\cl{\mathrel{{\to\hspace{-0.8ex}\!\!\!\to}}}}$ analogously.
We write $\homclfin{\mathcal{C}}$
for the class obtained by removing all infinite structures from $\homcl{\mathcal{C}}$.

Given a $\tau$-structure $\mathfrak{A}$ and some $\sigma \subseteq \tau$, let
$\mathfrak{A}|_\sigma$ denote the $\sigma$-reduct of $\mathfrak{A}$. Moreover, for some constant-free signature $\rho$ disjoint from $\tau$, we let $\mathfrak{A}\cdot{\widehat\rho}$ denote the $\tau{\uplus}\rho$-structure expanding~$\mathfrak{A}$ in which every element $\sig{P}$ of $\rho$ is mapped to the full relation $A^{\text{ar}(\sig{P})}$. Likewise, we let $\mathfrak{A}\cdot{\widecheck\rho}$ denote the \mbox{$\tau{\uplus}\rho$-structure} expanding $\mathfrak{A}$ in which every element of $\rho$ is mapped to the empty relation.

For a signature $\rho$ of only constants, let $\hat{\mathfrak{O}}_\rho$
denote the one-element $\rho$-structure (i.e., the up-to-isomorphism unique structure with all constants mapped to the only element), while $\check{\mathfrak{O}}_\rho$ denotes the $|\rho|$-element $\rho$-structure where each constant is interpreted separately.
For a signature $\tau=\rho \uplus \sigma$ of constants $\rho$ and predicates $\sigma$, we let $\mathfrak{I}_\tau = \check{\mathfrak{O}}_\rho \cdot \widecheck{\sigma}$ and $\mathfrak{F}_\tau = \hat{\mathfrak{O}}_\rho \cdot \widehat{\sigma}$.\footnote{Note that $\mathfrak{I}_\tau$
has a homomorphism into every \mbox{$\tau$-structure}, and every \mbox{$\tau$-structure} has a homomorphism into $\mathfrak{F}_\tau$, i.e., $\homcl{\{\mathfrak{I}_\tau\}}$ is the class of all \mbox{$\tau$-structures}, whereas $\mathfrak{F}_\tau \in \homcl{\mathcal{C}}$ for every non-empty class $\mathcal{C}$ of \mbox{$\tau$-structures}.} We omit signature subscripts if they are clear from the context.

\noindent\textbf{Logics.}\quad
We give a brief description of the logics we study in this paper. By default, equality is not allowed in a logic ${\mathbb L}$;
the variant of ${\mathbb L}$ where equality $=$ is allowed is denoted by ${\mathbb L}_=$. \emph{First-order logic $(\FO_{=})$} formulae are built from atomic formulae using
existential quantification $\exists$, universal quantification $\forall$, negation $\neg$, conjunction $\wedge$, and disjunction $\vee$ in the usual way.
We use the symbol $\Rightarrow$ for implication and $\Leftrightarrow$ for equivalence as the usual shortcuts for better readability.
All the considered logics are fragments of \emph{second-order logic} (\mbox{$\mathbb{SO}$}),\footnote{As $=$ can be axiomatized in \mbox{$\mathbb{SO}$}, we do not distinguish \mbox{$\mathbb{SO}$}{} from $\mbox{$\mathbb{SO}$}_=$.} which extends first-order logic by \emph{second-order quantifiers}, of the form $\exists \sig{P}$ or $\forall \sig{P}$ for a predicate symbol $\sig{P}$. A formula's \emph{quantifier rank} is the maximal nesting depth of its quantifiers.

\begin{itemize}[itemindent=2ex, leftmargin=0ex]
\item A  \emph{term} is either a variable or a constant symbol (as per our assumption that the signature may contain constant symbols but no function symbols of arities greater than zero).
\item
We use bold variable/term/element symbols (e.g., $\bold{x}$, $\bold{y}$, or $\bold{t}$, or $\bold{a}$) to denote finite sequences of such entities (e.g., $x_1,\ldots, x_n$) of appropriate length.
Whenever order and multiplicity are irrelevant, we take the liberty to consider such sequences as sets, justifying expressions like $\bold{x} \cup \bold{y}$.
 \item
For a (sub)formula $\varphi$, we write $\varphi[\bold{x}]$ to indicate that all free first-order variables in $\varphi$ are from $\bold{x}$. We write $\varphi(\bold{x})$ to indicate a formula with free occurrences of $\bold{x}$ and use $\varphi(\bold{t})$ to denote $\varphi$ with all occurrences of free variables from $\bold{x}$ replaced by the corresponding element from $\bold{t}$.     \end{itemize}

We study the following
fragments of first-order logic:
\begin{itemize}[itemindent=2ex, leftmargin=0ex, partopsep=0ex]
\item
\emph{Prefix classes} of $\mathbb{FO}$ / $\FO_{=}$.
For these logics, we assume that the formulae are in prenex normal form and that the quantifier prefix is restricted by a regular expression, following
standard nomenclature as used by Börger, Grädel and Gurevich \cite{BorgerGG1997}.
\item
\emph{Existential positive $\mathbb{FO}$} ($\mbox{$\Ex^*\FO^+_{=}$}$). In this fragment, $\forall$ and $\neg$
are disallowed; however, the special sentence $\bot$  is allowed in order to express falsity (it could be read as empty disjunction). We obtain (Boolean) conjunctive queries ($\mbox{$\mathbb{CQ}$}$) from $\mbox{$\Ex^*\FO^+_{=}$}$ by disallowing $\vee$. The \emph{canonical query} for a finite structure $\mathfrak{A}$, denoted by $\cq{\mathfrak{A}}$,  is the \mbox{$\mathbb{CQ}$}{} sentence obtained by existentially quantifying over each variable $x_a$, for all $a \in A$, in
\begin{equation}
\bigwedge_{\sig{c}\in\tau} \sig{c} \,{=}\, x_{\sig{c}^\mathfrak{A}} \wedge \hspace{-3ex} \bigwedge_{{\sig{P} \in \tau,\, k= \text{ar}(\sig{P})}\atop{{(a_1,\ldots,a_k) \in \sig{P}^\mathfrak{A}}}} \hspace{-3ex}
\sig{P}(x_{a_1},\ldots,x_{a_k}).
\end{equation}
\item
\emph{The guarded fragment of $\FO_{=}\!$} ($\mbox{$\mathbb{GFO}_{=}$}$).
All occurrences of $\forall$ have the form
$\forall \bold{x}.(\sig{P}(\bold{y}) {\,\Rightarrow\,} \varphi[\bold{y}])$,
and all of $\exists$ the form
$\exists \bold{x}.(\sig{P}(\bold{y}) \wedge \varphi[\bold{y}])$
for $\bold{x} \subseteq \bold{y}$ and predicates $\sig{P}{}$.
This shape is called \emph{guarded quantification} and $\sig{P}(\bold{y})$ the respective \emph{guard}.\footnote{It is innocuous to
conjunctively add further atoms to the guard, as long as they use only variables from $\bold{x}$. We will consider such variants part of the  language; they can be \textsc{LogSpace}-transformed into the plain form. The same holds for unguarded quantification over formulae with just one free variable.}
\item
\emph{The triguarded fragment of} $\mathbb{FO}$ ($\mbox{$\mathbb{TGF}$}$). Every quantification over formulae with at least two free variables must be guarded.
\item
\emph{The guarded negation fragment of} $\FO_{=}$ ($\mathbb{GNFO}_{=}$). The symbol $\forall$ is disallowed
and every occurrence of $\neg$ must be in the form of
$\sig{P}(\bold{x}) \wedge \neg \varphi[\bold{x}]$.
\item
\emph{The $n$-variable fragment of} $\FO_{=}$ / $\mathbb{FO}$. All variables must be from $\{x_1,\ldots,x_n\}$.  As special cases we obtain the 2-variable fragment with equality ($\mbox{$\FO_{=}^\mathbbm{2}$}$) and without it ($\FO^\mathbbm{2}$); here we normally use the variable names $x$, $y$ instead of $x_1$, $x_2$.
\item
\emph{(Disjunctive) tuple-generating dependencies} (TGDs). A \emph{disjunctive TGD} is a $\mathbb{FO}$ sentence of the form
\begin{equation}
\forall \bold{x}.\varphi(\bold{x}) \Rightarrow \exists \bold{y}.\psi(\bold{x},\bold{y}),
\end{equation}
where
$\varphi$ is a (possibly empty) conjunction over atoms while $\psi$ is a non-empty disjunction over conjunctions of atoms.\footnote{Non-emptiness of disjunction is common in database theory and a deliberate choice: it ensures desirable properties like guaranteed satisfiability. Empty disjunction would make disjunctive TGDs as expressive as $\mathbb{FO}$.}
Note that for finite structures $\mathfrak{A}, \mathfrak{B}$, the formula $\cq{\mathfrak{A}} \Rightarrow \cq{\mathfrak{B}}$ can be easily transformed into an equivalent TGD (by pulling out the existential quantifiers of $\cq{\mathfrak{A}}$ thus turning them into universal ones, using that the variable sets of  $\cq{\mathfrak{A}}$ and $\cq{\mathfrak{B}}$ are disjoint), so we will consider it as such right away.

We obtain \mbox{$\mathbb{DTGD}$}{} (sentences) as finite conjunctions over disjunctive TGDs. Likewise, we obtain \mbox{$\mathbb{TGD}$}{} (sentences) as finite conjunctions over (non-disjunctive) TGDs, wherein the $\psi$ are plain conjunctions over atoms. As a middle ground between \mbox{$\mathbb{TGD}$}{} and \mbox{$\mathbb{DTGD}$}{}, we introduce \emph{mildly disjunctive TGD sentences} (\mbox{$\mathbb{MDTGD}$}) as sentences of the form $\Phi \vee \Psi$ where $\Phi \in \mbox{$\mathbb{TGD}$}$ and $\Psi \in \mbox{$\mathbb{CQ}$}$. Note that any \mbox{$\mathbb{MDTGD}$}{} sentence can be equivalently rewritten into \mbox{$\mathbb{DTGD}$}{} in polynomial time.
\end{itemize}

\emph{Existential \mbox{$\mathbb{SO}$}{}} ($\mbox{$\mbox{$\bex$}{}\SO$}$) is the fragment of \mbox{$\mathbb{SO}$}\ where all second-order quantifiers are existential and prenex

We apply the standard model-theoretic semantics.
For a sentence $\Phi$,
we let
	$\getmodels{\Phi}$ denote the class of all models of $\Phi$ and
	$\getfinmodels{\Phi}$ the class of all finite models of $\Phi$.
A sentence in some logic is (finitely) satisfiable if it has a (finite) model.
A logic has the \emph{finite model property (FMP)} if satisfiability and finite satisfiability coincide. \Cref{fig:main} gives results on the FMP for logics considered by us.
A sentence $\Phi$ \emph{(finitely) characterizes} a class $\mathcal{C}$ of structures, if
$\getffinmodels{\Phi} = \mathcal{C}$.
For $\tau' \subseteq \tau$, we say that a $\tau$-sentence $\Phi$ \emph{(finitely) projectively characterizes} a class $\mathcal{C}$ of $\tau'$-structures if
$\getffinmodels{\Phi}|_{\tau'}  = \mathcal{C}$.
A logic is \emph{non-degenerate} if there exists an unsatisfiable sentence $\Phi_\textbf{false}$.

\noindent\textbf{Tilings.}\quad
We introduce a variant of the $\mathbb{N} \times \mathbb{N}$ tiling problem, which serves as a versatile and useful vehicle for various subsequent undecidability arguments.

\begin{definition}[margin-constrained tiling problem]\label{def:tiling}
A \emph{(margin-constrained) domino system} $\mathcal{D} = (D,B,L,H,V)$ consists of a finite set $D$ of \emph{dominoes}, some of which are
\emph{bottom-margin}  dominoes $B \subseteq D$
and some \emph{left-mar\-gin}  ones $L \subseteq D$. We refer to $L \cap B$ as \emph{seed dominoes}.
The two binary relations $H,V \subseteq D \times D$ specify \emph{horizontal} and \emph{vertical compatibility}.\footnote{In the context of domino systems, it will be convenient to let $R\in \{H,V\}$ also denote {the} map $R \colon D \rightarrow 2^D$ defined by $R(x):= \{d\in D\mid (x,d)\in R\}$. The intended meaning will always be clear from the context.}

We call  $\mathcal{D} = (D,B,L,H,V)$ \emph{deterministic} if\\[-3ex]
\begin{enumerate}[itemindent=0ex, leftmargin=3ex,  itemsep=-0.8ex, topsep=0ex]
	\item
	there is at most one seed domino (i.e., $|B \cap L|\leq 1$),
	\item for every $d \in B$ there is at most one $e$ such that $(d,e) \in H$, and in this case $e \in B$,
	\item
	for every $d \in L$ there is at most one $e$ such that $(d,e) \in V$, and in this case $e \in L$, and
	\item

	for any $d_1,d_2 \in D$ there is at most one $e$ with $(d_1,e) \in H$ and $(d_2,e)\in V$.
\end{enumerate}
A $\mathcal{D}$-\emph{tiling} (of $\mathbb{N} \times \mathbb{N}$) is a function $t\colon \mathbb{N} \times \mathbb{N} \to D$ such that for any $k, \ell \in \mathbb{N}$ hold
$t(0,\ell) \in L$ and $t(k,0) \in B$ as well as
$\big(t(k,\ell),t(k+1,\ell)\big) \in H$ and $\big(t(k,\ell),t(k,\ell+1)\big) \in V$.

A tiling $t$ is \emph{ultimately periodic}, if there are natural numbers $k_\mathrm{init},k_\mathrm{period},\ell_\mathrm{init},\ell_\mathrm{period}$ such that, for every $k, \ell \in \mathbb{N}$,
\begin{itemize}[itemindent=0ex, leftmargin=1.8ex, itemsep=-0.5ex, labelsep=0.7ex, topsep=0ex]
	\item
	$t(k,\ell) = t(k+k_\mathrm{period},\ell)$ whenever $k\geq k_\mathrm{init}$ and
	\item
    $t(k,\ell) = t(k,\ell+\ell_\mathrm{period})$ whenever $\ell\geq \ell_\mathrm{init}$.
\end{itemize}
\vspace{-1ex}
\end{definition}

It is straightforward to see that for deterministic domino systems, tilings are unique if they exist.
Also note that the ``classical'' $\mathbb{N} \times \mathbb{N}$ tiling problem without margin constraints is a special case of this variant (choose $D = L = B$).

\begin{lemma}[restate=gridlemma, label=gridlemma, name=]
The following problems are both undecidable even for deterministic margin-constrained domino systems $\mathcal{D}$:
\begin{enumerate}[itemindent=0ex, leftmargin=3ex, itemsep=-0.5ex]
\item
Given $\mathcal{D}$, does there exist a $\mathcal{D}$-\emph{tiling}?
\item
Given $\mathcal{D}$, does there exist an ultimately periodic $\mathcal{D}$-\emph{tiling}?
\end{enumerate}
\end{lemma}

\section{Some Tools}\label{sec:tools}

\newcommand{\indss}[2]{[#1]_{#2}}
In this section, we present basic tools that will be used in the subsequent sections; we start
with the folklore technique of \emph{relativization} to make statements about a model's induced substructures.
In the following, let $\sig{U}{}$ denote a unary predicate.
Given a $\tau {\uplus} \{\sig{U}{}\}$-structure $\mathfrak{A}$
we write
$\indss{\mathfrak{A}}{\sig{U}{}}$ for the $\tau$-reduct of the substructure of $\mathfrak{A}$ induced by $\sig{U}{}^\mathfrak{A}$.

Given an $\mbox{$\mathbb{SO}$}$ $\rho{\uplus}\tau$-sentence $\Phi$ with constants $\rho$ and predicates $\tau \mathrel{\rotatebox[y=0.57ex]{180}{$\notin$}}\sig{U}$, let $\Phi^{\mathrm{rel}(\sig{U}{})}$ denote
the \emph{$\sig{U}{}$-relativization} of $\Phi$, defined as
\begin{equation}
\Phi^{\mathrm{guard}(\sig{U}{})} \wedge \bigwedge_{c \in \rho} \sig{U}{}(c),
\end{equation}
where $\Phi^{\mathrm{guard}(\sig{U}{})}$ is obtained from $\Phi$ by (inside-out) replacing all subformulae $\forall x.\varphi$ by $\forall x.(\sig{U}{}(x) \Rightarrow \varphi)$ and all subformulae $\exists x.\varphi$ by $\exists x.(\sig{U}{}(x) \wedge \varphi)$.
Relativization preserves many aspects of the sentence, such as the number of variables, the quantifier rank, and membership in the fragments $\mathbb{GFO}_=$, $\mathbb{GNFO}_{=}$, $\mbox{$\mathbb{TGF}$}$, $\mbox{$\FO_{=}^\mathbbm{2}$}$, $\mbox{$\mathbb{TGD}$}$, $\mbox{$\mathbb{DTGD}$}$, $\mbox{$\mathbb{MDTGD}$}$, $\FO_{=}$ (modulo some trivial syntactic equivalence-preserving transformations) as well as all prefix classes. Obviously, $\Phi^{\mathrm{rel}(\sig{U}{})}$ is \textsc{LogSpace}-computable from $\Phi$.
Moreover, the models of $\Phi^{\mathrm{rel}(\sig{U}{})}$ are precisely those $\rho{\uplus}\tau {\uplus} \{\sig{U}{}\}$-structures $\mathfrak{A}$ for which $\indss{\mathfrak{A}}{\sig{U}{}} \in \getmodels{\Phi}$.

Next, we introduce some machinery for labeling structures with numbers and using such endowed structures as compact representations of other structures.

\newcommand{\mathrm{tr}}{\mathrm{tr}}
\newcommand{\mathit{as}}{\mathit{as}}

Given a $\tau$-structure $\mathfrak{A}$ and a number $n\in \mathbb{N}$, an \emph{$n$-labeling of $\mathfrak{A}$} is a function $\lambda \colon  A \to \{1,\ldots,n\}$. We will then call $(\mathfrak{A},\lambda)$ an \emph{$n$-labeled structure}. If
$(\mathfrak{A},\lambda)$ satisfies $\lambda(\sig{c}^\mathfrak{A})=1$ for every constant
$\sig{c} \in \tau$, we call it \emph{constant-sole}.
Given an $n$-labeled $\tau$-structure $(\mathfrak{A},\lambda)$, its \emph{implicit representation} $\mathfrak{A}_\lambda$ is the $\tau {\uplus} \{\sig{Bit}^\lambda_0,\ldots,\sig{Bit}^\lambda_{\ell}\}$-structure with $\ell = \lceil\log_2 n \rceil$ expanding $\mathfrak{A}$ by $(\sig{Bit}^\lambda_i)^{\mathfrak{A}_\lambda} = \{a \mid \lfloor\lambda(a) / 2^i\rfloor \mbox{ is odd}\}$.

We next define $\FO_{=}$ formulae allowing to compare some natural number against the label of a domain element associated with some term $t$ in $\mathfrak{A}_\lambda$. Given some $m \in \{1,\ldots,n\}$, assume $b_1\cdots b_\ell \in \{0,1\}^\ell$ is the fixed-length binary representation of $m-1$ (i.e., $m-1 = \sum_{i=1}^\ell b_i\cdot 2^{\ell-i}$).
Then we use the following abbreviations for $\FO_{=}$ sentences:
\begin{eqnarray}
{}[\lambda(t) = m] & \!\!\!\!:=\!\!\!\! &\!\!\bigg(\!\!\!\smallbigwedge_{{\ 1\leq j \leq \ell}\atop{b_j = 0}}\!\!\!\! \neg \sig{Bit}^\lambda_j(t) \!\bigg) \!\wedge\! \bigg(\!\!\!\smallbigwedge_{{\ 1\leq j \leq \ell}\atop{b_j = 1}}\!\!\! \sig{Bit}^\lambda_j(t) \!\bigg),\\
{}[\lambda(t) \geq m] & \!\!\!\!:=\!\!\!\! &\!\!\!\bigwedge_{{1\leq j \leq \ell}\atop{b_j = 1}}\! \bigg( \sig{Bit}^\lambda_j(t)   \vee \! \smallbigvee_{{1 \leq i \leq j-1}\atop{b_i=0}} \sig{Bit}^\lambda_i(t) \bigg) .
\end{eqnarray}
These formulae's
size is polynomial in $\ell$, and, for some $\mathfrak{A}$ and a variable assignment $v\colon \!V\!\! \to\! A$, we get $\mathfrak{A}_\lambda,\hspace{-1pt}v \models [\lambda(t) \hspace{1pt}{=}\hspace{1pt} m]$ whenever $\lambda(t^{\mathfrak{A},v}) = m$; analogously for  $[\lambda(t) \geq m]$.

For a constant-sole $(\mathfrak{A},\lambda)$, let its \emph{unfolding} $\mathfrak{A}^\lambda$ be the $\tau$-structure with $A^\lambda = \{(a,i) \mid a\in A,\ 1\leq i\leq \lambda(a)\}$
where, for any $\sig{P} \in \tau$ of arity $k$, holds $((a_1,m_1), \ldots ,(a_k,m_k)) \in \sig{P}{}^{\mathfrak{A}^\lambda}$ iff
$(a_1, \ldots ,a_k) \in \sig{P}{}^{\mathfrak{A}^\lambda}$. We define $\pi \colon A^\lambda \to A$ via $(a,m) \mapsto a$.
Obviously, $\pi$ is a strong surjective homomorphism from $\mathfrak{A}^\lambda$ to $\mathfrak{A}$. Conversely, for any strong surjective homomorphism $h \colon \mathfrak{B} \to \mathfrak{A}$ where every $a\in A$ satisfies $|h^{-1}(a)|\leq n$ (i.e., the size of each element's pre-image is bounded by $n$) there exists some $\lambda \colon A \to \{1,\ldots,n\}$ with $\mathfrak{B} \cong \mathfrak{A}^\lambda$ (witnessed by an isomorphism $g \colon \mathfrak{B} \to \mathfrak{A}^\lambda$ such that $h = \pi \circ g$).

For variable labelings $\mathit{as} \colon V\to \{1,\ldots,n\}$, let $\mathit{as}^+(t)$ denote $\mathit{as}(t)$ if $t$ is a variable and $1$ if $t$ is a constant. We recursively define the functions $\mathrm{tr}^n_\mathit{as}$ mapping $\FO_{=}$ $\tau$-formulae in negation normal form to $\FO_{=}$ $\tau{\uplus} \{\sig{Bit}^\lambda_0,\ldots,\sig{Bit}^\lambda_{\lceil\log_2 n \rceil}\}$-formulae as follows:
\begin{eqnarray}
\mathrm{tr}^n_\mathit{as} (\sig\sig{P}(\bold{t})) &\!\!\!\!=\!\!\!\! & \sig\sig{P}(\bold{t}) \\
\mathrm{tr}^n_\mathit{as} (\neg \sig\sig{P}(\bold{t})) & \!\!\!\!=\!\!\!\! & \neg \sig\sig{P}(\bold{t}) \\
\label{eq: 5}\mathrm{tr}^n_\mathit{as} (t_1=t_2) & \!\!\!\!=\!\!\!\! & \left\{\begin{array}{ll}
	t_1=t_2 & \mbox{ if } \mathit{as}^+(t_1)=\mathit{as}^+(t_2) \\
	\bot & \mbox{ otherwise } \\
\end{array}\right.\\
\label{eq: 6}\mathrm{tr}^n_\mathit{as} (t_1\not=t_2) & \!\!\!\!=\!\!\!\! & \left\{\begin{array}{ll}
	t_1\not=t_2 & \mbox{ if } \mathit{as}^+(t_1)=\mathit{as}^+(t_2)  \\
	\top & \mbox{ otherwise } \\
\end{array}\right.\\
\mathrm{tr}^n_\mathit{as} (\varphi \wedge \psi) &\!\!\!\!=\!\!\!\! & \mathrm{tr}^n_\mathit{as} (\varphi) \wedge \mathrm{tr}^n_\mathit{as}(\psi) \\
\mathrm{tr}^n_\mathit{as} (\varphi \vee \psi) &\!\!\!\!=\!\!\!\! & \mathrm{tr}^n_\mathit{as} (\varphi) \vee \mathrm{tr}^n_\mathit{as}(\psi) \\
\label{eq: 11}\mathrm{tr}^n_\mathit{as} (\exists x.\varphi) &\!\!\!\!=\!\!\!\! & \!\!\!\bigvee_{1 \leq i \leq n}\!\!\! \exists x. [\lambda(x) \geq i] \wedge \mathrm{tr}^n_{\mathit{as} \cup \{x \mapsto i\}} (\varphi) \\
\label{eq: 12}\mathrm{tr}^n_\mathit{as} (\forall x.\varphi) &\!\!\!\!=\!\!\!\! & \!\!\!\bigwedge_{1 \leq i \leq n}\!\!\! \forall x. [\lambda(x) \geq i] \Rightarrow \mathrm{tr}^n_{\mathit{as} \cup \{x \mapsto i\}} (\varphi)\ \ \ \ \
\end{eqnarray}
\vspace{-8pt}

Defining $\mathrm{tr}^n$ by letting
$\mathrm{tr}^n(\Phi) = \mathrm{tr}^n_\emptyset (\mathrm{NNF}(\Phi))$, we obtain a lemma stating that $\mathrm{tr}^n$ truthfully rewrites sentences for their evaluation over implicit representations of unfoldings.

\begin{lemma}[restate=translemma, label=translemma, name=]
Let $\Phi$ be any $\FO_{=}$ sentence. Then $\mathfrak{A}^\lambda \models \Phi$ exactly if
$\mathfrak{A}_\lambda \models \mathrm{tr}^n(\Phi)$.
\end{lemma}
\vspace{-6pt}

Note that
the size of $\mathrm{tr}^n(\Phi)$
may be exponential in the size of $\Phi$.
On the positive side, $\mathrm{tr}^n$ preserves (negation-)guardedness, number of variables, quantifier prefixes, and quantifier rank.