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

  • $\begingroup$ Shouldn't the extensionality axiom have a universal quantification over z instead? That's the usual formulation $\endgroup$
    – godelian
    Jun 16 '19 at 9:58
  • $\begingroup$ @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$. $\endgroup$ Jun 16 '19 at 10:58
  • $\begingroup$ @godelian I wanted to write it in prenex form. $\endgroup$ Jun 16 '19 at 12:22
  • 1
    $\begingroup$ @FedorPakhomov This is probably the fault of my notation but $\mathcal{L}_{A\exists B\forall}$ doesn't restrict the number of quantifier alternations. $\endgroup$ 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<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).$$

  • $\begingroup$ 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$? $\endgroup$ Jun 17 '19 at 15:04
  • $\begingroup$ Yes, you are right, this should work. $\endgroup$ Jun 17 '19 at 15:12
  • $\begingroup$ $\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$, ... $\endgroup$ Jun 17 '19 at 15:22
  • $\begingroup$ $\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. $\endgroup$ Jun 17 '19 at 15:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.