# Strength of BTEE

What is the consistency strength of Basic Theory of Elementary Embeddings (BTEE) from The spectrum of elementrary embeddings j : V → V 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.

BTEE is conservative over the stationary reflection principle, i.e. ZFC + (schema) {there is $$n$$-subtle cardinal}$$_{n∈\mathbb{N}}$$ . (Note that using $$n$$-ineffable in the schema is equivalent.) 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$$) 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.) 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.
$$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$$.