[proofplan] We prove the stronger fact that a countably closed forcing adds no new $\omega$-sequences of ground-model ordinals below $\omega_1^V$. Given a name for a function $\omega \to \omega_1^V$, we recursively build a descending sequence of conditions deciding one value at a time. Countable closure gives a single condition below the whole sequence, and that condition decides the entire function as a ground-model sequence. Finally, every countable ground-model subset of $\omega_1^V$ is bounded below $\omega_1^V$, so no such function can be cofinal. [/proofplan] [step:Decide each value of a name by a descending sequence of conditions] Let $\dot f$ be a $P$-name and let $p_0 \in P$ be a condition such that $p_0 \Vdash \dot f : \check{\omega} \to \check{\omega}_1^V$. We construct, by recursion on $n \in \omega$, a descending sequence $(p_n)_{n \in \omega}$ in $P$ and a sequence $(\alpha_n)_{n \in \omega}$ in $\omega_1^V$ such that $p_{n+1} \leq p_n$ and $p_{n+1} \Vdash \dot f(\check n) = \check \alpha_n$. Assume $p_n$ has been chosen. Since $p_n$ forces that $\dot f(\check n)$ is an ordinal below $\check{\omega}_1^V$, the standard forcing decision lemma says that the set of conditions below $p_n$ deciding the value of $\dot f(\check n)$ is dense below $p_n$. Hence there exist $p_{n+1} \leq p_n$ and $\alpha_n \in \omega_1^V$ such that $p_{n+1} \Vdash \dot f(\check n) = \check \alpha_n$. This completes the recursion. [guided] We want to turn the name $\dot f$ into an actual ground-model sequence. The obstacle is that a condition $p_0$ may force only that $\dot f$ is a function from $\omega$ to $\omega_1^V$, without deciding any particular value. The standard forcing move is therefore to strengthen the condition one coordinate at a time. Let $n \in \omega$ and suppose $p_n \in P$ has already been chosen. Since $p_n \Vdash \dot f : \check{\omega} \to \check{\omega}_1^V$, the condition $p_n$ forces that $\dot f(\check n)$ is some ordinal below $\check{\omega}_1^V$. By the standard forcing decision lemma, equivalently by the definition of the forcing relation for names, the conditions below $p_n$ that decide the value of $\dot f(\check n)$ are dense below $p_n$: otherwise there would be a stronger condition below which no ordinal value is forced, contradicting that $\dot f(\check n)$ is forced to be an element of $\check{\omega}_1^V$. Therefore we may choose a stronger condition $p_{n+1} \leq p_n$ and an ordinal $\alpha_n \in \omega_1^V$ such that $p_{n+1} \Vdash \dot f(\check n) = \check \alpha_n$. Repeating this for every $n \in \omega$ gives a descending sequence $(p_n)_{n \in \omega}$ in $P$ and a ground-model sequence $(\alpha_n)_{n \in \omega}$ of ordinals below $\omega_1^V$. The point of using countable closure later is that we will not have to stop after finitely many decisions: one condition will lie below all the $p_n$ at once. [/guided] [/step] [step:Use countable closure to decide the entire function] By countable closure, the descending sequence $(p_n)_{n \in \omega}$ has a lower bound $q \in P$ such that $q \leq p_n$ for every $n \in \omega$. Define the ground-model function $g : \omega \to \omega_1^V$ by setting $g(n) := \alpha_n$ for each $n \in \omega$. For each $n \in \omega$, since $q \leq p_{n+1}$ and $p_{n+1} \Vdash \dot f(\check n) = \check \alpha_n$, monotonicity of forcing gives $q \Vdash \dot f(\check n) = \check g(\check n)$. Also $q \leq p_0$, so $q$ forces that $\dot f$ is a function with domain $\check\omega$; the check name $\check g$ is forced to be the ground-model function with the same domain. The forcing semantics for bounded universal quantification over the check name $\check\omega$ applies here: because every element of $\check\omega$ is forced to be equal to some $\check n$ with $n \in \omega$, and because $q$ forces $\dot f(\check n)=\check g(\check n)$ for each ground-model $n$, the same condition $q$ forces $\forall m \in \check\omega\, (\dot f(m)=\check g(m))$. By extensionality of functions, it follows that $q \Vdash \dot f = \check g$. Thus below every condition forcing that $\dot f$ is a function $\omega \to \omega_1^V$, there is a stronger condition forcing that $\dot f$ is equal to a ground-model function. [/step] [step:Bound every ground-model countable subset of $\omega_1^V$] Since $g : \omega \to \omega_1^V$ belongs to the ground model, its range $A := g[\omega]$ is a countable subset of $\omega_1^V$ in the ground model. By the definition of $\omega_1^V$ as the first uncountable ordinal of $V$, the supremum $\beta := \sup A$ is an ordinal below $\omega_1^V$. Therefore $q \Vdash \operatorname{range}(\dot f) \subseteq \check \beta + 1$. In particular, $q$ forces that $\dot f$ is not cofinal in $\check{\omega}_1^V$. [/step] [step:Conclude that $\omega_1$ is preserved] Suppose toward a contradiction that some condition $p \in P$ forces that $\check{\omega}_1^V$ is countable in the forcing extension. By the [forcing theorem](/theorems/6531) and the truth lemma for names, this means that there is a $P$-name $\dot f$ such that $p \Vdash \dot f : \check{\omega} \to \check{\omega}_1^V$ and $p \Vdash \dot f \text{ is cofinal in } \check{\omega}_1^V$. Applying the preceding construction below $p$, we obtain a stronger condition $q \leq p$ and a ground-model function $g : \omega \to \omega_1^V$ such that $q \Vdash \dot f = \check g$. But the range of $g$ is bounded in $\omega_1^V$, so the previous step gives $q \Vdash \dot f \text{ is not cofinal in } \check{\omega}_1^V$. This contradicts $q \leq p$ and the fact that stronger conditions preserve forced statements. Hence no condition forces a countable cofinal sequence in $\omega_1^V$. Therefore $\omega_1^V$ remains uncountable in every $P$-generic extension. Forcing does not add new ordinals, and every ordinal $\gamma < \omega_1^V$ is countable in $V$ and remains countable in the extension because its ground-model bijection with $\omega$ is still present. Hence no ordinal below $\omega_1^V$ can become the first uncountable ordinal of the extension, while $\omega_1^V$ itself is still uncountable there. It follows that $\omega_1^{V[G]} = \omega_1^V$. Thus countably closed forcing preserves $\omega_1$. [/step]