= Solution
Let $\alpha=(\omega_1)^M$ and take
$$
\varphi_1(\alpha)\equiv\text{“there exists a function }f\text{ with }\operatorname{dom}f=\omega\text{ and }\operatorname{ran}f=\alpha\text{.”}
$$
This formula is <upward absolute formula>[upward absolute] between transitive models: if the smaller model contains such an $f$, the assumed absoluteness of “function”, domain, range, and $\omega$ shows that the same witness works in the larger model.
The generic union $g=\bigcup G$ is a total map $\omega\to\alpha$, because the conditions deciding each input form a dense set. For every $\beta<\alpha$, the conditions putting $\beta$ somewhere in the range are also dense, so $g$ is surjective. Thus $M[G]\models\varphi_1(\alpha)$. But $M\not\models\varphi_1(\alpha)$ because $M$ regards $\alpha$ as its first uncountable ordinal. Hence $\varphi_1$ is not downward absolute between $M$ and $M[G]$.
Back to article page
