Question: Is the following theory conservative over ZFC? And if not, what is its strength?
Language: $∈$, $j$ (unary function symbol)
Axioms:
1. ZFC (without separation and replacement for formulas using $j$).
2. (schema) $j$ is a nontrivial elementary embedding $(V,∈)→(V,∈)$.
3. (schema) $S∩φ ≡ \{s∈S:φ(s)\}$ exists whenever $φ$ is a formula with parameters and one free variable and set $S$ is definable (allowing $j$).
Note that (3) implies existence of $S'∩φ$ for all $S'$ with $|S'|≤|S|$ for some $S$ as above. Thus, (3) simply asserts the full Separation Schema for sets that are not too large, including all definable sets.
I am also interested in the extension (its strength is above $n$-Mahlo):
3a. Allow any $S$ definable (allowing $j$) from some set $T$ with $T=j(T$).
Background
An important phenomenon in mathematical logic is that if we extend a theory with new symbols (and sometimes new types) and add reasonable new axioms, the new theory will sometimes be conservative over the original one; and such correspondences often give key structural insight into both theories. A special case, relevant here, is that the new theory is seemingly stronger and captures a part of the structure of a stronger theory, but is missing a key ingredient.
Under various reasonable formalizations (that imply replacement for $j$-formulas), existence of a nontrivial elementary embedding $V→M$ ($M$ transitive) is equivalent to existence of a measurable cardinal, and $V=M$ is inconsistent with ZFC.
However, (1) + (2) is conservative over ZFC: Add Skolem functions for $V$ and add $ω$ constant symbols for indiscernible ordinals, use compactness to find a model, take the Skolem hull of the indiscernibles, and add a nontrivial order preserving injection between the indiscernibles, which will then extend to the desired elementary embedding.
Such a model (above) may be ill-founded, but we can try to make it well-behaved with respect to small sets. Every countable ZFC model $M$ has a nontrivial elementary end extension $N$; by elementarity, $N$ is also a top extension, that is for all $α∈\mathrm{Ord}^M$, $V_α^M$ and $V_α^N$ have the same elements. We can even require $N$ to have a nontrivial automorphism fixing all elements of $M$. And perhaps some way of incorporating $j$ there will give a positive answer to the question.
Under (1)-(3a), $\{s:s=j(s)\}$ (under '$∈$') is a rank-initial proper elementary substructure of $(V,∈)$, but it does not exist as a set unless its cardinality is $n$-huge for every $n$. Also, under (1)-(3a), if we let $I = \{β∈\mathrm{Ord}:j(β)=β\}$ and $C=\{x∩V_I:x∈V\}$, then $(V_I,C,∈)$ satisfies NBG + "$\mathrm{Ord}$ is weakly compact". NBG + "$\mathrm{Ord}$ is weakly compact" is equiconsistent with ZFC + $\{n\text{-Mahlo}\}_{n∈ω}$. A related theory is discussed in Automorphisms, Mahlo Cardinals, and NFU by Ali Enayat.
As an aside, there is a rich hierarchy theories based on how 'close' $j$ is to $V$. For example (see this question), if (3) is replaced with the critical point axiom (i.e. the least ordinal moved by $j$ exists), the resulting theory is conservative over ZFC + {there is $n$-ineffable cardinal}$_{n∈ℕ}$.
