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](http://pcorazza.lisco.com/papers/MVS/WholenessAxiom.pdf) by Paul Corazza, found to be [consistent with $\sf V=HOD$](https://arxiv.org/pdf/math/9902079.pdf), 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](https://en.wikipedia.org/wiki/New_Foundations#Axioms_and_stratification) criterion is defined after Quine as in Stratified Comprehension, plus the requirement that $j(x)$ is one type higher than $x$.


[Equivalently](https://arxiv.org/pdf/2009.13274.pdf) $\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](https://arxiv.org/pdf/2010.14949.pdf).


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?!



If we add stratified\acyclic replacement to the wholeness axiom, would that increase its consistency strength?
The statement beginning "The rationale beyond" is not quite correct. The critical sequence can be constucted by exploiting the facts that $\bigcup j(x)$ will be assigned the same number as $x$ in a stratification assignment, $\bigcup x=x$ for any limit ordinal, and $\omega$ is well ordered by proper subset relation $\subsetneq$.


Let $F(W,K,x,y)$ be the "formula":


$x∈W \land \exists f: f \text { is a function } \land \\ dom(f)=\{t \in W \mid t \subseteq x\} \land \\ f(0)=K \land f(x)=y\land \\ \forall t((t≠0 \land t∈ dom(f)) \to \\f(t) = \bigcup j(f(\bigcup \{s∈W \mid s\subsetneq t\}))))$


Then for all $n \in \omega $, there is a unique $y$ such that $F(\omega,\kappa,n,y)$, the $n$-th element of the critical sequence, where $\kappa$ is the critical point of $j$.


