[proofplan] We code the Cohen real as a function $f: \mathbb{N} \to \mathbb{N}$ by splitting the binary Cohen real into countably many infinite columns and letting $f(n)$ be the first place where the $n$-th column has value $1$. First we verify that this name is total in the generic extension. Then, for a fixed ground-model function $g$ and threshold $m$, we show that the conditions forcing some $n \geq m$ with $f(n) > g(n)$ form a dense set. Genericity meets these dense sets for every $m$, giving infinitely many failures of domination by $g$. [/proofplan]

[step:Define the Cohen real and decode it into a function on $\mathbb{N}$]Let $\langle \cdot,\cdot\rangle: \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be a fixed bijection in $M$. We view Cohen forcing $\mathbb{C}$ as the partially ordered set of finite partial functions $p: \mathbb{N} \rightharpoonup \{0,1\}$, ordered by extension: $q \leq p$ means $q \supseteq p$. Let $\dot c$ be the canonical $\mathbb{C}$-name for the generic binary sequence, and define its interpretation $c = \dot c^G$ in $M[G]$ as follows. For each $k \in \mathbb{N}$, let $H_k = \{p \in \mathbb{C} : k \in \operatorname{dom}(p)\}$. Given $p \in \mathbb{C}$, choose $i \in \{0,1\}$ and define $q = p \cup \{(k,i)\}$ if $k \notin \operatorname{dom}(p)$, while if $k \in \operatorname{dom}(p)$ set $q=p$. Then $q \leq p$ and $q \in H_k$, so $H_k$ is dense in $\mathbb{C}$. Since $H_k \in M$ and $G$ is $M$-generic, there is $p \in G \cap H_k$. Define $c: \mathbb{N} \to \{0,1\}$ by declaring $c(k)$ to be the unique value $i \in \{0,1\}$ such that some $p \in G$ satisfies $p(k)=i$. Existence follows from $G \cap H_k \neq \varnothing$, and uniqueness follows because any two conditions in the filter $G$ are compatible, so they cannot assign different values to the same coordinate. For each $n \in \mathbb{N}$, define the dense set \begin{align*} E_n = \{p \in \mathbb{C} : \text{there exists } k \in \mathbb{N} \text{ such that } p(\langle n,k\rangle)=1\}. \end{align*} Given $p \in \mathbb{C}$, choose $k \in \mathbb{N}$ such that $\langle n,k\rangle \notin \operatorname{dom}(p)$, which is possible because $\operatorname{dom}(p)$ is finite. Then $q = p \cup \{(\langle n,k\rangle,1)\}$ is a condition with $q \leq p$ and $q \in E_n$. Thus $E_n$ is dense in $\mathbb{C}$. Since $E_n \in M$ and $G$ is $M$-generic, $G \cap E_n \neq \varnothing$. Therefore, for each $n \in \mathbb{N}$, there exists $k \in \mathbb{N}$ with $c(\langle n,k\rangle)=1$. Let $\dot f$ be the $\mathbb{C}$-name for the decoded function obtained from $\dot c$, and let $f=\dot f^G$ be its interpretation in $M[G]$. Define $f: \mathbb{N} \to \mathbb{N}$ by \begin{align*} f(n) = \min\{k \in \mathbb{N} : c(\langle n,k\rangle)=1\}. \end{align*} The preceding paragraph proves that the set over which the minimum is taken is nonempty for every $n$, so $f$ is a total function in $M[G]$.[/step]

[guided]We need a function $f: \mathbb{N} \to \mathbb{N}$, but Cohen forcing directly adds a binary sequence. The fixed bijection $\langle \cdot,\cdot\rangle: \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ lets us regard the generic binary sequence as countably many columns: the $n$-th column is the sequence $k \mapsto c(\langle n,k\rangle)$. First we verify that the generic binary sequence is total. For each $k \in \mathbb{N}$, let $H_k = \{p \in \mathbb{C} : k \in \operatorname{dom}(p)\}$. Given any condition $p \in \mathbb{C}$, either $p$ already decides coordinate $k$, or we extend it by assigning one of the two values in $\{0,1\}$ to $k$. This gives an extension in $H_k$, so $H_k$ is dense. Since $H_k \in M$ and $G$ is $M$-generic, $G \cap H_k \neq \varnothing$. Thus each coordinate receives a value from some condition in $G$. The value is unique because two conditions in a filter are compatible, and compatible finite functions cannot assign different values to the same coordinate. Hence $c: \mathbb{N} \to \{0,1\}$ is well-defined in $M[G]$. Now we must ensure that every column contains a $1$, so that the first $1$ exists. Fix $n \in \mathbb{N}$ and define \begin{align*} E_n = \{p \in \mathbb{C} : \text{there exists } k \in \mathbb{N} \text{ such that } p(\langle n,k\rangle)=1\}. \end{align*} For any $p \in \mathbb{C}$, the set $\operatorname{dom}(p)$ is finite, while the set of coordinates $\{\langle n,k\rangle : k \in \mathbb{N}\}$ is infinite. Therefore we can choose $k \in \mathbb{N}$ with $\langle n,k\rangle \notin \operatorname{dom}(p)$ and extend $p$ by assigning value $1$ at that coordinate. This extension belongs to $E_n$, so $E_n$ is dense. Since $E_n \in M$ and $G$ is $M$-generic, some condition in $G$ belongs to $E_n$, and therefore $c(\langle n,k\rangle)=1$ for some $k$. Define $f: \mathbb{N} \to \mathbb{N}$ in $M[G]$ by \begin{align*} f(n) = \min\{k \in \mathbb{N} : c(\langle n,k\rangle)=1\}. \end{align*} The previous paragraph proves that the displayed set is nonempty for every $n \in \mathbb{N}$. Since every nonempty subset of $\mathbb{N}$ has a least element, $f(n)$ is defined for every $n$, so $f$ is total.[/guided]

[step:Show that every ground-model function fails to dominate the decoded real densely]Fix $g \in M \cap \mathbb{N}^{\mathbb{N}}$ and $m \in \mathbb{N}$. Define \begin{align*} D_{g,m} = \{p \in \mathbb{C} : p \Vdash \text{there exists } n \geq m \text{ such that } f(n) > g(n)\}. \end{align*} We prove that $D_{g,m}$ is dense in $\mathbb{C}$. Let $p \in \mathbb{C}$. Since $\operatorname{dom}(p)$ is finite and $\langle \cdot,\cdot\rangle$ is a bijection, there exists $n \geq m$ such that \begin{align*} \langle n,k\rangle \notin \operatorname{dom}(p) \quad \text{for every } k \leq g(n)+1. \end{align*} Define $q: \mathbb{N} \rightharpoonup \{0,1\}$ by extending $p$ as follows: \begin{align*} q = p \cup \{(\langle n,k\rangle,0) : k \leq g(n)\} \cup \{(\langle n,g(n)+1\rangle,1)\}. \end{align*} The choice of $n$ ensures that these new assignments do not conflict with $p$, so $q$ is a condition and $q \leq p$. The condition $q$ forces that the first $1$ in the $n$-th column occurs after every $k \leq g(n)$, and it also forces that there is a $1$ at $k=g(n)+1$. Hence \begin{align*} q \Vdash f(n)=g(n)+1. \end{align*} In particular, \begin{align*} q \Vdash f(n)>g(n). \end{align*} Since $n \geq m$, we have $q \in D_{g,m}$. Thus every $p \in \mathbb{C}$ has an extension in $D_{g,m}$, so $D_{g,m}$ is dense.[/step]

[guided]Fix a ground-model function $g: \mathbb{N} \to \mathbb{N}$ and a threshold $m \in \mathbb{N}$. Our goal is to force $f$ to beat $g$ somewhere beyond $m$. The important point is that a Cohen condition decides only finitely many bits, while there are infinitely many columns available. Define \begin{align*} D_{g,m} = \{p \in \mathbb{C} : p \Vdash \text{there exists } n \geq m \text{ such that } f(n) > g(n)\}. \end{align*} We prove density. Let $p \in \mathbb{C}$. Since $p$ is a finite partial function, $\operatorname{dom}(p)$ is finite. For each fixed $n$, the finitely many coordinates relevant to forcing $f(n)>g(n)$ are \begin{align*} \langle n,0\rangle,\langle n,1\rangle,\dots,\langle n,g(n)+1\rangle. \end{align*} Only finitely many columns can have any of these coordinates already mentioned by $p$. Therefore we may choose $n \geq m$ such that \begin{align*} \langle n,k\rangle \notin \operatorname{dom}(p) \quad \text{for every } k \leq g(n)+1. \end{align*} Now extend $p$ in the $n$-th column. We want the first $1$ in that column to occur after $g(n)$. To enforce this, define \begin{align*} q = p \cup \{(\langle n,k\rangle,0) : k \leq g(n)\} \cup \{(\langle n,g(n)+1\rangle,1)\}. \end{align*} The coordinates added to $p$ were chosen outside $\operatorname{dom}(p)$, so there is no conflict and $q$ is a finite partial function from $\mathbb{N}$ to $\{0,1\}$. Hence $q \in \mathbb{C}$, and $q \leq p$ because $q$ extends $p$. By construction, $q$ forces \begin{align*} c(\langle n,k\rangle)=0 \quad \text{for every } k \leq g(n) \end{align*} and also forces \begin{align*} c(\langle n,g(n)+1\rangle)=1. \end{align*} Since $f(n)$ is defined as the least $k$ with $c(\langle n,k\rangle)=1$, these forced values imply \begin{align*} q \Vdash f(n)=g(n)+1. \end{align*} Therefore \begin{align*} q \Vdash f(n)>g(n). \end{align*} Because $n \geq m$, this proves $q \in D_{g,m}$. We have shown that every condition $p$ has an extension in $D_{g,m}$, so $D_{g,m}$ is dense.[/guided]

[step:Use genericity and the forcing theorem to obtain infinitely many failures of domination]Let $g \in M \cap \mathbb{N}^{\mathbb{N}}$ be arbitrary. For each $m \in \mathbb{N}$, the name $\dot f$, the condition poset $\mathbb{C}$, and the parameters $g,m$ all belong to $M$. By the definability part of the [Forcing Theorem](/theorems/4290), the relation defining $D_{g,m}$ is definable in $M$ from these parameters; hence $D_{g,m} \in M$ by Separation in $M$. The previous step proves that $D_{g,m}$ is dense in $\mathbb{C}$. Since $G$ is $M$-generic, choose $p_m \in G \cap D_{g,m}$. By the definition of $D_{g,m}$, $p_m$ forces that there exists $n \geq m$ with $f(n)>g(n)$. Since $p_m \in G$, the soundness direction of the [Forcing Theorem](/theorems/4290) implies that the forced statement is true in $M[G]$. Thus, in $M[G]$, for every $m \in \mathbb{N}$ there exists $n \geq m$ such that \begin{align*} f(n)>g(n). \end{align*} This says exactly that $g$ does not eventually dominate $f$. Since $g \in M \cap \mathbb{N}^{\mathbb{N}}$ was arbitrary, no ground-model function eventually dominates $f$.[/step]

[guided]Fix an arbitrary ground-model function $g \in M \cap \mathbb{N}^{\mathbb{N}}$. We want to turn the density proved in the previous step into an actual statement about the generic extension. For each threshold $m \in \mathbb{N}$, the set $D_{g,m}$ was defined using only the parameters $g$, $m$, the forcing poset $\mathbb{C}$, and the name $\dot f$. These objects are all in $M$. The relevant forcing fact is the definability part of the [Forcing Theorem](/theorems/4290): for formulas with names and ground-model parameters, the forcing relation is definable over the ground model. Applying it to the formula "there exists $n \geq m$ such that $\dot f(n)>g(n)$" shows that $D_{g,m}$ is definable in $M$ from parameters in $M$. Therefore $D_{g,m} \in M$ by Separation in $M$. The previous step proves that $D_{g,m}$ is dense in $\mathbb{C}$. Since $G$ is $M$-generic, it meets every [dense subset](/page/Dense%20Subset) of $\mathbb{C}$ that belongs to $M$. Hence there is a condition $p_m \in G \cap D_{g,m}$. By the definition of $D_{g,m}$, this condition satisfies \begin{align*} p_m \Vdash \text{there exists } n \geq m \text{ such that } f(n)>g(n). \end{align*} Now we use the soundness direction of the [Forcing Theorem](/theorems/4290): if a condition in the generic filter forces a statement, then that statement holds in the generic extension. Since $p_m \in G$, it follows that in $M[G]$ there exists $n \geq m$ such that \begin{align*} f(n)>g(n). \end{align*} Because this argument works for every $m \in \mathbb{N}$, the inequalities $f(n)>g(n)$ occur arbitrarily far out. Therefore $g$ does not eventually dominate $f$. Since $g$ was an arbitrary member of $M \cap \mathbb{N}^{\mathbb{N}}$, no ground-model function eventually dominates the decoded Cohen real.[/guided]