What is the consistency strength of Basic Theory of Elementary Embeddings (BTEE) from [The spectrum of elementrary embeddings j : V → V](http://pcorazza.lisco.com/papers/spectrum_embeddings.pdf) by Paul Corazza?


BTEE uses the language of $(V,∈,j)$ and asserts:  

ZFC (without separation and replacement for formulas using $j$)  

(schema) $j$ a is nontrivial elementary embedding of $V$ into $V$ (for formulas without $j$)  

critical point: the least ordinal moved by $j$ exists.


Without critical point, the theory would be conservative over ZFC. With full replacement (and given the axiom of choice), the theory would be inconsistent; and there is a hierarchy between the two extremes.


BTEE suffices for a basic theory of $j$. For every natural number $n$, BTEE proves that $κ = \mathrm{crit}(j)$ is $n$-ineffable and totally indescribable (see the linked paper). However, the only upper bound on the strength of BTEE in the paper is $ω$-Erdős.


This question is in [Q/A format](https://stackoverflow.com/help/self-answer).



Strength of BTEE
BTEE is conservative over the stationary reflection principle (SRP), i.e. ZFC + (schema) {there is $n$-subtle cardinal}$\_{n∈\mathbb{N}}$. Using $n$-ineffable in the schema is equivalent.


Note that we get conservativity and not just equiconsistency, and also that (without full conservativity) SRP shows up in a number of other results including in a basic axiomatization of [reflective cardinals](https://arxiv.org/abs/1203.2270) of finite orders (an extension of the language of set theory), and (separately) in Harvey Friedman's natural arithmetic statements independent of ZFC.


As noted above, for every $n$, BTEE implies existence of $n$-subtle cardinals.


For the converse, given a proposition $A$, consistency of ZFC + $A$ + (schema) {there is $n$-subtle cardinal}$\_{n∈\mathbb{N}}$ implies existence of a model $M$ of ZFC + $A$ + $n$-subtle cardinal for a nonstandard number $n$, plus existence of $λ$ with $V\_λ^M≺M$. Fix such an $M$ and an $M$-well-ordering $<^\*$ of $V\_λ^M$, and (in $M$; $n$ is nonstandard outside of $M$) use an $n$-subtle cardinal $<λ$ to produce an $n$-tuple $(κ\_1,...,κ\_n)$ of good indiscernibles for $(V\_λ^M, ∈^M, <^\*)$. ("good" is a technical term here and is why we need the $n$-subtle cardinal; it will ensure that $j$ does not move $M$-ordinals below $κ\_1$.) Let $M'$ be the $(V\_λ^M, ∈^M, <^\*)$ Skolem hull of the first $ω$ of these indiscernibles (as computed in $V$ so all Gödel numbers are standard). $(M',∈^M,j)$ satisfies BTEE + $A$ where $j(κ\_i)=κ\_{i+1}$ and $j$ is extended to all sets in $M'$ using the Skolem hull.


Adding induction (and especially transfinite induction) would significantly increase the strength. For the strength of existence of a well-founded model of BTEE, see this [question](https://mathoverflow.net/questions/319231/consistency-strength-of-jl-%CE%B4%E2%86%92l-%CE%B4-for-some-%CE%B4).


*$n$-huge cardinals*


Nonstandard models can also be used to show that WA0 (bounded quantifier Wholeness Axiom, which consists of BTEE and separation for bounded quantifier $j$-formulas) is conservative over ZFC + (schema) {there is $n$-huge $κ$ with $V\_κ≺\_{Σ\_n}V$}$\_{n∈\mathbb{N}}$ . (In turn, this is $Σ\_2^V$ conservative over ZFC + (schema) {there is $n$-huge $κ$}$\_{n∈\mathbb{N}}$ .)


One direction is proved in the linked paper. For the converse, given a proposition $A$, consistency of ZFC + $A$ + (schema) {there is $n$-huge $κ$ with $V\_κ≺\_{Σ\_n}V$}$\_{n∈\mathbb{N}}$ implies existence of a model $M$ of ZFC + $A$ + $n$-huge cardinal $κ$ for a nonstandard number $n$, and with $V\_κ^M≺M$. Starting with such $M$ and an $n$-huge embedding $j$ in $M$ with $κ = \mathrm{crit}(j)$, let $M' = \{x∈M: ∃m<ω \,\, x ∈^M j^m(V\_κ^M)\}$. (Note that we use $ω$ rather than $ω^M$.) $(M', ∈^M, j)$ satisfies WA0 + $A$.


