[Edit]: This is an edit of question [the original question ends before the context is added], it only added the general context of that question, the question itself remains the same.
Is forcing needed to prove that there is a model of ZF that is a countable stage of Gödel's constructible universe? Formally, does the following requires forcing to prove it?
$$\exists \alpha : |\alpha|=\aleph_0 \land L_\alpha \models ZF$$
The context for that question is the following:
First I'll quote some of Noah's answer to a prior posting:
Quoting from this answer:
"we can build the $L$-hierarchy on any "starting set" of Quine atoms $A$ - let $L^A_0=A$, $L^A_\lambda=\bigcup_{\alpha<\lambda} L^A_\alpha$ for $\lambda$ limit, and $L^A_{\alpha+1}=L^A_\alpha\cup\mathcal{P}_{def}(L^A_\alpha)$. Letting $W_A$ be the $L$-hierarchy on $A$ continued until we get a model of ZF-Reg, we can show that the pure part of $W_A$ is countable regardless of whether $A$ is; now simply take an uncountable set of Quine atoms".
This was used to show that there can exist a set in ZF-Reg. that is not subnumerous to any well founded set; thereby proving that both choice and CH can fail in some models of ZF-Reg. [since $A$ won't be comparable to its Hartog number]. The same argument can be adopted to prove that failure in some models of ZFA.
Now the line written in bold is exactly what I'm asking about. My understanding of that is that the pure part of $W_A$ cannot be countable unless its height is countable, i.e. the $\alpha$ such that $W_A = L^A_\alpha$, must be countable. Now according to the answer suppose that $A$ is empty, then the "pure part" of $W_A$ would be $W_A$ itself, which mean that we can have a model of ZF at some countable stage of L.
The broader context of this question is the following:
Suppose that the proof of this countability doesn't require forcing. Now instead of letting $A$ be a set of quine atoms, let $A= L_{\omega+1} \cup P(\omega) $ [or one can let $A=V_\alpha$] of some transitive model $M$ of ZF, then build up a construction over $A$ along the above lines, i.e. iterate $A$ in a constructible manner up to some countable height so that $W_A \models ZF$. Now by the same argument we'd reach to the conclusion that $|P(\omega)| \neq \omega_1$, since $P(\omega)$ would be seen by $W_A$ to be not comparable to its Hartog number! The reason is because $P(\omega)$ is seen by $M$ to be uncountable, while each ordinal in $W_A$ would be seen by $M$ to be countable, so there is no injection in $W_A$ from $P(\omega)$ to its Hartog, while $\omega_1$ equals its Hartog is something provable in $W_A$, so $W_A$ doesn't satisfy the continuum hypothesis.
I realize that there must be something wrong in that line of thinking, otherwise this would mean that forcing is not needed to prove independence of CH and choice from ZF.
Forcing is totally irrelevant to the question of whether there is a countable level of $L$ satisfying $\mathsf{ZFC}$.
First, note that since the $L$-hierarchy is absolute and forcing adds no new ordinals, we have that forcing cannot change whether a model thinks there is a level of $L$ satisfying $\mathsf{ZFC}$: if $M[G]$ is a generic extension of $M$, then $$M\models\exists\alpha(L_\alpha\models\mathsf{ZFC})\quad\iff\quad M[G]\models\exists \alpha(L_\alpha\models\mathsf{ZFC}).$$
Next, we bring this down to the countable. Suppose $L_\alpha\models\mathsf{ZFC}$; applying downward Lowenheim-Skolem and then condensation, we get that there is some countable $\beta$ such that $L_\beta\models \mathsf{ZFC}$. So even though forcing can make uncountable things countable, it cannot affect the fact that the first level of $L$ satisfying $\mathsf{ZFC}$ - if such exists at all - is countable. Note moreover that this entire argument goes through in $\mathsf{ZFC}$ (or indeed vastly less).
(Relatedly, my quoted claim was a bit imprecise, albeit in a standard way: what we can show is that if $W_A$ exists at all then it has countable height and countable pure part. This is a genuine $\mathsf{ZFC}$ theorem, whereas what I wrote is an extension of $\mathsf{ZFC}$ - $\mathsf{ZFC}$ + "$\mathsf{ZFC}$ has transitive models of arbitrarily large cardinality" is enough.)
What about the putative $\mathsf{CH}$-related argument?
Well, the issue is that the result above simply doesn't apply to the situation you're considering. It's extremely limited to the specific "$L$-on-$A$" hierarchy defined above.
When we build the $L$-hierarchy on $A$ - in which context I'll write "$L_{\alpha,A}$" as opposed to "$L_\alpha^A$," since the latter clearly clashes with relativization notation (no idea what I was thinking originally) - it's crucial that there be no "structure" in the set of atoms $A$. From the perspective of each $L_{\alpha,A}$ (including $W_A$) the atoms are totally indistinguishable from each other: the subsets of $A$ in $L_{\alpha,A}$ are exactly the finite or cofinite ones, and (externally) every permutation of $A$ extends to a (unique) automorphism of $L_{\alpha,A}$. This means that we can't in any meaningful sense take $A$ to be $L_{\omega+1}\cup\mathcal{P}(\omega)$.
Of course this motivates an interesting question:
That is, how tall must a model of $\mathsf{ZF-Reg}$ "built on a copy of $\mathfrak{X}$" be? I don't know much about this specific question, but if we replace $\mathsf{ZF-Reg}$ with $\mathsf{KPU}$ we get a very well-trod topic in higher recursion theory - the canonical starting point for this is Barwise's wonderful (and freely-available!) book Admissible sets and structures.
Finally, given this question I should probably sketch the proof of my claim (granting the above-mentioned hypothesis) in the first place.
There are a couple ways to prove it, but in my opinion the "right" proof is via the following:
$(*)$ can be proved via Ehrenfeucht-Fraisse games. It implies my original claim as follows. Suppose $A$ is uncountable. Let $B$ be a countably infinite subset of $A$. By a downward Lowenheim-Skolem + collapsing argument, we have that $height(W_B)$ is countable. But by $(*)$ we have that $$L_{height(W_B), A}\models\mathsf{ZFC}.$$ So we have $height(W_A)\le height(W_B)<\omega_1$.
EDIT: if you prefer forcing to Ehrenfeucht-Fraisse games, here's another proof of $(*)$:
Consider a generic extension $V[G]$ of the universe in which both $A$ and $B$ are countable. In $V[G]$ we have $L_{\alpha,A}\cong L_{\alpha,B}$ (build an isomorphism between the two recursively from a bijection $A\rightarrow B$). A fortiori we have in $V[G]$ that $L_{\alpha,A}\equiv L_{\alpha,B}$. But first-order theories don't change under forcing, and so we get $L_{\alpha,A}\equiv L_{\alpha,B}$ in reality.
(This sort of trick can be used for all sorts of shenanigans. For example, one way to prove that every satisfiable $\mathcal{L}_{\omega_1,\omega}$-sentence $\varphi$ has a countable model is to collapse the cardinality of a given $\mathcal{M}\models\varphi$ to $\aleph_0$. We wind up with a generic extension satisfying the $\Sigma^1_1$ sentence "$\varphi$ has a countable model," so by Mostowski absoluteness $\varphi$ had a countable model in the ground universe already.)