Can $\sf ST$ interpret $\sf GST$? General set theory ($\sf{GST}$) is the theory defined by the axioms of Extensionality, Adjunction, and Specification (and an existence axiom, if necessary). The theory $\sf{ST}$ is just $\sf{GST}$, but with Specification replaced by Empty Set. My question is whether $\sf{ST}$ can interpret the full strength of $\sf{GST}$. If not, where can I find a proof?
I have determined that $\sf{ST}$ can interpret any finite subset of the $\sf{GST}$ axioms. Given this, if any finite fragment of $\sf{GST}$ can interpret the full $\sf{GST}$, then likewise $\sf{S}T$ can interpret $\sf{GST}$. At the very least, any theory which can at once prove all these interpretations will show that the two are equiconsistent, but this doesn't necessarily mean that they are mutually interpretable.

For the curious, my proof that $\sf{ST}$ can interpret any finite fragment of $\sf{GST}$ does so by constructing a definable class which models that fragment. In particular, for each formula $\phi(x,v_1,\cdots,v_n)$, we define a class $\mathcal{G}_\phi$ within which Specification by $\phi$ is permitted. Intersecting finitely many of these classes gives us any desired finite fragment of $\sf{GST}$. The definition of $\mathcal{G}_\phi$ is as follows.
$$\mathcal{S}_\cup\equiv\{X : \forall Y, (X\cup Y) \text{ is a set}\}$$
$$\mathcal{S}_\cap\equiv\{X : \forall Y, (X\cap Y)\text{ is a set}\}$$
$$\mathcal{S}_\phi\equiv\{X : \forall(\overline{v}), \{x\in X : \phi(x,\overline{v})\}\text{ is a set}\}$$
$$\mathcal{O}_{\phi}\equiv\{X : \forall(Z\subseteq X), Z\in\mathcal{S}_\cup\cap \mathcal{S}_\cap\cap \mathcal{S}_\phi\}$$
$$\mathcal{G}_\phi\equiv\{X : \exists(T\supseteq X), T\in\mathcal{O}_\phi\land\forall(t\in T), t\subseteq T\}$$
To clarify, we identify sets with classes whenever they are extensionally equal, so an expression like "the class C is a set" just means $\exists S, \forall x, x\in S\iff x\in C$. Now, $\mathcal{S}_\cup$ is the class of all sets for which their binary union with any other set will produce another set, and $\mathcal{S}_\cap$ is defined analogously for intersection. The class $\mathcal{S}_\phi$ consists of those sets for which specification by $\phi$ is permitted, and $\mathcal{O}_\phi$ is a subclass of all three, but in such a way that $\mathcal{O}_\phi$ is downwards closed under the subset relation. Finally, the class $\mathcal{G}_\phi$ just consists of all those $X$ admitting a transitive superset within $\mathcal{O}_\phi$.
Using transitive sets guarantees that $\mathcal{G}_\phi$ is a transitive class, so the axiom of Extensionality is preserved. Clearly specification by $\phi$ will also hold in $\mathcal{G}_\phi$, and it's not hard to prove that $\emptyset\in\mathcal{G}_\phi$. Proving that $\mathcal{G}_\phi$ is closed under adjunctions is the hardest part of this, but it is possible. Once we prove all these facts, we see that $\mathcal{G}_\phi$ lets us extend $\sf{ST}$ with the singular Specification instance corresponding to $\phi$. More importantly $\mathcal{G}_\phi$ is downward closed under inclusion, so intersecting finitely many of these classes (built from finitely many different $\phi$) will give us a class which models all those instances of Specification. This is how we interpret any finite fragment of $\sf{GST}$.
 A: The answer is a definite no. The reason is that $\sf{GST}$ is mutually interpretable with $\sf{PA}$, and $\sf{ST}$ is mutually interpretable with a finite fragment of $\sf{PA}$, and $\sf{PA}$ proves that fragment is consistent. If a finite fragment of $\sf{PA}$ could interpret the full $\sf{PA}$, then $\sf{PA}$ would detect the interpretation in such a way that $\sf{PA}$ would prove itself consistent. This is impossible due to Godel incompleteness, so no finite fragment of $\sf{PA}$ could interpret $\sf{PA}$, and consequently $\sf{ST}$ cannot interpret $\sf{GST}$.
That $\sf{PA}$ is mutually interpretable with $\sf{GST}$ is a bit esoteric, but it's a well known result. Using Ackermann's bijection we prove $\sf{PA}$ is bi-interpretable with $\sf{ZF}^{-\infty}$, which is $\sf{ZF}$ with infinity replaced by its negation, and $\sf{ZF}^{-\infty}$ interprets $\sf{GST}$ trivially. The reverse direction follows by defining the class ordinal $\omega$ from within $\sf{GST}$, and then using the well-foundedness of $\omega$ to verify all the $\sf{PA}$ axioms.
That $\sf{ST}$ is mutually interpretable with a finite fragment of $\sf{PA}$ follows from our combined results: $\sf{PA}$ interprets $\sf{ST}$ as a subtheory of $\sf{GST}$, and since $\sf{ST}$ is finite, a finite fragment of $\sf{PA}$ is sufficient to interpret $\sf{ST}$. Let this fragment be denoted by $\sf{PA}^-$. Conversely, $\sf{ST}$ interprets any finite fragment of $\sf{GST}$, and hence of $\sf{PA}$, so in particular $\sf{ST}$ interprets $\sf{PA}^-$. It follows that $\sf{ST}$ is mutually interpretable with $\sf{PA}^-$. Incidentally, this also proves that all sufficiently inclusive finite fragments of $\sf{PA}$ are mutually interpretable (with each other, with $\sf{ST}$, and with $\sf{PA}^-$).
In pursuit of contradiction, suppose $\sf{ST}$ interprets $\sf{GST}$, then $\sf{PA}^-$ interprets $\sf{PA}$. According to theorem 6.4 of the paper Arithmetization of mathematics in a general setting, there must be an enumeration $\alpha$ of $\sf{PA}^-$ and an enumeration $\beta$ of $\sf{PA}$ such that $\sf{PA}$ proves $\operatorname{Con}_\alpha\implies \operatorname{Con}_\beta$. Since the theory $\sf{PA}^-$ is finite, it's not hard to understand $\operatorname{Con}(\sf{PA}^-)\iff\operatorname{Con}_\alpha$, therefore $\sf{PA}$ proves $\operatorname{Con}(\sf{PA}^-)\implies\operatorname{Con}_\beta$. Moreover, theorem 5.6 of the same paper shows that $\sf{PA}$ can't prove $\operatorname{Con}_\beta$, so it follows that $\sf{PA}$ also can't
prove $\operatorname{Con}(\sf{PA}^-)$. This is a contradiction however. We therefore conclude that $\sf{ST}$ cannot interpret $\sf{GST}$.
