Finitely accessible arboreal adjunctions and Hintikka formulae

Luca Reggio

Department of Computer Science

University College London, UK

Email<EMAIL_ADDRESS>
Colin Riba
ENS de Lyon, France

Email<EMAIL_ADDRESS>
fullResearch supported by the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837724.

Arboreal categories provide an axiomatic framework  in which abstract notions of bisimilarity and back-and-forth games can be defined.

They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions.
In the examples, equivalence of structures in various fragments of infinitary first-order logic (with finitely many variables) can be captured by transferring  bisimilarity along the adjunction.

In most applications, the categories involved  are  locally finitely presentable and the adjunctions finitely accessible.

Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic.

Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges' .

§ INTRODUCTION

Model comparison games are one of the few tools of
model theory still available in finite model theory, see e.g. [27, 20, 37].
Important examples include Ehrenfeucht-Fraïssé games
for first-order equivalence (possibly with bounded quantifier rank),
pebble games
for the finite-variable fragments,
and modal bisimulation games
for the modal fragment.

In this paper, we are interested in abstract notions
of model comparison games provided by
arboreal categories [6, 5],
an axiomatic framework for
games comonads.
Game comonads were introduced in [2]
as a categorical syntax-free approach to (finite) model theory,
in which
coalgebras encode
important combinatorial parameters of structures
(see [1] for a recent survey).
A crucial step for their development was taken
in [7, 8],
various back-and-forth games
(such as Ehrenfeucht-Fraïssé, pebble, and modal
bisimulation games)
were captured
by means of a refinement of
Joyal, Nielsen and Winskel's
notion of bisimulation via open maps [32, 33, 34].

The framework of arboreal categories takes as input a
class of monomorphisms, called embeddings, and provides concrete notions of bisimilarity and back-and-forth games.
An arboreal category $\A$ acts on an extensional category $\E$ (typically consisting of relational structures) via an arboreal adjunction:

\begin{equation*}
\label{eq:intro:arbadj}
\begin{tikzcd}
\A
\arrow[bend left]{r}[above]{\Ladj}
\arrow[phantom]{r}[description]{\bot}
& \E
\arrow[bend left]{l}[below]{R}
\end{tikzcd}
\end{equation*}

Transferring the bisimilarity relation along the adjunction,
we recover relevant logical equivalences of structures in $\E$.
In many applications, the categories involved are locally finitely presentable,
the arboreal adjunctions are finitely accessible
and the logics are
fragments of infinitary first-order logic $\Lang_{\infty, \omega}$.

In fact, the full logic $\Lang_{\infty, \omega}$ is captured by an arboreal adjunction.

Our main result yields a converse to this for
finitely accessible arboreal adjunctions.
Under mild assumptions,
we show that for each $M \in \E$, the ranks of the
back-and-forth games played in $R M$
are definable in $\Lang_{\infty,\omega}$.
Hence, arboreal bisimilarity cannot distinguish between $\Lang_{\infty,\omega}$-equivalent models.
This identifies the expressive power of finitely accessible arboreal adjunctions.
Note that while
the isomorphism type of a finite structure is
definable in finitary first-order logic,
Corollary 8 in [2] (for pebble games)
forces $\E$ to contain infinite objects in general,
on which $\Lang_{\infty,\omega}$ is strictly more expressive.

Our approach relies
on Gabriel-Ulmer duality
for locally finitely presentable categories [24]
(cf. also [12, 11]):
each locally finitely presentable category
is equivalent to the category of models
of a theory written
finite conjunctions
and provably unique existential quantifiers.

The back-and-forth games in $\A$
are closed in the usual sense,
and are equipped with a customary notion of ordinal
rank of positions
(cf. e.g. <cit.> or <cit.>).

Working with Coste's syntactic categories [17]
(cf. also <cit.>),
we devise “Hintikka formulae” for $R M$ for each ordinal rank,
along the usual pattern
(cf. e.g. <cit.> or <cit.>).
These formulae are then translated to formulae for $M$ in $\E$

interpretation induced by the right adjoint $R$.

In most applications, the class
of embeddings in $\A$
determined by
the class of substructure embeddings in $\E$.

The Hintikka formulae for $R M$ in $\A$
then depend on formulae over $\Ladj R M$ in $\E$.
To translate the infinitary theory of

$\Ladj R M$

to the infinitary theory of $R M$,

a slight generalisation of
Hodges' word-constructions [25, 26]
(cf. also <cit.>).

The paper is organised as follows:
after some preliminaries in <ref>,
in <ref>
we recall the basic theory of arboreal categories.
an overview of
locally presentable categories,
leading us to
the concept of
finitely accessible arboreal adjunction in <ref>.
Coste's syntactic categories
are presented in <ref>.
Our main results are
in <ref>–<ref>.
In the former, we devise Hintikka formulae for ordinal ranks,
assuming some definability of embeddings in $\A$.
In the latter, we use word-constructions to transfer  to $\A$
formulae defining substructure embeddings in $\E$.

Missing details are
in the appendices.

We assume the reader is familiar with the basic notions of category theory;
standard references include [38, 9].
Throughout, $\Set$ denotes the category of (small) sets and functions.
If $\cat C$ and $\cat D$ are categories,
$\funct{\cat C, \cat D}$ is the category of functors from $\cat C$ to $\cat D$,
with morphisms the natural transformations.
The functor category $\funct{\cat C^\op,\Set}$ is denoted by $\presh{\cat C}$
and referred to as the category of presheaves over $\cat C$.
Finally, a functor is finitary if it preserves filtered colimits.

§ PRELIMINARIES

§.§ Structures and infinitary first-order logic

We consider many-sorted,
possibly infinite, first-order signatures.
Such a signature $\Sig$
consists of
a set $\Sort(\Sig)$ of sorts
together with collections
$\Fun(\Sig)$ and $\Rel(\Sig)$
of, respectively,

and relation symbols.

We reserve the symbol $\sig$ for mono-sorted

relational signatures.

A $\Sig$-structure $M$
is a family of sets $(M(\sortbis) \mid \sortbis \in \Sort(\Sig))$

together with,
for each function symbol $f \in \Fun(\Sig)$,
a function $f^M$ interpreting $f$,
and for each relation symbol $R \in \Rel(\Sig)$,
a relation $R^M$ interpreting $R$.

A homomorphism of $\Sig$-structures
$h \colon M \to N$
a family
of functions
\(
h^\sortbis \colon M(\sortbis) \to N(\sortbis)
\mid
\sortbis \in \Sort(\Sig)
\)
preserving the interpretations of function and relation symbols.

We denote by $\Struct(\Sig)$ the category of $\Sig$-structures and their homomorphisms.

The atomic formulae over $\Sig$
are the (sorted) equalities $(t \Eq_\sortbis u)$
and the formulae of the form $R(t_1,\dots,t_n)$,
where $R \in \Rel(\Sig)$
$t,u,t_1,\dots,t_n$ are terms over $\Sig$.

We write $\Lang_\infty = \Lang_\infty(\Sig)$
for the (large) set
from atomic formulae over $\Sig$
using arbitrary (set-indexed) conjunctions and disjunctions,
along with $\neg, \exists, \forall$.
For a cardinal $\kappa$,
we write
for the set of formulae whose conjunctions and disjunctions
have cardinality $<\kappa$.
Hence, $\Lang_\omega$ consists of the ordinary finite first-order formulae.

In any case,
we only consider formulae whose subformulae have
finitely many free variables
(thus, with the notation of [20], $\Lang_\infty=\Lang_{\infty,\omega}$).

A formula-in-context is pair $\Env \sorting \varphi$
consisting of a formula $\varphi$
and a context
$\Env = x_1:\sortbis_1,\dots,x_n:\sortbis_n$ (where the $x_i$'s are pairwise distinct)
such that all the free variables of $\varphi$
occur in $\Env$.

Given a structure $M \in \Struct(\Sig)$,
a formula-in-context
$\Env \sorting \varphi$
$\Env = x_1:\sortbis_1,\dots,x_n:\sortbis_n$
induces a set

\[
\begin{array}{*{5}{l}}
\I{\Env \mid \varphi}_M
& \coloneqq
& \{ \vec a \in M(\vec\sortbis) \mid M \models \varphi(\vec a) \}.
% & \sle
% & M(\sortbis_1) \times \dots \times M(\sortbis_n)
\end{array}
\]

We say that $\Env \sorting \varphi$
is valid in $M \in \Struct(\Sig)$

\[
\begin{array}{l l l}
\I{\Env \mid \varphi}_M
& =
& M(\sortbis_1) \times \cdots \times M(\sortbis_n).
\end{array}
\]

When sorts are notationally irrelevant,
we write simply $\vec x$ for $\Env = x_1:\sortbis_1,\dots,x_n:\sortbis_n$,
and similarly with
homomorphisms and carriers of structures.

§.§ Factorisation systems

Given arrows $e$ and $m$ in a category $\C$,
we say that $e$ has the left lifting property with respect to $m$,
or that $m$ has the right lifting property with respect to $e$,
and write $e\pitchfork m$, if every commutative square as on the left-hand side below

\[
\begin{array}{l !{\qquad} l}

\begin{tikzcd}
\unit
\arrow{d}
\arrow{r}{e}
& \unit
\arrow{d}
\\
\unit
\arrow{r}{m}
& \unit
\end{tikzcd}

\begin{tikzcd}
\unit
\arrow{d}
\arrow{r}{e}
& \unit
\arrow{d}
\arrow{dl}[description]{d}
\\
\unit
\arrow{r}{m}
& \unit
\end{tikzcd}

\end{array}
\]

admits a diagonal filler,
i.e. an arrow $d$ making the rightmost diagram commute.

A pair of classes of morphisms $(\Q,\M)$ in a category $\C$ is a
weak factorisation system provided it satisfies:

* Every morphism $f$ in $\C$ can be decomposed as $f = m \comp e$
with $e\in \Q$ and $m\in \M$.

* $\Q=\{e\mid \forall m\in \M, e\pitchfork m\}$,
$\M=\{m\mid \forall e\in \Q, e\pitchfork m\}$.

If, in addition, each arrow in $\Q$ is epic and each arrow in $\M$ is monic,
then $(\Q,\M)$ is a proper factorisation system.

For the next example, recall that a monomorphism is strong
if it has the right lifting property with respect to all epis.

In $\Struct(\Sig)$,
the monomorphisms (respectively, epimorphisms)
are the homomorphisms that are sortwise injective
(respectively, surjective).
The strong monomorphisms

are exactly the embeddings

of structures,
i.e. the monomorphisms

(as well as preserve)
the interpretations of relation symbols.

Taking as $\Q$ the class of epimorphisms
and as $\M$ the class of embeddings of structures
yields a proper factorisation system on $\Struct(\Sig)$.
Cf. <cit.>.

Let $\C$ be a category equipped with a proper factorisation system $(\Q,\M)$. We shall refer to $\M$-morphisms as embeddings and denote them by $\emb$. $\Q$-morphisms will be referred to as quotients and denoted by $\epi$.

Akin to the (possibly large) poset of subobjects of a given object $X\in\C$,
we define the (large) poset $\Emb{X}$ of $\M$-subobjects of $X$.
The elements of $\Emb{X}$ are $\sim$-equivalence classes of embeddings into $X$,
where $m\colon S\emb X$ and $n\colon T\emb X$ are $\sim$-equivalent
provided that $m = n \comp i$ for some isomorphism $i\colon S\to T$.
We systematically represent a $\sim$-equivalence class by any of its representatives.
The collection $\Emb{X}$ carries a partial order $\leq$ given by $m\leq n$
if, and only if,
$m = n\comp i$ for some morphism $i\colon S\to T$.

Note that $\Emb{X}$ is small whenever $\C$ is well-powered.

Consider the factorisation system on $\Struct(\Sig)$ defined in Example <ref>. For all $M\in \Struct(\Sig)$, $\Emb{M}$ is isomorphic to the poset of substructures of $M$ (i.e., subsets of $M$ equipped with the induced relations) ordered by inclusion.

When dealing with arboreal categories in <ref>,
we shall consider proper factorisation systems that are stable,
meaning that for any quotient $e$ and embedding $m$ with common codomain,
the pullback of $e$ along $m$ exists and is a quotient.

§ ARBOREAL CATEGORIES

We recall from [5, 6] the main definitions and
facts pertaining to the theory of arboreal categories.

§.§ Paths and arboreal categories

Let us fix an arbitrary (well-powered) category $\C$ endowed with a proper factorisation system $(\Q,\M)$.

An object $P$ of $\C$ is a path if $\Emb{P}$ is a finite chain. A path embedding into an object $X$ is an embedding $P\emb X$ whose domain is a path.

Paths will be denoted by $P,Q$ and variations thereof.
We let $\Path{X}$ denote the sub-poset of $\Emb{X}$ consisting of the path embeddings. It follows from the definition of path that $\Path{X}$ is a forest
(recall that a poset $(\forest,\leq)$ is a forest if,
for all $x\in \forest$,
the set $\down x \deq \{y\in \forest \mid y\leq x\}$ is a finite chain).

Let $X$ be an object of $\C$.

* $X$ is connected if, for all non-empty sets of paths $\{P_i\mid i\in I\}$ admitting a coproduct $Y$ in $\C$, any morphism
X\to Y
factors through some coproduct map $P_i\to Y$.

* Consider the diagram with vertex $X$ consisting of all path embeddings into $X$. The morphisms between paths are those making the obvious triangles commute:

\[\begin{tikzcd}[column sep=1.2em, row sep=2em]
& X & \\
P \arrow[bend left=20,rightarrowtail]{ur} \arrow[rightarrowtail]{rr} & & Q \arrow[bend right=20,rightarrowtail]{ul}
\end{tikzcd}\]

Choosing representatives in a suitable way, this yields a cocone over the small diagram $\Path{X}$. We say that $X$ is path-generated provided this is a colimit cocone in $\C$.

An arboreal category is a category $\A$,
equipped with a stable proper factorisation system, satisfying:

$\A$ has all coproducts of sets of paths.

Every path in $\A$ is connected.

For any paths $P,Q,Q'$ in $\A$,
if a composite $P\to Q \to Q'$ is a quotient then so is $P\to Q$.

Every object of $\A$ is path-generated.

The full subcategory of $\A$ defined by the paths is denoted $\pth\A$.

Throughout, we assume that arboreal categories are well-powered and locally small, and that their full subcategories of paths are essentially small (i.e., equivalent to small categories).

Assuming that items <ref>–<ref> in
Definition <ref> hold,
item <ref> is equivalent to the fact that the inclusion functor
$I \colon \pth\A \into \A$
is dense <cit.>.

This means that the functor
$\ladj I \colon \A \to \presh{\pth\A}$
taking $a$ to $\A\funct{I(-),a}$
is full and faithful, or equivalently that each $a \in \A$
is the colimit of the canonical diagram
$(I/a) \to \pth\A \into \A$
(i.e. the canonical cocone $\gamma$
with $\gamma_{(P,k \colon P \to a)} \deq k$ is colimiting).

Recall that the roots of a forest $(\forest,\leq)$ are the minimal elements.
The covering relation $\cvr$ associated with the partial order $\leq$ is
defined by $x\cvr y$ if and only if $x < y$ and there is no $z$ such that $x < z < y$.
A forest morphism is a function between forests that preserves roots
and the covering relation.
Further, a tree is a forest with at most one root.
The category of forests and forest morphisms is denoted by $\Forest$,
and the full subcategory of non-empty trees by $\Tree$.

The categories $\Forest$ and $\Tree$ are equivalent
(via the functor $\Forest\to\Tree$ that adds a least element,
whose quasi-inverse $\Tree\to\Forest$ removes the

and they are equivalent to the presheaf category $\presh{\NN}$.

For any arboreal category $\A$,
the assignment $X\mapsto \Path{X}$ extends to a functor $\Path\colon \A\to\Tree$
by <cit.>.
The action of $\Path$ on morphisms is defined as follows:
for all arrows $f\colon a\to b$ in $\A$,
$\Path{f}\colon \Path{a}\to\Path{b}$ is the forest morphism sending
a path embedding $m\colon P\emb a$
to the path embedding $\exists_f P\emb b$ obtained by taking the
(quotient, embedding) factorisation of $f \comp m\colon P \epi \exists_f P \emb Y$.
This assignment is well-defined because factorisations are unique up to isomorphism,
and a quotient of a path is again a path <cit.>.

We conclude with some examples of arboreal categories.

The category $\Tree$ (and thus also $\Forest$) is arboreal when equipped with the
(epimorphisms, monomorphisms) factorisation system; its paths are the finite chains.
This follows e.g. from
Remarks <ref> and <ref>.

The following examples from [8]
were shown to be arboreal in [5, 6].

Let $\sig$ be a finite mono-sorted relational signature.
A forest-ordered $\sig$-structure is a pair
$(M, {\leq})$ where $M$ is a $\sig$-structure and $\leq$ a forest order on $M$.
A morphism of forest-ordered $\sig$-structures

is a homomorphism of $\sig$-structures
that is also a forest morphism. This yields a category $\cat R(\sig)$.

Equip $\cat R(\sig)$ with the factorisation system $(\Q,\M)$
where $\Q$ consists of the surjective morphisms and
$\M$ of the morphisms that are embeddings of $\sig$-structures.

Let $\cat R^E(\sig)$ be the full subcategory of $\cat R(\sig)$
determined by those objects $(M, {\leq})$ satisfying the following condition:

If $a,b\in M$ are distinct elements that appear in a tuple of related elements
$(a_1,\ldots,a_\ell)\in R^{M}$ for some $R\in\sig$,
then either $a<b$ or $b<a$.

The category $\cat R^E(\sig)$ is arboreal when equipped with the restriction of the factorisation system on $\cat R(\sig)$. The paths in $\cat R^E(\sig)$ are those objects in which the order is a finite chain.

For each $k>0$, let $\cat R^E_k(\sig)$ be the full subcategory of $\cat R^E(\sig)$ (see Example <ref>) defined by the forest-ordered structures of height $\leq k$.
$\cat R^E_k(\sig)$ is an arboreal category when equipped with the restriction of the factorisation system on $\cat R(\sig)$. The paths in $\cat R^E_k(\sig)$ are those objects in which the order is a finite chain of cardinality $\leq k$.

In <cit.>, it is shown that $\cat R^E_k(\sig)$ is isomorphic to the category of coalgebras for the Ehrenfeucht-Fraïssé comonad $\gc{E}_k$ on $\Struct(\sig)$. The objects $(M, {\leq})$ of $\cat R^E_k(\sig)$ are forest covers of $M$ witnessing that its tree-depth is at most $k$ [42].

In the same vein as Example <ref>, the categories of coalgebras for other game comonads, such as the pebble and modal comonads [2, 7] (encoding, respectively, pebble and bisimulation games), are also arboreal. See [5] for more details.

§.§ Bisimilarity and back-and-forth games

Let $\A$ be an arboreal category, and let ${f\colon a\to b}$ be an arrow in $\A$.

* $f$ is open if it satisfies the following path-lifting property.
Given any commutative square

\[
\begin{tikzcd}
\arrow[rightarrowtail]{r}
\arrow[rightarrowtail]{d}
& Q
\arrow[rightarrowtail]{d}
\arrow[dashed]{dl}
\\
\arrow{r}{f}
& b
\end{tikzcd}
\]

with $P,Q$ paths, there is a diagonal filler $Q\to a$.

* $f$ is a pathwise embedding if $f\comp m\colon P \to b$
is an embedding whenever $m\colon P\emb a$ is a path embedding.

Every arboreal category supports a notion of bisimilarity:
objects $a$ and $b$ are bisimilar, written $a\bisim b$,
provided there is a span of open pathwise embedding
$a \leftarrow \cdot \rightarrow b$ connecting them.
Crucially, under mild assumptions,
bisimilarity can be captured in terms of a back-and-forth game $\G(a,b)$:

Positions in the game are pairs $(m,n)\in\Path{a}\times\Path{b}$;
the initial position is denoted by $(m_0,n_0)$.
The winning relation $\W(a,b)$ consists of the pairs $(m,n)$ such that

If $(m_0,n_0)\notin \W(a,b)$, Duplicator loses the game. Otherwise, the game proceeds as follows:

* At the start of each round,
the position is specified by a pair $(m,n)\in\Path{a}\times\Path{b}$
and the round proceeds as follows:
Either Spoiler chooses some $m'\succ m$
and Duplicator must respond with some $n'\succ n$,
or Spoiler chooses some $n''\succ n$ and Duplicator must respond with $m''\succ m$.

* Duplicator wins the round if they are able to respond
and the new position is in $\W(a,b)$.
Duplicator wins the game with initial position $(m_0,n_0)$ if they have a strategy that is winning after $t$ rounds,
for all $t\geq 0$.

The game $\G(a,b)$ need not

have finite length;
however, by the definition of path, its length is at most $\omega$.

Given objects $a,b$ of an arboreal category,

let $\bot_a\colon \zero_a \emb a$ and $\bot_b\colon \zero_b \emb b$ be
the roots of $\Path{a}$ and $\Path{b}$, respectively.

For a proof of the next result, see e.g. <cit.>.

Let $a,b$ be objects of an arboreal category admitting a product.

Duplicator wins the game $\G(a,b)$ with initial position $(\bot_a,\bot_b)$
if, and only if,
$a$ and $b$ are bisimilar.

It follows that, in an arboreal category with binary products,
bisimilarity is an equivalence relation; see <cit.>.

§.§ Arboreal adjunctions

An arboreal adjunction is an adjoint pair

\[ \begin{tikzcd}
\A \arrow[r, bend left=25, ""{name=U, below}, "\Ladj"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D}, "R"{below}]
& \E
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U, to=D]
\end{tikzcd}
\]

where $\A$ is an arboreal category. Since the left adjoint is unique (up to natural isomorphism), we denote an arboreal adjunction simply by $R\colon \E\to\A$.

We think of $\E$ as an “extensional” category;
this is typically a category of relational structures
(but not always, see e.g. Example <ref> below).

An arboreal adjunction $R\colon \E\to\A$ allows us to transfer the
bisimilarity relation $\bisim$ from $\A$ to $\E$,

yielding an $R$-bisimilarity relation $\bisim_R$

given by

\[
\forall d,e\in \E, \
d \bisim_R e
\ \iff \
Rd \bisim Re.
\]

If $\A$ has binary products, $R$-bisimilarity is an equivalence relation.
In fact, since $R$ is right adjoint and thus preserves limits,
it suffices that $\E$ admit binary products.

Choosing the arboreal adjunction $R\colon \E\to\A$ in a suitable way,
we can capture equivalence of structures in various fragments of first-order
logic by means of the relations $\bisim_R$. Cf. Examples <ref> and <ref> below.
In fact, the arboreal category $\A$ allows us to specify the
logical resources,
leading to categorical characterisations of (resource-bounded) logic fragments.

To model this idea of resources, the notion of resource-indexed arboreal adjunction was introduced in [5]. This is an indexed family of right adjoints $R_k\colon \E\to\A_k$, where each $\A_k$ is a full subcategory of $\A$ determined by an appropriate choice of paths. By <cit.>, each $R_k$ is an arboreal adjunction in the sense of Definition <ref>.

We recall from [8] an arboreal adjunction whose bisimilarity relation captures precisely equivalence in finitary first-order logic with bounded quantifier rank.

Let $\sig$ be a finite (mono-sorted, relational) signature.
For each $k>0$, consider the arboreal category $\cat R^E_k(\sig)$ from
Example <ref>.
The obvious forgetful functor
$\Ladj_k \colon \cat R^E_k(\sig) \to \Struct(\sig)$
has a right adjoint $R_k$, hence it yields an arboreal adjunction
(in fact, this adjunction is comonadic, thus an arboreal cover
in the terminology of [6]).
The functor $R_k$ sends $M\in \Struct(\sig)$ to the set of all
non-empty sequences of length $\leq k$ of elements of $M$,
equipped with the prefix order and an appropriate lifting of the relations of
$M$ <cit.>.

To model the equality symbol, consider a fresh binary relation $I$ and the signature $\sig^I\deq \sig \cup\{I\}$. The fully faithful functor $J\colon \Struct(\sig) \to \Struct(\sig^I)$ that interprets $I$ as the identity relation has a left adjoint $H$, which sends $M\in \Struct(\sig^I)$ to the quotient of (the $\sig$-reduct of) $M$ by the equivalence relation generated by $I^M$ <cit.>.

The composite adjunction

\begin{equation}
\label{eq:EF-arboreal-adjunction}
\begin{tikzcd}
{\cat R^E_k(\sig^I)} \arrow[r, bend left=25, ""{name=U, below}, "\Ladj_k"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D}, "R_k"{below}]
& {\Struct(\sig^I)} \arrow[r, bend left=25, ""{name=U', below}, "H"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D'}, "J"{below}] & {\Struct(\sig)}
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U, to=D]
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U', to=D']
\end{tikzcd}
\end{equation}

(we write again $\Ladj_k \dashv R_k$ for the adjunction defined above,
this time for the signature $\sig^I$) is arboreal but not comonadic.

Let $R^I_k\deq R_k J$. For all $\sig$-structures $M,N$, the game $\G(R^I_k (M), R^I_k (N))$ (cf. Definition <ref>) corresponds precisely to the $k$-round Ehrenfeucht-Fraïssé game played between $M$ and $N$ <cit.>. By Theorem <ref> and the classical Ehrenfeucht-Fraïssé theorem [21, 23], the relation $\bisim_{R^I_k}$ coincides with equivalence of $\sig$-structures in the fragment of $\Lang_{\omega}$ with quantifier rank $\leq k$.

The arboreal adjunctions in the previous example, corresponding to finite Ehrenfeucht-Fraïssé games,
can be restricted by taking finite structures on both sides.
This is not always the case: for instance, in the case of pebble games one is forced to consider infinite structures as well <cit.>.

In the same spirit as Example <ref>, we can construct an arboreal adjunction whose bisimilarity relation captures equivalence in the infinitary logic

Consider the arboreal category $\cat R^E(\sig)$ from Example <ref>
and note that the forgetful functor
$\Ladj \colon \cat R^E(\sig) \to \Struct(\sig)$
has a right adjoint $R$.
The action of $R$ is akin to that of $R_k$ in Example <ref>,
except that $R(M)$ consists of all finite sequences of elements from $M$.
Composing with the adjunction between $\sig$-structures and $\sig^I$-structures,

\begin{equation*}
\begin{tikzcd}
{\cat R^E(\sig^I)} \arrow[r, bend left=25, ""{name=U, below}, "\Ladj"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D}, "R"{below}]
& {\Struct(\sig^I)} \arrow[r, bend left=25, ""{name=U', below}, "H"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D'}, "J"{below}] & {\Struct(\sig)}
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U, to=D]
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U', to=D']
\end{tikzcd}
\end{equation*}

we get an arboreal adjunction between $\Struct(\sig)$ and $\cat R^E(\sig^I)$.

Let $R^I\deq RJ$. The game $\G(R^I (M), R^I (N))$ corresponds again to the  Ehrenfeucht-Fraïssé game played between $M$ and $N$, but this time there is no bound on the number of rounds. Hence, by Karp's Theorem (see e.g. <cit.>), $\bisim_{R^I}$ coincides with equivalence of $\sig$-structures in

Other logic fragments can be captured using arboreal adjunctions,
such as finite-variable fragments of

[2], and modal logic with bounded modal-depth [7].

Besides bisimilarity, arboreal adjunctions can be used to transfer other relations from the arboreal category to the extensional one, such as the isomorphism relation or the homomorphism preorder. These also result in characterisations of equivalence in important logic fragments. Cf. <cit.>.

§ LOCALLY FINITELY PRESENTABLE CATEGORIES

Gabriel-Ulmer duality can be seen a syntax-semantics duality relating certain first-order theories—namely, cartesian theories—to their categories of models (in $\Set$). It is a dual (bi)equivalence between small finitely complete categories (encoding cartesian theories) and locally finitely presentable categories (the categories of models of cartesian theories).

In its original form [24], the duality involves small $\kappa$-complete categories and locally $\kappa$-presentable categories, for $\kappa$ a regular cardinal. We shall focus on the case $\kappa = \aleph_0$.

For posetal categories, Gabriel-Ulmer duality restricts to the well known duality between semilattices and algebraic lattices [41], see Appendix <ref>.

§.§ Finitely complete and locally finitely presentable categories

Let $\cat C$ be a small finitely complete category.

Recalling that a lex-morphism is a functor between finitely complete categories that preserves finite limits,
denote by $\lex\funct{\cat C,\Set}$
the full subcategory of the functor
category $\funct{\cat C,\Set}$ consisting of the lex-morphisms.
Since representable functors preserve limits, the (contravariant) Yoneda embedding factors as

\[
\begin{tikzcd}
\cat C^\op
\arrow{r}{\yoneda}
& \lex\funct{\cat C,\Set}
\arrow[hook]{r}{\incl}
& \funct{\cat C,\Set}.
\end{tikzcd}
\]

(Co)limits in $\funct{\cat C,\Set}$ exist and are computed pointwise. Since filtered colimits in $\Set$ commute with finite limits, $\lex\funct{\cat C,\Set}$ is closed in $\funct{\cat C,\Set}$ under filtered colimits (i.e., filtered colimits in $\lex\funct{\cat C,\Set}$ exist and are preserved by $\incl$). Similarly, as limits commute with limits, $\lex\funct{\cat C,\Set}$ is closed in $\funct{\cat C,\Set}$ under limits. Further, $\lex\funct{\cat C,\Set}$ admits also finite colimits (although they are not computed pointwise), and so is cocomplete; see e.g. <cit.>, where it is also proved that $\yoneda \colon \cat C^\op \to \lex\funct{\cat C,\Set}$ preserves finite colimits.

Every lex-morphism $f\colon \cat C \to \cat D$ induces a functor

\begin{equation}
\label{eq:f-upper-star}
\ladj f\colon \lex\funct{\cat D,\Set} \to \lex\funct{\cat C,\Set},
\
\ladj f G \deq G\comp f.
\end{equation}

Recall that $-\comp f\colon \funct{\cat D,\Set} \to \funct{\cat C,\Set}$
preserves all limits and colimits because it is both right and left adjoint
(cf. e.g. <cit.>).

Hence, $\ladj f$ is limit-preserving and finitary since $\lex\funct{\cat C,\Set}$ and
$\lex\funct{\cat D,\Set}$ are closed under limits and filtered colimits in
the respective functor

The left adjoint to $-\comp f\colon \funct{\cat D,\Set} \to \funct{\cat C,\Set}$,
sending $F$ to the left Kan extension
$\Lan_{\yoneda}(\yoneda f)(F)=\Lan_f{F}$,
restricts to a left adjoint to $\ladj f$;
see e.g. <cit.>.
Cf. also Proposition <ref> below.

Recall that an object $e$ of a (locally small) category $\E$ is finitely presentable if the functor $\E\funct{e,-} \colon \E \to \Set$ preserves all filtered colimits that exist in $\E$. By Yoneda Lemma, all representable functors are finitely presentable in $\funct{\cat C,\Set}$, hence in $\lex\funct{\cat C,\Set}$ because the inclusion $\incl$ preserves filtered colimits (in fact, the finitely presentable objects of $\lex\funct{\cat C,\Set}$ are exactly the representable ones, cf. <cit.>).

Since every object $F$ of $\funct{\cat C,\Set}$ is the colimit of the canonical diagram of representable functors

\[
\begin{tikzcd}
\arrow{r}{\pi}
& \cat C^\op
\arrow{r}{\yoneda}
& \lex\funct{\cat C,\Set}
\arrow[hook]{r}{\incl}
& \funct{\cat C,\Set},
\end{tikzcd}
\]

and the latter is filtered whenever $F$ is a lex-morphism (cf. e.g. <cit.>), every object of $\lex\funct{\cat C,\Set}$ is a filtered colimit of representable (hence finitely presentable) ones. Thus, $\lex\funct{\cat C,\Set}$ is locally finitely presentable:

A category $\E$ is locally finitely presentable (lfp) provided it satisfies the following conditions:

$\E$ is cocomplete.

admits a small full subcategory $\cat C$ consisting of finitely presentable objects
such that every object of $\E$ is a filtered colimit
of objects from $\cat C$.

A morphism of lfp categories is a limit-preserving finitary functor between lfp categories.

The following fact is a consequence of e.g. <cit.>.

Let $\E$ be a cocomplete category admitting a full dense subcategory $\cat K$.
If $\cat K$ is (essentially) small and consists of finitely presentable objects, then $\E$ is lfp.

For any small category $\cat K$, the presheaf category $\presh{\cat K}$ is lfp. This follows from Lemma <ref>, since the representable functors form a full dense subcategory of $\presh{\cat K}$ consisting of finitely presentable objects.

Given an lfp category $\E$, its full subcategory $\fp\E$ defined by the finitely presentable objects is closed under finite colimits and essentially small, see e.g. <cit.>. Replacing $\fp\E$ with a small skeleton if necessary, $\fp\E^\op$ is a small finitely complete category. To see that every morphism of lfp categories $F\colon \cat E \to \cat F$ induces a lex-morphism $f\colon \fp{\cat F}^\op \to \fp{\cat E}^\op$, recall the following fact:

A functor between lfp categories is a morphism of lfp categories if, and only if, it has a left adjoint preserving finitely presentable objects.

By the Adjoint Functor Theorem for lfp categories (cf. <cit.>), any limit-preserving finitary functor between lfp categories is right adjoint. Further, a right adjoint between lfp categories is finitary precisely when its left adjoint preserves finitely presentable objects (cf. the proof in loc. cit.).

Thus, we can define $f$ as (the opposite of) the restriction of the left adjoint of $F$.

Recall that an
$L\dashv R$ between lfp categories is finitely accessible if $R$ is finitary.
By Proposition <ref>, the morphisms of lfp categories can be characterised
as the
(right adjoints in)
finitely accessible adjunctions.

§.§ Gabriel-Ulmer duality

Write $\LFP$ for the 2-category whose 0-cells (objects) are locally finitely presentable categories, whose 1-cells (morphisms) are morphisms of lfp categories (i.e., limit-preserving finitary functors), and whose 2-cells are natural transformations.

Moreover, write $\Lex$ for the 2-category of small finitely complete categories, lex-morphisms and natural transformations.

In view of <ref>,
there is a 2-functor from $\Lex^\op$ (reverse the 1-cells) to
$\LFP$ sending $\cat C$ to $\lex\funct{\cat C,\Set}$.

Gabriel-Ulmer duality states that the latter is a
biequivalence $\Lex^\op \to \LFP$
(this was established at the level of objects
in [24]
and later extended to a fully fledged duality, cf. [40, 11]).

In particular, a category is lfp if and only if it is equivalent to one of the form
$\lex\funct{\cat C,\Set}$ for some small finitely complete category $\cat C$,
and every morphism of lfp categories
$\lex\funct{\cat D,\Set} \to \lex\funct{\cat C,\Set}$
is naturally isomorphic to one of the form $\ladj f$ for a lex-morphism
$f\colon \cat C \to \cat D$ (see eq. (<ref>)).

Observe that, as a consequence of this duality, every lfp category is complete, locally small and well-powered.

§ FINITELY ACCESSIBLE ARBOREAL ADJUNCTIONS

In this section, we study arboreal categories that are also lfp, and arboreal adjunctions that are finitely accessible in the sense of Remark <ref>.

These concepts play a fundamental role in this paper. In fact, we shall see in <ref>–<ref> that for this class of adjunctions we are able, under mild assumptions, to give a purely logical characterisation of the $R$-bisimilarity relation induced on the extensional category.

To this end, in the next section we recall a logical perspective on Gabriel-Ulmer duality based on the notion of cartesian theory.

To start with, we specialise the concept of arboreal adjunction
(Definition <ref>) to the case of lfp categories:

A finitely accessible arboreal adjunction is an arboreal adjunction

\[
\begin{tikzcd}
\A
\arrow[r, bend left=25, ""{name=U, below}, "\Ladj"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D}, "R"{below}]
& \E
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U, to=D]
\end{tikzcd}
\]

where $\A$ and $\E$ are lfp, and $R$ is finitary.
Equivalently, it is a morphism of lfp categories $R\colon \E \to \A$
such that $\A$ is arboreal.

The following immediate consequence of Lemma <ref>
provides sufficient conditions for an arboreal category $\A$ to be lfp
(recall from <ref> that the full subcategory $\pth\A$
of paths is assumed to be essentially small).

Let $\A$ be a cocomplete arboreal category.
If every path in $\A$ is finitely presentable, then $\A$ is lfp.

Let $\sig$ be a finite (mono-sorted, relational) signature.
For all $k>0$, the (comonadic) arboreal adjunction
$\Ladj_k \colon {\cat R^E_k(\sig)} \inadj {\Struct(\sig)} \cocolon R_k$
in Example <ref> is a finitely accessible arboreal adjunction.

To see this, note that the comonad $\Ladj_k R_k$ is finitary
(this can be deduced e.g. using the criterion in <cit.>).
It follows that $R_k$ is finitary and $\Ladj_k$
preserves and reflects finitely presentable objects,
cf. e.g. <cit.> or <cit.>.
It remains to show that $\cat R^E_k(\sig)$ is lfp.
Since the underlying $\sig$-structure of any path in $\cat R^E_k(\sig)$ is finite,
hence finitely presentable in $\Struct(\sig)$,
we see that paths in $\cat R^E_k(\sig)$ are finitely presentable.
By Lemma <ref>, the latter category is lfp;
just observe that $\cat R^E_k(\sig)$ is cocomplete because
$\Struct(\sig)$ has this property and comonadic functors create colimits.

The adjunction in eq. (<ref>) obtained by composing with the adjunction $H\dashv J$ between $\sig$-structures and $\sig^I$-structures is also a finitely accessible arboreal adjunction, since $J$ (which interprets $I$ as the identity relation) is easily seen to be finitary.

In the previous example, the assumption that $\sig$ be finite is necessary, otherwise Lemma <ref> would not apply. If the signature is infinite, we can still prove that the category $\cat R^E_k(\sig)$ is lfp by invoking a result of Diers providing sufficient conditions for a category of coalgebras for a comonad to be lfp (see <cit.> and also <cit.>).

By a reasoning completely analogous to that in Example <ref>, we see that the functor $R^I\colon \Struct(\sig)\to \cat R^E(\sig^I)$ from Example <ref> is a morphism of lfp categories, hence it yields a finitely accessible arboreal adjunction.

To provide an example of a different nature, we state the following result, where a forest is seen as a (posetal) category.

Let $\forest$ be a forest. The presheaf category $\presh{\forest}$ is an arboreal lfp category.

In view of Example <ref>, $\presh{\forest}$ is lfp. Since it is a topos, it admits precisely one proper factorisation system, namely (epimorphisms, monomorphisms). With respect to the latter, the paths are the representable functors and the initial object. For a proof that $\presh{\forest}$ satisfies the conditions for an arboreal category, see Theorem <ref> in the appendix.

Setting $\forest=\NN$ in Theorem <ref>,
we see that $\Tree$ and $\Forest$ are arboreal categories.
Cf. Remark <ref>.

This example
is inspired by the Diaconescu cover
of a topos,
in <cit.>.

Given a small category $\cat C$,
let $\forest(\cat C)$ be the forest whose nodes
are finite sequences $s$ of composable arrows

\[
\begin{tikzcd}
\arrow{r}{k_1}
& a_1
\arrow[dashed]{r}
& a_{n-1}
\arrow{r}{k_{n}}
& a_n
\end{tikzcd}
\]

in $\cat C$, and where $s \leq t$

if $s$ is a prefix of $t$, say

\[
\begin{tikzcd}
\arrow[dashed]{r}{s}
& a_n
\arrow{r}{k_{n+1}}
& a_{n+1}
\arrow[dashed]{r}
& a_{n+m-1}
\arrow{r}{k_{n+m}}
& a_{n+m}.
\end{tikzcd}
\]

Let $\pi$ be the functor $\forest(\cat C) \to \cat C$
such that, for $s \leq t$ as above,
$\pi(s \leq t) \colon a_n \to a_{n+m}$ is the composition
$k_{n+m} \comp \dots \comp k_{n+1}$.

The functor $\ladj\pi \colon \presh{\cat C} \to \presh{\forest(\cat C)}$
(precompose with $\pi$)
has adjoints on both sides
(cf. e.g. <cit.>).
In view of Example <ref> and Theorem <ref>,
this yields a finitely accessible arboreal adjunction between
$\presh{\cat C}$ and the arboreal category $\presh{\forest(\cat C)}$.

§ CARTESIAN THEORIES

Building on the idea of functorial semantics,
logical characterisations of lfp categories
have been proposed (see e.g. [12]).
We recall the approach of Coste [17],
according to which lfp categories correspond exactly
to categories of $\Set$-models of certain $\land\exists$-theories,
called cartesian, in which only provably unique existential quantifications
are allowed (Corollary <ref><ref>).
We mostly follow the presentation of <cit.>.

Let $\Sig$ be a signature.

sequent over $\Sig$
is a triple
of the form

\[
\begin{array}{l l l}
\psi
& \thesis_\Env
& \varphi
\end{array}
\]

$\Env \sorting \psi$
$\Env \sorting \varphi$
formulae-in-context of $\Sig$.

theory $\theory$ over $\Sig$
is a set of
over $\Sig$.

Let $\Sig$ be a signature.

* Let $\theory$ be a theory over $\Sig$.
The set of formulae-in-context
that are cartesian over $\theory$
is inductively defined by:

* atomic formulae-in-context are cartesian over $\theory$;

* cartesian formulae are closed under finite conjunctions;

* given a cartesian formula-in-context
$\Env,x:\sortbis \sorting \varphi$,
the formula
$\Env \sorting (\exists x:\sortbis) \varphi$
is cartesian over $\theory$ if $\theory$ proves the sequent
\(
\varphi
\land
\varphi[y/x]
~\thesis_{\Env, x: \sortbis, y: \sortbis}~
x \Eq_\sortbis y
\).

* A sequent $\psi \thesis_\Env \varphi$ is cartesian over $\theory$
if both $\psi, \varphi$ are.

* A cartesian theory
is a
theory $\theory$
whose axioms can be well-ordered so that each axiom
is cartesian over the set of its predecessors.

Cartesian theories consist of (sequents of)
$\land\exists$-formulae, hence they are special cases of regular theories.
Further, they admit a classical completeness theorem stating that
any cartesian theory has enough models in $\Set$ to determine provability,
see e.g. <cit.>.
Thus, classical and intuitionistic provability coincide for cartesian theories.

Cartesian theories strictly extend Horn theories,
cf. e.g. <cit.>
(theory of categories).

Let $M \in \Struct(\Sig)$.
A sequent $\psi \thesis_\Env \varphi$ is valid in

if $\I{\Env \mid \psi}_M \sle \I{\Env \mid \varphi}_M$.
$M$ is a model of a theory $\theory$

if all the sequents in $\theory$
are valid in $M$.
We denote by

\[
\Mod(\theory)
\]

the full subcategory
of $\Struct(\Sig)$ defined by the models of $\theory$.

[Cartesian theories of functors]

Given a small category $\cat C$, consider the signature $\Sig(\cat C)$
with sorts the objects of $\cat C$,
function symbols the morphisms of $\cat C$,
and no predicate symbols.
Let $\theory(\cat C)$ be
the cartesian theory with axioms

\[
\begin{array}{l !{\qquad} l}
\True
\thesis_{x:a}
\id_a(x) \Eq_a x

& \True
\thesis_{x:a}
(g \comp f)(x) \Eq_c g(f(x))
\end{array}
\]

where $f \in \cat C\funct{a,b}$ and $g \in \cat C\funct{b,c}$.
Then $\Mod(\theory(\cat C))$
is equivalent to the functor category

$\funct{\cat C,\Set}$.
Further, $\theory(\cat C)$ can be extended to a cartesian theory

$\theory$ such that $\Mod(\theory) \cong \lex\funct{\cat C,\Set}$.
See e.g. <cit.>.

§.§ Syntactic categories and functorial semantics

A basic idea of categorical logic
is that a theory $\theory$ should be seen as a category, its syntactic category, and models of $\theory$ as certain functors defined on the latter category. Theorem <ref> and Corollary <ref><ref> below establish these equivalences for cartesian theories and their $\Set$-based models.

In the remainder of this <ref>, all theories $\theory$ under consideration are assumed to be cartesian.

The syntactic category $\cat T$ of a

theory $\theory$
is defined as follows.

$\Env \sorting \varphi$
up to renaming of variables
$\OI{\Env \mid \varphi}$.

$\OI{\vec x \mid \varphi}$
$\OI{\vec y \mid \psi}$
are $\theory$-provable equivalence classes of $\theory$-provable functional
relations from
$\OI{\vec x \mid \varphi}$ to
$\OI{\vec y \mid \psi}$,
i.e. $\theory$-provable equivalence classes of
$\vec x,\vec y \sorting \theta$
cartesian over $\theory$
such that $\theory$ proves the sequents:

\[
\begin{array}{r l l}
\theta
& \thesis_{\vec x,\vec y}
& \varphi \land \psi
\\

\theta
\theta[\vec z/\vec y]
& \thesis_{\vec x,\vec y,\vec z}
& \vec z \Eq \vec y
\\

\varphi
& \thesis_{\vec x}
& (\exists \vec y)\theta
\end{array}
\]

We denote by $\MI{\vec x,\vec y \mid \theta}$ the equivalence class
of $\vec x,\vec y \sorting \theta$.

Note that the last sequent above is cartesian
over the penultimate one.

It is clear that $\cat T$ is a category.

The syntactic category $\cat T$ of a theory $\theory$ is finitely complete.

The terminal object is given by the formula $\True$ in the empty context, and binary products by binary conjunctions. Equalisers are obtained by means of binary conjunctions and (provably unique) existential quantifiers.

Given a model $M \in \Mod(\theory)$,
we can associate with each $\OI{\vec x \mid \varphi} \in \cat T$
the set $\I{\vec x \mid \varphi}_M \in \Set$.
Further, each morphism
\(
\MI{\vec x,\vec y \mid \theta}
\colon
\OI{\vec x \mid \varphi}
\to
\OI{\vec y \mid \psi}
\)
induces a functional relation

\[
\begin{tikzcd}
\I{\vec x,\vec y \mid \theta}_M
\arrow[hook]{r}
& \I{\vec x \mid \varphi}_M
\times
\I{\vec y \mid \psi}_M
\end{tikzcd}
\]

and is thus the graph of a function
$\I{\vec x \mid \varphi}_M \to \I{\vec y \mid \psi}_M$.

This yields a functor $F_M \colon \cat T \to \Set$ on the syntactic category of $\theory$,
which is easily seen to be a lex-morphism.
In fact,

\[
\Mod(\theory) \to \lex\funct{\cat T, \Set}, \ \ M \mapsto F_M
\]

is (part of) an equivalence of categories for any theory $\theory$.

The previous theorem, combined with Example <ref> and Gabriel-Ulmer duality (<ref>),
entails the following result (for a proof, see Corollary <ref> in the appendix):

The following statements hold:

*  A small category is finitely complete if, and only if, it is equivalent to the syntactic category of a theory $\theory$.

*  A category is lfp if, and only if, it is equivalent to $\Mod(\theory)$
for some theory $\theory$.

In particular, for any signature $\Sig$, Theorem <ref> entails that
$\Struct(\Sig)$ is lfp as $\Struct(\Sig) \cong \lex\funct{\cat T(\Sig),\Set}$,

where $\theory(\Sig)$ is the cartesian
theory over $\Sig$ with no axioms
and $\cat T(\Sig)$ is its syntactic category.

Filtered colimits in $\Struct(\Sig)$ are simple: they are computed in $\Set$; see e.g. <cit.>. In fact, filtered colimits in categories of models are also simple:

Let $\theory$ be a theory. The inclusion functor $\Mod(\theory) \into \Struct(\Sig)$ preserves filtered colimits.

§.§ Finitely presentable models

Syntactic categories become particularly
useful when combined with the Yoneda lemma (cf. <cit.> or <cit.>).

Let $\theory$ be a theory and $\cat T$ its syntactic category.

Fix a model $M$ of $\theory$.

By the Yoneda Lemma,
for any $\OI{\vec x \mid \varphi}\in \cat T$,

\begin{equation}
\label{eq:Yoneda-interpretations}
\begin{array}{l l l}
\I{\vec x \mid \varphi}_M
& \cong
& \lex\funct{\cat T,\Set}\funct{\yoneda\OI{\vec x \mid \varphi},\, F_M}.
\end{array}
\end{equation}

Just recall that $F_M(\OI{\vec x \mid \varphi}) = \I{\vec x \mid \varphi}_M$.
Explicitly, given

$\vec a \in \I{\vec x \mid \varphi}_M$,
the unique natural transformation

\begin{equation}
\label{eq:lambda-vec-a}
\begin{array}{*{5}{l}}
\lambda^{\vec a}
& \colon
& \yoneda\OI{\vec x \mid \varphi}
& \longto
& F_M
\end{array}
\end{equation}

corresponding to
$\vec a$
has component at $C \in \cat T$ defined by

\[
(\lambda^{\vec a})_C
\ \colon \
\cat T\funct{\OI{\vec x \mid \varphi}, C}
\to F_M(C),
\ \
\theta\mapsto F_M(\theta)(\vec a).
\]

Recall from <ref>
that the finitely presentable objects of $\lex\funct{\cat T,\Set}$
are exactly the representable functors.

For each $\OI{\vec x \mid \varphi}\in \cat T$, write $\FG{\vec x \mid \varphi}$

for the finitely presentable model of $\theory$
to the representable functor
$\yoneda \OI{\vec x \mid \varphi} \in \lex\funct{\cat T,\Set}$
via Theorem <ref>.

By eq. (<ref>),
for each sort $\sortbis$,

the set $\FG{\vec x \mid \varphi}(\sortbis)$ admits the following description:

\[
\begin{array}{l l l}
\FG{\vec x \mid \varphi}(\sortbis)
& =
& \I{\OI{y : \sortbis \mid \True}}_{\FG{\vec x \mid \varphi}}
\\

& \cong
& \lex\funct{\cat T,\Set}
\funct{\yoneda \OI{y:\sortbis \mid \True}, F_{\FG{\vec x \mid \varphi}}}
\\

& \cong
& \cat T\funct{\OI{\vec x \mid \varphi},\OI{y :\sortbis \mid \True}}.
\end{array}
\]

With this notation, Theorem <ref> yields a natural bijection

\begin{equation}
\label{eq:fp-models-nat-bij}
\lex\funct{\cat T,\Set}\funct{\yoneda\OI{\vec x \mid \varphi},\, F_M}
\cong
\Mod(\theory)\funct{\FG{\vec x \mid \varphi} ,\, M}.
\end{equation}

Given a homomorphism $\ell \colon \FG{\vec x \mid \varphi} \to M$
and $\vec a \in M$ of the same sorts as $\vec x$,
we say that $\ell$ takes $\vec x$ to $\vec a$ when
$\ell$ is the image of the natural transformation $\lambda^{\vec a}$ in eq. (<ref>) under the bijection (<ref>).

The next result gives
a logical description of composition
in $\fp{\Mod(\theory)}/M$.
We use it reapeatedly in <ref> and <ref>.

finitely presentable models

$\FG{\vec x \mid \varphi}$, $\FG{\vec y \mid \psi}\in \Mod(\theory)$.
Given $\vec a,\vec b \in M$
of the same sorts as $\vec x$ and $\vec y$, respectively,
the following statements are equivalent:

There exist homomorphisms
$h \colon \FG{\vec x \mid \varphi} \to M$
$k \colon {\FG{\vec y \mid \psi}} \to M$
taking, respectively,
$\vec x$ to $\vec a$
$\vec y$ to $\vec b$,
$\ell \colon \FG{\vec x \mid \varphi} \to \FG{\vec y \mid \psi}$
such that
$k \comp \ell = h$:

\[
\begin{tikzcd}[row sep=0cm]
\FG{\vec x \mid \varphi}
\arrow{dd}[left]{\ell}
\arrow{dr}[above]{h}
\\
& M
\\
\FG{\vec y \mid \psi}
\arrow{ur}[below]{k}
\end{tikzcd}
\]

\(
\models
\varphi(\vec a)
\land
\psi(\vec b)
\land
% \bigvee_{\theta \in \cat T\funct{\OI{\vec y \mid \psi},\OI{\vec x \mid \varphi}}}
% \theta(\vec b, \vec a)
\bigvee
\{
\theta(\vec b, \vec a)
\mid
\theta \in \cat T\funct{\OI{\vec y \mid \psi},\OI{\vec x \mid \varphi}}
\}
\).

The formula in item <ref> above may be infinite.

We note the following, which will be crucial to our use
of word-constructions in <ref>.

Let $\OI{\vec x \mid \varphi} \in \cat T$
with $\vec x = x_1,\dots,x_n$.
There exist $\const x_1,\ldots,\const x_n \in \FG{\vec x \mid \varphi}$
such that for every $M \in \Mod(\theory)$
and $h \colon \FG{\vec x \mid \varphi} \to M$
taking $\vec x$ to $\vec a \in \I{\vec x \mid \varphi}_M$,
we have $h(\const x_i) = a_i$ for all $i = 1,\dots,n$.

Assume $x_i$ is of sort $\sortbis_i$.
The formula

\[
\vec x,x_i' \sorting \varphi ~\land~ x_i \Eq x'_i
\]

corresponds to a $\cat T$-morphism
$\varpi_i \colon \OI{\vec x \mid \varphi} \to \OI{x_i : \sortbis_i \mid \True}$.

By Remark <ref>, we can take $\const x_i$ to be the image
of $\varpi_i$ under
the bijection
\(
\cat T\funct{\OI{\vec x \mid \varphi},\OI{x_i : \sortbis_i \mid \True}}
\cong
\FG{\vec x \mid \varphi}(\sortbis_i)
\).

The elements $\const x_i$ in Lemma <ref> can be thought of as “generators” of $\FG{\vec x \mid \varphi}$. They are induced by projections, akin to the way in which generators of free algebras are modelled by projections in categorical algebra.

Up to iso,
we can
assume that a finitely presentable model is of the form
$\FG{\vec x \mid \varphi}$ with $\varphi$ quantifier-free

§ A LOGICAL DESCRIPTION OF $R$-BISIMILARITY

Our main goal in this paper is to show that, for any finitely accessible arboreal adjunction $R\colon \E \to \A$ (Definition <ref>), the $R$-bisimilarity relation induced on the extensional category $\E$ is definable in the infinitary first-order logic $\Lang_{\infty}$ (in the signature associated with $\E$).

This is achieved in two steps: first, we give a logical description of the games $\G(a,b)$ in the arboreal category $\A$ (<ref>). Then we transfer this description along (the Gabriel-Ulmer dual of) $R$ to obtain a characterisation in the signature of $\E$ (<ref>). In this section, we assume the existence of formulae defining path embeddings in $\A$; we will see in <ref> how to enforce this condition.

§.§ Hintikka formulae for arboreal games

To motivate the logical perspective on the games $\G(a,b)$, recall that in the classical setting of finite Ehrenfeucht-Fraïssé games, the number of rounds corresponds to the quantifier rank of formulae in $\Lang_{\omega}$. This correspondence can be established by means of $m$-Hintikka formulae (see e.g. <cit.>).

Given a relational structure $M$ and a tuple $\vec a$ of elements from $M$,
the $0$-Hintikka formula $\varphi^0_{\vec a}$ describes the isomorphism type of $\vec a$.
For $m>0$, the $m$-Hintikka formula $\varphi^m_{\vec a}$
encodes the isomorphism types to which $\vec a$ can be extended in $m$ steps,
adding one element at each step.

In the infinite Ehrenfeucht-Fraïssé game, (an infinitary variant of) Hintikka formulae yield a correspondence between quantifier rank of formulae in $\Lang_{\infty}$ and the rank of positions in the game (see e.g. <cit.>). We recall the latter notion, tailored to the case of the games $\G(a,b)$, and then proceed to construct “Hintikka formulae” $\Theta$ for these games.

Let $\A$ be an arboreal category.

Following <cit.>
(see also <cit.>),
given a game $\G(a,b)$ as in
Definition <ref>
we define for each ordinal $\ord$
a set $\Rk(\ord)$ of positions of rank $\geq \ord$
in $\G(a,b)$.
The definition is by induction on $\ord$:

* $(m,n) \in \Rk(0)$ if $(m,n) \in \W(a,b)$;

* $(m,n) \in \Rk(\ord+1)$

$(m,n) \in \W(a,b)$
for each Spoiler move from position $(m,n)$,
there is a Duplicator move reaching

a position in $\Rk(\ord)$;

* $(m,n) \in \Rk(\ord)$, for $\ord$ a limit ordinal,
if ${(m,n) \in \Rk(\ordbis)}$ for all $\ordbis < \ord$.

Note that
$\Rk(\ord) \subseteq \W(a,b)$
for all ordinals $\ord$
(this must be enforced
in the clause for successor ordinals, as there may be
no possible Spoiler moves from position $(m,n)$).

$\Rk(\ord) \subseteq \Rk(\ordbis)$
for all $\ordbis < \ord$.

We thus have a decreasing sequence of
sets $(\Rk(\ord))_{\ord} \sle \Path a \times \Path b$,
and this sequence is
The rank of $\G(a,b)$,
denoted by $\ord_{a,b}$,
is the least ordinal $\ord$
such that $\Rk(\ord) \sle \Rk(\ord+1)$.
Positions of rank $\geq \ord_{a,b}$
are winning,
as stated in the following variant of <cit.>.

For all $(m,n) \in \Rk(\ord_{a,b})$,
Duplicator has a winning strategy in the game $\G(a,b)$ from position $(m,n)$.

We then arrive at the following characterisation,
based on <cit.>.

Let $(m,n)$ be an arbitrary position in the game $\G(a,b)$.
The following statements are equivalent:

* $(m,n) \in \Rk(\ord)$ for every ordinal $\ord$.

* $(m,n) \in \Rk(\ord_{a,b})$.

* Duplicator has a winning strategy from position $(m,n)$.

From a position of rank $\geq k$, with $k \in \NN$,
Duplicator has a strategy which is winning for $k$ rounds in $\G(a,b)$.
the rank of $\G(a,b)$ is finite if the plays of
$\G(a,b)$ have bounded length
(cf. Remark <ref>).

For instance, the games played in the arboreal category $\cat R^E_k(\sig)$
(Examples <ref> and <ref>)
have finite rank because

all plays have length at most $k$.
Just observe that each path has cardinality at most $k$.

From a position of rank $\omega$,
for all $k \in \NN$ Duplicator has a strategy
which is winning for $k$ rounds.
But they need not have a strategy which
is winning for $k$ rounds for all $k$.

We now turn to the definition of Hintikka formulae for the games $\G(a,b)$.

For the remainder of <ref>, we fix an arbitrary cocomplete arboreal category $\A$ such that all its paths are finitely presentable.
Note that, by Lemma <ref>,
$\A$ is lfp.

Thus, by Gabriel-Ulmer duality,
we can identify $\A$ with $\Mod(\theorybis)$,
for a cartesian theory $\theorybis$ of signature $\Sigbis$.

We shall assume for the moment that path embeddings in $\A$ are definable;
this assumption will be weakened in <ref>.

$\Delta 1$

For each path $P \cong \FG{\vec y \mid \psi}$ in $\A$,
there is a formula
$\FEmb(\FG{\vec y \mid \psi})(\vec y)$
of $\Sigbis$
such that

for all
${h \colon \FG{\vec y \mid \psi} \to a}$
taking $\vec y$ to
$\vec b \in \I{\vec y \mid \psi}_a$,
$h$ is an embedding, if, and only if
$a \models \FEmb(\FG{\vec y \mid \psi})(\vec b)$.

\[
\begin{array}{r c l}
\Theta(a)_{\A}^{m,Q,0}(\vec z)
& \deq
& \FIso(\dom(m),Q)

\hfill
\begin{array}{l l l}
\Theta(a)_{\A}^{m,Q,\ord}(\vec z)
& \deq
& \bigwedge_{\ordbis < \ord} \Theta(a)_{\A}^{m,Q,\ordbis}(\vec z)
\end{array}
\quad\text{($\ord$ limit ordinal)}
\\
\\

\Theta(a)_{\A}^{m,Q,\ord+1}(\vec z)
& \deq
& \FIso(\dom(m),Q)
\FForth(a)^{m,Q,\ord+1}(\vec z)
\FBack(a)^{m,Q,\ord+1}(\vec z)
\\
\\

\FForth(a)^{m,Q,\ord+1}(\vec z)
& \deq
& \bigwedge_{\substack{m' \colon P' \emb a \\ m \prec m'}}
\bigvee_{\substack{\ell \colon Q \emb Q' \\ \ell \prec \id_{Q'}}}
(\exists \vec z')
\left(
\vartheta_\ell(\vec z',\vec z)
\FEmb(Q')(\vec z')
\Theta(a)_{\A}^{m',Q',\ord}(a)(\vec z')
\right)
\\
\\

\FBack(a)^{m,Q,\ord+1}(\vec z)
& \deq
& \bigwedge_{\substack{\ell \colon Q \emb Q' \\ \ell \prec \id_{Q'}}}
(\forall \vec z')
\left(
\big( \vartheta_\ell(\vec z',\vec z) ~\land~ \FEmb(Q')(\vec z') \big)
\bigvee_{\substack{m' \colon P' \emb a \\ m \prec m'}}
\Theta(a)_{\A}^{m',Q',\ord}(a)(\vec z')
\right)
\end{array}
\]

Hintikka formulae for
the arboreal category $\A$ (<ref>).

Fix an object $a \in \A$.
For each ordinal $\ord$,
path embedding $m \colon P \emb a$,
and path $Q \cong \FG{\vec z \mid \varpi_Q}$,
we define a formula

\[
\Theta(a)_{\A}^{m,Q,\ord}(\vec z).
\]

The definition is by induction on $\ord$
and is given in Figure <ref>,
we use the following notations.
We let ${Q' \cong \FG{\vec z' \mid \varpi_{Q'}}}$.
Moreover, given an embedding $\ell\colon Q\emb Q'$, we denote by
\(
\MI{\vec z',\vec z \mid \vartheta_\ell}
\colon
\OI{\vec z' \mid \varpi_{Q'}}
\to
\OI{\vec z \mid \varpi_{Q}}
\)
the arrow corresponding to $\ell$ via the Yoneda embedding
$\yoneda \colon \cat U^\op \to \lex\funct{\cat U,\Set}$,
where $\cat U$ is the syntactic category of $\theorybis$.

Finally, $\FIso(\dom(m),Q)$ is the formula
$\True$ if $\dom(m) \cong Q$,
and $\False$ otherwise.

The next result follows by induction on $\ord$,
along the same lines as,
e.g., <cit.>.

Assume <ref>.
The following are equivalent for all
$a, b \in \A$, and all $n \colon Q \emb b$
induced by $\vec c \in \I{\vec z \mid \varpi_{Q}}_b$:

* $b \models \Theta(a)_{\A}^{m,Q,\ord}(\vec c)$.

* $(m,n)$ is a position of rank $\geq \ord$
in the game $\G(a,b)$.

Let $\forest$ be a
forest and consider the presheaf category
$\A \deq \presh{\forest}$.
By Theorem <ref>,
$\A$ is arboreal and lfp.
Note that $\A$ is cocomplete and
its paths are the representable functors and the initial object,
which are finitely presentable.

In fact, recall from Example <ref>
the cartesian theory $\theory(\forest^\op)$
of functors $\forest^\op \to \Set$.
The signature of $\theory(\forest^\op)$
has one sort $P$ for each $P \in \forest$,
and exactly one function symbol $f \colon P \to Q$
if, and only if, $Q \leq P$ in $\forest$.

We have $\A \cong \Mod(\theory(\forest^\op))$
this gives finite formulae satisfying
Assumption <ref>, as we now explain.

Note that, in a topos, any arrow from the initial object is monic.
As for non-initial paths,

the representable
to the finitely presentable model
$\FG{x:P \mid \True}$.
Then, for each $P \in \forest$ there is a
finite formula $\FMono(P)(x)$
(see <ref>
for a definition)
such that
the following are equivalent:

$h \colon \FG{x:P \mid \True} \to M$ is a monomorphism.

\(
\models
\FMono(P)(a)
\),
where $h$ takes $x$ to $a \in M(P)$.

In particular, in this case the Hintikka formulae
can be assumed to be finite for each finite ordinal $\ord$.

§.§ Interpretations and a transfer result

In this section, we shall transfer Theorem <ref> along a finitely accessible arboreal adjunction.
Recall from Corollary <ref> that Gabriel-Ulmer duality (<ref>) can be seen as a syntax-semantics duality.
Accordingly, morphisms of lfp categories induce interpretations of formulae.

To see this, consider cartesian theories $\theory$ and $\theorybis$ with syntactic categories $\cat T$ and $\cat U$, respectively.
By Gabriel-Ulmer duality,
for each morphism of lfp categories
$R \colon \Mod(\theorybis) \to \Mod(\theory)$
there is a lex-morphism
$\inclth \colon \cat T \to \cat U$
such that
$R$ corresponds, via Theorem <ref>,
to the functor
$\ladj\inclth \colon \lex\funct{\cat U,\Set} \to \lex\funct{\cat T,\Set}$.

Given a model $M \in \Mod(\theorybis)$ and
$\OI{\vec x \mid \varphi} \in \cat T$,
the formula $\vec x \sorting \varphi$ is interpreted in $R M$

\[
\I{\vec x \mid \varphi}_{R M}
F_{R M}\OI{\vec x \mid \varphi}
\cong
F_M \inclth\OI{\vec x \mid \varphi}
\I{\inclth\OI{\vec x \mid \varphi}}_M.
\]

In particular, for each sort $\sortbis$ of the signature $\Sig$ of $\theory$,

\begin{equation}\label{eq:iso-RM-sortwise}
\begin{array}{l l l}
(R M)(\sortbis)
& \cong
& \I{\inclth\OI{y : \sortbis \mid \True}}_M.
\end{array}
\end{equation}

It follows that $R$ induces an interpretation $(-)^{\inclth}$
of (possibly infinitary) first-order formulae over

as formulae over the signature $\Sigbis$ of $\theorybis$.

Let $\psi(\vec y)$, with $\vec y = y_1,\dots,y_n$,
be a formula over $\Sig$.

We define
a formula
$\psi^{\inclth}(\vec x_1,\dots,\vec x_n)$
over $\Sigbis$,
by induction on $\psi$, as follows.
If $\psi$ is atomic then
$\psi^{\inclth}$ is
$\inclth\OI{\vec y \mid \psi} = \OI{\vec x \mid \varphi}$, and
$(-)^{\inclth}$ commutes with propositional connectives.
$\psi = (\exists y : \sortbis)\psi'(\vec y,y)$,
$\OI{\vec x \mid \varphi}$
${\inclth\OI{y : \sortbis \mid \True}}$,
and define
$\psi^{\inclth}(\vec x_1,\dots,\vec x_n)$

\[
(\exists \vec x)
\left(
\varphi(\vec x)
(\vec x_1,\dots,\vec x_n,\vec x)
\right).
\]

The case of
$\psi = (\forall y)\psi'(\vec y,y)$
is similar.

For the next

given a formula $\psi(y_1,\dots,y_n)$
over $\Sig$ with $y_i$ of sort $\sortbis_i$,
set $\OI{\vec x_i \mid \varphi_i} \deq \inclth\OI{y_i : \sortbis_i \mid \True}$
for each $i$.
Further, for any model
$M$ of $\theorybis$
and sort $\sortbis$ of $\Sig$,
we denote by
\(
\chi^{\sortbis}_M
\I{\inclth\OI{y : \sortbis \mid \True}}_M
\to
(R M)(\sortbis)
\)
inverse of the isomorphism in eq. (<ref>).

In the above situation,
for all tuples
$\vec a_1,\dots,\vec a_n \in M$

$\vec a_i \in \I{\vec x_i \mid \varphi_i}_M$,
for each $i = 1,\dots,n$,

\[
\begin{array}{l !{\text{iff}} l}
R M
\models
\psi\left( \chi^{\sortbis_1}_M(\vec a_1) ,\dots, \chi^{\sortbis_n}_{M}(\vec a_n) \right)
& M \models \psi^{\inclth}(\vec a_1,\dots,\vec a_n).
\end{array}
\]

Note that $(-)^{\inclth}$ interprets
$\Lang_\kappa(\Sig)$ in $\Lang_\kappa(\Sigbis)$,
for each regular cardinal $\kappa$.
In particular, it interprets $\Lang_\omega(\Sig)$ in $\Lang_\omega(\Sigbis)$.
This is a crucial difference between interpretations and word-constructions

Now, consider an arbitrary finitely accessible arboreal adjunction

$R \colon \E \to \A$
and assume

w.l.o.g.that $\E$ is of the form $\Mod(\theory)$
for a cartesian theory $\theory$ over a signature $\Sig$.

The morphism of lfp categories $R \colon \E \to \A$
induces a formula interpretation $(-)^{\inclth}$ from $\Lang_\infty(\Sigbis)$ to
We thus obtain the following result from Theorems <ref>
and <ref>.

Assume <ref>.

Let $M \in \E$,
let $m \colon P \emb R M$ be a path embedding,
and let $Q$ be a path with $Q \cong \FG{\vec z \mid \varpi_Q}$.
Write $\OI{\vec x \mid \varphi} \in \cat T$
for $\inclth \OI{\vec z \mid \varpi_Q}$.

For each ordinal $\ord$,
there is a formula

$\Theta(M)_{R}^{m,Q,\ord}(\vec x)$ over $\Sig$
such that
for all $N \in \E$ and all $n \colon Q \emb R N$ induced by
$\vec b \in \I{\vec x \mid \varphi}_{N} \cong \I{\vec z \mid \varpi_Q}_{R N}$,
the following are equivalent:

* \(
\models
\Theta(M)_{R}^{m,Q,\ord}(\vec b)
\).

Position $(m,n)$ has rank $\geq \ord$ in the game $\G(R M, R N)$.

Let $\ordbis\coloneqq \ord_{R M, R N}$.
By Theorem <ref> and Corollary <ref>,
Duplicator wins the game $\G(R M, R N)$ from position $(m,n)$
precisely when $N \models \Theta(M)_{R}^{m,Q,\ordbis}(\vec b)$,
where $\vec b$ induces
$n \colon Q \emb R N$.

Thus, if $M$ and $N$ are $\Lang_\infty(\Sig)$-equivalent,
they are $R$-bisimilar.
By Example <ref>, this applies to the adjunctions between $\presh{\cat C}$ and $\presh{\forest(\cat C)}$ in Example <ref>.

§ FORMULAE FOR PATH EMBEDDINGS

Given a finitely accessible
arboreal adjunction

$\Ladj \colon \A \inadj \E \cocolon R$,

in Corollary <ref>
we obtained a logical description of $R$-bisimilarity under
the assumption that path embeddings in $\A$ are definable.

With the aim of weakening this assumption,
we note that in many concrete cases a morphism in $\A$ is an embedding
precisely when its image under the left adjoint $\Ladj$ is an embedding of structures,
i.e. $\Ladj$ “detects embeddings”.
In turn, embeddings of structures (with finitely presentable domain)
admit a simple logical description, as we now explain.

\[
\begin{array}{l l l}
\FEmb(\FG{\vec x \mid \varphi})(\vec x)
& \deq
& \bigwedge_{\substack{ \OI{\vec y \mid \atom} \in \cat T
\\
\text{$\atom$ atomic}
\
\bigwedge_{
\theta \in \cat T\funct{\OI{\vec x \mid \varphi}, \OI{\vec y \mid \True}}
(\forall \vec y)
\left(
\big( \atom(\vec y) ~\land~ \theta(\vec x,\vec y) \big)
\mathord{\bigvee}_{
\delta \in \cat T\funct{\OI{\vec x \mid \varphi}, \OI{\vec y \mid \atom}}
\delta(\vec x,\vec y)
\right)
\end{array}
\]

Formulae for embeddings of structures in $\Mod(\theory)$
with finitely presentable domains (Lemma <ref>).

Let $\theory$ be a cartesian theory over a signature $\Sig$,
with syntactic category $\cat T$.
We devise (infinitary) formulae describing
when a morphism in $\Mod(\theory)$
with finitely presentable domain is an embedding of structures, i.e. its image under the inclusion $\Mod(\theory) \into \Struct(\Sig)$ is a strong monomorphism.

Every strong monomorphism $m$ in $\Mod(\theory)$ is an embedding of structures.
The converse is not true,
even if we assume that the domain of $m$ is finitely presentable
(consider e.g. the inclusion of (additive) monoids $\NN \into \ZZ$).

Given $\OI{\vec x \mid \varphi} \in \cat T$,
we write
$\MI{\vec x, \vec x' \mid \iota_\varphi}$
for the morphism
$\OI{\vec x \mid \varphi} \to \OI{\vec x \mid \True}$
given by

\[
\begin{array}{l l l}
\MI{\vec x, \vec x' \mid \iota_\varphi}
& \deq
& \MI{\vec x, \vec x' \mid \varphi(\vec x) ~\land~ \vec x \Eq \vec x'}.
\end{array}
\]

$\imath_{\varphi} \colon \FG{\vec x \mid \True} \to \FG{\vec x \mid \varphi}$
stands for
the homomorphism corresponding to
the natural transformation
$\yoneda \MI{\vec x, \vec x' \mid \iota_\varphi}$
Theorem <ref>
(recall that $\yoneda$ is contravariant).

$h \colon \FG{\vec x \mid \varphi} \to M$
be a morphism in $\Mod(\theory)$.
The following statements are equivalent:

$h$ is an embedding of structures.

For all atomic formulae

$\vec y \sorting \atom$
and all morphisms $k, \ell$
such that
the leftmost square below commutes,

\[
\begin{array}{l !{\quad} l}

\begin{tikzcd}
\FG{\vec y \mid \True}
\arrow{r}[above]{\imath_\atom}
\arrow{d}[left]{\ell}
& \FG{\vec y \mid \atom}
\arrow{d}[right]{k}
\\
\FG{\vec x \mid \varphi}
\arrow{r}{h}
& M
\end{tikzcd}

\begin{tikzcd}
\FG{\vec y \mid \True}
\arrow{r}[above]{\imath_\atom}
\arrow{d}[left]{\ell}
& \FG{\vec y \mid \atom}
\arrow{dl}[description]{d}
\\
\FG{\vec x \mid \varphi}
\arrow{r}{h}
& M
\end{tikzcd}

\end{array}
\]

as in the rightmost diagram above.

\(
\models
\FEmb(\FG{\vec x \mid \varphi})(\vec a),
\)
$h$ takes $\vec x$ to $\vec a \in \I{\vec x \mid \varphi}_M$

$\FEmb(\FG{\vec x \mid \varphi})(\vec x)$
is defined as in Figure <ref>.

Assume without loss of generality
that a finitely presentable model is of the form
$\FG{\vec x \mid \varphi}$ with $\varphi$ quantifier-free
(cf. Remark <ref>).

If $\theory$ is empty and $\Sig=\sig$ is a finite relational signature,
hence $\Mod(\theory) = \Struct(\sig)$, we can replace the formula in
Figure <ref>
with the following finite
where $\const x_1,\dots,\const x_n$ are as in Lemma <ref>:

\[
\FEmb^{\sig}(\FG{\vec x \mid \varphi})(\vec x)
\mathord{\bigwedge}_{\substack{
\text{$\vec x \sorting \atom$ atomic}
\\
\FG{\vec x \mid \varphi} \models \lnot \atom(\const x_1,\dots,\const x_n)
\lnot \atom(\vec x)
\]

The next step consists in lifting the formulae for embeddings of structures
from $\E$ to $\A$.
This time, there is no formula interpretation associated with the functor $\Ladj$,
as the latter is not a morphism of lfp categories.
We overcome this hurdle by considering a variant of
Hodges' word-constructions (<ref>).
Under the assumption that $\Ladj$ detects embeddings,
word-constructions yield formulae for path embeddings in $\A$,
refining our logical description of $R$-bisimilarity (<ref>).

§.§ Hodges' word-constructions

Let $\theory$ and $\theorybis$ be cartesian theories
of signatures $\Sig$ and $\Sigbis$, respectively.
Recall from <ref> that
morphisms of lfp categories
$\Mod(\theorybis) \to \Mod(\theory)$,
i.e. limit-preserving finitary functors,
induce interpretations of formulae over $\Sig$
as formulae over $\Sigbis$.
Hodges' word-constructions [25, 26]
(see also <cit.>) are a relaxed form
of interpretations that apply to all finitary functors
$\Mod(\theorybis) \to \Mod(\theory)$;
in particular, to left adjoints.

Note that Hodges considered (infinitary) Horn theories,
while we allow for cartesian theories.

We outline the main ideas; for a self-contained exposition,
see Appendix <ref>.

Fix a finitary functor
$F \colon \Mod(\theorybis) \to \Mod(\theory)$.

Given a model $M \in \Mod(\theorybis)$,
since $F$ is finitary,
$F M$ is the filtered colimit in $\Mod(\theory)$
of the
$F \FG{\vec x \mid \varphi} \to F M$
with connecting maps induced by commuting triangles in $\Mod(\theorybis)$.

Recall from Lemma <ref>
that filtered colimits in $\Mod(\theory)$
are computed in $\Struct(\Sig)$.
for each sort $\sortbis \in \Sort(\Sig)$,
$F M(\sortbis)$
is the filtered colimit in $\Set$ of the
$F \FG{\vec x \mid \varphi}(\sortbis) \to F M(\sortbis)$

In other words,
$F M(\sortbis)$
is given by taking the disjoint sum of the

$F \FG{\vec x \mid \varphi}(\sortbis)$,
and quotienting by the equivalence relation that
identifies elements having the same image
in cospans of the form

\[
\begin{tikzcd}[column sep=large]
F \FG{\vec x \mid \varphi}(\sortbis)
\arrow{r}[above]{(F h)^{\sortbis}}
& F \FG{\vec z \mid \theta}(\sortbis)
& F \FG{\vec y \mid \psi}(\sortbis).
\arrow{l}[above]{(F k)^{\sortbis}}
\end{tikzcd}
\]

The key idea of word-constructions is to extend $\Sig$
to a signature $\WC(\Sig)$
with additional function symbols

\[
\begin{array}{*{5}{l}}
f^c_{\FG{\Env \mid \varphi}}
& :
& \sort_1 \ldots \sort_k
& \longto
& \sortbis
\end{array}
\]

$\Env = x_1 : \sort_1,\dots,x_k : \sort_k$
and $c \in (F\FG{\Env \mid \varphi})(\sortbis)$.
Here, $\sort_1,\dots,\sort_k$ are sorts of $\Sigbis$
and $\sortbis$ is a sort of $\Sig$.

Given $M \in \Mod(\theorybis)$, the intended interpretation
of $f^c_{\FG{\vec x \mid \varphi}}$
is the map

\[
\begin{array}{l l l}
\vec a \in \I{\vec x \mid \varphi}_M
& \longmapsto
& (F h_{\vec a})(c) \in F M
\end{array}
\]

where $h_{\vec a}$ takes $\vec x$ to $\vec a$
(cf. <ref>).
It follows that $F M$ is generated
(in the sense of <cit.>,
see <ref>)
by the valuation

\[
%\tag{$h_{\vec a} \colon \FG{\vec x \mid \varphi} \to M$}
\begin{array}{*{5}{l}}
& :
& (f^c_{\FG{\vec x \mid \varphi}} %(\vec a)
\vec a \in \I{\vec x \mid \varphi}_M)
& \longmapsto
& (F h_{\vec a})(c) \in F M
\end{array}
\]

where $\vec x \sorting \varphi$ ranges over
the cartesian formulae over $\theorybis$.

Moreover, given an atomic formula $\atom$ over $\Sig$,
we can check whether the formula

\[
\atom\left(
f^{c_1}_{\FG{\vec x_1 \mid \varphi_1}}(\vec x_1)
f^{c_n}_{\FG{\vec x_n \mid \varphi_n}}(\vec x_n)
\right)
\]

holds in $F M$,
under the valuation $C$ above,
by means of a (possibly infinitary) formula over $\Sigbis$.
This is a consequence of Lemma <ref>
combined with the following observation.

Let $\atom$ be an atomic formula over $\Sig$

and let $M \in \Mod(\theorybis)$.

The following
are equivalent
for all morphisms $h_i \colon \FG{\vec x_i \mid \varphi_i} \to M$,
with $i = 1,\dots,n$:

* $F M \models \atom((F h_1)(c_1),\dots,(F h_n)(c_n))$.

* There is some
$h \colon \FG{\vec x \mid \varphi} \to M$
such that

\[
\begin{array}{l l l}
F \FG{\vec x \mid \varphi}
& \models
& \atom\big( (F k_1)(c_1),\dots, (F k_n)(c_n) \big)
\end{array}
\]

where each $h_i$ factors as
\(
\FG{\vec x_i \mid \varphi_i}
\stackrel{k_i}\longto
\FG{\vec x \mid \varphi}
\stackrel{h}\longto
\).

We deduce a formula translation
from $\Lang_\infty(\Sig)$ to $\Lang_\infty(\Sigbis)$
(cf. <cit.>):

Let $\psi(y_1,\dots,y_n)$
be a formula over $\Sig$,
and let
\(
\vec f =
f^{c_1}_{\FG{\vec x_1 \mid \varphi_1}}(\vec x_1)
f^{c_n}_{\FG{\vec x_n \mid \varphi_n}}(\vec x_n)
\)
be additional function symbols from $\Sig(\WC)$.

There is a formula
$\psi(\vec f)^\WC(\vec x_1,\dots,\vec x_n)$
over $\Sigbis$
such that,
for all $M \in \Mod(\theorybis)$
and all tuples $\vec a_1,\dots,\vec a_n \in M$

$\vec a_i \in \I{\vec x_i \mid \varphi_i}_M$
for each $i = 1,\dots,n$,
the following are equivalent:

* $F M \models \psi\left( (F h_1)(c_1) ,\dots, (F h_n)(c_n) \right)$
where, for each $i = 1,\dots,n$, $h_i \colon \FG{\vec x_i \mid \varphi_i} \to M$

takes $\vec x_i$ to $\vec a_i$.

* $M \models \psi(\vec f)^\WC(\vec a_1,\dots,\vec a_n)$.

By Theorem <ref>,

if $M$ and $N$ are equivalent
in $\Lang_{\infty}(\Sigbis)$,
$F M$ and $F N$ are equivalent in $\Lang_{\infty}(\Sig)$.

In contrast with the case of interpretations, if $M$ and $N$ are equivalent
in $\Lang_{\omega}(\Sigbis)$,
it does not follow that $F M$ and $F N$ are equivalent in $\Lang_{\omega}(\Sig)$.

When $\Mod(\theorybis)$ and $\Mod(\theory)$
categories of structures,

item (1)

follows from <cit.>.

§.§ Word-constructions for path embeddings

As in <ref>,
we fix a finitely accessible arboreal adjunction

$\Ladj \colon \A \inadj \E \cocolon R$
such that $\A$ is cocomplete and its paths are finitely presentable.
We use the word-construction induced by $L$ to show that
Assumption <ref>
is entailed by the following

$\Delta 2$

For $P$ a path, a morphism $f \colon P \to a$ in $\A$ is an embedding

if and only if $\Ladj f$ is an embedding of structures.

(1) The concept of “embedding of structures” in $\E$ is not stable under Morita equivalence, as it depends on the choice of
a theory $\theory$ such that ${\E \cong \Mod(\theory)}$.

(2) In many examples,
$\E$ is of the form $\Struct(\sig)$,
the arboreal adjunction is comonadic,
and <ref> is satisfied for all morphisms in $\A$.

In this case, it follows that
the factorisation system of $\A$
is given by (epimorphisms, strong monomorphisms).

As usual, we shall identify $\E$ with $\Mod(\theory)$, for a cartesian theory $\theory$ of signature $\Sig$, and $\A$ with $\Mod(\theorybis)$, for a cartesian theory $\theorybis$ of signature $\Sigbis$. We have:

Assume <ref>.
For each path

$P \cong \FG{\vec y \mid \psi}$,
there is a formula

$\FEmb(\FG{\vec y \mid \psi})^{\WC(\Ladj)}(\vec y)$

over $\Sigbis$
such that the following statements are equivalent
for all $a \in \A$,
and all homomorphisms $h \colon \FG{\vec y \mid \psi} \to a$
taking $\vec y$ to $\vec b \in \I{\vec y \mid \psi}_a$.

* $h \colon \FG{\vec y \mid \psi} \to a$ is an embedding in $\A$.

* \(
\models
\FEmb(\FG{\vec y \mid \psi})^{\WC(\Ladj)}(\vec b).
\)

By Proposition <ref>,
$L$ sends paths to finitely presentable objects.
If $\FG{\vec x \mid \varphi} \cong \Ladj \FG{\vec y \mid \psi}$,
Lemma <ref>
gives us
a formula
$\FEmb(\FG{\vec x \mid \varphi})(\vec x) \in \Lang_\infty(\Sig)$
such that the following are equivalent
for all $a \in \A$
and all $h \colon \FG{\vec y \mid \psi} \to a$:

* $h \colon \FG{\vec y \mid \psi} \to a$
is an embedding in $\A$.

* \(
\Ladj a
\models
\FEmb(\FG{\vec x \mid \varphi})(\vec c)
\),
where $\Ladj h \colon \FG{\vec x \mid \varphi} \to \Ladj a$
is induced by
$\vec c \in \I{\vec x \mid \varphi}_{\Ladj a}$.

Write $\vec x = x_1,\dots,x_n$
and let
\(
\vec f = f^{\const x_1}_{\FG{\vec y \mid \psi}}(\vec y_1)
f^{\const x_n}_{\FG{\vec y \mid \psi}}(\vec y_n)
\)
be additional function symbols in $\Sig(\WC)$,
where $\const x_1,\ldots, \const x_n \in \FG{\vec x \mid \varphi}$ are as in Lemma <ref>.
By Theorem <ref>,
we can define
$\FEmb(\FG{\vec y \mid \psi})^{\WC(\Ladj)}(\vec y)$
as the formula

\[
\FEmb(\FG{\vec x \mid \varphi})(\vec f)^{\WC(\Ladj)}(\vec y,\dots,\vec y).
\qedhere
\]

The formulae
$\FEmb(\FG{\vec y \mid \psi})^{\WC(\Ladj)}(\vec y)$
of Lemma <ref>
can be assumed to be finite
if $\E \cong \Struct(\sig)$
for a finite relational signature $\sig$
and, up to isomorphism, each path in $\A$ admits finitely many quotients.

Lemma <ref>, combined with Corollary <ref>,

Assume <ref>.

$m \colon P \emb R M$ be a path embedding
with $M \in \E$,
and let $Q \cong \FG{\vec z \mid \varpi_Q}$ be a path.
Write $\OI{\vec x \mid \varphi} \in \cat T$
for $\inclth \OI{\vec z \mid \varpi_Q}$.

For each ordinal $\ord$,
there is a formula

$\Theta(M)^{m,Q,\ord}(\vec x)$ over $\Sig$
such that,
for all $N \in \E$ and all $n \colon Q \emb R N$
induced by
$\vec b \in \I{\vec x \mid \varphi}_{N} \cong \I{\vec z \mid \varpi_Q}_{R N}$,
the following are equivalent:

* \(
\models
\Theta(M)^{m,Q,\ord}(\vec b)
\).

* Position $(m,n)$ has rank $\geq \ord$ in the game $\G(R M, R N)$.

Remark <ref>
so we get the following result on the expressive power of finitely accessible arboreal adjunctions:

Assuming <ref>, models $M,N\in \Mod(\theory)$ are $R$-bisimilar provided they are $\Lang_\infty(\Sig)$-equivalent.

We conclude by discussing how the arboreal adjunction

\[
\begin{tikzcd}
{\cat R^E_k(\sig^I)} \arrow[r, bend left=25, ""{name=U, below}, "\Ladj_k"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D}, "R_k"{below}]
& {\Struct(\sig^I)} \arrow[r, bend left=25, ""{name=U', below}, "H"{above}]
\arrow[r, leftarrow, bend right=25, ""{name=D'}, "J"{below}] & {\Struct(\sig)}
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U, to=D]
\arrow[phantom, "\textnormal{\footnotesize{$\bot$}}", from=U', to=D']
\end{tikzcd}
\]

from Example <ref> fits in our framework (the same reasoning applies to Example <ref>). The composite adjunction does not satisfy <ref>, but the comonadic adjunction $L_k \dashv R_k$ does. We can then apply Corollary <ref>
to reduce $R^I_{k}$-bisimilarity to $\Lang_\infty(\sig^I)$, and take an interpretation along the morphism of lfp categories
to obtain formulae

in $\Lang_\infty(\sig)$.

In fact, by Remark <ref>,
the formulae $\Theta(M)^{m,Q,\ord}$
are finite for finite $\ord$.
It follows by Remark <ref>
that, as expected, we obtain finite Hintikka formulae
for $R^I_k$-bisimilarity.

§ CONCLUSION AND FUTURE WORK

We have introduced finitely accessible arboreal adjunctions, and  proved that the ranks of back-and-forth games in the arboreal category can be defined in the infinitary logic of the extensional category. This relies on the assumption that path embeddings in the arboreal category are definable, and we have shown how this condition can be ensured in a broad range of examples.
Therefore, the induced model comparison games  cannot distinguish  between models that are equivalent in infinitary first-order logic.

We explained how our assumptions are satisfied by the comonadic approach to  Ehrenfeucht-Fraïssé games. This applies also to pebble and modal bisimulation games [8, 5], and we expect that the same methodology will extend to guarded fragments [3] and  hybrid logic [4]. On the other hand, our results show that game comonads for MSO [28] cannot lead to finitely accessible arboreal adjunctions with the obvious choice of embeddings.

This suggests that in order to handle stronger logics, one would have to consider $\kappa$-accessible arboreal adjunctions for uncountable regular cardinals $\kappa$.
We believe this is a natural line for future investigation. In particular, games for generalised Lindström quantifiers [15, 16] may be instrumental in developing a systematic study.
Other interesting examples to look at include [22].

In a different direction, having provided novel examples of arboreal categories based on presheaves, we intend to carry out a thorough comparison with bisimulation via open maps [34].

§ ACKNOWLEDGMENT

Research supported by the EPSRC grant EP/V040944/1
and the ANR project ReCiProg (ANR-21-CE48-0019).

[1]
S. Abramsky, “Structure and Power: an Emerging Landscape,” Fundam.
Informaticae, vol. 186, no. 1-4, pp. 1–26, 2022. [Online]. Available:

[2]
S. Abramsky, A. Dawar, and P. Wang, “The Pebbling Comonad in Finite Model
Theory,” in Proceedings of LICS'17, 2017.

[3]
S. Abramsky and D. Marsden, “Comonadic semantics for guarded fragments,” in
36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS
2021, Rome, Italy, June 29 - July 2, 2021, 2021, pp. 1–13. [Online].
Available: <https://doi.org/10.1109/LICS52264.2021.9470594>

[4]
——, “Comonadic semantics for hybrid logic,” in 47th International
Symposium on Mathematical Foundations of Computer Science, MFCS 2022,
August 22-26, 2022, Vienna, Austria, 2022, pp. 7:1–7:14. [Online].
Available: <https://doi.org/10.4230/LIPIcs.MFCS.2022.7>

[5]
S. Abramsky and L. Reggio, “Arboreal Categories: An Axiomatic Theory of
Resources,” 2021, abs/2102.08109. [Online]. Available:

[6]
——, “Arboreal Categories and Resources,” in 48th International
Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16,
2021, Glasgow, Scotland (Virtual Conference), 2021, pp. 115:1–115:20.
[Online]. Available: <https://doi.org/10.4230/LIPIcs.ICALP.2021.115>

[7]
S. Abramsky and N. Shah, “Relating structure and power: Comonadic semantics
for computational resources,” in Proceedings of CSL'18, 2018, pp.

[8]
——, “Relating structure and power: Comonadic semantics for computational
resources,” J. Log. Comput., vol. 31, no. 6, pp. 1390–1428, 2021.
[Online]. Available: <https://doi.org/10.1093/logcom/exab048>

[9]
J. Adámek, H. Herrlich, and G. Strecker, Abstract and concrete
categories: The joy of cats.1em plus 0.5em minus 0.4emReprints in Theory and Applications of Categories, 2006, vol. 17, originally
published by John Wiley and Sons, New York, 1990.

[10]
J. Adámek, S. Milius, L. Sousa, and T. Wissmann, “On finitary
functors,” Theory Appl. Categ., vol. 34, no. 35, pp. 1134–1164,

[11]
J. Adámek and H.-E. Porst, “Algebraic Theories of Quasivarieties,”
Journal of Algebra, vol. 208, no. 2, pp. 379 – 398, 1998.

[12]
J. Adámek and J. Rosický, Locally Presentable and Accessible
Categories, ser. London Mathematical Society Lecture Notes Series.1em plus 0.5em minus 0.4emCambridge University Press, 1994, vol. 189.

[13]
T. Beke and J. Rosický, “Elementary equivalences and accessible
functors,” Annals of Pure and Applied Logic, vol. 169, no. 7, pp.
674–703, 2018. [Online]. Available:

[14]
F. Borceux, Handbook of Categorical Algebra: Volume 1, Basic Category
Theory, ser. Encyclopedia of Mathematics and its Applications.1em
plus 0.5em minus 0.4emCambridge University Press, 1994.

[15]
X. Caicedo, “Back-and-Forth Systems for Arbitrary Quantifiers,” in
Mathematical Logic in Latin America, ser. Studies in Logic and the
Foundations of Mathematics, A. Arruda, R. Chuaqui, and N. Da Costa,
Eds.1em plus 0.5em minus 0.4emElsevier, 1980, vol. 99, pp.
83–102. [Online]. Available:

[16]
A. ConghaileÓ Conghaile and A. Dawar, “Game Comonads &
Generalised Quantifiers,” in 29th EACSL Annual Conference on
Computer Science Logic, CSL, vol. 183.1em plus 0.5em minus
0.4emSchloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021,
pp. 16:1–16:17.

[17]
M. Coste, “Une approche logique des théories définissables par
limites projectives finies,” Université Paris-Nord, Séminaire
Bénabou, 1976.

[18]
A. Dawar, T. Jakl, and L. Reggio, “Lovász-type theorems and game
comonads,” in Proceedings of LICS'21, 2021.

[19]
Y. Diers, Categories of Boolean sheaves of simple algebras, ser. Lecture
Notes in Mathematics.1em plus 0.5em minus 0.4emSpringer-Verlag,
Berlin, 1986, vol. 1187.

[20]
H.-D. Ebbinghaus and J. Flum, Finite Model Theory, 2nd ed., ser.
Springer Monographs in Mathematics.1em plus 0.5em minus 0.4emSpringer, 1999.

[21]
A. Ehrenfeucht, “An application of games to the completeness problem for
formalized theories,” Fund. Math., vol. 49, pp. 129–141, 1960/61.

[22]
C. Ford, S. Milius, L. Schröder, H. Beohar, and B. König, “Graded
Monads and Behavioural Equivalence Games,” in LICS '22: 37th Annual
ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 -
5, 2022, C. Baier and D. Fisman, Eds.1em plus 0.5em minus 0.4emACM, 2022, pp. 61:1–61:13. [Online]. Available:

[23]
R. Fraïssé, “Sur quelques classifications des systèmes de relations,”
Publ. Sci. Univ. Alger. Sér. A, vol. 1, pp. 35–182, 1954.

[24]
P. Gabriel and F. Ulmer, Lokal Präsentierbare Kategorien, ser.
Lecture Notes in Mathematics.1em plus 0.5em minus 0.4emSpringer, 1971, vol. 221.

[25]
W. Hodges, “A normal form for algebraic constructions,” Bulletin of the
London Mathematical Society, vol. 6, no. 1, pp. 57–60, 1974.

[26]
——, “A normal form for algebraic constructions II,” Logique et
Analyse, vol. 18, no. 71/72, pp. 429–487, 1975. [Online]. Available:

[27]
——, Model Theory, ser. Encyclopedia of Mathematics and its
Applications.1em plus 0.5em minus 0.4emCambridge University
Press, 1993, vol. 42.

[28]
T. Jakl, D. Marsden, and N. Shah, “A game comonadic account of Courcelle and
Feferman-Vaught-Mostowski theorems,” 2022,

[29]
T. Jech, Set Theory: The Third Millennium Edition, revised and
expanded, ser. Springer Monographs in Mathematics.1em plus 0.5em
minus 0.4emSpringer, 2006.

[30]
P. Johnstone, Stone Spaces, ser. Cambridge Studies in Advanced
Mathematics.1em plus 0.5em minus 0.4emCambridge University
Press, 1982.

[31]
——, Sketches of an Elephant: A Topos Theory Compendium, ser.
Oxford Logic Guides.1em plus 0.5em minus 0.4emClarendon Press,

[32]
A. Joyal and I. Moerdijk, “A completeness theorem for open maps,” Ann.
Pure Appl. Log., vol. 70, no. 1, pp. 51–86, 1994. [Online]. Available:

[33]
A. Joyal, M. Nielsen, and G. Winskel, “Bisimulation and open maps,” in
Proceedings of the Eighth Annual Symposium on Logic in Computer Science
(LICS'93), Montreal, Canada, June 19-23, 1993, 1993, pp. 418–427.
[Online]. Available: <https://doi.org/10.1109/LICS.1993.287566>

[34]
——, “Bisimulation from Open Maps,” Inf. Comput., vol. 127,
no. 2, pp. 164–185, 1996.

[35]
M. Kashiwara and P. Schapira, Categories and Sheaves, ser. Grundlehren
der mathematischen Wissenschaften.1em plus 0.5em minus 0.4emSpringer-Verlag Berlin Heidelberg, 2006, vol. 332.

[36]
A. S. Kechris, Classical Descriptive Set Theory, ser. Graduate Texts
in Mathematics.1em plus 0.5em minus 0.4emSpringer, 1995, vol.

[37]
L. Libkin, Elements of Finite Model Theory, ser. Texts in Theoretical
Computer Science. An EATCS Series.1em plus 0.5em minus 0.4emSpringer Berlin, Heidelberg, 2004.

[38]
S. Mac Lane, Categories for the Working Mathematician, 2nd ed.1em plus 0.5em minus 0.4emSpringer, 1998.

[39]
S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic: A First
Introduction to Topos Theory.1em plus 0.5em minus 0.4emSpringer, 1992.

[40]
M. Makkai and A. M. Pitts, “Some Results on Locally Finitely Presentable
Categories,” Transactions of the American Mathematical Society, vol.
299, no. 2, pp. 473–496, 1987. [Online]. Available:

[41]
M. Mislove, “When are order scattered and topologically scattered the
same?” in Orders: description and roles (L'Arbresle, 1982), ser.
North-Holland Math. Stud.1em plus 0.5em minus 0.4emNorth-Holland, Amsterdam, 1984, vol. 99, pp. 61–80.

[42]
J. Nešetřil and P. Ossona de Mendez, “Tree-depth, subgraph coloring
and homomorphism bounds,” European Journal of Combinatorics,
vol. 27, no. 6, pp. 1022–1041, 2006.

[43]
L. Reggio, “Polyadic sets and homomorphism counting,” Advances in
Mathematics, vol. 410, Part A, no. 108712, 2022.

§ ADDITIONAL MATERIAL FOR <REF> (SEC:PRELIM)

§.§ Structures and homomorphisms

A many-sorted signature $\Sig$
consists of
a set $\Sort(\Sig)$ of sorts
together with collections

\begin{align*}
\Fun(\Sig)
& =
\mathord{\bigcup}_{(\sortbis_1,\dots,\sortbis_n;\sortbis) \in \Sort(\Sig)^{n+1}}
\Fun(\Sig)(\sortbis_1,\dots,\sortbis_n;\sortbis)
\\
\Rel(\Sig)
& =
\mathord{\bigcup}_{(\sortbis_1,\dots,\sortbis_n) \in \Sort(\Sig)^{n}}
\Rel(\Sig)(\sortbis_1,\dots,\sortbis_n)
\end{align*}

of, respectively,
and relation
We write
$f \colon \sortbis_1 \dots \sortbis_n \to \sortbis$
$f \in \Fun(\Sig)(\sortbis_1,\dots,\sortbis_n;\sortbis)$,
$R \into \sortbis_1 \dots \sortbis_n$
$R \in \Rel(\Sig)(\sortbis_1,\dots,\sortbis_n)$.

Let $\Sig$ be a signature.

* A $\Sig$-structure $M$
is given by the following data:

* for each sort
$\sortbis \in \Sort(\Sig)$,
a set $M(\sortbis)$;

* for each function symbol

$f \colon \sortbis_1 \dots \sortbis_n \to \sortbis$,
a function
$f_M \colon M(\sortbis_1) \times \dots \times M(\sortbis_n) \to M(\sortbis)$;

* for each relation symbol
$R \into \sortbis_1 \dots \sortbis_n$,
a relation
$R_M \sle M(\sortbis_1) \times \dots \times M(\sortbis_n)$.

* A homomorphism of $\Sig$-structures
$h \colon M \to N$

a family
of functions
\(
%h =
h^\sortbis \colon M(\sortbis) \to N(\sortbis)
\mid
\sortbis \in \Sort(\Sig)
\)
such that
for every
$f \colon \sortbis_1 \dots \sortbis_n \to \sortbis$
$R\into \sortbis_1 \dots \sortbis_n$,
and for all
$a_1 \in M(\sortbis_1),\dots,a_n \in M(\sortbis_n)$,
we have

\[
\begin{array}{r c r}
h^{\sortbis}( f_M(a_1,\dots,a_n) )
& =
& f_N( h^{\sortbis_1}(a_1), \dots, h^{\sortbis_n}(a_n) )
\\

& \imp
& R_N\left( h^{\sortbis_1}(a_1), \dots, h^{\sortbis_n}(a_n) \right)
\end{array}
\]

* We write $\Struct(\Sig)$ for the category
whose objects are $\Sig$-structures
and whose morphisms are homomorphisms.

§.§ Infinitary first-order logic

We shall consider different fragments of infinitary first-order logic.
In contrast with <cit.> but in accordance
with <cit.>
we work with formulae having at most finitely many free variables.
These variables are declared contexts
of the form $x_1 : \sortbis_1,\dots,x_n : \sortbis_n$
where the variables $x_1,\dots,x_n$ are pairwise distinct.

The terms-in-context
$\Env \sorting t : \sortbis$
over a signature $\Sig$
are inductively defined as follows:

* $x_1:\sortbis_1,\dots,x_n:\sortbis_n \sorting x_i : \sortbis_i$
is a term-in-context for every $i =1,\dots,n$,

* $\Env \sorting f(t_1,\dots,t_n) : \sortbis$
is a term-in-context

$f \colon \sortbis_1 \dots \sortbis_n \to \sortbis$
$\Env \sorting t_i : \sortbis_i$
is a
for each $i = 1,\dots,n$.

We now turn to formulae.

Let $\Sig$ be a signature.
The many-sorted language
$\Lang_\infty(\Sig) = \Lang_{\infty} (= \Lang_{\infty,\omega})$
consists of the formulae-in-context
$\Env \sorting \varphi$
inductively defined as follows.

* $\Env \sorting (t \Eq_\sortbis u)$ is a formula-in-context
$\Env \sorting t : \sortbis$ and $\Env \sorting u : \sortbis$
are terms-in-context.

* $\Env \sorting R(t_1,\dots,t_n)$ is a formula-in-context
$R \into \sortbis_1 \dots \sortbis_n$
$\Env \sorting t_i : \sortbis_i$
is a term-in-context for each $i = 1,\dots,n$.

* $\Env \sorting \lnot \varphi$ is a formula-in-context
$\Env \sorting \varphi$
is a formula-in-context.

* $\Env \sorting (\forall x : \sortbis)\varphi$
$\Env \sorting (\exists x : \sortbis)\varphi$
are formulae-in-context
$\Env,x : \sortbis \sorting \varphi$
is a formula-in-context.

* $\Env \sorting \bigwedge_{i \in I}\varphi_i$
$\Env \sorting \bigvee_{i \in I}\varphi_i$
are formulae-in-context
if $I$ is a small set and if
$\Env \sorting \varphi_i$
is a formula-in-context for each $i \in I$.

Note that $\Lang_\infty$ is a large set.
Note also that by construction, formulae-in-context
have at most finitely many free variables.
Finally, note that in case $\Sig$ is purely relational
(i.e. $\Fun(\Sig) = \emptyset$),
the notion of term-in-context still properly
handles the contexts of atomic formulae:
e.g.$\Env \sorting P(x_1,\dots,x_n)$
requires all the $x_i$ to be declared in $\Env$ with
appropriate sort,
but $\Env$ may declare additional variables.

§ ADDITIONAL MATERIAL FOR <REF> (SEC:LFP)

The restriction of Gabriel-Ulmer duality to posetal categories yields the well known duality between semilattices and algebraic lattices [41], which we recall in this appendix.
Gabriel-Ulmer duality, as outlined in <ref>, can then be obtained by retracing the steps leading to the duality between semilattices and algebraic lattices.

A (meet-)semilattice is a poset in which every finite subset has an infimum. Morphisms of semilattices are maps that preserve finite infima. Let $\SL$ denote the ensuing category.

A poset, regarded as a (small) category, is finitely complete if and only if it is a semilattice. Morphisms of semilattices correspond precisely to lex-morphisms.

In the same way Boolean algebras correspond to classical propositional theories via the Lindenbaum-Tarski construction, semilattices correspond to theories in the $\{\top,\wedge\}$-fragment.

A model of a semilattice $L$ is a morphism of semilattices $h\colon L\to 2$
into the two-element semilattice.
The set $\SL[L,2]$ of all models of $L$ is a poset with respect to the pointwise order,
and is order-isomorphic to the poset $\Filter L$ of filters on $L$
(ordered by set-theoretic inclusion)
via the map $h\mapsto h^{-1}(1)$,
where $1$ denotes the infimum of the empty set.

Regarding a semilattice $L$ as a category, the
functor category $[L,2]$ (equivalently, the category of presheaves over $L^\op$)
can be identified with the poset $\Up L$ of upwards closed subsets of $L$.
The (contravariant) Yoneda embedding $L^\op \to \Up L$,
sending $a$ to $\up a$,
then factors through the inclusion $\Filter L\into \Up L$.

The intersection of a set of filters is again a filter,
hence the poset $\Filter L$ is a complete lattice.
Further, directed suprema in $\Filter L$ are given by unions.
It follows that, for all morphisms of semilattices $k\colon L\to M$,
the map $\Filter k\colon \Filter M \to \Filter L$
defined by $F\mapsto k^{-1}(F)$ preserves arbitrary infima and directed suprema.

To characterise the lattices of the form $\Filter L$,
recall that an element $x$ of a poset $X$ is compact
if, for all directed subsets $S\subseteq X$ admitting a supremum,
$x\leq \bigvee{S}$ implies $x\leq y$ for some $y\in S$.

Regarding the poset $X$ as a category, an element $x\in X$ is finitely presentable precisely when it is compact.

Principal filters are (exactly the) compact elements of $\Filter L$,
thus each element of $\Filter L$ is a directed supremum of compact ones.
That is, $\Filter L$ is an algebraic lattice:

A poset $X$ is an algebraic lattice if it satisfies:

* $X$ is a complete lattice.

* Every element of $X$ is the supremum of a directed set of compact elements.

Write $\Alg$ for the category of algebraic lattices and maps preserving all infima and directed suprema.

A poset, regarded as a (small) category, is lfp if and only if it is an algebraic lattice. Maps between algebraic lattices that preserve all infima and directed suprema correspond precisely to morphisms of lfp categories.

Given an algebraic lattice $X$, let $KX$ be the set of compact elements of $X$ with the induced order. Note that $KX$ admits finite suprema (computed in $X$), hence $(KX)^\op$ is a semilattice. Now, consider a morphism $f\colon X\to Y$ in $\Alg$. Since $f$ preserves all infima, it has a left adjoint $g$; in turn, $g$ preserves compact elements because $f$ preserves directed suprema. If $Kf\colon KY\to KX$ denotes the restriction of $g$ to the compact elements, its order-dual $(Kf)^\op \colon (KY)^\op\to (KX)^\op$ is a morphism of semilattices.

We thus have functors

\[
\Filter(-)\colon \SL^\op \leftrightarrows \Alg \cocolon K(-)^\op.
\]

These functors are quasi-inverse each other,
yielding an equivalence between $\SL^\op$ and $\Alg$; see [41].
In particular, for every semilattice $L$ and algebraic lattice $X$ there are (natural)
isomorphisms $L\cong (K(\Filter L))^\op$ and $X\cong \Filter (K(X)^\op)$.

For any algebraic lattice $X$, the set $\Alg[X,2]$ equipped with the pointwise order is isomorphic to $(KX)^\op$. In fact, $K(-)^\op\colon \Alg\to\SL^\op$ is naturally isomorphic to (the appropriate co-restriction of) the functor $\Alg[-,2]$. In other words, the duality above is induced by the dualising object $2$, regarded as either a semilattice or an algebraic lattice.

§ ADDITIONAL MATERIAL FOR <REF> (SEC:FINACCARB)

This Appendix <ref>
is devoted to the proof of Theorem <ref>.

Let $\forest$ be a forest, seen as a (posetal) category.
The presheaf category $\presh{\forest}$ is arboreal when equipped with the
factorisation system (epimorphisms, monomorphisms).
the paths in $\presh{\forest}$ are precisely the representable functors,
along with the initial object.

Throughout this section, we fix an arbitrary forest $\forest$
(regarded as a thin category) and consider the presheaf category

\[
\begin{array}{l l l}
\A
& \deq
& [\forest^\op,\Set].
\end{array}
\]

Recall that an object of $\A$ is representable if it is
(naturally) isomorphic to one of the form $\yo a$ for some $a\in \forest$, where

\[
\begin{array}{*{5}{l}}
\yo
& \colon
& \forest
& \longto
& \A
\end{array}
\]

is the Yoneda embedding.
The aim of this section is to prove that $\A$ is an arboreal category.

Because $\A$ as a presheaf topos is in particular an elementary topos,
the usual (epi, mono) factorisation system on $\A$ is a stable proper factorisation
(see e.g. <cit.>).
Therefore, we can consider paths in $\A$ with respect to this factorisation system.
To start with,
in the next two lemmas we shall see that a non-initial object is a path
if, and only if,
it is representable.

Any representable object of $\A$ is a path.

It suffices to show that $\yo a$ is a path for any $a\in \forest$.

\[
a_1 \prec \dots \prec a_n=a
\]

be the finite chain of predecessors of $a$ in $\forest$.
Direct inspection shows that the lattice $\Emb{(\yo a)}$
can be identified with the finite chain

\[
\zero
\prec
\yo a_1
\prec
\dots
\prec
\yo a
\]

where $\zero$ is the initial object of $\A$, i.e. the empty presheaf
(recall that, in a topos,
the unique arrow from the initial object is monic).
Therefore, $\yo a$ is a path.

Conversely, we shall show in Lemma <ref>
below that every non-initial path of $\A$
is representable.
But before, we note the following simple fact on presheaf

Let $\cat C$ be a thin category.
Then in $\presh{\cat C}$,
every morphism $\yo c \to P$ is a monomorphism.

An $f \in \presh{\cat C}\funct{\yo c, P}$
is a (natural) family of functions
$(f_d : \cat C\funct{d,c} \to P(d) \mid d \in \cat C)$.
But since each $\cat C\funct{d,c}$ has at most one element,
each $f_d$ is necessarily injective,
and $f$ is indeed monic.

Let $P$ be a non-initial object of $\A$. If $P$ is a path, then it is representable.

Suppose that $P$ is a non-initial object of $\A$.

As the Yoneda embedding $\yo \colon \forest \to \A$ is dense,
$P$ is the colimit of the canonical diagram

\[
\begin{array}{*{7}{l}}
& \colon
& \yo/{P}
& \stackrel{\pi}\longto
& \forest
& \stackrel{\yo}\longto
& \A.
\end{array}
\]

This diagram is non-empty because $P$ is not initial.
Further, every morphism $\yo a\to P$, with $a\in\forest$, is monic by
Lemma <ref>.

So, if $P$ is a path, there exists an object $i$ of $\yo/{P}$ such that,
for any other $j$ in $\yo/{P}$,
the colimit map $D(j)\to P$ factors through the colimit map $D(i)\to P$.
It follows at once that $P\cong \yo a$ where $a \deq \pi(i)$.

With regards to Lemma <ref>,
the reason why we need to assume that $P$ is non-initial
is simply that the initial object of a presheaf category is never representable.

Every path in $\A$ is a subterminal object.
This is clearly the case for the initial object of $\A$.
For paths that are not initial in $\A$,
this is a direct consequence of Lemma <ref>.

Combining Lemmas <ref> and <ref>,
we obtain the following result:

The Yoneda embedding $\yo \colon \forest\to \A$ co-restricts to an equivalence between
$\forest$ and the full subcategory of $\A$ defined by the non-initial paths.

A slightly different perspective on the previous result is as follows.
As the lattice of subterminal objects in $\A$ can be identified with the lattice
$\Down(\forest)$ of downwards closed subsets of $\forest$,
the representable objects of $\A$
coincide with the completely join-irreducible elements of $\Down(\forest)$.
Proposition <ref> then states that the completely
join-irreducible elements of $\Down(\forest)$ are precisely the paths.

$\A$ satisfies the 2-out-of-3 condition
(condition <ref> in Definition <ref>).

Consider paths $P,Q,R$ in $\A$ and assume that the composition

\[
\begin{array}{*{5}{l}}
& \stackrel{\alpha}\longto
& Q
& \stackrel{\beta}\longto
& R
\end{array}
\]

is an epimorphism.
It suffices to show that, for any $a\in \forest$,
the component $\alpha_a\colon P(a)\to Q(a)$ is surjective.
Recall from Remark <ref> that paths are subterminal objects.
Hence, we must show that, for any $a\in \forest$,
$Q(a)\neq\emptyset$ entails $P(a)\neq\emptyset$.
We prove the contrapositive.
If $P(a)=\emptyset$ then, since $(\beta\comp \alpha)_a$ is an epimorphism,
also $R(a)=\emptyset$.
Since there is no function from a non-empty set to the empty set,
it must be $Q(a)=\emptyset$.

$\A$ is a path category.

As already mentioned, the (epi, mono) factorisation system in $\A$ is proper and stable.
Further, $\A$ has all coproducts of small families of paths
(in fact, a presheaf category admits all small colimits, which are computed in $\Set$).
Finally, $\A$ satisfies the 2-out-of-3 condition by Lemma <ref>.

Every path in $\A$ is weakly connected, and every non-initial path is connected.

The initial object of $\A$ is trivially weakly connected.
Now, suppose that $P$ is a non-initial path in $\A$.
In view of Lemma <ref>,
we can assume without loss of generality that
$P$ is of the form $\yo a$ for some $a\in \forest$.
For any non-empty small family of paths $\{P_i\mid i\in I\}$, we have:

\begin{align*}
\A\funct{\yo a, \mathord{\coprod}_{i\in I}{P_i}}
& \cong
\big(\coprod_{i\in I}{P_i}\big)(a)
\tag{Yoneda Lemma}
\\
& \cong
\coprod_{i\in I}{P_i(a)}
\tag{colimits computed in $\Set$}
\\
& \cong
\coprod_{i\in I}{\A\funct{\yo a, P_i}}.
\tag{Yoneda Lemma}
\end{align*}

Direct inspection shows that the ensuing bijection

\[
\coprod_{i\in I}{\A\funct{\yo a, P_i}}
\longto
\A\funct{\yo a, \mathord{\coprod}_{i\in I}{P_i}}
\]

is the canonical map that, on a summand
$\A\funct{\yo a, P_j}$,
sends an arrow $\yo a\to P_j$ to its composition with the coproduct map
$P_j \to \coprod_{i\in I}{P_i}$. Therefore, $\yo a$ is connected.

Every object of $\A$ is path-generated.

By Remark <ref>
and Proposition <ref>,
it is enough to show that the full subcategory
of $\A$
defined by the paths is dense.
By Proposition <ref>,
the full subcategory of $\A$ defined by the non-initial paths is dense.
It follows easily that $\pth{\A}$ is also dense.

$\A$ is an arboreal category.

This is a consequence of Proposition <ref> and
Lemmas <ref> and <ref>.

§ ADDITIONAL MATERIAL FOR <REF> (SEC:COSTE)

We shall give more details on Example <ref>
(on cartesian theories of functors)
in Example <ref>
(<ref>) below.

§.§ Additional material for <ref> (sec:coste:synt)

Syntactic categories are finitely complete (<cit.>):

Let $\theory$ be a

The syntactic category $\cat T$ of $\theory$
is finitely complete and small.
More precisely:

* the terminal object of $\cat T$
$\OI{\mid \True}$
(i.e. the formula $\True$ in the empty context);

* given objects
$\OI{\vec x \mid \varphi}$
$\OI{\vec y \mid \psi}$
of $\cat T$
(where $\vec x$ and $\vec y$ are assumed to be disjoint),
their product in $\cat T$ is

\[
\begin{tikzcd}[row sep=0cm]
& \OI{\vec x, \vec y \mid \varphi \land \psi}
\arrow{dl}[above, xshift=-8ex]
{\MI{\vec x,\vec y,\vec x' \mid \varphi \land \psi \land \vec x \Eq \vec x'}}
\arrow{dr}
{\MI{\vec x,\vec y,\vec y' \mid \varphi \land \psi \land \vec y \Eq \vec y'}}
\\
\OI{\vec x \mid \varphi}
& \OI{\vec y \mid \psi}
\end{tikzcd}
\]

* the equalizer of
\(
\MI{\vec x, \vec y \mid \theta}
\MI{\vec x, \vec y \mid \vartheta}
\colon
\OI{\vec x \mid \varphi}
\to
\OI{\vec y \mid \psi}
\)
the morphism
\(
\MI{\vec x,\vec x'
\mid
(\exists \vec y)(\theta \land \vartheta) \land \vec x \Eq \vec x'}
\)
of domain
$\OI{\vec x \mid (\exists \vec y)(\theta \land \vartheta)}$.

The following hold:

A small category is finitely complete
if, and only if, it is equivalent to the syntactic category of a theory $\theory$.

A category is lfp if, and only if, it is equivalent to $\Mod(\theory)$
for some theory $\theory$.

One direction follows from Lemma <ref>.
Conversely, if $\cat C$ is small and finitely complete,
by Example <ref> there is a theory $\theory$ such that
$\lex\funct{\cat C,\Set}\cong \Mod(\theory)$.
An application of Theorem <ref> yields
$\lex\funct{\cat C,\Set}\cong \lex\funct{\cat T, \Set}$ and so,
by Gabriel-Ulmer duality, $\cat C \cong \cat T$.
(Alternatively, observe that the equivalence
$\lex\funct{\cat C,\Set}\cong \lex\funct{\cat T, \Set}$
restricts to an equivalence between the full subcategories
on the finitely presentable objects, which in turn yields $\cat C \cong \cat T$.)

This follows from Example <ref> and Theorem <ref>,
combined with the fact that, by Gabriel-Ulmer duality,
a category is lfp if and only if it is equivalent to one of the form
$\lex\funct{\cat C,\Set}$ for some small finitely complete category $\cat C$.

We now turn to a generalization of Theorem <ref>
involving models of cartesian theories in arbitrary
finitely complete categories.
This requires a few additional definitions.

Let $\Sig$ be a signature and let $\cat C$ be a category with finite products.

A $\Sig$-structure $M$ in $\cat C$
is given by the following data:

* an object $M(\sortbis)$
for each sort
$\sortbis \in \Sort(\Sig)$,

* a morphism
$f_M \in \cat C \funct{M(\sortbis_1) \times \dots \times M(\sortbis_n),M(\sort)}$
for each function symbol
$f \in \Fun(\Sig)(\sortbis_1,\dots,\sortbis_n;\sort)$,

* a subobject
$R_M \in \Sub_{\cat C}(M(\sortbis_1) \times \dots \times M(\sortbis_n) )$
for each relation symbol
$R \in \Rel(\Sig)(\sortbis_1,\dots,\sortbis_n)$.

A homomorphism of $\Sig$-structures
$h : M \to N$
is given by a morphism
$h^\sortbis \in \cat C\funct{M(\sortbis), N(\sortbis)}$
for each sort $\sortbis \in \Sort(\Sig)$,
such that:

* for each function symbol
$f \in \Fun(\Sig)(\sortbis_1,\dots,\sortbis_n;\sort)$
we have

\[
\begin{tikzcd}
M(\sortbis_1) \times \dots \times M(\sortbis_n)
\arrow{r}{f_M}
\arrow{d}[left]{h^{\sortbis_1} \times \dots \times h^{\sortbis_n}}
& M(\sort)
\arrow{d}{h^{\sort}}
\\
N(\sortbis_1) \times \dots \times N(\sortbis_n)
\arrow{r}{f_N}
& N(\sort)
\end{tikzcd}
\]

* for each predicate symbol
$R \in \Rel(\Sig)(\sortbis_1,\dots,\sortbis_n)$,
there is in $\cat C$ a commutative diagram of the form

\[
\begin{tikzcd}
\arrow[hook]{r}
\arrow{d}
& M(\sortbis_1) \times \dots \times M(\sortbis_n)
\arrow{d}{h^{\sortbis_1} \times \dots \times h^{\sortbis_n}}
\\
\arrow[hook]{r}
& N(\sortbis_1) \times \dots \times N(\sortbis_n)
\end{tikzcd}
\]

* We write $\cat C\text{-}\Struct(\Sig)$ for the category

whose objects are $\Sig$-structures in $\cat C$
and whose morphisms are homomorphisms.

Hence $\Struct(\Sig)$ (as defined in <ref>)
is $\Set\text{-}\Struct(\Sig)$.

Definition <ref> does not mention equality
because given $h \in \cat C\text{-}\Struct(\Sig)\funct{M,N}$,
for each $\sortbis \in \Sort(\Sig)$
we have

\[
\begin{tikzcd}
\arrow[hook]{r}{\Delta}
\arrow{d}[left]{h^\sortbis}
& M(\sortbis) \times M(\sortbis)
\arrow{d}{h^\sortbis \times h^\sortbis}
\\
\arrow[hook]{r}[below]{\Delta}
& N(\sortbis) \times N(\sortbis)
\end{tikzcd}
\]

where $\Delta = \pair{\id,\id}$ is the diagonal.

Consider a structure
$M \in \cat C\text{-}\Struct(\Sig)$,
where $\cat C$ has finite limits.
Each term-in-context
$\Env \sorting t : \sort$,
$\Env = x_1:\sortbis_1,\dots,x_n:\sortbis_n$,
has an interpretation

\[
\begin{tikzcd}
M(\sortbis_1) \times \dots \times M(\sortbis_n)
\arrow{r}{\I{t}_M}
& M(\sort)
\end{tikzcd}
\]

defined in the obvious way.
Note that term substitution is interpreted using composition
in $\cat C$
(see <cit.>).

Let $\cat C$ be a
category with finite limits.
Let $\theory$ be a cartesian theory over a signature $\Sig$,
consider a structure $M \in \cat C\text{-}\Struct(\Sig)$.
The formulae-in-context
$(\Env \sorting \varphi) \in \Lang$
which are cartesian over $\theory$ are interpreted
as subobjects

\[
\begin{tikzcd}
\I{\Env \sorting \varphi}_M
\arrow[hook]{r}
& M(\Env)
\end{tikzcd}
\]

The definition of
$\I{\Env \sorting \varphi}_M$
is by induction on $\varphi$
as follows.

The formula $\Env \sorting (t \Eq_\sort u)$
is interpreted by the equalizer

\[
\begin{tikzcd}
\I{\Env \sorting (t \Eq_\sort u)}_M
\arrow[hook]{r}
& M(\Env)
\arrow[shift left]{r}{\I{t}_M}
\arrow[shift right]{r}[below]{\I{u}_M}
& M(\sort)
\end{tikzcd}
\]

Given $R \in \Rel(\Sig)(\sortbis_1,\dots,\sortbis_n)$,
the formula
$\Env \sorting R(t_1,\dots,t_n)$
is interpreted by the pullback

\[
\begin{tikzcd}
\I{\Env \sorting R(t_1,\dots,t_n)}_M
\arrow{r}
\arrow[hook]{d}
\arrow[phantom]{dr}[very near start]{\pb}
& R_M
\arrow[hook]{d}
\\
\arrow{r}[below]{\I{t_1} \times \cdots \times \I{t_n}}
& M(\sortbis_1) \times \cdots \times M(\sortbis_n)
\end{tikzcd}
\]

The formula $\Env \sorting \bigwedge_{i \in I} \varphi_i$
is interpreted as the intersection of the

\[
\begin{tikzcd}
\I{\Env \sorting \varphi_i}_M
\arrow[hook]{r}
& M(\Env)
\end{tikzcd}
\]

Consider finally the case of
$\Env \sorting (\exists x : \sort)\varphi$.
Since $\theory$ proves

\[
\begin{array}{l l l}
\varphi
\varphi[y/x]
& \thesis_{\Env, x: \sort, y: \sort}
& x \Eq_\sort y
\end{array}
\]

it follows from <cit.>
that the composition

\[
\begin{tikzcd}
\I{\Env,x:\sort \sorting \varphi}_M
\arrow[hook]{r}
& M(\Env) \times M(\sort)
\arrow{r}{\pi}
& M(\Env)
\end{tikzcd}
\]

is monic,
and can be taken to be the interpretation
of $\Env \sorting (\exists x:\sort) \varphi$.

Let $\cat C$ be a
category with finite limits.
Let $\theory$ be a cartesian theory over a signature $\Sig$,
and consider a structure $M \in \cat C\text{-}\Struct(\Sig)$.

* A sequent $\psi \thesis_\Env \varphi$
which is cartesian over $\theory$
is valid in $M$

\[
\begin{array}{l l l l}
\I\psi_M
\leq
\I\varphi_M
& \text{in $\Sub(M(\Env))$}
\end{array}
\]

A formula-in-context $\Env \sorting \varphi$
which is cartesian over $\theory$
is valid in $M$
whenever so is the sequent
$\True \thesis_\Env \varphi$.

* We say that $M$ is a model of $\theory$
if all sequents of $\theory$ are valid in $M$.

* We let $\cat C\text{-}\Mod(\theory)$
be the full subcategory of $\cat C\text{-}\Struct(\Sig)$
on the models of $\theory$ in $\cat C$.

Consider a cartesian theory $\theory$ with syntactic category $\cat T$.
A model $M$ of $\theory$ in a category $\E$ with finite limits
induces a finite-limits-preserving functor

\[
\begin{array}{*{5}{l}}
& :
& \cat T
& \longto
& \E
\end{array}
\]

$F_M$ takes an object $\OI{\vec x \mid \varphi}$
to the interpretation $\I{\vec x \mid \varphi}_M$
of $\vec x \sorting \varphi$ in $M$.

The action of $F_M$ on morphisms requires some explanations.
Let us say that a graph is a morphism $G \colon A \to A \times B$
such that the composition $\pi_1 \comp G \colon A \to A$
is the identity.
In particular, our graphs are monomorphisms,
and are thus graphs in the sense of <cit.>.
A graph $G \colon  A \to A \times B$
induces a morphism

\[
\begin{array}{*{7}{l}}
& \deq
& \pi_2 \comp G
& :
& A
& \longto
& B
\end{array}
\]

Conversely, any morphism $f \colon A \to B$
has a graph

\[
\begin{array}{*{7}{l}}
& \deq
& \pair{\id_A,f}
& :
& A
& \longto
& A \times B
\end{array}
\]

Moreover, one easily checks that

\[
\begin{array}{r c l}
& =
& f
\\

& =
& G
\end{array}
\]

Let $M$ be a model of a cartesian theory $\theory$ in a category $\E$
with finite limits.
Then for every morphism

\[
\begin{array}{*{5}{l}}
\MI{\vec x, \vec y \mid \theta}
& :
& \OI{\vec x \mid \varphi}
& \longto
& \OI{\vec y \mid \psi}
\end{array}
\]

in the syntactic category $\cat T$ of $\theory$,
the induced morphism

\[
\begin{array}{*{5}{l}}
\I{\vec x \mid \varphi}_M
& \longto
& \I{\vec x,\vec y \mid \theta}_M
& \longto
& \I{\vec x \mid \varphi}_M \times \I{\vec y \mid \psi}_M
\end{array}
\]

in $\E$ is a graph.

The following generalization of Theorem <ref>
is <cit.>.

Let $\theory$ be a cartesian theory,
of syntactic category $\cat T$.
For every category $\E$ with finite limits,

\[
\begin{array}{r c l}
\E\text{-}\Mod(\theory)
& \longto
& \lex\funct{\cat T, \E}
\\

& \longmapsto
& F_M
\end{array}
\]

is (part of) an equivalence of categories.

In the above discussion on Theorem <ref>,
we said nothing about morphisms
(i.e. homomorphisms in $\Mod(\theory)$ v.s.natural transformations in $\lex\funct{\cat T,\E}$).
We note here for the record some basic facts on these.

Given models $M,N \in \E\text{-}\Mod(\theory)$,
consider some homomorphism $\ell \colon N \to M$
and let $\lambda \colon F_N \to F_M$
be the corresponding natural transformation,
$F_N,F_M \in \lex\funct{\cat T,\E}$.

$N(\sort) = \I{y:\sort \mid \True}_N = F_N\OI{y:\sort \mid \True}$
for each sort $\sort \in \Sort(\Sig)$
(and similarly for $M$);

$N(\sort) = \I{y:\sort \mid \True} = F_N\OI{y:\sort \mid \True}$
$\ell^\sort = \lambda_{\OI{y : \sort \mid \True}}$
for each sort $\sort \in \Sort(\Sig)$.

given $\vec y = y_1 : \sort_1,\dots,y_n : \sort_n$
we have

* $F_M\OI{\vec y \mid \True}$
the product
of the
$F_N\OI{y_i : \sort_i \mid \True}$
for $i = 1,\dots,n$
(and similarly for $F_M$);

* $\lambda_{\OI{\vec y \mid \True}}$
the product
of the
\(
\lambda_{\OI{y_i : \sort_i \mid \True}}
\colon
F_N\OI{y_i : \sort_i \mid \True}
\to
F_M\OI{y_i : \sort_i \mid \True}
\)
for $i = 1,\dots,n$;

* When $\E = \Set$,
for $\vec a \in \I{\vec y \mid \True}_N$ we have

\[
\begin{array}{*{5}{l}}
%\ell(\vec a)
& =
& \lambda_{\OI{\vec y \mid \True}}(\vec a)
& \in
& \I{\vec y \mid \True}_N
\end{array}
\]

Items <ref>
and <ref>
are follows from the definitions of
$F_M$ and $\lambda$ from $M$ and $\ell$.

* By Lemma <ref>,
in $\cat T$
we have

\[
\begin{array}{l l l}
\OI{\vec y \mid \True}
& \cong
& \OI{y_1 : \sort_1 \mid \True}
\times
\dots
\times
\OI{y_n : \sort_n \mid \True}
\end{array}
\]

\[
\begin{array}{l l l}
F_N\OI{\vec y \mid \True}
& \cong
& F_N\OI{y_1 : \sort_1 \mid \True}
\times
\dots
\times
F_N\OI{y_n : \sort_n \mid \True}
\end{array}
\]

since $F_N$ preserves finite limits.

* By naturality of $\lambda \colon F_N \to F_M$,
for $i = 1,\dots,n$ we have

\[
\begin{tikzcd}
F_N\OI{\vec y \mid \True}
\arrow{r}[above]{F_N(\pi_i)}
\arrow{d}[left]{\lambda_{\OI{\vec y \mid \True}}}
& F_N\OI{y_i : \sort_i \mid \True}
\arrow{d}[right]{\lambda_{\OI{y_i : \sort_i \mid \True}}}
\\
F_M\OI{\vec y \mid \True}
\arrow{r}[above]{F_M(\pi_i)}
& F_M\OI{y_i : \sort_i \mid \True}
\end{tikzcd}
\]

$\pi_i \colon \OI{\vec y \mid \True} \to \OI{y_i : \sort_i \mid \True}$
is the $i$-th projection in $\cat T$.
But since $F_N$ and $F_M$ preserve finite limits,
the arrows
$F_N(\pi_i)$ and $F_M(\pi_i)$ are also projections,
and the result follows.

We now come back to Example <ref>.

[Example <ref>]

The following is based on <cit.>.
Given a small category $\cat C$, consider the signature $\Sig(\cat C)$
with sorts the objects of $\cat C$,
function symbols the morphisms of $\cat C$,
and no predicate symbols.
Let $\theory(\cat C)$ be
the cartesian theory with axioms

\[
\begin{array}{l !{\qquad} l}
\True
\thesis_{x:a}
\id_a(x) \Eq_a x

& \True
\thesis_{x:a}
(g \comp f)(x) \Eq_c g(f(x))
\end{array}
\]

where $f \in \cat C\funct{a,b}$ and $g \in \cat C\funct{b,c}$.
for each fiintely complete $\E$, we have
an equivalence of categories

\[
\begin{array}{l l l}
\funct{\cat C,\E}
& \cong
& \E\text{-}\Mod(\theory(\cat C))
\end{array}
\]

Writting $\cat T(\cat C)$ for
the syntactic category of $\theory(\cat C)$,
Theorem <ref> yields an equivalence

\[
\begin{array}{l l l}
\funct{\cat C,\E}
& \cong
& \lex\funct{\cat T(\cat C),\E}
\end{array}
\]

for each finitely complete $\E$.
Hence $\cat T(\cat C)$ is the finite completion of $\cat C$.

Further, $\theory(\cat C)$ can be extended to a cartesian theory

$\theory$ such that $\E\text{-}\Mod(\theory) \cong \lex\funct{\cat C,\E}$
for each finitely complete $\E$.

§.§ Categories of structures

We shall need a concrete description of the filtered colimits
in $\Mod(\theory)$.

This can be obtained from

$\lex\funct{\cat T,\Set}$, and thus from $\funct{\cat T,\Set}$.
But it is

more convenient to

go via

Given a signature $\Sig$, we write $\theory(\Sig)$ for the cartesian
theory over $\Sig$ without axioms.
It is clear that
$\Mod(\theory(\Sig)) = \Struct(\Sig)$.

Write $\cat T(\Sig)$ for the syntactic category of $\theory(\Sig)$.

$\Struct(\Sig)$ is lfp as $\Struct(\Sig) \cong \lex\funct{\cat T(\Sig),\Set}$.

Next, consider a theory $\theory$ over $\Sig$
and write $\cat T$ for its syntactic category.
Since $\theory(\Sig)$
has less axioms than $\theory$,

every sequent provable in
is also provable in $\theory$.
In particular, every morphism of
$\cat T(\Sig)$ is a morphism of $\cat T$,
and we have

an identity-on-objects

\[
\begin{array}{*{5}{l}}
\inclth
& :
& \cat T(\Sig)
& \longto
& \cat T
\end{array}
\]

It is clear that $\inclth$ preserves finite limits.
Hence (via <ref>)
we have a finitary right adjoint

\[
\begin{array}{l l r c l}
\ladj\inclth
& :
& %\Mod(\theory)
\lex\funct{\cat T,\Set}
& \longto
& \lex\funct{\cat T(\Sig),\Set}
\\

& F
& \longmapsto
& %\lex\funct{\cat T,\Set}\funct{\yoneda \inclth(-),F}
F \comp \inclth
\end{array}
\]

Let now $M \in \Mod(\theory)$.
Recall that the functor
$F_M \in \lex\funct{\cat T,\Set}$
induced by $M$

to its interpretation in $M$.

$\cat T(\Sig)$ has the same objects as $\cat T$,

so that
$\ladj\inclth(F_M) = F_M \comp \inclth$
is the inclusion
of $M \in \Mod(\theory)$ into $\Struct(\Sig)$.

The inclusion $\Mod(\theory) \into \Struct(\Sig)$ preserves filtered colimits.

<cit.> gives a direct proof of the fact that $\Struct(\Sig)$ is lfp.
See also <cit.> for Lem. <ref>.

§.§ Additional material for <ref> (sec:coste:fp)

The machinery of syntactic categories becomes particularly
interesting when combined with Yoneda (see <cit.>).

Let $\theory$ be a cartesian theory with syntactic category $\cat T$.
Let $M \in \Mod(\theory)$
and consider
a finitely presentable model
$\FG{\vec x \mid \varphi} \in \Mod(\theory)$.
There is a bijection

\[
\begin{array}{l l l}
\I{\vec x \mid \varphi}_M
& \cong
& \Mod(\theory)\funct{\FG{\vec x \mid \varphi}, M}
\end{array}
\]

By the Yoneda Lemma,
for any $\OI{\vec x \mid \varphi}\in \cat T$ and $M \in \Mod(\theory)$,

\[
\begin{array}{l l l}
\I{\vec x \mid \varphi}_M
& \cong
& \lex\funct{\cat T,\Set}\funct{\yoneda\OI{\vec x \mid \varphi},\, F_M}.
\end{array}
\]

Just recall that $F_M(\OI{\vec x \mid \varphi}) = \I{\vec x \mid \varphi}_M$.
Explicitly, given

$\vec a \in \I{\vec x \mid \varphi}_M$,
the unique natural transformation

\[
\begin{array}{*{5}{l}}
\lambda^{\vec a}
& \colon
& \yoneda\OI{\vec x \mid \varphi}
& \longto
& F_M
\end{array}
\]

corresponding to
$\vec a$
has component at $C \in \cat T$ defined by

\[
(\lambda^{\vec a})_C
\ \colon \
\cat T\funct{\OI{\vec x \mid \varphi}, C}
\to F_M(C),
\ \
\theta\mapsto F_M(\theta)(\vec a).
\]

finitely presentable models

$\FG{\vec x \mid \varphi}$, $\FG{\vec y \mid \psi}\in \Mod(\theory)$.
Given $\vec a,\vec b \in M$
of the same sorts as $\vec x$ and $\vec y$, respectively,
the following are equivalent:

there is a homomorphism
$\ell \colon \FG{\vec x \mid \varphi} \to \FG{\vec y \mid \psi}$
and there are homorphisms
$h \colon \FG{\vec x \mid \varphi} \to M$
taking $\vec x$ to $\vec a$
$k \colon \FG{\vec y \mid \psi} \to M$
taking $\vec y$ to $\vec b$
such that
$k \comp \ell = h$:

\[
\begin{tikzcd}[row sep=0cm]
\FG{\vec x \mid \varphi}
\arrow{dd}[left]{\ell}
\arrow{dr}[above]{h}
\\
& M
\\
\FG{\vec y \mid \psi}
\arrow{ur}[below]{k}
\end{tikzcd}
\]

\(
\models
\varphi(\vec a)
\land
\psi(\vec b)
\land
% \bigvee_{\theta \in \cat T\funct{\OI{\vec y \mid \psi},\OI{\vec x \mid \varphi}}}
% \theta(\vec b, \vec a)
\bigvee
\{
\theta(\vec b, \vec a)
\mid
\theta \in \cat T\funct{\OI{\vec y \mid \psi},\OI{\vec x \mid \varphi}}
\}
\).

Let $\OI{\vec x \mid \varphi} \in \cat T$
with $\vec x = x_1,\dots,x_n$.
There exist $\const x_1,\ldots,\const x_n \in \FG{\vec x \mid \varphi}$
such that for every $M \in \Mod(\theory)$
and $h \colon \FG{\vec x \mid \varphi} \to M$
taking $\vec x$ to $\vec a \in \I{\vec x \mid \varphi}_M$,
we have $h(\const x_i) = a_i$ for all $i = 1,\dots,n$.

Fix an arbitrary $i\in \{1,\ldots,n\}$. Assume $x_i$ is of sort $\sort_i$
consider the $\cat T$-morphism
$\varpi_i \colon \OI{\vec x \mid \varphi} \to \OI{x_i : \sort_i \mid \True}$
given by the formula

\[
\vec x,x_i' \sorting \varphi ~\land~ x_i \Eq x'_i.
\]

Given $M \in \Mod(\theory)$,

\[
\begin{array}{*{5}{l}}
& :
& \I{\vec x \mid \varphi}_M
& \longto
& M(\sort_i)
\I{x_i : \sort_i \mid \True}_M
\end{array}
\]

$\I{\vec x,x'_i \mid \varphi ~\land~ x_i \Eq x'_i}_M$
and is thus the $i$th projection.

In particular,
given $\vec a \in \I{\vec x \mid \varphi}_M$,
the component of $\lambda^{\vec a}$ at
$\OI{x_i : \sort_i \mid \True}$
$\varpi_i \in \cat T\funct{\OI{\vec x \mid \varphi},\OI{x_i : \sort_i \mid \True}}$

\[
\begin{array}{*{7}{l}}
F_M(\varpi_i)(\vec a)
& =
& a_i
& \in
& M(\sort_i).
\end{array}
\]

By Remark <ref>, we can take $\const x_i$ to be the image
of $\varpi_i$ under
the bijection $\cat T\funct{\OI{\vec x \mid \varphi},\OI{x_i : \sort_i \mid \True}}\cong \FG{\vec x \mid \varphi}(\sort_i)$.

§ PROOFS OF <REF> (SEC:HINTIKKA)

§.§ Proofs of <ref>

Let $\A$ be an arboreal category and $a,b \in \A$.
Below, $\ord,\ordbis$ range over ordinals.
Recall that $(m,n) \in \Rk(\ord)$ implies $(m,n) \in \W(a,b)$.

If $(m,n) \in \Rk(\ord)$ then $(m,n) \in \Rk(\ordbis)$
for all $\ordbis < \ord$.

By induction on $\ord$,
we show that for all position $(m,n)$,
if $(m,n) \in \Rk(\ord)$ then $(m,n) \in \Rk(\ordbis)$
for all $\ordbis < \ord$.
The cases of $0$ and of limit ordinals are trivial.
So consider the case of a successor ordinal $\ord+1$, and let
$(m,n) \in \Rk(\ord+1)$.
We reason by cases on $\ord$.

Case of $\ord = 0$.

Trivial, since $\Rk(0) = \W(a,b)$ by definition.

Case of $\ord = \ordbis + 1$.

Since $(m,n) \in \Rk(\ord+1)$,
after each Spoiler move, there is a Duplicator move reaching
a position $(m',n') \in \Rk(\ord)$.
By induction hypothesis, all such $(m',n')$ are in $\Rk(\ordbis)$.
Hence $(m,n) \in \Rk(\ordbis+1)$ by definition,
and the result follows from the induction hypothesis.

Case of $\ord$ a limit ordinal.

Since $(m,n) \in \Rk(\ord+1)$,
after each Spoiler move, there is a Duplicator move reaching
a position $(m',n') \in \Rk(\ord)$.

By definition,
we have $(m',n') \in \Rk(\ordbis)$
for all $\ordbis < \ord$.
It follows that for all $\ordbis < \ord$,
after all Spoiler move from position $(m,n)$,
there is a Duplicator move reaching
a position $(m',n') \in \Rk(\ordbis)$.
Hence $(m,n) \in \Rk(\ordbis+1)$ for all $\ordbis < \ord$.
Since $\ord$ is a limit ordinal, we have
$\ordbis + 1 < \ord$ whenever $\ordbis < \ord$,
so that the induction hypothesis implies
$(m,n) \in \Rk(\ordbis)$ for all $\ordbis < \ord$.
Hence $(m,n) \in \Rk(\ord)$ by definition.

We now verify that our notion of rank of a game $\G(a,b)$ is well defined.
This relies on the following.

Let $\ord_0$ be an ordinal such that $\Rk(\ord_0) \sle \Rk(\ord_0+1)$.
Then $\Rk(\ord) = \Rk(\ord_0)$ for all $\ord \geq \ord_0$.

The proof is by induction on $\ord \geq \ord_0$.
The result is trivial if $\ord = \ord_0$.
We consider the two possible cases for $\ord > \ord_0$.
Note that $\Rk(\ord_0) = \Rk(\ord_0 +1)$
by Lemma <ref>.

Case of $\ord = \ordbis + 1$.

Let $(m,n) \in \Rk(\ord_0)$.
We have to show that $(m,n) \in \Rk(\ordbis+1)$,
i.e. that for every Spoiler move from position $(m,n)$,
Duplicator has a move reaching a position $(m',n') \in \Rk(\ordbis)$.
But since $(m,n) \in \Rk(\ord_0 + 1)$,
for every Spoiler move from position $(m,n)$,
Duplicator has a move reaching a position $(m',n') \in \Rk(\ord_0)$.
Hence, by induction hypothesis,
for every Spoiler move from position $(m,n)$,
Duplicator has a move reaching a position $(m',n') \in \Rk(\ordbis)$,
and we are done.

Case of $\ord$ a limit ordinal.

Given $(m,n) \in \Rk(\ord_0)$,
by induction hypothesis we have
$(m,n) \in \Rk(\ordbis)$ for all $\ordbis < \ord$.
Hence $(m,n) \in \Rk(\ord)$ by definition and we are done.

Let $\ord$ be an ordinal such that in the game $\G(a,b)$,
for every $(m,n) \in \Rk(\ord)$ we also have $(m,n) \in \Rk(\ord+1)$.
Then for every $(m,n) \in \Rk(\ord)$,
Duplicator has a winning strategy from position $(m,n)$.

Fix some $(m,n) \in \Rk(\ord)$.
Since $(m,n) \in \Rk(\ord+1)$,
for every Spoiler move from position $(m,n)$,
Duplicator can reach a position $(m',n') \in \Rk(\ord)$.
Iterating this process induces a strategy for Duplicator.

This strategy is winning since $\Rk(\ord) \sle \W(a,b)$.

In full generality, Lemma <ref>
requires the Axiom of Dependent Choices
(of intermediate
strength between the axiom of Countable Choice
and the full Axiom of Choice,
cf. e.g. <cit.> and <cit.>).

For each game $\G(a,b)$,
we can actually exhibit an ordinal as in Lemma <ref>.

For each game $\G(a,b)$,
there is an ordinal $\ord$ such that
for every $(m,n) \in \Rk(\ord)$ we also have $(m,n) \in \Rk(\ord+1)$.

Let $S$ be the set of positions $(m,n)$ of $\G(a,b)$
such that $(m,n) \notin \Rk(\ordbis)$ for some ordinal $\ordbis$.

Since $S$ is a set,

\[
\begin{array}{l l l}
\ord
& \deq
& \bigvee \left\{
\bigwedge \left\{ \text{$\ordbis$ ordinal} \mid (m,n) \notin \Rk(\ordbis) \right\}
\mid (m,n) \in S \right\}
\end{array}
\]

is a well-defined ordinal.
Now, if $(m,n) \in \Rk(\ord)$, then $(m,n) \notin S$

since $(m,n) \in S$ would imply
$(m,n) \notin \Rk(\ordbis)$ for some $\ordbis \leq \ord$,
contradicting Lemma <ref>.
Hence $(m,n) \in \Rk(\ord)$ implies that there is no ordinal $\ordbis$
such that $(m,n) \notin \Rk(\ordbis)$;
in particular $(m,n) \in \Rk(\ord+1)$.

We now arrive at the following characterization,
based on <cit.>.

Let $(m,n)$ be a position in $\G(a,b)$.
The following are equivalent.

$(m,n) \in \Rk(\ord)$ for every ordinal $\ord$;

$(m,n)$ has rank $\geq$ the rank of $\G(a,b)$;

Duplicator has a winning strategy from position $(m,n)$.

The implication
\(
\text{\ref{item:proof:hintikka:rank:ord}}
\imp
\text{\ref{item:proof:hintikka:rank:rank}}
\)
follows from Lemma <ref>
\(
\text{\ref{item:proof:hintikka:rank:rank}}
\imp
\text{\ref{item:proof:hintikka:rank:win}}
\)
is given by Lemma <ref>.
It remains to prove
\(
\text{\ref{item:proof:hintikka:rank:win}}
\imp
\text{\ref{item:proof:hintikka:rank:ord}}
\).

We show by induction on $\ord$ that
for all position $(m,n)$ in $\G(a,b)$,
if Duplicator
has a winning strategy from position $(m,n)$, then $(m,n) \in \Rk(\ord)$.

Case of $\ord = 0$.

If Duplicator has a winning strategy from position $(m,n)$
then by definition we have $(m,n) \in \W(a,b)$.

Case of $\ord = \ordbis +1$.

Assume that Duplicator has winning strategy from position $(m,n)$.
Then by induction hypothesis we have $(m,n) \in \Rk(\ordbis)$.
for every Spoiler move, this strategy leads to a winning position $(m',n')$,
and by induction hypothesis we have $(m',n') \in \Rk(\ordbis)$.
Hence $(m,n) \in \Rk(\ord)$ by definition.

Case of $\ord$ limit.

By induction hypothesis.

Theorem <ref>
deserves a few comments:

From a position of rank $\geq k$, with $k \in \NN$,
Duplicator has a strategy which is winning for $k$ rounds in $\G(a,b)$.
the rank of $\G(a,b)$ is finite if the plays of
$\G(a,b)$ have bounded length
(cf. Remark <ref>).

For instance, the games played in the arboreal category $\cat R^E_k(\sig)$
(Examples <ref> and <ref>)
have finite rank because

all plays have length at most $k$.
Just observe that each path has cardinality at most $k$.

* From a position of rank $\omega$,
for all $k \in \NN$ Duplicator has a strategy
which is winning for $k$ rounds.
But they need not have a strategy which
is winning for $k$ rounds for all $k$.

\begin{align*}
\FMono(\FG{\vec x \mid \varphi})(\vec x)
& \deq
\bigwedge_{\OI{\vec y \mid y_i \Eq y_j}}
\bigwedge_{\theta \in \cat T\funct{\OI{\vec x \mid \varphi}, \OI{\vec y \mid \True}}}
(\forall \vec y)
\left(
y_i \Eq y_j
\theta(\vec x,\vec y)
\mathord{\bigvee}_{
\delta \in \cat T\funct{\OI{\vec x \mid \varphi}, \OI{\vec y \mid y_i \Eq y_j}}
\delta(\vec x,\vec y)
\right)
\\
\FMono(P)(x)
& \deq
\bigwedge_{Q \leq P}
\bigwedge_{\theta \in \cat T\funct{\OI{x:P \mid \True}, \OI{y,y':Q \mid \True}}}
(\forall y,y')
\left(
y \Eq y'
\theta(x,y,y')
\bigvee_{