Let $Th_\zeta$ be a Mono-sorted first order theory with $\zeta$ representing some recursive ordinal notation system.

Primitives: =, $\in$, $T_0, T_1, ..,T_i,..$ where i is an $\zeta$ ordinal, and each $T_i$ is a unary predicate symbol.

Axioms: those of first order identity theory +

Extensionality: $\forall a,b [\forall x (x \in a \leftrightarrow x \in b) \to a=b]$

Comprehension: if $\phi(y)$ is a formula in which symbol $``y"$ occurs free, and only free, and symbol $``x"$ never occurrs, then all closures of:

$$\exists x [T_{i+1}(x) \wedge \forall y (y \in x \leftrightarrow T_i(y) \wedge \phi(y))]$$, are axioms.

- Membership: $\forall x,y \ [y \in x \to ( T_{i+1}(x) \leftrightarrow T_i(y))] $
- Accumulation: if $i<j$, then $\forall x [T_i(x) \to T_j(x)]$
- Ground: $\forall x [T_0(x) \to \forall y (y \not \in x)]$

This is a simple theory of sets with accumulative typing that are indexed below the limit of all $\zeta$ ordinals.

Obviously we can have many theories of that kind, so we can have $Th_\eta$, $Th_\delta$, .. etc where $\eta, \delta,..$ are recursive ordinal notation systems, in general we can have a theory $Th_\alpha$ for each $\alpha \in \mathcal{O}$, where the latter is Kleene's $\mathcal{O}$, of course the set of all these theories is not effectively generated.

It is clear that we would have $Z$ interpreted as early as the second limit ordinal, i.e. by $Th_{\omega.2}$

Question: What would be the limit to the consistency strength of all $Th_{\alpha}$, $\alpha \in \mathcal{O}$ theories? Would it be simply the consistency strength of a fragment of ZFC that has $\langle V_{\omega_1^{CK}}, \in_{V_{\omega_1^{CK}}}\rangle$ as a model?