Is $\mathrm{ZFC}^E$ outright inconsistent?

Question

From $\mathrm{ZFC},$ define a new theory $\mathrm{ZFC}^E$ by adjoining a constant symbol $E$ together with axioms to the effect that:

• $E$ is countable and transitive
• $(E,\in)$ is an elementarily equivalent to $(V,\in).^*$ (This is an axiom schema).

Question. Is $\mathrm{ZFC}^E$ outright inconsistent?

Motivation. The idea (or motivation) is to have a "miniature copy" of the universe available, that is nonetheless "very small" from our omniscient $V$-like perspective.

Answer 1

This is Feferman's extension of $\sf ZFC$, and it is a conservative extension of $\sf ZFC$. But note that you cannot state that $E$ is an elementary substructure of the universe with an axiom, since that would violate Tarski's theorem. You can, however, do it one axiom at a time.

To see that the new theory is a conservative extension, note that it follows immediately from the reflection theorem: everything true in $V$, is true in a countable transitive model (well, here we apply Lowenheim-Skolem and Mostowski's collapse lemma).

I couldn't find a specific citation, but I did find several references by other people to the following paper.

Feferman, Solomon. "Set-Theoretical foundations of category theory", Reports of the Midwest Category Seminar III, Lecture Notes in Mathematics Volume 106, 1969, pp 201-247.

Answer 2

As you point out in the comments, if $E$ is an elementary substructure of $V$, then the theory is inconsistent. If it were an elementary substructure, we'd have $\omega^E_1 = \omega_1$.

If $E$ is merely elementary equivalent, on the other hand, then the theory is consistent. To see this, note that for any finite list of sentences $\phi_0,...,\phi_n$, ZFC proves the existence of a countable transitive model $M$ which is elementary equivalent to $V$ with respect to those sentences. This can be established by first taking a countable Skolem Hull with respect to the subformulas of $\phi_0,...,\phi_n$ and then doing a Mostowski collapse. So ZFC can interpret arbitrarily large finite fragments of your theory, and thus it's consistent.