[proofplan] We prove the statement by showing that every name for a short ordinal-valued function is decided coordinate-by-coordinate by a single strengthening. For each coordinate $\alpha < \lambda$, we form a dense [open set](/page/Open%20Set) of conditions that either avoid the original condition or decide the value of the name at $\alpha$. The $\kappa$-distributivity of $\mathbb{P}$ lets us meet all these dense open sets at once, because there are only $\lambda < \kappa$ many of them. The resulting condition decides the entire function as a ground-model function, and genericity then identifies the interpreted function with that ground-model object. [/proofplan] [step:Choose a name and a condition forcing the function statement] Let $\dot f \in V$ be a $\mathbb{P}$-name and let $p \in \mathbb{P}$ be a condition such that $p \Vdash_{\mathbb{P}} ``\dot f: \check{\lambda} \to \operatorname{Ord}^V"$. We use the forcing convention that $q \le p$ means that $q$ is stronger than $p$. It is enough to prove that there are $q \le p$ and $g \in V$ such that $q \Vdash_{\mathbb{P}} \dot f = \check g$. Indeed, if $f \in V[G]$ is any function $f: \lambda \to \operatorname{Ord}^V$, then $f = \dot f^G$ for some $\mathbb{P}$-name $\dot f \in V$, and since $G$ is a filter containing some condition forcing the displayed statement, the conclusion will give $f = g \in V$. [/step] [step:Build dense open sets deciding each coordinate] For each ordinal $\alpha < \lambda$, define $D_\alpha \subset \mathbb{P}$ by declaring that $r \in D_\alpha$ iff either $r$ is incompatible with $p$, or else $r \le p$ and there is an ordinal $\beta \in \operatorname{Ord}^V$ such that $r \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta}$. Each $D_\alpha$ belongs to $V$, since $p$, $\dot f$, and $\alpha$ belong to $V$, and the forcing relation for set forcing is definable in $V$. We verify that $D_\alpha$ is dense. Let $s \in \mathbb{P}$. If $s$ is incompatible with $p$, then $s \in D_\alpha$. If $s$ is compatible with $p$, choose $t \le s,p$. Since $p \Vdash_{\mathbb{P}} ``\dot f(\check{\alpha}) \in \operatorname{Ord}^V"$, also $t \Vdash_{\mathbb{P}} ``\dot f(\check{\alpha}) \in \operatorname{Ord}^V"$ by monotonicity of forcing. The [forcing theorem](/theorems/6531) gives the density below $t$ of conditions deciding the set-valued name $\dot f(\check{\alpha})$; choose $u \le t$ deciding it. Since $t$ forces that the value is an ordinal of $V$, there is $\beta \in \operatorname{Ord}^V$ such that $u \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta}$. Then $u \le p$ and $u \le s$, so $u \in D_\alpha$. The set $D_\alpha$ is open downward. If $r \in D_\alpha$ and $u \le r$, then either $r$ is incompatible with $p$, in which case $u$ is incompatible with $p$, or $r \le p$ decides $\dot f(\check{\alpha})$, in which case $u \le r$ decides the same value. Therefore each $D_\alpha$ is dense open. [guided] The goal of this step is to manufacture one dense open set for each coordinate of the function. Fix $\alpha < \lambda$. We define $D_\alpha \subset \mathbb{P}$ so that a condition belongs to $D_\alpha$ precisely when it is harmless for the coordinate $\alpha$: either it cannot appear below $p$, because it is incompatible with $p$, or it is already below $p$ and decides the value of $\dot f(\check{\alpha})$. Formally, $r \in D_\alpha$ means that either $r \perp p$, or there exists an ordinal $\beta \in \operatorname{Ord}^V$ such that $r \le p$ and $r \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta}$. This set is an element of $V$ because all parameters used in its definition are in $V$, and the forcing relation for set forcing is definable in $V$. We now prove density. Let $s \in \mathbb{P}$. If $s$ is incompatible with $p$, then $s \in D_\alpha$ by the first clause of the definition. Suppose instead that $s$ is compatible with $p$. Then there is a common strengthening $t \le s,p$. Since $p$ forces that $\dot f$ maps $\lambda$ into $\operatorname{Ord}^V$, the stronger condition $t$ also forces that $\dot f(\check{\alpha})$ is an ordinal of $V$. The forcing theorem gives the density below any condition of conditions deciding a set-valued name. Applying this to the name $\dot f(\check{\alpha})$ below $t$, choose $u \le t$ that decides its value. Since $t$ already forces that this value is an ordinal of $V$, the decided value is some $\beta \in \operatorname{Ord}^V$, so $u \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta}$. Because $u \le t \le p$ and $u \le t \le s$, this $u$ lies in $D_\alpha$ and strengthens $s$. Hence $D_\alpha$ is dense. Finally, $D_\alpha$ is open downward. If $r \in D_\alpha$ and $u \le r$, then incompatibility with $p$ is preserved by strengthening, and a statement forced by $r$ is also forced by every stronger condition $u$. Therefore $u \in D_\alpha$. This proves that $D_\alpha$ is dense open. [/guided] [/step] [step:Use $\kappa$-distributivity to decide all coordinates at once] The family $(D_\alpha)_{\alpha < \lambda}$ has length $\lambda < \kappa$, and every $D_\alpha$ is dense open in $\mathbb{P}$. Since $\mathbb{P}$ is $\kappa$-distributive, the intersection $D := \bigcap_{\alpha < \lambda} D_\alpha$ is dense in $\mathbb{P}$. Applying density below $p$, choose $q \le p$ with $q \in D$. For every $\alpha < \lambda$, we have $q \in D_\alpha$. Since $q \le p$, the condition $q$ is compatible with $p$, so the incompatible-with-$p$ clause in the definition of $D_\alpha$ cannot hold. Therefore, for every $\alpha < \lambda$, there is an ordinal $\beta_\alpha \in \operatorname{Ord}^V$ such that $q \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta_\alpha}$. [/step] [step:Assemble the decided coordinates into a ground-model function] Define $g: \lambda \to \operatorname{Ord}^V$ in $V$ by $g(\alpha) = \beta_\alpha$ for each $\alpha < \lambda$, where $\beta_\alpha$ is the unique ordinal satisfying $q \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta_\alpha}$. Uniqueness follows because no condition can force one name to be equal to two distinct ordinal check-names. The function $g$ belongs to $V$ by Replacement in $V$, applied to the definable relation $q \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{\beta}$. We claim that $q \Vdash_{\mathbb{P}} \dot f = \check g$. Indeed, $q$ forces that both $\dot f$ and $\check g$ are functions with domain $\check{\lambda}$. For each $\alpha < \lambda$, the definition of $g$ gives $q \Vdash_{\mathbb{P}} \dot f(\check{\alpha}) = \check{g(\alpha)}$. By extensionality for functions, $q$ forces equality of the two functions: $q \Vdash_{\mathbb{P}} \dot f = \check g$. [/step] [step:Conclude that the generic interpretation lies in the ground model] Let $G \subset \mathbb{P}$ be $V$-generic and suppose $f \in V[G]$ is a function $f: \lambda \to \operatorname{Ord}^V$. Choose a $\mathbb{P}$-name $\dot f \in V$ with $\dot f^G = f$ and choose $p \in G$ such that $p \Vdash_{\mathbb{P}} ``\dot f: \check{\lambda} \to \operatorname{Ord}^V"$. Let $D := \bigcap_{\alpha < \lambda} D_\alpha$, the dense open set constructed above. Since $D \in V$ is dense and $G$ is $V$-generic, choose $r \in G \cap D$. Since $p,r \in G$ and $G$ is a filter, choose $q \in G$ with $q \le p$ and $q \le r$. Since $D$ is open downward and $r \in D$, we have $q \in D$. The preceding coordinate-decision argument applied to this $q$ gives a function $g \in V$ such that $q \Vdash_{\mathbb{P}} \dot f = \check g$. Therefore $f = \dot f^G = \check g^G = g$. Thus $f \in V$. Since $\lambda < \kappa$ and $f$ were arbitrary, $\mathbb{P}$ adds no new ordinal-valued sequences of length less than $\kappa$. [/step]