To the language of set theory add a primitive unary predicate $\operatorname {Universe}$ and a primitive total unary function $j$. Add all axioms of $\sf ZF$ in the language of this theory, i.e. the new primitives allowed to be used in instances of Separation and Replacement, I'll refer to this simply as $\sf ZFj$.
We add the following axioms:
Cumulative: $\forall X: \operatorname {Universe}(X) \to \exists \lambda: X=V_\lambda$
Modeling: if $\psi$ is an axiom of $\sf ZFj$, and $\psi^X$ is the $“\in X"$ bounded form of $\psi$; then: $$\forall X: \operatorname {Universe}(X) \to \psi^X$$
Elementarity: if $\phi(x_1,..,x_n)$ is a formula in signature $\{=,\in\}$, having $“x_1,..,x_n\! \!"$ as its sole free variables, and none of them occur bound, then: $$\forall X: \operatorname {Universe}(X) \to\forall x \in X \, (j(x) \in X) \land \\\forall x_1,..,x_n \in X \\ (\phi(x_1,..,x_n) \iff \phi(j(x_1),..,j(x_n))) \\ \land \exists x \in X: j(x) \neq x$$
The intention is to render the restriction of $j$ to any Universe $X$ a non-trivial elementary embedding from $X \to X$.
Reflection: if $\phi$ is a formula [defined functions and predicates allowed] not using the symbol $X$, and $\phi^X$ is the $“\in X"$ bounded form of $\phi$; then: $$\forall \vec{p} \, (\phi \to \exists X: \operatorname {Universe} (X) \land \phi^X)$$
Is this consistent? If so, what's its consistency strength?
In particular does it manage to interpret Reinhardt cardinals at each universe? Would we have a club of Reinhardt cardinals?
Best Answer
It is inconsistent. Call an ordinal b an independent critical point if for every for every Universe X,
if c∈X then there is a function f with domain X and an ordinal α, such that "f is an elementary
embedding from X to Vα" holds, for all x∈X f(x)∈X, and b is the least ordinal with f(b)≠b.
Note that the critical point of j is an independent critical point because the restriction of j to any
Universe X has the above property of f. Let c be the least independent critical point. By the
axiom schema of Reflection, there is a universe K such that "c is the least independent critical
point" holds relativized to K. By the definition of independent critical point, there is a function
g with domain K and ordinal γ such tha g is an elementary embedding from K to Vγ, and for all x∈K g(x)∈K
and c is the least ordinal with g(c)≠c. Let F(x) be a formula expressing
"x is the least independent critical point". Define a sequence s by
s0=c and s(n+1) is the least ordinal α such that α is greater than g(s(n)) and for K, Vα reflects all
subformulas of F. Let t=U{sn|n∈𝜔}. Then g(t)=t, and F(c) holds in V(t). By elementarity,F(g(c)) holds
in V(g(t)). That is F(g(c)) holds in V(t). But this is impossible.