A mixed preservation theorem for two-sorted structures?

Question

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

Answer 1

$\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).$$