# What is the consistency limit of accumulative typing below $\omega_1^{CK}$?

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 +

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

2. 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.

1. Membership: $\forall x,y \ [y \in x \to ( T_{i+1}(x) \leftrightarrow T_i(y))]$
2. Accumulation: if $i<j$, then $\forall x [T_i(x) \to T_j(x)]$
3. 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?

• The $V_\alpha$ are sets, not measures of consistency strength. You may want to clarify the final line. – Andrés E. Caicedo Jun 17 '18 at 12:29
• @AndrésE.Caicedo acknowledged! question corrected. – Zuhair Al-Johar Jun 17 '18 at 17:30