[proofplan] We prove that every ground-model real $a\subset \omega$ differs from the generic Cohen real by meeting a dense set tailored to $a$. For a fixed $a\in M\cap\mathcal P(\omega)$, we define a dense set $D_a\in M$ of conditions that decide some fresh coordinate opposite to $a$. Since $G$ is $M$-generic, it meets $D_a$, and the condition in the intersection forces the corresponding coordinate of $c=\bigcup G$ to disagree with $a$. Applying this to a hypothetical $a=c\in M$ gives a contradiction. [/proofplan] [step:Define the dense set that makes the generic real disagree with a fixed ground-model real] Let $\mathbb P:=\operatorname{Add}(\omega,1)^M$ denote the Cohen forcing poset in $M$, ordered by reverse inclusion of finite partial functions from $\omega$ to $2$. Let $\mathcal P(\omega)$ denote the power set of $\omega$. For every subset $a\subset \omega$, let $\mathbb{1}_a:\omega\to 2$ denote its indicator function, so $\mathbb{1}_a(n)=1$ exactly when $n\in a$. Fix $a\in M$ with $a\subset \omega$. Define $D_a:=\{p\in \mathbb P:\text{ there exists }n\in \operatorname{dom}(p)\text{ such that }p(n)=1\iff n\notin a\}$. Thus a condition $p\in D_a$ explicitly assigns at least one coordinate $n$ the value opposite to the indicator function of $a$. Because $a\in M$, $\mathbb P\in M$, and the formula defining $D_a$ uses only the parameters $a$ and $\mathbb P$, the Separation axiom inside $M$ gives $D_a\in M$. [guided] Let $\mathbb P:=\operatorname{Add}(\omega,1)^M$ be the Cohen forcing poset in $M$, ordered by reverse inclusion of finite partial functions from $\omega$ to $2$. Let $\mathcal P(\omega)$ denote the power set of $\omega$. We identify a subset $a\subset \omega$ with its indicator function $\mathbb{1}_a:\omega\to 2$, where $\mathbb{1}_a(n)=1$ exactly when $n\in a$. Thus saying that the Cohen real disagrees with $a$ means that it disagrees with $\mathbb{1}_a$ at some coordinate. Fix a ground-model real $a\in M$ with $a\subset \omega$. We want a dense set of Cohen conditions whose only purpose is to guarantee disagreement with $\chi_a$ somewhere. Since a Cohen condition is a finite partial function $p:\omega\to 2$, it can decide finitely many bits of the eventual generic real. We define $D_a:=\{p\in \mathbb P:\text{ there exists }n\in \operatorname{dom}(p)\text{ such that }p(n)=1\iff n\notin a\}$. The condition $p(n)=1\iff n\notin a$ says exactly that the bit assigned by $p$ at $n$ is the opposite of the membership value of $n$ in $a$: if $n\in a$, then $p(n)=0$, and if $n\notin a$, then $p(n)=1$. We also need this dense set to be one that the generic filter is required to meet. That requires $D_a\in M$. Since $a\in M$ and $\mathbb P\in M$, and since $D_a$ is the subset of $\mathbb P$ defined by a first-order formula with parameter $a$, the Separation axiom in $M$ yields $D_a\in M$. [/guided] [/step] [step:Extend every condition to one in the dense set] Let $q\in \mathbb P$. Since $\operatorname{dom}(q)$ is finite and $\omega$ is infinite, choose $n\in \omega\setminus \operatorname{dom}(q)$. Define a condition $p:\omega\rightharpoonup 2$ by setting $\operatorname{dom}(p)=\operatorname{dom}(q)\cup\{n\}$, by setting $p(k)=q(k)$ for every $k\in \operatorname{dom}(q)$, and by setting $p(n)=1$ iff $n\notin a$. Since $q\in\mathbb P=\operatorname{Add}(\omega,1)^M$, we have $q\in M$. The natural number $n$ belongs to $M$ because $M$ is transitive and contains $\omega$, and the finite function $p$ is definable in $M$ from the parameters $q$, $a$, and $n$. Hence $p\in M$. Also $p$ is a finite partial function from $\omega$ to $2$, so $p\in\mathbb P$. Since the order on $\mathbb P$ is reverse inclusion, $p\le q$, and $p\in D_a$ by the choice of the value at $n$. Hence $D_a$ is dense in $\mathbb P$. [/step] [step:Use genericity to force disagreement with the fixed ground-model real] Since $D_a\in M$ is dense in $\mathbb P$ and $G$ is $M$-generic, choose $p\in G\cap D_a$. By the definition of $D_a$, choose $n\in \operatorname{dom}(p)$ such that $p(n)=1\iff n\notin a$. Because $c=\bigcup G$ and $p\in G$, the value of $c$ at $n$ is the value already assigned by $p$, so $c(n)=p(n)$. Therefore $c(n)=1\iff n\notin a$. Equivalently, $c$ disagrees with the indicator function $\mathbb{1}_a$ at the coordinate $n$. Hence $c\ne \mathbb{1}_a$ as functions from $\omega$ to $2$, and therefore the subset coded by $c$ is not equal to $a$. [guided] Now we use the defining property of an $M$-generic filter. We have proved that $D_a$ is dense in $\mathbb P$, and we have also proved that $D_a\in M$. Since $G$ is $M$-generic, it meets every [dense subset](/page/Dense%20Subset) of $\mathbb P$ that belongs to $M$. Therefore there is a condition $p\in G\cap D_a$. Because $p\in D_a$, there is some coordinate $n\in \operatorname{dom}(p)$ such that $p(n)=1\iff n\notin a$. The Cohen real is $c=\bigcup G$. Since $G$ is a filter, its conditions are pairwise compatible, so the union $\bigcup G$ is a well-defined function. In particular, any bit assigned by a condition in $G$ is inherited by $c$. Since $p\in G$ and $n\in\operatorname{dom}(p)$, we get $c(n)=p(n)$. Combining this with $p(n)=1\iff n\notin a$ gives $c(n)=1\iff n\notin a$. Thus $c$ and $\mathbb{1}_a$ disagree at the coordinate $n$: if $n\in a$, then $c(n)=0=1-\mathbb{1}_a(n)$, while if $n\notin a$, then $c(n)=1=1-\mathbb{1}_a(n)$. Hence $c\ne \mathbb{1}_a$ as functions from $\omega$ to $2$, and the subset coded by $c$ is not equal to $a$. [/guided] [/step] [step:Apply the disagreement argument to rule out membership in the ground model] The preceding step proves that for every $a\in M$ with $a\subset\omega$, the function $c$ differs from the indicator function $\mathbb{1}_a$. Suppose, for contradiction, that $c\in M$. Since $c:\omega\to 2$, define the associated subset $a_c:=\{n\in\omega:c(n)=1\}$ of $\omega$. The set $a_c$ belongs to $M$ by Separation inside $M$, applied to $\omega$ with parameter $c$. Thus $a_c\in M\cap\mathcal P(\omega)$. Applying the preceding conclusion with $a=a_c$ gives $c\ne \mathbb{1}_{a_c}$. But by the definition of $a_c$, one has $\mathbb{1}_{a_c}(n)=c(n)$ for every $n\in\omega$, so $c=\mathbb{1}_{a_c}$, a contradiction. Therefore $c\notin M$. [guided] The preceding step has proved a uniform statement: for every ground-model real $a\in M$ with $a\subset\omega$, the Cohen real $c$ differs from the indicator function $\mathbb{1}_a$. To finish, assume for contradiction that $c\in M$. The theorem writes $c=\dot c^G$ as the Cohen real, equivalently a function $c:\omega\to 2$. From such a function we form the subset $a_c:=\{n\in\omega:c(n)=1\}$ of $\omega$ coded by its ones. This set is not obtained from transitivity alone. Rather, because $c\in M$ by the contradiction hypothesis and $\omega\in M$, the Separation axiom inside $M$ applied to the formula $c(n)=1$ with parameter $c$ gives $a_c\in M$. Hence $a_c\in M\cap\mathcal P(\omega)$. Now the uniform disagreement result applies to this particular ground-model real $a_c$. It yields $c\ne \mathbb{1}_{a_c}$ as functions from $\omega$ to $2$. But the definition of $a_c$ gives, for every $n\in\omega$, the equivalence $n\in a_c$ iff $c(n)=1$, and hence $\mathbb{1}_{a_c}(n)=c(n)$. Therefore $c=\mathbb{1}_{a_c}$, contradicting $c\ne\mathbb{1}_{a_c}$. The assumption $c\in M$ is false, and $c\notin M$. [/guided] [/step]