Is the class of models of Zermelo set theory that have a hierarchy elementary? Let $\mathrm Z$ be original Zermelo set theory with the foundation scheme (aka ZF-Replacement). Let us say that a model $M$ of $\mathrm Z$ has a hierarchy if there is a $M$-definable sequence $\langle H_i\mid i\in\mathrm{Ord}^M\rangle$ that vaguely resembles the Von Neumann hierarchy in a model of ZF. More precisely it should satisfy (from the point of view of $M$):


*

*All $H_i$ are transitive sets

*$H_i\subseteq H_j$ for $i\leq j$

*$M=\bigcup_{i\in\mathrm{Ord}^M} H_i$
The models of $\mathrm Z$ that come up in practice usually have a hierarchy as they often are limit points of a hierarchy of a larger model, this can, but need not come in the form of the Von Neumann hierarchy. For example $V_\alpha$ if $\alpha$ is a limit ordinal, $H_\kappa$ if $\kappa$ is a strong limit cardinal, and also $L_\alpha[B]$ fits this bill if $B\in L_\alpha[B]\models\mathrm Z$. There are, however, many models of $\mathrm Z$ that do not have a hierarchy. Models of $\mathrm Z$ that have a hierarchy must satisfy some sentences that are not provable in $\mathrm Z$, for example the axiom $\mathrm{TC}$ of transitive containment (every set is a subset of a transitive set), and more.
My question is:

Is the class of models of $\mathrm Z$ that have a hierarchy axiomatisable?

If anyone is interested, some notes with more information are available as A transitive model of $\mathrm{ZC}+\neg\mathrm{TC}$ on my website.
 A: One formula to rule them all?
Given a model $M$ of Z, we say that a formula $\varphi$ witnesses that $M$ has a hierarchy if it satisfies :

*

*for $i \in \operatorname{Ord}(M)$, $\varphi(i, M)$ is transitive.

*for $i \leqslant j \in \operatorname{Ord}(M)$, $\varphi(i,M) \subseteq \varphi(j, M)$.

*for all $x \in M$, there is $i \in \operatorname{Ord}(M)$ such that $x \in \varphi(i, M)$.

We can speak of the  set $H$ of all formulas that witness that some model $M$ of Z has a hierarchy. Now, assuming that having a hierarchy is elementary, there are two possibilities :

*

*either there are finitely many $\varphi_1, \dots, \varphi_n \in H$ such that for any model $M$ of Z with a hierarchy some $\varphi_i$ witnesses that $M$ has a hierarchy. Then the class of models of Z having a hierarchy is axiomatized by the formula stating "some $\varphi_i, 1 \leqslant i \leqslant n$ witnesses that $M$ has a hierarchy".


*or we should be able to use compactness to get a model of "$M$ has a hierarchy but no formula of $H$ witnesses it", which would be a contradiction.
Hence, an axiomatization of "having a hierarchy" must boil down to a single formula of the said form.
