# A mixed preservation theorem for two-sorted structures?

A well known model theory fact is that for any first-order theory $$T$$ the collection of universal consequences of $$T$$, written $$T_\forall$$, is a precise axiomatization of the class of substructures of models of $$T$$. This is related to the fact that a sentence is preserved under passing to substructures if and only if it is logically equivalent to a universal sentence.

Dually a sentence is preserved under passing to superstructures if and only if it is logically equivalent to an existential sentence. The characterization of models of $$T_\exists$$ is less clean, specifically it axiomatizes the class of elementary substructures of superstructures of models of $$T$$.

Suppose $$\mathcal{L}$$ is a two-sorted language with sorts $$A$$ and $$B$$. Given $$\mathcal{L}$$-structures $$\mathfrak{M}$$ and $$\mathfrak{N}$$, we'll say that $$\mathfrak{N}$$ is an $$A$$-super-$$B$$-substructure of $$\mathfrak{M}$$ if $$A(\mathfrak{N}) \supseteq A(\mathfrak{M})$$ and $$B(\mathfrak{N}) \subseteq B(\mathfrak{M})$$ with the interpretations of all relation and function symbols agreeing on the common substructure $$A(\mathfrak{M}) \cup B(\mathfrak{N})$$. Intuitively speaking we've allowed $$A$$ to grow and $$B$$ to shrink when passing from $$\mathfrak{M}$$ to $$\mathfrak{N}$$. This relationship is obviously transitive.

We'll say that a sentence $$\varphi$$ is preserved under passing to $$A$$-super-$$B$$-substructures if for any $$\mathcal{L}$$-structures $$\mathfrak{M}$$ and $$\mathfrak{N}$$, if $$\mathfrak{M}\models \varphi$$ and $$\mathfrak{N}$$ is an $$A$$-super-$$B$$-substructure of $$\mathfrak{M}$$, then $$\mathfrak{N}\models \varphi$$. We may also requires that $$\mathfrak{M}$$ and $$\mathfrak{N}$$ be models of some particular theory.

A natural example of a sentence with this property is extensionality. Suppose that $$B$$ is a sort of sets of elements of $$A$$ and consider the extensionality axiom: $$(\forall x,y:B)(\exists z : A)((z\in x \leftrightarrow z \in y)\rightarrow x=y)$$

Adding more elements to $$A$$ cannot spoil extensionality, regardless of how you extend $$\in$$, and removing sets from $$B$$ cannot spoil extensionality.

This sentence has a particular syntactic form, specifically it is prenex and has the property that all $$A$$-quantifiers are $$\exists$$ and all $$B$$-quantifiers are $$\forall$$. Let's call the collection of sentences of this form $$\mathcal{L}_{A\exists B\forall}$$ (note that there is no restriction on the number of alternations). An easy argument shows that any sentence in this form is preserved under passing to $$A$$-super-$$B$$-substructures. My question is about the converse:

Question 1: Fix a theory $$T$$. Suppose that $$\varphi$$ is a sentence that is preserved under passing to $$A$$-super-$$B$$-substructures provided that both structures are models of $$T$$. Does it follow that $$\varphi$$ is equivalent to a sentence in $$\mathcal{L}_{A\exists B\forall}$$ modulo $$T$$?

Question 2: Let $$T_{A\exists B\forall}$$ be the set of consequences of a theory $$T$$ that are sentences in $$\mathcal{L}_{A\exists B\forall}$$. Are the models of $$T_{A\exists B\forall}$$ precisely the class of elementary substructures of $$A$$-super-$$B$$-substructures of models of $$T$$?

• Shouldn't the extensionality axiom have a universal quantification over z instead? That's the usual formulation – godelian Jun 16 '19 at 9:58
• @James It is easy to produce a counter-example to Question 1. Namely consider two-sorted language that extends the signature of $\mathsf{PA}$ by a second sort and a unary functional symbol $f$ that maps objects of the first sort to objects of the second. Let $T$ be $\mathsf{PA}+$ "$f$ is a bijection". Observe that all sentences are preserved under passing to $A$-super-$B$-substructure. However, since over $\mathsf{PA}$ there are sentences non-equivalent to $\exists\forall$-sentences, there would be sentences that wouldn't be equivalent to $\mathcal{L}_{A\exists B\forall}$-sentences over $T$. – Fedor Pakhomov Jun 16 '19 at 10:58
• @godelian I wanted to write it in prenex form. – James Hanson Jun 16 '19 at 12:22
• @FedorPakhomov This is probably the fault of my notation but $\mathcal{L}_{A\exists B\forall}$ doesn't restrict the number of quantifier alternations. – James Hanson Jun 16 '19 at 12:28

$$\let\fii\varphi\def\fk{\mathfrak}\def\cL{\mathcal L}\def\aeba{A\exists B\forall}\let\TO\Rightarrow$$Here is a quick and dirty proof that Q1 is true for countable languages, using an approach to preservation theorems suggested by §1.5 of Barwise & Schlipf, An introduction to recursively saturated and resplendent models. I have no doubts it holds for uncountable languages as well, though this may require a more elaborate argument.

So, assume that $$\fii$$ is not equivalent over $$T$$ to an $$\cL_{A\exists B\forall}$$ sentence. This implies $$T+(T+\fii)_{\aeba}\nvdash\fii$$, thus there exists $$\fk N\models T+\neg\fii$$ such that $$\fk N\models(T+\fii)_{\aeba}$$. The latter means that $$T+\fii+\mathrm{Th}_{A\forall B\exists}(\fk N)$$ is consistent, hence there exists $$\fk M\models T+\fii$$ such that $$\fk M\TO_{\aeba}\fk N,$$ by which I mean that $$\fk M\models\psi\implies\fk N\models\psi$$ for all $$\psi\in\cL_{\aeba}$$.

Using the Löwenheim–Skolem theorem and standard results on the existence of recursively saturated models, we may assume that $$\fk M$$ and $$\fk N$$ are countable, and the joint 4-sorted model $$(\fk M,\fk N)$$ is recursively saturated.

Let us fix enumerations $$A(\fk M)=\{a_n:n\in\omega\}$$ and $$B(\fk N)=\{b_n:n\in\omega\}$$. By induction on $$n$$, we will construct sequences $$\{c_n:n\in\omega\}\subseteq A(\fk N)$$ and $$\{d_n:n\in\omega\}\subseteq B(\fk M)$$ such that $$(\fk M,\{a_i:i for each $$n$$. (I will write $$a_{ etc.) Once we carry this out, the assignments $$a_n\mapsto c_n$$ and $$b_n\mapsto d_n$$ will provide embeddings of $$A(\fk M)$$ in $$A(\fk N)$$ and $$B(\fk N)$$ in $$B(\fk M)$$ (respectively), witnessing that $$\fii$$ is not preserved under passing to $$A$$-super-$$B$$-substructures.

For $$n=0$$, we have nothing to do. Assume that the construction has been carried out up to $$n$$, and consider $$a_n$$. The set of formulas $$p(x)=\{\psi^{\fk M}(a_{ is a recursive type of $$(\fk M,\fk N)$$: in particular, if $$\psi_j$$, $$j, are $$\cL_{\aeba}$$ formulas such that $$\fk M\models\psi_j(a_{, then $$\fk M\models\exists x^A\,\bigwedge_{j hence $$\fk N\models\exists x^A\,\bigwedge_{j using $$(\fk M,a_{, which shows that $$p(x)$$ is consistent. Thus, by recursive saturation, there exists $$c_n\in A(\fk N)$$ such that $$(\fk M,a_{\le n},d_{.

Dually, we can find a suitable $$d_n\in B(\fk M)$$ as a realization of the recursive type $$q(y)=\{\psi^{\fk M}(a_{\le n},d_{ Again, to see that $$q(y)$$ is consistent, let $$\psi_j$$, $$j, be $$\cL_{\aeba}$$ formulas such that $$\fk N\nvDash\psi_j(c_{\le n},b_{. Then $$\fk N\nvDash\forall y^B\,\bigvee_{j thus using $$(\fk M,a_{\le n},d_{, we have $$\fk M\nvDash\forall y^B\,\bigvee_{j

• Thank you. For an uncountable language can't you run the same argument in every countable reduct containing the symbols in the sentence $\varphi$ and then take an ultraproduct of the resulting pairs of structures to get a witness that $\varphi$ is not preserved in models of $T$? – James Hanson Jun 17 '19 at 15:04
• Yes, you are right, this should work. – Emil Jeřábek Jun 17 '19 at 15:12
• $\let\fk\mathfrak$I believe a direct argument proving both Q1 and Q2 for arbitrary languages might go as follows. It is easy to see that it suffices to show the following: if $\fk M_0\Rightarrow_{A\exists B\forall}\fk N_0$, there exist $\fk M_\infty\succeq\fk M_0$ and $\fk N_\infty\succeq\fk N_0$ such that $\fk N_\infty$ is an $A$-super-$B$-substructure of $\fk M_\infty$. Then, similar to common proofs of Robinson’s joint consistency theorem, you build elementary chains $\fk M_0\preceq\fk M_1\preceq\fk M_2\preceq\dots$ and $\fk N_0\preceq\fk N_1\preceq\fk N_2\preceq\dots$, ... – Emil Jeřábek Jun 17 '19 at 15:22
• $\let\fk\mathfrak$... and embeddings $f_n\colon A(\fk M_n)\to A(\fk N_{n+1})$, $g_{n+1}\colon B(\fk N_{n+1})\to B(\fk M_{n+1})$ such that $f_0\let\sset\subseteq\sset f_1\sset f_2\sset\dots$ and $g_1\sset g_2\sset g_3\sset\dots$, and we take $\fk M_\infty$ and $\fk N_\infty$ to be the limits of the chains. The embedings will actually have to preserve $A\exists B\forall$ formulas in a suitable way to make the inductive construction to go through. This will be kind of a mess to set it up properly, but I think there should not be any substantial difficulty. – Emil Jeřábek Jun 17 '19 at 15:25