An abstract infinitary presevervation theorem

We generalize the following results of infinitary first order logic:
A class $\C K$ of models is axiomatizable by universal / existential / positive / negative formulas iff it is closed under submodels / extensions / homomorphic images / surjective homomorphic preimages.

Assume we are given a class $\Bbb M$ of ‘models’ and a class $\Bbb F$ of formulas, forming a (complete) Boolean algebra (so that operations ‘and’/’or’ are defined for arbitrary many formulas), and assume we are given a complete Boolean relation $\models$ between them (for ‘validity’), i.e. a relation satisfying $M\models\lnot\fii \iff M\not\models\fii$ and $M\models\land_i\fii_i\iff\forall i:M\models\fii_i$ .

Let $\C K\subseteq\Bbb M,\ \Gamma,\Delta\subseteq\Bbb F$ .
We write $\R{Mod}\Gamma:=\{M\in\Bbb M: M\models\Gamma\}=\ \bigcap_{\gamma\in\Gamma}\{M:M\models\gamma\}$ and
$\R{Th}^\Delta\C K:=\{\fii\in\Delta:\C K\models\fii\}=\ \bigcap_{M\in\C K}\{\fii\in\Delta:M\models\fii\}$ .

A class of models $\C K$ is axiomatizable by $\Delta$ -formulas if $\C K=\R{Mod}\Delta'$ for some $\Delta'\subseteq\Delta$ , equivalently, if $\C K=\R{Mod}\R{Th}^\Delta\C K$ .

Let $Q$ be a reflexive binary relation on the class of models (typically stating the existence of a morphism of certain type), and write $\overset{\leftarrow}Q\C K:=\{M\in\Bbb M:\exists K\in\C K.\ M\overset Q-K\}$ , similarly define $\overset\to Q\C K$ .

Definition. A binary relation $Q$ is modelwise expressible by $\Delta$ -formulas, if for every model $A\in\Bbb M$ there is a formula $\delta_A\in\Delta$ which is valid on $A$ , and whenever $B\models\delta_A$ , it implies $A\overset Q-B$ .

Examples.
Let the formulas be infinitary first order formulas for a similarity type $t$ , and the models be the corresponding relational / algebraic structures.

Let $A\overset Q-B$ mean that $B$ is a homomorphic image of $A$ , i.e. isomorphic to a quotient of $A$ , and choose $\Delta$ to be the class of positive formulas. Set
$\delta_A:=\exists (x_a)_{a\in A}:\Delta_0(A)\land\forall y:\bigvee_{a\in A}(y=x_a)$

where $\Delta_0(A)$ is the conjunction of all atomic predicates that hold in $A$ , the element $a$ replaced by the corresponding variable $x_a$ .
Let $A\overset Q-B$ mean that $A$ is isomorphic to a substructure of $B$ , i.e. there is a relationally full embedding $A\hookrightarrow B$ , and choose $\Delta$ to be the class of existential formulas. Set
$\delta_A:=\exists (x_a)_{a\in A}:\Delta_0(A)\land\bigwedge_{\sigma:A\not\models\sigma\,[x_a/a]}\lnot\sigma$

where $\sigma$ runs over atomic formulas which are not valid on $A$ under the substitution $x_a\mapsto a$ .

Theorem. Suppose $Q$ is modelwise expressible by $\Delta$ -formulas. Then
a) If $\overset{\leftarrow}Q\C K\subseteq\C K$ , then $\C K$ is axiomatizable by $\lnot\Delta$ -formulas.
b) If $\overset{\to}Q\C K\subseteq\C K$ , then $\C K$ is axiomatizable by disjunctions of $\Delta$ -formulas.

Proof.
a) Let $\Gamma:=\R{Th}^{\lnot\Delta}\C K$ and $A\models\Gamma$ . As $A\models\delta_A$ , we have $\lnot\delta_A\notin\Gamma$ yielding a $B\in\C K$ with $B\models\delta_A$ which shows by hypothesis that $A\in\overset{\leftarrow}Q\C K$ .
b) Let $\Gamma:=\R{Th}^{\lor\Delta}\C K$ and $B\models\Gamma$ . We want to show $B\in\C K$ .
Define $\Theta:=\{\delta\in\Delta: B\models\lnot\delta\}$ and $\psi:=\lor\Theta$ . Then $B\not\models\psi$ , so $\psi\notin\Gamma$ , meaning that there is an $A\in\C K$ for which $A\not\models\psi$ .
Now use the hypothesis for model $A$ : there is a $\delta_A\in\Delta$ , so that $A\models\delta_A$ . But it can’t be in $\Theta$ because $A\not\models\lor\Theta$ , so $B\models\delta_A$ , yielding $A\overset Q-B$ thus $B\in\overset\to Q\C K\subseteq\C K$ .

This theorem proves one direction in all of the above mentioned preservation theorems.
The converse direction, that the specific types of formulas are preserved under the specific operator on the class of models is a straightforward verification in each case.
However, we can prove a common generalization for them, using the more specific logic described in this post.
Let $\ct L:\ct S\ag\ct M$ be an arbitrary profunctor with an initial object $0$ , objects of $\ct S$ regarded as ‘situations’ and objects of $\ct M$ as ‘models’, and introduce the relation ‘diagonal fill-in‘ (or ‘left lifting property‘) between arrows of $\ct S$ and arrows of $\ct M$ as follows:

$\alpha\T f \ \overset{\text{def}}\iff\ \forall\, \big[\alpha v=uf\big]\ \exists\, \big[\alpha d=u,\,df=v\big]$

that is, iff every commutative square with $\alpha\in\ct S$ on the top and $f\in\ct M$ on the bottom has a diagonal fill-in $d$ making the whole diagram commutative:

$\dia{\ar[r]^\alpha \ar[d]_u & \ar[d]^v \ar@{-->}[ld]|d \\\ar[r]_f &}$

For a subclass of morphisms $\ct N\subseteq\ct M$ , we write ${}^{\T}\ct N\,:=\{\alpha\in\ct S\mid\,\forall f\in\ct N:\alpha\T f\}$ . Similarly, for $\ct A\subseteq\ct S$ , let $\ct A^{\T}:=\{f\in\ct M\mid\,\forall\alpha\in\ct A:\alpha\T f\}$ .

For example, in the first order case, we have
$\big[(\emptyset,\emptyset)\to(\{x\},\emptyset)\big]^{\T}=\{$ surjective morphisms of $\ct M\}=:Surj$ , and
$\big[(\{x,y\},\emptyset)\to(\{x,y\},\{x=y\})\big]^{\T}=\{$ injective morphisms of $\ct M\}=:Inj$ .
Moreover,
$\big[(X,\Gamma)\to (X',\Gamma)\big]\,{\T}\, Surj$ whenever $X\subseteq X'$ , and
$\big[(X,\Gamma)\to (X,\Gamma')\big]\,{\T}\, Inj$ whenever $\Gamma\subseteq\Gamma'$ and $\Gamma'\setminus\Gamma$ consists only of equations.

Universal formulas correspond to those trees in which Eve doesn’t select new variables (so that the $X$ part doesn’t change in arrows on odd levels), and positive formulas correspond to trees in which Adam doesn’t select new relations or equations to hold (so that the $\Gamma$ part is empty in the root situation and doesn’t change in arrows on even levels).

Theorem. Let $\ct Q$ be an arbitrary class of morphisms in $\ct M$ , and let $\fii$ be a tree in which every arrow Eve can possibly choose is in ${}^{\T}\ct Q$ . Then $(f:A\to B)\in\ct Q,\ B\models\fii$ implies $A\models\fii$ .
Dually, if $0\to\fii$ is of the above form, then $(f:A\to B)\in\ct Q,\ A\models\fii$ implies $B\models\fii$ .

It turns out that examples 1. and 2. above have a common generalization in this setting.

Theorem. Let $\Delta:\ct M\to\ct S$ be a functor, surjective on hom-sets, suppose $\ct S$ has pushouts and assume that a class $H\subseteq\ct M$ of morphisms is defined by a set $C_0\subseteq\ct S$ of arrows by the diagonal-fill-in relation: $H={C_0}^{\T}$ .
Then the relation between objects $m,n\in Ob\ct M$ stating $\exists h:m\to n\, \in H$ is modelwise expressible by trees in which the arrows that Adam might choose are all $\T H$ in the profunctor $\Delta^*:\ct S\ag\ct M$ .

Proof. Since $\Delta^*$ is opfunctorial, every $m\in Ob\ct M$ has a coreflection arrow $j:m^\Delta\to m$ , which is now also a pre-reflection: each heteromorphism $m^\Delta\to n$ factors through (not necessarily uniquely) $j$ , because of the surjectivity condition.
For all $c_0:x\to y\ \in C_0$ and arrow $x\to z\,\in\ct S$ , fix a pushout square $\nzt{c_0}{}{}{}{c}$ and collect all such $c$ ‘s in a class $C$ . Note that from each $z\in Ob\ct S$ there starts out only set-many arrows of $C$ , and also note that $c\T H$ holds because $c$ is a pushout of $c_0\in C_0$ .

For a given $m\in Ob\ct M$ , consider the following tree:

$\dia{&&&& \ar[r]^r_{}="U" & m^\Delta \ar@{}[d]|{\displaystyle{m^\Delta}}="R" \ar[l];"R"^{}="V" \ar@{}"U";"V"|: & : cr=1_{m^\Delta}\\\delta_m & := & 0\ar[r]& m^\Delta \ar[ur]^c_{}="A" \ar[r]|{}="B" \ar[dr]^{}="C" \ar@{}"A";"B"|\vdots \ar@{}"B";"C"|\vdots^{\in C} &&\\&&&&&}$

where every arrow $c$ of $C$ starting at $m^\Delta$ gives a branch (for Adam) and the next layer of the tree consists of all right inverses $r$ of $c$ .

Proving $m\models \delta_m$ is straightforward after letting Eve choose the coreflection arrow $j:m^\Delta\to m$ .
Now, assume $a\models \delta_m$ for an arbitrary object $a\in Ob\ct M$ . We want to show the existence of an arrow $m\to a\,\in H$ .
Let’s call $u:m^\Delta\to a$ the interpretation Eve chooses on $a$ . By hypothesis, $j$ is also a pre-reflection arrow, yielding an arrow $f:m\to a$ such that $jf=u$ . We show $f\in H$ .

Let $c_0:x\to y\ \in C_0$ and assume a commutative square $\nzt{c_0}\alpha{}\beta{f}$ is given. Since $j$ is a coreflection arrow, there is a (unique) $\alpha_1:x\to m^\Delta$ such that $\alpha=\alpha_1 j$ . Then use the chosen pushout of $c_0$ and $\alpha_1$ to form

$\dia{x \ar@/_1pc/[dd]_\alpha \ar[r]^{c_0} \ar[d]^{\alpha_1} & y \ar@/^1pc/[dd]^\beta \ar[d]_t \\ m^\Delta \ar[r]^c \ar[d]|j \ar[rd]_u & \ar@{}[lu]|(.14){\displaystyle{\ulcorner}} \ar[d]|(.4){\beta_1} \\m \ar[r]_f & a }$

and let Adam choose branch $c$ with interpretation $\beta_1$ . Let $r$ be Eve‘s answer branch with interpretation forced to be $u$ as $cr=1_{m^\Delta}$ , so that $ru=\beta_1$ , and define $d\ :=\ t\,r\,j$ .
This is going to work as a diagonal-fill-in in the originally given square $\nzt{c_0}\alpha{}\beta{f}$ .