*Short version: there is a natural, very "thin" (but probably not minimal) model of Zeremelo set theory; I'm curious what is known about it.*

Zermelo set theory (= ZF without the Replacement scheme) is an incredibly weak theory in many ways: for example, it can't even prove the existence of $\omega+\omega$ or of the set of hereditarily finite sets. So its models can look quite weird.

I'm interested in one model in particular, and I'm wondering whether anything is known about it. It's defined as follows. As usual, we start with $G_0=\emptyset$, take unions at limit stages, and let $G$ be the union of all stages. The successor stages however are a bit more complicated. We want to make sure we satisfy:

"Tallness" (= contains all ordinals),

Pairing,

Union,

Separation, and

Powerset.

(Foundation is trivially satisfied; Extensionality will follow from transitivity, which is proved inductively.)

We'll handle each of these explicitly. Suppose we have $G_\alpha$. Then we define:

$G_{\alpha,0}=G_\alpha\cup\{\alpha\}$.

$G_{\alpha,1}=G_{\alpha,0}\cup\{(x, y): x, y\in G_{\alpha,0}\}$.

$G_{\alpha,2}=G_{\alpha,1}\cup\{\bigcup x: x\in G_{\alpha,1}\}$.

$G_{\alpha,3}=G_{\alpha,2}\cup\{\varphi^{G_{\alpha,2}}\cap x: x\in G_{\alpha,2},\mbox{ $\varphi$ a formula}\}$.

*Compare with the successor stages in the construction of $L$: $L_{\alpha+1}=L_\alpha\cup\{\varphi^{L_\alpha}: \mbox{ $\varphi$ is a formula}\}$.*$G_{\alpha,4}=G_{\alpha,3}\cup\{\mathcal{P}(x)\cap G_{\alpha,3}: x\in G_{\alpha,3}\}$.

*The set $\mathcal{P}(x)\cap G_{\alpha,3}$ seems worth keeping track of; call it "$\mathcal{P}(x)[\alpha]$."*

We then let $G_{\alpha+1}=G_{\alpha,4}$.

It's not hard to show that $G$ satisfies Z; the nontrivial steps are Powerset *(eventually we run out of new subsets of $x$, so for some $\alpha$ we have $\mathcal{P}_\alpha(x)=\mathcal{P}^G(x)$)* and Separation *(by induction on formula complexity, if $G$ satisfies $\varphi$ then so does $G_\alpha$ for club-many $\alpha$)*. And while I see no reason for $G$ to be a *minimal* model of Z *(since we've potentially added lots of unnecessary steps by performing "separation-moves" and "powerset-moves" at each successor stage in the construction)*, it does seem reasonably natural. So I'm curious:

What is known about this model?

I'm also interested in variations on this construction. The most natural one is probably $G^+$, where we throw $G_\alpha$ in as an element of $G_{\alpha+1}$. Another class of variations can be gotten by only performing the Separation and Powerset "guesses" some of the time. *(Actually this one seems vaguely interesting in a different way: consider a game where - while the tallness, union, and pairing "moves" continue to be performed automatically - one player is making Separation-moves, and the other is making Powerset-moves, and they're trying to control the behavior of the resulting model ...)*. But from the point of view of looking for natural "thin" models of Z, I think the specific G above is a reasonable place to start, so that's what I'm asking about here.

It's worth pointing out that there is a body of literature on models of Zermelo set theory, including in particular Mathias' paper on slim models; but I haven't been able to find this particular model in that literature.