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.

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

  1. 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.
  2. 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.

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.
\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}.