What is the limit to iterating class comprehension, reflection and limitation of size?

Question

In posting about a reflection principle coupled with a limitation of size axiom over Ackermann set theory, the answer is that the theory is blown up to a Mahlo cardinal.

I'm here just wondering if this method can be iterated, and what is the maximal that it can reach to via this iteration process.

For example lets define a theory $\mathsf{K}^{+}(V_{\lambda})$ in the language of $FOL(=,\in, V_1, V_2,..,V_{\lambda})$ as long as $\lambda$ is some specific recursive ordinal having some specific ordinal notation, i.e. as long as $\lambda < \omega_1^{CK}$

Now the idea is that each theory $\mathsf{K}^{+}(V_{\lambda})$ has axioms of Extensionality, Class comprehension axiom schema for $V_{\alpha}$, a reflection axiom scheme for $V_{\alpha}$, and limitation of size axiom for $V_{\alpha}$, for each $\alpha < \lambda$, also we have the axiom schema:

if $\alpha < \beta$, then: $``\forall x (x \subset V_{\alpha} \to x \in V_{\beta})"$ is an axiom.

More specifically the formula of class comprehension for $V_{\alpha}$ is:

$$\forall x_1,..,x_n \subseteq V_{\alpha} \exists x \forall y (y \in x \leftrightarrow y \in V_{\alpha} \wedge \varphi(y,x_1,..,x_n))$$, where $\varphi(y,x_1,..,x_n)$ is a formula that do not use primitives $V_{\beta}$ when $\beta>\alpha$.

While the formula of reflection schema for $V_{\alpha}$ would be written as:

$$\forall x_1,..,x_n \in V_{\alpha} \\ [\exists y (\varphi(y,x_1,..,x_n)) \to \exists y \in V_{\alpha}(\varphi(y,x_1,..,x_n)) ]$$ where $\varphi(y,x_1,..,x_n)$ doesn't use any primitive symbol $V_{\beta}$ as long as $\beta \geq \alpha$.

Now what is the limit to the consistency strength of the $\mathsf{K}^{+}(V_{\lambda})$ theories?

Answer 1

I claim $K^+(V^\lambda)$, for any $\lambda$ (I switched the notation so not to be confused with the von Neumann universe) is equiconsistent with the schema "$ORD$ is Mahlo" (Not to be confused with full stationarity, which could be called "$Ord$ is Mahlo" if you really wanted to distinguish them). First off each $V^\lambda$ is a Grothendieck universe, and so of the form $V_\kappa$ for inaccessible $\kappa$. Second of all, $V_\kappa\prec W$, where $W=\{x|x=x\}$. To see this, suppose $\exists x(\phi(x,x_0...x_n))$ where $\phi(x,x_0...x_n)$ is absolute.

Then $\exists x(\phi(x,x_0...x_n))$ if and only if $\exists x\in V^\lambda(\phi(x,x_0...x_n))$ if and only if $\exists x\in V^\lambda(\phi^{V^\lambda}(x,x_0...x_n))$ if and only if $V^\lambda\vDash\exists x(\phi(x,x_0...x_n))$. Note that at no point do we use reflection for a formula that uses $V^\lambda$. Therefore $K^+(V^\lambda)$ proves that there exists a reflection cardinal, and so the consistency strength of $K^+(V^\lambda)\ge$ the consistency strength of "$ORD$ is Mahlo."

Then, suppose $ORD$ is Mahlo. Then there exists a proper class of reflecting cardinals, and if we take $V^\lambda=V_\kappa$ for reflecting $\kappa$, we get $K^+(V^\lambda)$. Therefore the consistency strength of "$ORD$ is Mahlo"$\ge$ the consistency strength of $K^+(V^\lambda)$, and so the consistency of "$ORD$ is Mahlo"$=$ the consistency strength of $K^+(V^\lambda)$.