[proofplan] We represent the alleged new function by a forcing name and work below a condition forcing that the name is an $\omega$-sequence of ground-model ordinals. For each natural number, we strengthen the current condition so that it decides the corresponding value of the name. Countable closure gives a single lower bound for the whole descending sequence, and this lower bound forces the name to equal the ground-model sequence of decided ordinals. [/proofplan] [step:Choose a name and a condition forcing it to be an ordinal sequence] Let $f: \omega \to \operatorname{Ord}^V$ be an element of $V[G]$. Choose a $P$-name $\dot{f} \in V$ such that $\dot{f}^G = f$. Since $f$ is a function from $\omega$ to $\operatorname{Ord}^V$ in $V[G]$, choose a condition $p \in G$ such that \begin{align*} p \Vdash \dot{f}: \check{\omega} \to \operatorname{Ord}^V. \end{align*} Here the displayed forcing assertion is shorthand for the following first-order assertion: $p$ forces that $\dot{f}$ is a function with domain $\check{\omega}$ and that, for every $n \in \omega$, the value $\dot{f}(\check{n})$ is equal to $\check{\alpha}$ for some ordinal $\alpha \in \operatorname{Ord}^V$. It is enough to show that the set of conditions below $p$ which force $\dot{f}$ to be equal to a sequence belonging to $V$ is dense below $p$. [guided] We begin by replacing the object $f \in V[G]$ with a name from the ground model. By definition of the forcing extension, there is a $P$-name $\dot{f} \in V$ whose interpretation by the generic filter $G$ is the function $f$, so $\dot{f}^G = f$. The statement that $f$ is a function from $\omega$ into the ground-model ordinals is true in the extension. Therefore we may strengthen inside the generic filter and choose a condition $p \in G$ deciding this structural fact: \begin{align*} p \Vdash \dot{f}: \check{\omega} \to \operatorname{Ord}^V. \end{align*} This is shorthand for the assertion that $p$ forces $\dot{f}$ to have domain $\check{\omega}$ and that every value $\dot{f}(\check{n})$ is equal to $\check{\alpha}$ for some ordinal $\alpha \in \operatorname{Ord}^V$. The key point is that it is not enough merely to build one stronger condition below $p$: that stronger condition need not belong to the original generic filter $G$. Instead, we prove a density statement below $p$. Fix an arbitrary condition $r \leq p$. Starting with $p_0 := r$, we recursively choose, for each $n \in \omega$, a condition $p_{n+1} \leq p_n$ and an ordinal $\alpha_n \in \operatorname{Ord}^V$ such that \begin{align*} p_{n+1} \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} The existence of such a strengthening follows directly from the forcing semantics: since $p_n \leq p$, the condition $p_n$ forces that $\dot{f}(\check{n})$ is a ground-model ordinal, so there must be some extension of $p_n$ and some ordinal $\alpha_n \in V$ deciding this value. Countable closure of $P$ then gives a single lower bound $q \in P$ with $q \leq p_n$ for every $n \in \omega$. By the definition of forcing under stronger conditions, every assertion forced by $p_{n+1}$ is also forced by $q$, so $q$ decides all coordinates of $\dot{f}$ at once. The sequence $a: \omega \to \operatorname{Ord}^V$ defined by $a(n) = \alpha_n$ belongs to $V$, and $q \Vdash \dot{f} = \check{a}$. Thus below every $r \leq p$ there is a stronger condition forcing $\dot{f}$ to equal a ground-model sequence. This density statement is what will allow the original generic filter $G$ to contain a deciding condition. [/guided] [/step] [step:Build a descending sequence deciding one value at a time below an arbitrary stronger condition] Let $r \in P$ be an arbitrary condition with $r \leq p$. We recursively define a sequence $(p_n)_{n \in \omega}$ of conditions in $P$ and a sequence $(\alpha_n)_{n \in \omega}$ of ordinals in $V$ such that $p_0 = r$ and, for every $n \in \omega$, \begin{align*} p_{n+1} \leq p_n \end{align*} and \begin{align*} p_{n+1} \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} Set $p_0 := r$. Suppose $p_n$ has been defined. Since $p_n \leq p$ and $p \Vdash \dot{f}: \check{\omega} \to \operatorname{Ord}^V$, we have \begin{align*} p_n \Vdash \dot{f}(\check{n}) \in \operatorname{Ord}^V. \end{align*} We use the following standard consequence of the forcing relation, proved directly from its definition in this instance: if no extension of $p_n$ decided the value of $\dot{f}(\check{n})$, then $p_n$ could not force that this value is some ground-model ordinal. Therefore there are a condition $p_{n+1} \leq p_n$ and an ordinal $\alpha_n \in \operatorname{Ord}^V$ such that \begin{align*} p_{n+1} \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} This completes the recursion in $V$. [/step] [step:Use countable closure to obtain one lower bound] The sequence $(p_n)_{n \in \omega}$ is a descending $\omega$-sequence of conditions in $P$ and belongs to $V$. Since $P$ is countably closed in $V$, there exists a condition $q \in P$ such that \begin{align*} q \leq p_n \end{align*} for every $n \in \omega$. For each $n \in \omega$, the condition $q$ is stronger than $p_{n+1}$. By the order-preservation built into the forcing relation, every statement forced by $p_{n+1}$ is also forced by $q$. Hence \begin{align*} q \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} [/step] [step:Assemble the decided values into a ground-model sequence] Define the function $a: \omega \to \operatorname{Ord}^V$ by the rule, for every $n \in \omega$, \begin{align*} a(n) = \alpha_n. \end{align*} The recursion producing $(\alpha_n)_{n \in \omega}$ was carried out in $V$, so $a \in V$. We claim that \begin{align*} q \Vdash \dot{f} = \check{a}. \end{align*} Indeed, $q \leq p$, so \begin{align*} q \Vdash \dot{f}: \check{\omega} \to \operatorname{Ord}^V. \end{align*} Also, for every $n \in \omega$, \begin{align*} q \Vdash \dot{f}(\check{n}) = \check{\alpha}_n = \check{a}(\check{n}). \end{align*} Thus $q$ forces that the two functions $\dot{f}$ and $\check{a}$ have the same domain $\check{\omega}$ and agree at every element of that domain. Therefore \begin{align*} q \Vdash \dot{f} = \check{a}. \end{align*} [/step] [step:Use genericity to meet the dense set of deciding conditions] Define the set \begin{align*} D = \{s \in P : s \leq p \text{ and there exists } b \in V \text{ with } b: \omega \to \operatorname{Ord}^V \text{ and } s \Vdash \dot{f} = \check{b}\}. \end{align*} The preceding construction started with an arbitrary $r \leq p$ and produced $q \leq r$ together with $a \in V$ such that $a: \omega \to \operatorname{Ord}^V$ and $q \Vdash \dot{f} = \check{a}$. Hence $D$ is dense below $p$. The set $D$ is defined in $V$ from $P$, $p$, and $\dot{f}$. To use ordinary $V$-genericity over $P$, define \begin{align*} E = D \cup \{t \in P : t \text{ is incompatible with } p\}. \end{align*} The density of $D$ below $p$ implies that $E$ is dense in $P$: if $t \in P$ is incompatible with $p$, then $t \in E$, while if $t$ is compatible with $p$, choose $u \leq t,p$ and then choose $s \leq u$ with $s \in D$. Since $E \in V$ and $G$ is $V$-generic, choose $s \in G \cap E$. Because $p \in G$ and $G$ is a filter, no condition in $G$ is incompatible with $p$; hence $s \in D$. By the definition of $D$, there is a function $b \in V$ with $b: \omega \to \operatorname{Ord}^V$ and \begin{align*} s \Vdash \dot{f} = \check{b}. \end{align*} The meaning of $s \Vdash \dot{f} = \check{b}$ is that every generic filter containing $s$ interprets the two names equally. Since $s \in G$, we get \begin{align*} \dot{f}^G = b. \end{align*} Since $\dot{f}^G = f$, we have $f = b$. Because $b \in V$, it follows that $f \in V$. [guided] The lower bound produced by countable closure need not itself lie in the original generic filter $G$. This is why the construction must be converted into a dense-set argument. Define \begin{align*} D = \{s \in P : s \leq p \text{ and there exists } b \in V \text{ with } b: \omega \to \operatorname{Ord}^V \text{ and } s \Vdash \dot{f} = \check{b}\}. \end{align*} We now verify density below $p$ in full. Let $r \leq p$ be arbitrary. Set $p_0 := r$. Suppose $p_n$ has been constructed. Since $p_n \leq p$ and $p$ forces that $\dot{f}$ is a function from $\check{\omega}$ to the ground-model ordinals, the condition $p_n$ forces that $\dot{f}(\check{n})$ is some ground-model ordinal. By the definition of the forcing relation, there are an extension $p_{n+1} \leq p_n$ and an ordinal $\alpha_n \in \operatorname{Ord}^V$ such that \begin{align*} p_{n+1} \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} Carrying this out for all $n \in \omega$ gives a descending sequence $(p_n)_{n \in \omega}$ in $V$ and a sequence $(\alpha_n)_{n \in \omega}$ of ordinals in $V$. Now countable closure is used at exactly one point. Since $P$ is countably closed and $(p_n)_{n \in \omega}$ is a descending $\omega$-sequence of conditions, there is $q \in P$ such that $q \leq p_n$ for every $n \in \omega$. For each $n$, the condition $q$ is stronger than $p_{n+1}$, so the order-preservation of forcing gives \begin{align*} q \Vdash \dot{f}(\check{n}) = \check{\alpha}_n. \end{align*} Define $a: \omega \to \operatorname{Ord}^V$ in $V$ by $a(n) = \alpha_n$ for each $n \in \omega$. Since $q \leq p$, the condition $q$ still forces that $\dot{f}$ has domain $\check{\omega}$. It also forces agreement with $\check{a}$ at each input $\check{n}$. Therefore \begin{align*} q \Vdash \dot{f} = \check{a}. \end{align*} Thus $q \in D$ and $q \leq r$, proving that $D$ is dense below $p$. To pass from density below $p$ to the actual generic filter, define \begin{align*} E = D \cup \{t \in P : t \text{ is incompatible with } p\}. \end{align*} The set $E$ belongs to $V$ and is dense in $P$: a condition incompatible with $p$ is already in $E$, while a condition compatible with $p$ has a common extension with $p$, and then the density of $D$ below $p$ gives a further extension in $D$. Since $G$ is $V$-generic, choose $s \in G \cap E$. Because $p \in G$ and $G$ is a filter, $s$ cannot be incompatible with $p$; hence $s \in D$. By the definition of $D$, there is a ground-model function $b: \omega \to \operatorname{Ord}^V$ such that \begin{align*} s \Vdash \dot{f} = \check{b}. \end{align*} The assertion $s \Vdash \dot{f} = \check{b}$ means that every generic filter containing $s$ interprets the two names equally. Since $s \in G$, it follows that \begin{align*} \dot{f}^G = b. \end{align*} But $\dot{f}^G = f$, so $f = b$. Since $b \in V$, the function $f$ belongs to $V$. [/guided] Since $f: \omega \to \operatorname{Ord}^V$ was arbitrary in $V[G]$, every countable sequence of ground-model ordinals in $V[G]$ already belongs to $V$. [/step]