Is there a concept similar to but not homomorphism and underlying the theorem of syntactic interpretation? I spot something from an example (the theorem of syntactic interpretation, c.f. Theorem VIII.2.2 in Ebbinghaus' Mathematical Logic), which might be a concept already defined, and similar to but not homomorphism.
Roughly, given two relations $R_s \subseteq S_1 \times S_2$ and $R_t \subseteq T_1 \times T_2$ (which are actually the same relation. See the example, but I don't know how to formulate that), for a mapping $f_1: S_1 \to T_1$ ,  there exists $f_2: T_2 \to S_2$, s.t. $\forall s_1 \in S_1, t_2 \in T_2$, $$ s_1 R_s f_2(t_2) \text{ iff } f_1(s_1) R_t t_2.$$
I was wondering if there is a concept (in set theory, category theory, ...) already for the relationship between $f_1$ and $f_2$, with respect to relations $R_s$ and $R_t$ (which are actually the same relation. see the example)?
If there is indeed such a concept already, can you reformulate the theorem of syntactic interpretation in terms of it?
Thanks.
 A: This is an example of a Galois connection, which is a relationship between two partially ordered sets. It's a special case of the concept of adjunction in category theory.
In particular, let $\mathscr S$ be a thin category (i.e. a preorder) whose object set is $S_1 + S_2$, such that $\mathscr S(s, s')$ is inhabited iff $s R_1 s'$. Likewise, let $\mathscr T$ be a thin category whose object set is $T_1 + T_2$, such that $\mathscr T(t, t')$ is inhabited iff $t R_2 t'$. Then a monotone function (i.e. a functor) $f_1 : \mathscr S \to \mathscr T$ is left-adjoint to a monotone function $f_2 : \mathscr T \to \mathscr S$ iff
$$\mathscr S(s, f_2(t)) \cong \mathscr T(f_1(s), t)$$
for all $s \in \mathscr S$, $t \in \mathscr T$. Under the definition of $\mathscr S$ and $\mathscr T$, this corresponds to the relationship described in the question.
(Here, we've actually extended $R_1$ and $R_2$ so that $s_1 R_1 s_1$ and $s_2 R_1 s_2$ hold, for all $s_1 \in S_1$ and $s_2 \in S_2$, and analogously for $R_2$. This is necessary to form a category, but functionally this makes no difference to the relationship.)

Regarding the structure described in the theorem statement. Every map between theories in the categorical sense, i.e. interpretations $I : S' \to S$ sending $\psi \mapsto \psi^I$, induces a functor between models $(-)^{-I} : \mathrm{Mod}(S) \to \mathrm{Mod}(S')$. I believe the syntactic interpretation theorem states that this functor preserves subobjects: categorically, this is true because $(-)^{-I}$ has a left adjoint, hence preserves limits and thus subobjects.  I'm afraid I don't know of a reference that spells this out precisely, but Regular Categories and Regular Logic is a good starting point to understand relational structures in category theory.
