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?
Best Answer
$\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).