Let $\mathbb{S}$ denote Sacks forcing. This is forcing with perfect trees or equivalently forcing with uncountable Borel subsets of ${}^\omega 2$ with the relation $\subseteq$. 


Let $G \subseteq \mathbb{S}$ be a generic filter over $V$. Suppose $B$ is a Borel set coded in $V[G]$. This means $B$ is a subset of $({}^\omega 2)^{V[G]}$ definable by a $\Delta\_1^1$ formula using a parameter in $({}^\omega 2)^{V[G]}$. Furthermore, suppose $B$ is an uncountable Borel set. 


The question is: Does $B$ have a ground model coded uncountable Borel subset? 


I believe that if the above is answered yes then in $V[G]$, the identity map is a dense embedding of $(\mathbb{S})^V$ and $\mathbb{S}$. Does this lead to any problems?


A one further question: Is there some forcing property that can be used to show that the product $\mathbb{S} \times \mathbb{S}$ is different (not equivalent in the forcing sense) from the iteration $\mathbb{S} \* \dot{\mathbb{S}}$? Or to differentiate between countable support products and countable support iterations of Sacks forcing?


Thanks for any information or clarification.



Borel Sets in Sacks Generic Extension
No. For example, let $B$ be the set of reals Turing above $G$. Then $B$ has no nonempty Borel subset with a Borel code in $V$.


