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 the ‘validity’ relation \models between them, which is ‘elementlike’, i.e. 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.

Leave a Reply

Your email address will not be published. Required fields are marked *