Consistency of Nontrivial Elementary Embedding from $\omega_1$ to itself?

I was wondering about a way to make really large countable ordinals. It turns out that in certain models of ZFC (for example pointwise definable ones) every ordinal is definable with no parameters, which means you can't expect your ordinal to exist in every model of ZFC without having some FOST (language of first-order set theory) equivalent characterization.

Of course, one can simply make an axiom (a scheme with constant a symbol) to create such an ordinal which is not definable within ZFC (unless something with $\omega$-consistency, I don’t know what really). One can then make a scheme with more constant symbols that are all ordinals which cannot be defined from previous ordinals.

A sort of "limit" of this is making an axiom stating the existence of an elementary embedding from $\omega_1$ to itself with a critical point. I believe this could quite easily be proven inconsistent, but I'm not sure how to start.

I call this "The Axiom of Countable Ineffability" or $\text{CI}$ for short. Here's the formal definition of $\text{CI}(Q)$ for a set of formulae $Q$:

1. There is some ordinal $\alpha\in\omega_1$ such that $j(\alpha)\neq\alpha$
2. For every $\alpha\in\omega_1$, $j(\alpha)\in\omega_1$.
3. For every $\varphi\in Q$, an axiom stating that for any $\alpha_0,\alpha_1...\in\omega_1$ with $\varphi^{\omega_1}(\alpha_0,\alpha_1...)$, $\varphi^{\omega_1}(j(\alpha_0),j(\alpha_1)...)$

Of course, because it only quantifies over $\varphi^{\omega_1}$ for FOST $\varphi$, for which there exists a set-sized truth predicate in $V$ (defined on the set of all finite sequences of countable ordinals), this can be stated as a single FOST axiom (as long as the class $\{\varphi^{\omega_1}:\varphi\in Q\}$). In fact, this is true for any uncountable ordinal, not just $\omega_1$.

The Questions

1. What is the consistency of $\text{ZFC}+\text{CI}(\Sigma_n)$?
2. What is the consistency of $\text{ZFC}+\text{CI}$?
• Does your ZFC+CI include instances of replacement (or collection and separation) that involve the new symbol $j$, or only the instances in the original language of ZFC? – Andreas Blass Aug 28 '18 at 17:10
• What is FOST and IDK? – Emil Jeřábek Aug 28 '18 at 17:15
• It follows from $0^\sharp$. I would guess it’s equivalent. – Monroe Eskew Aug 28 '18 at 17:26
• When you say elementary embedding of $\omega_1$ into itself what language are you talking about? If it's just $\omega_1$ as a linear order then I think there's an explicit ZFC definable non-trivial elementary embedding of it into itself. – James Hanson Aug 28 '18 at 22:43
• Very little is actually first-order definable in ordinals as pure linear orders. I believe that $\omega^{\omega+1} = \omega^\omega \times \omega$ has $\omega^{\omega}\times \{0,2,3,4,\dots\}$ (i.e. delete the second $\omega^\omega$ block) as an isomorphic proper elementary substructure, which implies that for any ordinal $\alpha \geq \omega^{\omega+1}$ there's an explicit ZFC definable non-trivial elementary embedding of $\alpha$ into itself as a linear order. – James Hanson Aug 29 '18 at 5:45