# $\sigma$-closed forcing notions do not add reals

Suppose $\mathbb{P}$ is a $\sigma$-closed forcing notion, i.e. for any decreasing countable sequence $(p_n)_{n<\omega}$ of conditions, there exists a condition $p$ such that for every $i < \omega$, we have $p \leq p_i$.

$\sigma$-closed forcing notions do not add reals.

To see this, take an arbitrary real $A \subseteq \omega$ and suppose $A \in V[G]$ belongs to a forcing extension by $G \subseteq \mathbb{P}$. We want to see that $A$ was already in $V$.

Since $A$ is in the forcing extension, it has a name $\dot A \in V$.

Since $A$ is a real in the forcing extension, then by the Forcing Theorem we must have a condition $p \in G$ that forces this. Let $p$ be such that $$p \Vdash \dot A \subseteq \check \omega$$

We inductively construct a countable decreasing sequence of conditions.

Either $V[G] \vDash 0 \in A$ or $V[G] \vDash 0 \notin A$, so by the Forcing Theorem we get a $p_0 \in G$ such that $p_0 \Vdash \check 0 \in \dot A$ (or that forces the negation). Since $p_0, p \in G$, we assume without loss of generality that $p_0 \leq p$, thanks to the downwards directedness of $G$. Then we can repeat this idea for every natural, and use the downwards directedness of $G$ to ensure that the sequence is decreasing. By $\sigma$-closedness of $\mathbb{P}$, we find a lower bound $r$ on the sequence, which forces, for every natural, whether that natural is in $A$.

Now I'm not exactly sure how to proceed. I have the following idea.

Define the set $$E = \{ p \in \mathbb{P} \mathbin{|} \exists C \subseteq \omega : C \in V \land p \Vdash \dot A = \check C \}$$ of conditions that force that $A$ is already in $V$.

Now we want to show that $E$ is dense below $p$, so that $G$ will meet it, forcing that $A$ was in fact already in $V$.

I'm unsure how to show the density. Any advice on how to proceed?

You're basically done already - you don't need to go through $E$ at all. Rather, based on what you know already, you build in $V$ a real and a condition forcing that that real is $A$; since you can do this below an arbitrary $p$, the result follows.
So think about what you've got already. You have a decreasing sequence of conditions $p_0\ge p_1\ge ...$ such that $p_i$ forces "$i\in A$" or "$i\not\in A$". By $\sigma$-closure, you get a $p$ such that $p\le p_i$ for each $i$.
Now think about $\{n: p\Vdash n\in A\}$ . . . (Note that this is in fact a set in $V$ by the definability of the forcing relation.)