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$?
> 
> 
> 



A mixed preservation theorem for two-sorted structures?
$\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<n\},\{d\_i:i<n\})\TO\_{\aeba}(\fk N,\{c\_i:i<n\},\{b\_i:i<n\})$$
for each $n$. (I will write $a\_{<n}=\{a\_i:i<n\}$ 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\_{<n},d\_{<n},a\_n)\to\psi^{\fk N}(c\_{<n},b\_{<n},x):\psi\in\cL\_{\aeba}\}$$
is a recursive type of $(\fk M,\fk N)$: in particular, if $\psi\_j$, $j<k$, are $\cL\_{\aeba}$ formulas such that $\fk M\models\psi\_j(a\_{<n},d\_{<n},a\_n)$, then
$$\fk M\models\exists x^A\,\bigwedge\_{j<k}\psi\_j(a\_{<n},d\_{<n},x^A),$$
hence
$$\fk N\models\exists x^A\,\bigwedge\_{j<k}\psi\_j(c\_{<n},b\_{<n},x^A)$$
using $(\fk M,a\_{<n},d\_{<n})\TO\_{\aeba}(\fk N,c\_{<n},b\_{<n})$, 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\_{<n})\TO\_{\aeba}(\fk N,c\_{\le n},b\_{<n})$.


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\_{<n},y)\to\psi^{\fk N}(c\_{\le n},b\_{<n},b\_n):\psi\in\cL\_{\aeba}\}.$$
Again, to see that $q(y)$ is consistent, let $\psi\_j$, $j<k$, be $\cL\_{\aeba}$ formulas such that $\fk N\nvDash\psi\_j(c\_{\le n},b\_{<n},b\_n)$. Then
$$\fk N\nvDash\forall y^B\,\bigvee\_{j<k}\psi\_j(c\_{\le n},b\_{<n},y^B),$$
thus using $(\fk M,a\_{\le n},d\_{<n})\TO\_{\aeba}(\fk N,c\_{\le n},b\_{<n})$, we have
$$\fk M\nvDash\forall y^B\,\bigvee\_{j<k}\psi\_j(a\_{\le n},d\_{<n},y^B).$$


