How to force $\diamondsuit$

Question

I have heard that forcing with the set of countable functions $\omega_1\to\omega_1$ makes $\diamondsuit$ true in the extension $M[G]$, if $CH$ is true in a ctm $M$. Can somebody please point me to a (place with a) proof of this, or give me a hint on how to prove this myself? Thanks.

Answer 1

With the hint (and another one), I'm trying a detailed proof:

Let $(B_{\alpha})_{\alpha < \omega_1}$ enumerate the bounded subsets of $\omega_1$. These (and $\omega_1$ itself) are absolute between $M$ and $M[G]$ because of $\omega_1$-closedness of the forcing and there are $\omega_1$ many of them because of $CH$ in $M$.

With $f=\bigcup G$, let $A_{\alpha}=B_{f(\alpha)}\cap \alpha$ for $\alpha <\omega_1$. Claim that this is a diamond sequence in $M[G]$.

Given $X\subseteq \omega_1$, $X\in M[G]$ and a club $C\subseteq \omega_1$, it needs to be shown that there is $\alpha\in C$ with $X\cap \alpha = A_{\alpha}$. Choose names $\dot X, \dot C \in M$. Let $q\in G$ with $q\Vdash \dot X \subseteq \omega_1\land \dot C \text{ is club in } \omega_1.$ To prove the claim, show that the set of conditions $r\leq q$, for which an $\alpha<\omega_1$ exists so that $dom(r)=\alpha+1$ and $r$ forces $\dot X\cap \check \alpha$ to equal $\check B_{r(\alpha)}\cap \check \alpha$ and also forces $\check \alpha\in \dot C$, is dense below $q$. Then there is also such an $r$ in $G$, proving the claim.

Let $q'\leq q$ be given arbitrarily. Choose $\beta_0 <\omega_1$ with $dom(q')\subseteq \beta_0$ and $q_0\leq q'$ with $dom(q_0)=\beta_0$ and construct an ascending $\omega$-sequence of ordinals $\beta_n<\omega_1$ starting with $\beta_0$ together with a descending sequence $q_n$ starting with $q_0$ like this:

Given $(\beta_n,q_n)$, choose a generic $G_n\ni q_n$ and $dom(q_n) < \beta_{n+1} <\omega_1$ with $\beta_{n+1}\in \dot C^{G_n}$. Let $T_n=\dot X^{G_n} \cap \beta_{n+1}\in M$. Let $q_{n+1}\in G_n$ with $q_{n+1}\leq q_n$ so that $q_{n+1}\Vdash (\dot X \cap \check \beta_{n+1} = \check T_n) \land (\check \beta_{n+1}\in \dot C)$ and also $dom(q_{n+1})$ is an ordinal $\geq \beta_{n+1}$.

Let $\alpha$ be the limit of the $\beta_n$ and $p$ the union of the $q_n$. $dom(p)=\alpha$, and looking at a generic $G'\ni p$ shows that $p\Vdash \dot X\cap \check \alpha = \bigcup_n \check T_n\land \alpha\in \dot C$. Define $r\leq p$ with $dom(r)=\alpha+1$ by $r(\alpha)=\gamma$ where $B_{\gamma} = \bigcup_n T_n$.