Can we iteratively reflect on self elementary embeddable stages of the cumulative hierarchy?

Question

Is it possible to iterate elementary embeddability and reflect on those stages that are elementary embeddable to themselves?

The following is a formal capture of that idea:

To the language of $\sf ZF$ (i.e., mono-sorted $\sf FOL(=,\in)$) add primitive partial unary functions $W$ and $j$.

To the axioms of $\sf ZF$, add the following axioms:

Restriction: $\forall \alpha: W_\alpha \lor j_\alpha \to \operatorname {ordinal}(\alpha)$

Injectivity: $W_\alpha \land W_\beta \land \alpha \neq \beta \to W_\alpha \neq W_\beta$

Cumulation: $\forall \operatorname {ordinal} \alpha \exists \lambda: W_\alpha=V_\lambda$

Elementarity: $\forall \operatorname {ordinal} \alpha \, (j_\alpha: W_\alpha \to W_\alpha \land \\ \forall \vec{x} \in W_\alpha [ \phi(\vec x) \leftrightarrow \phi(j_\alpha[\vec x ])] \land \\ \exists x: j_\alpha (x) \neq x) \\\text {where } \phi \text { is purely set theoretic }$

Reflection: $\forall \vec{x} \in W_\alpha \, (\phi \to \phi^{W_\alpha})$

if $\phi$ [in Reflection] is a formula of the language of set theory + $``j_\alpha \!"$, meaning that $W$ doesn't occur in it and every occurence of $j$ must be subscripted with $\alpha$; also $``\alpha \!"$ only appears in $\phi$ as a subscript of $j$.

Where $V_\lambda$ stands for the $\lambda^{th}$ stage of the cumulative hierarchy, defined in the customary manner. $\phi^X$ stands for relativising all quantifiers in $\phi$ to $``\in X\!"$.

Is the above theory consistent relative to some large cardinal property? If so, Which one?

Answer 1

$\newcommand\Ord{\mathit{Ord}}$The edit to the question has changed it enough so I think it deserves its own answer.

I assume that in reflection we have $\forall \vec{x} \in W_\alpha \, (\phi \to \phi^{W_\alpha})$ holds for all ordinals $\alpha$.

The theory with this strong reflection is inconsistent in a strong sense.

Specifically it fails even when you only consider $W_0$.

Indeed assume that $W_0$ reflects all formulae in the language of $\{\in,j_0\}$ then it reflects $\eta=\exists x(x\notin \operatorname{Dom}(j_0))$, so let $p\in W_0$ be witness of $\eta^{W_0}$.

$W_0$ also reflects $\psi(y)=\exists x\in \Ord (y\in V_x)$, let $r$ be witness of $\psi(p)$ in $W_0$.

Lastly reflect $\phi(y)=y\in \Ord\land V_y\subseteq \operatorname{Dom}(j_0)$ to get that $W_0$ thinks that $\phi(r)$, but this is a contradiction to the choice of $r$, $p$ (note that I only chose 1 arbitrary element, $p$, so I didn't use any choice).

Answer 2

Any model of $ZF$+stationary proper class of $I3$ ordinals (whose consistency strength is at most $ZF$+$I2$) where $W_α$ is listing of $V_{κ}$ where $κ$ is $I3$ and $j_α$ the witness of $I3(V_κ)$ will be a model of your theory.

Injectivity and Cumulation are trivial, $ZF$+Elementarity is part of our assumption.

For Reflection, let $φ$ be any formula, by Levy's reflection principle there is a proper class club $C_φ$ that reflect $φ$ (note that Levy's reflection works even with a modified language).

Because there is a stationary set of $I3$ cardinals, there exists a $I3$ cardinal in $C_φ$, then this ordinal will witness Reflection of $φ$.

---

This section is a follow-up based on the comments.

Let $\cal L$ be the language of our theory (or any other language extending $\{∈\}$), and let $ZF_{ \cal L}$ be $ZF$ with schema over the language $\cal L$ then any model of $ZF$ is (under a suitable interpretations) a model of $ZF_{ \cal L}$.

The reason for this is that we do not have any axioms to restrict any of our new symbols, let interpret each relation symbol in $\cal L\setminus\{∈\}$ as a tautology, each function symbol as the identity, and each constant as the emptyset.

Because all 3 of those are definable, any formula containing any symbols in $\cal L$ will be equivalent to a formula in $\{∈\}$.

So $\forall \alpha \,( W_\alpha \models \sf ZF_{\cal L})$ doesn't imply $W_\alpha$ is a model of ZF+Reinhardt, because while it does satisfy schema over the symbol $j$ and $W$, it does not see any nee from the universe to itself (The symbol of $j$ in $W_α$ has no relation to the symbol $j$ in $V$)

Now what about the reflection principle? In our language we have $2$ extra symbols, $j,W$.

We can restrict ourselves to $α$ such that $W_α$ reflects enough to prevent the triviality we had in the second paragraph of the follow-up, but it doesn't matter.

To show that it doesn't matter, look at the sentence $∀x(x∈Ord\implies ∃y∈Ord(\text{such that $W_x=V_y$ and $j_x$ is nee from $W_x$ to itself}))$, assume it is reflected into $W_α$, why is $W_α$ not Reinhardt? The reason is that $W_α$ does not see all of the ordinals, so while we may have $α∈W_α$ (well, for this specific sentence if it is reflected to $W_\alpha$ then $V_\alpha=W_\alpha$ so $\alpha\notin W_\alpha$, but this is irrelevant to my point), the value of $W_α^{W_α}$ is a proper subset of $W_α$, so $j,W$ inside of $W_α$ cannot say anything about the real $W_α,j_α$, i.e. we can not see any nee on $W_α$ inside of $W_α$.

So how can we get Reinhardt? To get Reinhardt we must adjust the nee $j_α$ to $W_α$, define for a set $X,Y$ the model $(X,∈,Y^{(k)})$ be the model $(X,∈,Y)$ but the symbol for $Y$ is $k$ and add the following axiom (remember that as long as we don't add interpretations/axioms on new symbols, they don't change the theory, so we can require just $ZF_{\{∈,k\}}$ instead of $ZF_{\{∈,k,j,W\}}$):

For every ordinal $α$, $(W_{α},∈,j_{α}^{(k)})⊨ZF_{\{∈,k\}}$

This is exactly your theory with the extra axiom that "$W_α$ can see the nee on itself".

This theory is very strong, I want to say that this theory is equivalent to "ZF + there is stationary proper class of $α$ such that $V_α$ is a model of Reinhardt", but I am not 100% sure about the $⇒$ direction (the proof of $⇐$ direction is essentially the same as my original answer but replacing $I3$ with Reinhardt).