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?

12more comments