We generalize the following results of infinitary first order logic:

A class 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 of ‘models’ and a class 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 between them (for ‘validity’), i.e. a relation satisfying and .

Let .

We write and

.

A class of models is axiomatizable by -formulas if for some , equivalently, if .

Let be a reflexive binary relation on the class of models (typically stating the existence of a morphism of certain type), and write , similarly define .

**Definition.** A binary relation is *modelwise expressible* by -formulas, if for every model there is a formula which is valid on , and whenever , it implies .

**Examples.**

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

- Let mean that is a
*homomorphic image*of , i.e. isomorphic to a quotient of , and choose to be the class of*positive*formulas. Set

where is the conjunction of all atomic predicates that hold in , the element replaced by the corresponding variable . - Let mean that is isomorphic to a
*substructure*of , i.e. there is a relationally full embedding , and choose to be the class of*existential*formulas. Set

where runs over atomic formulas which are not valid on under the substitution .

**Theorem.** Suppose is modelwise expressible by -formulas. Then

a) If , then is axiomatizable by -formulas.

b) If , then is axiomatizable by disjunctions of -formulas.

*Proof.*

a) Let and . As , we have yielding a with which shows by hypothesis that .

b) Let and . We want to show .

Define and . Then , so , meaning that there is an for which .

Now use the hypothesis for model : there is a , so that . But it can’t be in because , so , yielding thus .

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 be an arbitrary profunctor with an initial object , objects of regarded as ‘situations’ and objects of as ‘models’, and introduce the relation ‘*diagonal fill-in*‘ (or ‘*left lifting property*‘) between arrows of and arrows of as follows:

that is, iff every commutative square with on the top and on the bottom has a diagonal fill-in making the whole diagram commutative:

For a subclass of morphisms , we write . Similarly, for , let .

For example, in the first order case, we have

surjective morphisms of , and

injective morphisms of .

Moreover,

whenever , and

whenever and consists only of equations.

Universal formulas correspond to those trees in which `Eve`

doesn’t select new variables (so that the 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 part is empty in the root situation and doesn’t change in arrows on even levels).

**Theorem.** Let be an arbitrary class of morphisms in , and let be a tree in which every arrow `Eve`

can possibly choose is in . Then implies .

Dually, if is of the above form, then implies .

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

**Theorem.** Let be a functor, surjective on hom-sets, suppose has pushouts and assume that a class of morphisms is defined by a set of arrows by the diagonal-fill-in relation: .

Then the relation between objects stating is modelwise expressible by trees in which the arrows that `Adam`

might choose are all in the profunctor .

**Proof.** Since is opfunctorial, every has a coreflection arrow , which is now also a pre-reflection: each heteromorphism factors through (not necessarily uniquely) , because of the surjectivity condition.

For all and arrow , fix a pushout square and collect all such ‘s in a class . Note that from each there starts out only set-many arrows of , and also note that holds because is a pushout of .

For a given , consider the following tree:

where every arrow of starting at gives a branch (for

`Adam`

) and the next layer of the tree consists of all right inverses of .
Proving is straightforward after letting `Eve`

choose the coreflection arrow .

Now, assume for an arbitrary object . We want to show the existence of an arrow .

Let’s call the interpretation `Eve`

chooses on . By hypothesis, is also a pre-reflection arrow, yielding an arrow such that . We show .

Let and assume a commutative square is given. Since is a coreflection arrow, there is a (unique) such that . Then use the chosen pushout of and to form

and let

`Adam`

choose branch with interpretation . Let be `Eve`

‘s answer branch with interpretation forced to be as , so that , and define .This is going to work as a diagonal-fill-in in the originally given square .