Solution (source code)

= Solution

Let $M$ be an externally <countable> model of <ZFC>, and let $\kappa=(\omega_1)^M$. In $M$ form the forcing order
$$
\mathbb P=\{p:p\text{ is a finite partial function }\omega\longrightarrow\kappa\},\qquad q\le p\iff q\supseteq p.
$$
This is the <finite-function collapse to countable size>. For every $n\in\omega^M$ and $\alpha\in\kappa^M$, the internal <sets>
$$
D_n=\{p:n\in\operatorname{dom}(p)\},\qquad E_\alpha=\{p:\alpha\in\operatorname{ran}(p)\}
$$
are dense: extend a finite <function> by assigning a missing input, and use a fresh input to put any required value in its range.

Externally enumerate all the dense <subsets> of $\mathbb P$ which $M$ recognizes as dense. There are only countably many, because $M$ is <countable>. Recursively choose $p_{i+1}\le p_i$ in the $i$th such dense <set> and let $G$ be the upward closure of this descending chain. This produces a <generic filter> over $M$. By the <forcing theorem>, its <generic extension> $M[G]$ satisfies <ZFC>. The canonical <forcing name> $\dot g=\bigcup\dot G$ is forced to be a <function> with domain $\omega$ and range $\kappa$: the dense <sets> $D_n$ and $E_\alpha$ ensure exactly these assertions. Therefore
$$
\boxed{M[G]\models\text{“the old }\omega_1\text{ is countable.”}}
$$
Its new first <uncountable> <ordinal> is accordingly different from $\kappa$.

For a transitive $M$, ordinary evaluation of names gives the familiar literal extension. The question only assumes a <countable> model, so one must also cover externally ill-founded models. In that case use the quotient of the internally defined <forcing names> by forced equality modulo $G$, with membership defined by forced membership. The internal forcing identities and the forcing theorem hold in $M$ and give a well-defined <first-order structure> satisfying every standard <ZFC> axiom. Check names embed the original membership structure, so identify their images with $M$. Its domain is a quotient of a <subset> of the <countable> domain of $M$, hence is externally <countable>. Thus \b[the required extension exists even without assuming transitivity.] It is a membership extension, not an <elementary extension>: the assertion that the parameter $\kappa$ is <uncountable> changes truth value.