Consistency strength of an attempt at higher order set theory

Question

Work in a theory with (deep breath) a countable number of primitives denoted with capital letters from the end of the alphabet with numerical subscripts $\{X_n,Y_n,Z_n,\dots\}_{n<\omega}$ indicating which kind of primitive they are together with primitive relations $\{\in_n\}_{n<\omega}$ with numerical subscripts indicating which kind of primitive they are a relation on, such that each $n$-primitive is also an $n+1$-primitive for all $n<\omega$ and such that $\in_n$ is $\in_{n+1}$ restricted to $n$-primitives for all $n<\omega$, and such that each $\in_n$ is left closed so primitives to the left of $\in_n$ are at most $n$-primitives. Call $0$-primitives sets, and suppress subscripts when they are obvious from context.

For axioms assume $Z$ plus foundation (denoted $Z^+$) for each level of primitives, so we can pair/union/powerset/separate/etc. at each primitive stage. Note that we can pair etc. $n$- and $m$-primitives for $n<m$ since all $n$-primitives are also $m$-primitives. For all $n<\omega$, say that a predicate $\phi$ in the language of this theory is safe above $n$ iff no $m$-primitives for $m>n$ occur in $\phi$, and let $\Phi_n$ denote the set of all predicates safe above $n$. Add

Class Building Axioms. For all $n$, if $\phi$ is a predicate in the language of this theory safe above $n$, then there exists an $n+1$-primitive $X_{n+1}$ whose members are precisely the $n$-primitives $Y_n$ sayisfying $\phi$. $$\forall\phi\in\Phi_n\exists X_{n+1}\big(Y_n\in X_{n+1}\iff\phi(Y_n)\big).$$ We denote the $n+1$-primitive guaranteed by this axiom together with a predicate $\phi$ safe above $n$ by $$\{Y_n:\phi(Y_n)\}_{n+1}.$$

Define functions as subsets of arbitrary Cartesian products as usual. For all $n<\omega$, define the $n+1$-primitive of all $n$-primitives by $$\widehat{V_{n+1}}=\{X_n:X_n=X_n\}_{n+1}.$$

Replacement. If $F$ is a function and $dmnF$ is an $n$-primitive and $F(X)$ is an $n$-primitive for all $X\in dmnF$, then $rngF$ is an $n$-primitive. $$\forall n\forall F(F\ \text{is a function}\wedge dmnF\in \widehat{V_{n+1}}\wedge\forall X\in dmnF(F(X)\in\widehat{V_{n+1}})\implies rngF\in\widehat{V_{n+1}}).$$

This gives us replacement at each stage, since (for example) we can form the $1$-primitive $$X=\{\mathcal{P}^n(\emptyset):n\in\omega\}$$ by class building and form the surjective function $$\langle\mathcal{P}^n(\emptyset):n<\omega\rangle\subset\omega\times X$$ to prove that $X$ is in fact a set by replacement, then take $\mathcal{P}^\omega(\emptyset)=\bigcup X$ and proceed to define $\mathcal{P}^{\omega+\omega}(\emptyset)$ and higher stages of the cumulative hierarchy as usual.

Question. What is the consistency strength of this theory?

It's bounded above trivially by $ZFC$ plus the existence of a countable number of inaccessible cardinals $\{\kappa_i\}_{i<\omega}$ with $\kappa_i<\kappa_{i+1}$ for all $i<\omega$, where we take $\widehat{V_{n+1}}=V_{\kappa_n}$ for all $n<\omega$ together with usual membership. Is this also a lower bound?

---

Edit: Replacement as originally phrased made the theory inconsistent, since for all $n$ we have that $\{(0,\widehat{V_n})\}$ is trivially a function whose domain is a set, so $\{\widehat{V_n}\}$ would be a set for all $n$ and this together with unions yields obvious inconsistencies. I believe the fix proposed above avoids this issue and still allows for use of the axiom in all desired situations, since it correctly describes the kind of replacement we have in the inaccessible cardinal situation.

Answer 1

I believe $ZFC$ plus the existence of a countable collection of strictly inaccessible cardinals is also a lower bound on the consistency strength of this theory, and am posting this as a CW answer to close the question.

For a proof sketch, define ordinals to be hereditarily membership transitive primitives, define rank $\rho$ as usual for all primitives, and for each $n<\omega$ define $$Ord_n=\{X:X\ \text{is an ordinal}\}_{n+1}.$$ In particular, each $Ord_n$ is a proper $n+1$ primitive (it is not also an $n$-primitive) since it is also an ordinal and would thusly be a member of itself by definition if it were an $n$-primitive, contradicting foundation. Further, defining stages of the cumulative hierarchy $V_\alpha$ for ordinals $\alpha$ using rank in the usual way we have that $$V_{Ord_n+1}\models MK$$ for all $n<\omega$. To see this, observe that for all $n<\omega$ we have that $$V_{Ord_n}=\widehat{V_{n+1}}\models ZFC$$ and if we have two $n+1$-primitives $X,Y\in V_{Ord_n+1}$ (viewed as 'classes over $V_{Ord_n}$') with $X\in Y$ then $$\rho(X)<\rho(Y)\leq Ord_n\implies X\in V_{Ord_n}=\widehat{V_{n+1}},$$ so a 'class $X$ over $V_{Ord_n}$' becomes a 'set in $V_{Ord_n}$' as soon as it is a member of another 'class over $V_{Ord_n}$'. Using the characterization of strictly inaccessible cardinals as those ordinals $\alpha$ such that $V_{\alpha+1}\models MK$, we see that $Ord_n$ is strictly inaccessible for all $n<\omega$.

Answer 2

Replacement is not one of your background axioms, and your theory doesn't prove it. Extend $\sf ZFC$ with countably infinite many inaccessibles $icc_0, icc_1,icc_2,...$ ; now let $\kappa= \bigcup \{icc_n \mid n \in \omega\}$, then $(V_\kappa,\in^{V_\kappa})$ is a model of your main theory, and $(V_{\kappa+\omega}, \in^{V_{\kappa+\omega}})$ is a model of your theory with the completion axiom A6. And clearly none of these models satisfy replacement. The lower bound on your main theory is $\sf Z +$$ \forall n \in \omega: icc_n \text{ exists }$, and on your theory with A6 schema is $\sf Z$$+ V_\kappa \text{ exists }$, where $\kappa$ defined above.