Smallest ordinal modelling $\aleph_1$? Let $X_1$ be the class of all ordinals $\alpha$ such that there exists a transitive model $M$ of ZF(C) such that $M$ thinks that $\alpha$ is $\aleph_1$.
Every class of ordinals has a minimum element (because ordinals are well-ordered), so let $\alpha_1$ be the smallest ordinal in $X_1$.
So, I have 2 questions:


*

*Is the class $X_1$ actually well-defined?

*If it is well-defined, what can we determine about the actual value of $\alpha_1$?


We could also ask the same question for $\aleph_\beta$ (for any ordinal $\beta$) instead of $\aleph_1$, which I'd also be interested in.

My thoughts:
There are two points I think to verify that $X_1$ is well-defined. The first is that "is a transitive model of ZF(C)" is definable in the language of ZF(C), and the second is that "$M$ thinks $\alpha$ is $\aleph_1$" needs to be definable.
Being transitive is definable, so really, the first part reduces to whether "being a model of ZF(C)" is definable. I'm a little unsure of whether or not it is, because ZFC is not finitely axiomatizable, but NBG is, which makes me think the idea behind this question might still be salvageable even if it's not definable in ZF(C).
As for that "$M$ thinks $\alpha$ is $\aleph_1$" is definable, it seems very true, because countability is definable, and then "every ordinal less than $\alpha$ is countable, but $\alpha$ is not countable", which should definitely be definable.
So, that means, that part 2 makes sense to talk about. We know that (at least for small enough $\beta$), $\alpha_\beta$ must be countable, because countable models of ZF(C) exist (by Lowenheim Skolem), which is already interesting. I suspect they are all fairly big countable ordinals, almost certainly larger than $\omega_1^{CK}$.
 A: About well-definedness of $X_1$, "being a model of ZFC" is definable since ZFC is a recursive theory, so we could construct some $\Sigma_1^0$ predicate $\textrm{isZFCAxiom}(e)$ for $e$ a Godel-coding of a formula in the language of ZFC. Then I believe we can formalize "$M$ is a model of ZFC" by $\forall(e\in\mathbb N)(\textrm{isZFCAxiom}(e)\rightarrow M\vDash e)$ using some formalization of $\vDash$ for Godel-codes, such as the one (for an explicit example, this set of notes "Models of Set Theory I" by Koepke).

Bounding $\alpha_1$: The following paragraph is an argument I heard by personal communication.
To avoid considering arbitrary transitive models, for any transitive $M$ where $(M,\in)\vDash\textrm{ZF}$ we have $L^M\subseteq M$ and $(L^M,\in)\vDash\textrm{ZF}$. These models $L^M$ must be of the form $L_\xi$ (or $(L_\xi)^V$) for some ordinal $\xi$, and we have $\aleph_1^{(L^M)}\leq\aleph_1^M$, so without loss of minimality we can just consider the ordinals $\aleph_1^{L_\xi}$ where $(L_\xi,\in)\vDash\textrm{ZF}$. Also, to ensure we're bounding $\alpha_1$ and not just the $\aleph_1$ of the minimal model, we can show that $\gamma<\delta$ implies $\aleph_1^{L_\gamma}\leq\aleph_1^{L_\delta}$, since any bijection $\omega\rightarrow \aleph_1^{L_\delta}$ that's a member of $L_\gamma$ must also be a member of $L_\delta$. So the $\aleph_1$ of the minimal model of ZF is indeed $\alpha_1$.
From here on let $\xi$ be least such that $L_\xi\vDash\textrm{ZF}$. Each $L_\xi$ modeling ZF is admissible, so we can apply Theorem 10.2 of Arai's "A sneak preview of proof theory of ordinals", stating admissible $L_\xi$ satisfying "$\alpha$ is a cardinal $>\rho$" for some $\rho<\xi$ must have $L_\xi\cap\mathcal P(\omega)=L_\alpha\cap\mathcal P(\rho)$. Using some results from §4 of Marek and Srebrny's thesis "Gaps in the constructible universe" we obtain some weak lower bounds on $\alpha$: it's larger than the ordinal of ramified analysis $\beta_0$, and larger than the ordinal $\xi$ starting a gap of length $\beta^\beta$ of corollary 4.12. For the bonus question on $\aleph_n^M$, similar results apply when $\rho>\omega$, using the analogous notions of $\rho$-gaps (i.e. gaps in $L_\bullet\cap\mathcal P(\rho)$) introduced in §7.

Strengthening the bounds: Since we know the gap starts at $\alpha_1$ and ends at $\xi$, we can strengthen this bound by showing that the gap is long, e.g. contains many admissibles: let $\sigma_0$ be the $\Pi_3$ formula expressing "the universe is an admissible set" from Richter and Aczel's "Inductive Definitions and Reflecting Properties of Admissible Ordinals". Working in $L_\xi$, ZF proves $\forall\rho((\rho\textrm{ is a cardinal }>\omega)\rightarrow(\sigma_0)^{L_\rho})$, we assumed ZF is sound by assuming ZF has a transitive model, so $L_\rho$ satisfies this sentence. Since each relativization $(\sigma_1)^{L_\rho}$ is $\Delta_0$, each one is absolute and therefore true in $V$, so each $L_\rho$-cardinal, while not really a cardinal, is really admissible. So we get many admissibles (e.g. $\aleph_2^{L_\xi}$,  $\aleph_\omega^{L_\xi}$,  $\aleph_{\omega_1^{L_\xi}+\varepsilon_0^{234}}^{L_\xi}$) between the start and end points of the gap.
We can repeat this section but based on stronger properties of $L_\rho$-cardinals to improve this further. For instance Barwise's Admissible Sets and Structures has an exercise to show each $L_\rho$-cardinal $>\omega$ must be $\rho$-stable for admissible $\rho$, from which we can show each aforementioned $L_\rho$-cardinal in our gap is inaccessibly-stable. (However we need to be careful about showing these properties are absolute w.r.t. $V$)
