[proofplan] We count, in the ground model $M$, the possible nice names for reals. Because $\operatorname{Add}(\omega,\omega_2)^M$ has the countable chain condition, every name for a real is equivalent to a nice name whose membership decisions are organized by countable antichains. Each such nice name mentions only countably many Cohen coordinates, and for each fixed [countable set](/page/Countable%20Set) of coordinates there are only $2^\omega = \omega_1$ possible nice names. Since $M$ satisfies $\omega_2^\omega = \omega_2$, there are only $\omega_2$ many countable coordinate sets, hence only $\omega_2$ many nice names for reals; evaluating these names in the generic extension gives all reals of $M[G]$. [/proofplan] [step:Fix the forcing notation and verify the countable chain condition] Work in $M$. Let $\mathbb{P}$ denote $\operatorname{Add}(\omega,\omega_2)^M$, presented as the set of finite partial functions $p: \omega_2^M \times \omega \to 2$, ordered by reverse inclusion. For $p \in \mathbb{P}$, let $\operatorname{dom}(p) \subseteq \omega_2^M \times \omega$ denote its finite domain. We first record that $M$ satisfies that $\mathbb{P}$ has the countable chain condition. Let $A \subseteq \mathbb{P}$ be uncountable in $M$. Since each $\operatorname{dom}(p)$ is finite, the Delta System Lemma for finite sets in $M$ gives an uncountable subset $A_0 \subseteq A$ and a finite set $r \subseteq \omega_2^M \times \omega$ such that the family $(\operatorname{dom}(p))_{p \in A_0}$ forms a $\Delta$-system with root $r$. There are only finitely many functions from $r$ to $2$, so there is an uncountable subset $A_1 \subseteq A_0$ such that all conditions in $A_1$ agree on $r$. If $p,q \in A_1$ are distinct, then $p \cup q$ is a finite partial function from $\omega_2^M \times \omega$ to $2$ extending both $p$ and $q$. Thus $p$ and $q$ are compatible in $\mathbb{P}$. Hence $A$ is not an antichain, and $\mathbb{P}$ is ccc in $M$. [guided] The forcing $\operatorname{Add}(\omega,\omega_2)^M$ consists of finite pieces of information about $\omega_2^M$ many Cohen reals. A condition $p$ says finitely many values of the generic function $g: \omega_2^M \times \omega \to 2$. The ordering is reverse inclusion because a stronger condition gives more information. We need the countable chain condition because it is what makes names for reals manageable: membership of each integer in a named real can be decided by a countable maximal antichain. So we verify ccc directly. Let $A \subseteq \mathbb{P}$ be uncountable in $M$. For each $p \in A$, the set $\operatorname{dom}(p)$ is finite. Applying the Delta System Lemma for finite sets inside $M$ to the finite family $(\operatorname{dom}(p))_{p \in A}$, we obtain an uncountable subset $A_0 \subseteq A$ and a finite root $r \subseteq \omega_2^M \times \omega$ such that for distinct $p,q \in A_0$, $\operatorname{dom}(p) \cap \operatorname{dom}(q) = r$. There are only finitely many possible restrictions $p|_r: r \to 2$. Since $A_0$ is uncountable, one restriction occurs on an uncountable subset $A_1 \subseteq A_0$. Now take distinct $p,q \in A_1$. They agree on the common root $r$, and outside $r$ their domains are disjoint. Therefore $p \cup q$ is a well-defined finite partial function from $\omega_2^M \times \omega$ to $2$. It extends both $p$ and $q$, so it is a common strengthening of $p$ and $q$. Thus $p$ and $q$ are compatible. Since every uncountable subset of $\mathbb{P}$ contains two compatible conditions, no antichain is uncountable. Hence $M$ satisfies that $\mathbb{P}$ is ccc. [/guided] [/step] [step:Replace every name for a real by a nice name] Let $\dot{x} \in M$ be a $\mathbb{P}$-name such that $\Vdash_{\mathbb{P}} \dot{x} \subseteq \check{\omega}$. Here $\Vdash_{\mathbb{P}}$ denotes the forcing relation for the poset $\mathbb{P}$ as computed in $M$, and for each object $a \in M$, the symbol $\check{a}$ denotes the canonical $\mathbb{P}$-name for $a$. For each $n \in \omega$, define in $M$ the dense set \begin{align*} D_n := \{p \in \mathbb{P} : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \text{ or } p \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}\}. \end{align*} The set $D_n$ is dense because every condition has an extension deciding the forcing statement $\check{n} \in \dot{x}$. For each $n \in \omega$, [Zorn's Lemma](/theorems/1226) in $M$, applied to the partially ordered set of antichains contained in $D_n$ ordered by inclusion, gives at least one maximal antichain contained in $D_n$. Using the choice axiom and Replacement in $M$, fix in $M$ a sequence $(A_n)_{n \in \omega}$ such that each $A_n \subseteq D_n$ is such a maximal antichain. Because $D_n$ is dense in $\mathbb{P}$, this antichain is maximal in all of $\mathbb{P}$: if $q \in \mathbb{P}$ were incompatible with every member of $A_n$, choose $d \leq q$ with $d \in D_n$; then $A_n \cup \{d\}$ would be a larger antichain contained in $D_n$, contradicting maximality. Thus every condition in $A_n$ decides the statement $\check{n} \in \dot{x}$. Replace $A_n$ by the sub-antichain \begin{align*} B_n := \{p \in A_n : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}\}. \end{align*} Since $\mathbb{P}$ is ccc in $M$, each $A_n$ is countable in $M$, hence each $B_n$ is countable in $M$. Define the nice name \begin{align*} \dot{y} := \{(\check{n},p) : n \in \omega \text{ and } p \in B_n\}. \end{align*} Then $\dot{y} \in M$, and for every $n \in \omega$ the maximality of $A_n$ implies \begin{align*} \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \iff \check{n} \in \dot{y}. \end{align*} Therefore $\Vdash_{\mathbb{P}} \dot{x} = \dot{y}$. Thus every real in $M[G]$ is the interpretation of a nice name of the displayed form, where each $B_n$ is a countable antichain in $\mathbb{P}$. [guided] The purpose of this step is to replace an arbitrary name for a subset of $\omega$ by a name whose structure can be counted. Let $\dot{x} \in M$ be a $\mathbb{P}$-name satisfying $\Vdash_{\mathbb{P}} \dot{x} \subseteq \check{\omega}$. Here $\Vdash_{\mathbb{P}}$ is the forcing relation for the poset $\mathbb{P}$ as computed in $M$, and $\check{a}$ is the canonical $\mathbb{P}$-name for a ground-model object $a \in M$. For each $n \in \omega$, we first force a decision about whether $n$ belongs to the named real. Define \begin{align*} D_n := \{p \in \mathbb{P} : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \text{ or } p \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}\}. \end{align*} This set is dense in $\mathbb{P}$: if $p \in \mathbb{P}$ did not have an extension deciding $\check{n} \in \dot{x}$, then neither membership nor nonmembership could be forced below $p$, contradicting the definition of the forcing relation for a first-order statement. Since $D_n \in M$ and $M$ satisfies ZFC, [Zorn's Lemma](/theorems/1226) in $M$ gives at least one maximal antichain contained in $D_n$ for each $n \in \omega$. Because the set of possible choices is nonempty for every $n$, the choice axiom in $M$ lets us choose one such antichain for each $n$, and Replacement in $M$ collects these choices into a sequence $(A_n)_{n \in \omega}$ with $A_n \subseteq D_n$. We also need each $A_n$ to be maximal for the whole forcing, not merely among antichains contained in $D_n$. This follows from density: if some $q \in \mathbb{P}$ were incompatible with every condition in $A_n$, then density of $D_n$ would give a condition $d \leq q$ with $d \in D_n$; this $d$ would still be incompatible with every member of $A_n$, so $A_n \cup \{d\}$ would contradict the maximality of $A_n$ inside $D_n$. Every member of $A_n$ decides whether $\check{n}$ is in $\dot{x}$. Keep only the positive decisions by setting \begin{align*} B_n := \{p \in A_n : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}\}. \end{align*} The countable chain condition proved in the previous step now enters: because $A_n$ is an antichain in the ccc forcing $\mathbb{P}$, the set $A_n$ is countable in $M$, and therefore $B_n$ is countable in $M$. Define \begin{align*} \dot{y} := \{(\check{n},p) : n \in \omega \text{ and } p \in B_n\}. \end{align*} This is a $\mathbb{P}$-name in $M$ because it is built in $M$ from the sequence $(B_n)_{n \in \omega}$. For a fixed $n \in \omega$, the maximality of $A_n$ means every generic filter meets $A_n$ in exactly one condition. That condition decides $\check{n} \in \dot{x}$, and it belongs to $B_n$ exactly in the positive case. Hence \begin{align*} \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \iff \check{n} \in \dot{y}. \end{align*} Since this holds for every $n \in \omega$ and both names are forced to be subsets of $\check{\omega}$, we conclude \begin{align*} \Vdash_{\mathbb{P}} \dot{x} = \dot{y}. \end{align*} Thus every real in the extension is represented by a nice name whose $n$th coordinate is a countable antichain of positive decisions. This is the standard nice-name reduction for ccc forcing, proved here in the special case of names for subsets of $\omega$. [/guided] [/step] [step:Show that each nice name uses only countably many Cohen coordinates] Let \begin{align*} \dot{y} = \{(\check{n},p) : n \in \omega \text{ and } p \in B_n\} \end{align*} be a nice name for a real, where each $B_n$ is a countable antichain in $\mathbb{P}$. Define the coordinate support of $\dot{y}$ by \begin{align*} S_{\dot{y}} := \{\alpha \in \omega_2^M : \text{there exist } n \in \omega,\ p \in B_n,\ k \in \omega \text{ with } (\alpha,k) \in \operatorname{dom}(p)\}. \end{align*} For each $n \in \omega$, the set $B_n$ is countable in $M$, and each condition $p \in B_n$ has finite domain. Hence $S_{\dot{y}}$ is a countable union of finite sets in $M$, so $S_{\dot{y}}$ is countable in $M$. For a countable set $S \subseteq \omega_2^M$, define the complete subforcing \begin{align*} \mathbb{P}_S := \{p \in \mathbb{P} : \operatorname{dom}(p) \subseteq S \times \omega\}. \end{align*} If $S = S_{\dot{y}}$, then every condition appearing in $\dot{y}$ belongs to $\mathbb{P}_S$. [guided] A nice name for a real is a countable sequence of countable antichains, but each condition in those antichains mentions only finitely many Cohen coordinates. We isolate exactly the coordinates that occur. Define \begin{align*} S_{\dot{y}} := \{\alpha \in \omega_2^M : \text{there exist } n \in \omega,\ p \in B_n,\ k \in \omega \text{ with } (\alpha,k) \in \operatorname{dom}(p)\}. \end{align*} For each fixed $n \in \omega$, the antichain $B_n$ is countable in $M$, and for each $p \in B_n$ the domain $\operatorname{dom}(p)$ is finite. Therefore the set of coordinates used by all conditions in $B_n$ is countable in $M$. Taking the union over $n \in \omega$ gives a [countable union of countable sets](/theorems/755) in $M$, so $S_{\dot{y}}$ is countable in $M$. For a countable coordinate set $S \subseteq \omega_2^M$, define \begin{align*} \mathbb{P}_S := \{p \in \mathbb{P} : \operatorname{dom}(p) \subseteq S \times \omega\}. \end{align*} This is the subforcing whose conditions mention only coordinates from $S$. By the definition of $S_{\dot{y}}$, if $S = S_{\dot{y}}$, then every condition appearing in the nice name $\dot{y}$ has domain contained in $S \times \omega$, hence belongs to $\mathbb{P}_S$. [/guided] [/step] [step:Count the nice names supported on one countable coordinate set] Fix a countable set $S \subseteq \omega_2^M$ in $M$. Since $S \times \omega$ is countable in $M$, the set of finite partial functions from $S \times \omega$ to $2$ is countable in $M$. Thus $M$ satisfies $|\mathbb{P}_S| = \omega$. A nice name supported on $S$ is determined by a sequence $(B_n)_{n \in \omega}$ such that each $B_n$ is an antichain in $\mathbb{P}_S$. The number of possible subsets of $\mathbb{P}_S$ is $2^\omega$ in $M$, because $\mathbb{P}_S$ is countable in $M$. Therefore the number of possible sequences $(B_n)_{n \in \omega}$ is at most \begin{align*} (2^\omega)^\omega = 2^\omega \end{align*} in $M$. Since $M \models 2^\omega = \omega_1$, there are at most $\omega_1^M$ nice names for reals supported on this fixed $S$. [guided] Fix a countable coordinate set $S \subseteq \omega_2^M$ in $M$. The product $S \times \omega$ is countable in $M$, and every condition in $\mathbb{P}_S$ is a finite partial function from $S \times \omega$ to $2$. The set of finite partial functions on a countable set is countable, so $M$ satisfies $|\mathbb{P}_S| = \omega$. Now count possible nice names supported on $S$. Such a name is determined by a sequence $(B_n)_{n \in \omega}$, where each $B_n$ is an antichain in $\mathbb{P}_S$. We do not need to count only antichains exactly; it is enough to overcount them by all subsets of $\mathbb{P}_S$. Since $\mathbb{P}_S$ is countable in $M$, the number of its subsets is $2^\omega$ in $M$. Therefore the number of possible sequences $(B_n)_{n \in \omega}$ is at most \begin{align*} (2^\omega)^\omega = 2^\omega \end{align*} in $M$. Using the hypothesis $M \models 2^\omega = \omega_1$, there are at most $\omega_1^M$ nice names supported on the fixed countable set $S$. [/guided] [/step] [step:Count all nice names for reals] In $M$, the number of countable subsets of $\omega_2^M$ is \begin{align*} |[\omega_2]^\omega| \leq (\omega_2)^\omega = \omega_2. \end{align*} The equality is one of the hypotheses on $M$. For each countable $S \subseteq \omega_2^M$, the previous step gives at most $\omega_1^M$ nice names supported on $S$. Hence the total number of nice names for reals is at most \begin{align*} \omega_2^M \cdot \omega_1^M = \omega_2^M \end{align*} in $M$. [guided] We now remove the assumption that the support $S$ is fixed. A nice name has a countable support $S \subseteq \omega_2^M$ by the previous support step. Thus we first count the possible supports and then multiply by the number of names over each support. In $M$, every countable subset of $\omega_2^M$ is coded by an $\omega$-sequence of elements of $\omega_2^M$, so \begin{align*} |[\omega_2]^\omega| \leq (\omega_2)^\omega = \omega_2. \end{align*} The equality is exactly the hypothesis $M \models \omega_2^\omega = \omega_2$. For each such countable support $S$, the fixed-support count gives at most $\omega_1^M$ nice names. Therefore the total number of nice names for reals is at most \begin{align*} \omega_2^M \cdot \omega_1^M = \omega_2^M \end{align*} in $M$. [/guided] [/step] [step:Evaluate the names to obtain the continuum bound in the extension] Define $\mathcal{N} \in M$ to be the set of all nice $\mathbb{P}$-names for reals in $M$, meaning names of the form \begin{align*} \{(\check{n},p) : n \in \omega \text{ and } p \in B_n\} \end{align*} where each $B_n$ is a countable antichain in $\mathbb{P}$. Since $M$ satisfies that $|\mathcal{N}| \leq \omega_2^M$, choose in $M$ a map $E: \omega_2^M \to \mathcal{N}$ whose range contains every member of $\mathcal{N}$. In $M[G]$, define \begin{align*} F: \omega_2^M \to \mathcal{P}(\omega)^{M[G]} \end{align*} by letting $F(\alpha) = E(\alpha)^G$ when $E(\alpha)$ is a name for a real, and assigning any fixed real otherwise. By the nice-name reduction, every real $x \in \mathcal{P}(\omega)^{M[G]}$ is equal to $\dot{y}^G$ for some nice name $\dot{y} \in \mathcal{N}$, and therefore $x = F(\alpha)$ for some $\alpha \in \omega_2^M$. Thus $F$ is a surjection from $\omega_2^M$ onto the reals of $M[G]$. It remains to justify that the ordinal in the domain is still the second uncountable cardinal in the extension. We use the standard ccc preservation theorem for Cohen forcing: forcing with $\operatorname{Add}(\omega,\kappa)^M$ preserves ground-model cardinals and preserves regularity of uncountable regular cardinals. The hypothesis of this theorem is satisfied by the first step, where $M$ proves that $\mathbb{P}=\operatorname{Add}(\omega,\omega_2)^M$ is ccc. Therefore $\omega_1^M$ and $\omega_2^M$ remain cardinals in $M[G]$. If an ordinal $\lambda$ with $\omega_1^M < \lambda < \omega_2^M$ were an initial ordinal in $M[G]$, then because $\lambda$ was not an initial ordinal in $M$, there would be in $M$ a bijection between $\lambda$ and some smaller ordinal $\mu < \lambda$; the same bijection belongs to $M[G]$, contradicting that $\lambda$ is a cardinal there. Hence no new cardinal lies strictly between $\omega_1^M$ and $\omega_2^M$, so \begin{align*} \omega_2^M = \omega_2^{M[G]}. \end{align*} Consequently \begin{align*} M[G] \models 2^\omega \leq \omega_2. \end{align*} This is the desired upper bound. [guided] The counting argument has produced a surjection in the extension, \begin{align*} F: \omega_2^M \to \mathcal{P}(\omega)^{M[G]}, \end{align*} where $F(\alpha)=E(\alpha)^G$ whenever $E(\alpha)$ is a nice name for a real. Why is this enough to conclude $2^\omega \leq \omega_2$ in $M[G]$? We must check that the domain ordinal $\omega_2^M$ is still the ordinal called $\omega_2$ after forcing. The needed preservation input is the standard ccc preservation theorem for Cohen forcing: forcing with $\operatorname{Add}(\omega,\kappa)^M$ preserves all ground-model cardinals and preserves regularity of uncountable regular cardinals. Its hypothesis is the ccc verification for the Cohen forcing, and that hypothesis was proved in the first step for $\mathbb{P}=\operatorname{Add}(\omega,\omega_2)^M$. Applying the theorem inside the forcing extension gives that $\omega_1^M$ and $\omega_2^M$ remain cardinals in $M[G]$. Since forcing does not change the ordinals themselves, the ordinal interval between $\omega_1^M$ and $\omega_2^M$ is the same interval in $M[G]$. We now rule out a new initial ordinal in that interval. Let $\lambda$ be an ordinal satisfying $\omega_1^M < \lambda < \omega_2^M$. In $M$, the ordinal $\lambda$ is not a cardinal, because $\omega_2^M$ is the next cardinal after $\omega_1^M$. Hence there are an ordinal $\mu < \lambda$ and a bijection $b: \mu \to \lambda$ belonging to $M$. The same function $b$ belongs to $M[G]$, so $\lambda$ still cannot be an initial ordinal in the extension. Therefore no ordinal strictly between $\omega_1^M$ and $\omega_2^M$ becomes a new cardinal, and the second uncountable cardinal of $M[G]$ is precisely \begin{align*} \omega_2^{M[G]} = \omega_2^M. \end{align*} The map $F$ is onto $\mathcal{P}(\omega)^{M[G]}$, so the extension satisfies \begin{align*} |\mathcal{P}(\omega)^{M[G]}| \leq \omega_2^{M[G]}. \end{align*} Equivalently, \begin{align*} M[G] \models 2^\omega \leq \omega_2. \end{align*} [/guided] [/step]