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