If we add to the wholeness axiom, the axiom of stratified\acyclic replacement, what would be the consistency state and strength of the resulting theory?
The wholeness axiom $\sf WA$, introduced by Paul Corazza, found to be consistent with $\sf V=HOD$, is axiomatized in the first order language with signature $\{ \in , j\}$, where $j$ is a primitive total one place function symbol. An "$\in$-formula" is a formula in which $j$ doesn't occur.
$\sf WA$ is the statement that "$j$ is a non-trivial elementary embedding from $V$ to $V$ over signature $\{ \in \}$".
More explicity:
- $\exists x: j(x) \neq x$
- if $\varphi(x_1,..,x_n)$ is an $\in$-formula, then: $$ \forall x_1,.., \forall x_n \\(\varphi(x_1,..,x_n) \iff \varphi(j(x_1),..,j(x_n)))$$
Now, the theory is:
$\sf ZC + \sf Rep^\in + WA$
where $\sf Rep^\in$ is replacement scheme restricted to $\in$-formulas.
To be especially noticed that there is no restriction on $\sf Z$, so $j$ can be used in instances of Separation.
Now, stratified replacement "$\sf Rep^\equiv $" is Replacement schema restricted to stratified formulas.
Stratification criterion is defined after Quine as in Stratified Comprehension, plus the requirement that $j(x)$ is one type higher than $x$.
Equivalently $\sf Rep^\equiv$ can be formalized by the restriction of replacement schema to acyclic formulas, with an edge stipulated to occur between $x$ and $j(x)$ in the definition of acyclic formula.
The rationale beyond this is that the stratification\acyclicity criterion precludes Kunen's known proof of the critical sequence $\langle \kappa_n | n \in \omega \rangle $, defined as usual by $\kappa_0 = \kappa = \operatorname{cp}(j)$ and $\kappa_{n+1} = j(\kappa_n)$, being a set.
So, formally the question is:
Would $\sf ZC + \sf Rep^\in + Rep^\equiv + WA$, be stronger than, $\sf ZC + \sf Rep^\in + WA$ ?
[After note]: Stratified replacement proved to be inconsistent, since it does capture the critical sequence as shown in the answer by Greg Kiramyer. But, still the Acyclic variant remains viable. I initially thought it to be equivalent to the stratified one; I'm realizing now that the proof of equivalence of acyclicity with stratification is not carried for the language using $j$ with this particular specifications of stratification, so they might not be equivalent!? Therefore Acyclic Replacement might stand a chance?!