I'm reading Kanamori's construction of the Solovay model, and had a question regarding random reals. We are forcing with the poset $\mathcal{B}^*$ of non-null Borel subsets of $\omega^\omega$, ordered by inclusion.
Kanamori writes:
For any $n\in\omega$,
$$
\left\{C\in \mathcal{B}^*: C\text{ is closed } \wedge \exists k(C\subset \{f\in\omega^\omega: f(n)=k\})\right\} \tag{i}\label{(i)}
$$
is dense in $\mathcal{B}^*$.Arguing in $V[G]$ there is a unique $x\in \omega^\omega$ specified by
$$ \{x\}=\bigcap\left\{ A^{V[G]}_c: c\in V\text{ is a closed code }\wedge A^V_c\in G\right\}$$
since this is an inersection of closed sets with the finite intersection property and (i) holds.
I think I see why the intersection is a singleton, namely, if there are two points there, we could separate them with a set as in (i).
That being said, I don't quite see why the intersection should be non-empty. Why is the finite intersection property relevant here, since we're not dealing with compact sets nor with sets of vanishing diameter?
Also, on a slightly unrelated note, I know one can talk about the ground model when working in the generic extension by adding a symbol $\check V$ to our forcing language. That being said, in this particular case, can we get away without the definability of the ground model? What I have in mind is that we have a canonical name for $(\omega^\omega)^V$, and thus can say "$c\in V$ is a closed code" iff "$c\in \check{(\omega^\omega)}_G$ is a clode code"
Best Answer
A strengthening of $(i)$ is in fact true: for each $n$, the set of codes for positive-measure closed sets contained in some $$\{f\in\omega^\omega: \sigma\prec f\}$$ for some $\sigma\in\omega^n$ is dense in $\mathcal{B}^*$. This means that we effectively are forcing with closed sets of vanishing diameter.
In fact, here's an explicit definition of the unique real in question: it's the real $r\in V[G]$ such that for each $n\in\omega$ there is some $X\in G$ such that $$V[G]\models X\subseteq\{f\in\omega^\omega: r\upharpoonright n\prec f\}.$$ (Incidentally, if we let $A_\sigma=\{f\in\omega^\omega: \sigma\prec f\}$ we have $(A_\sigma)^{V[G]}\cap V=(A_\sigma)^V$, and even though $r\not\in V$ we have $r\upharpoonright n\in V$ for each $n\in\omega$, so we can basically juggle between models at will in this context.)
As to definability, we don't need definability of the ground model (although we have it) to lift codes for closed sets from $V$ to $V[G]$. Specifically, the set of codes for closed sets is appropriately absolute: if $c\in V$ is a code for a closed set in the sense of $V$, then $c$ is also a code for a closed set in the sense of $V[G]$. (A code for a closed set is really just a subtree of $\omega^{<\omega}$, after all, and its interpretation is the set of paths through the tree.) Moreover, basic properties of closed sets are also appropriately absolute: if, in $V$, $f$ is a real in the closed set coded by $c$, then $f$ is also a real in the closed set coded by $c$ in $V[G]$. (Because being a path through a tree is absolute.)
(In fact, the "atomic" absoluteness mentioned above isn't limited to closed sets: by Shoenfield absoluteness, for any $\Pi^1_2$ code $p$ we have $Set(p)^{V[G]}\cap V=Set(p)^V$. It's only at higher complexity levels that this breaks down. Of course, more nuanced statements break down earlier - for example, closed codes don't switch from empty to non-empty or vice versa, but since being constructible is a $\Sigma^1_2$ property we know that $\Pi^1_2$ codes can.)