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



Can we iteratively reflect on self elementary embeddable stages of the cumulative hierarchy?
$\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).


