Problem with forcing with perfect trees
I've been reading the section on Forcing with Perfect Trees in Jech's Set Theory. The notion of forcing consists of all perfect trees $T\subseteq Seq(\{0,1\})$, where $p$ is stronger than $q$ if $p\subset q$.
Now, let $G$ be generic set of perfect trees. Define $f=\bigcup\{s:(\forall p\in G)s\in p\}.$ Let us see why $f$ is indeed a function. For each $n<\omega$ let $D_n$ be the set of all perfect trees $p$ such that $s\upharpoonright n$ is constant for $s\in p$, then $D_n$ is dense, and thus we can pick $p_n\in G\cap D_n$, then it is easy to prove that $f=\bigcup_n s_n$, where $s_n\in p_n$ is the only element of $p_n$ of length $n$.
Next the author states that $V[G]=V[f]$ with no argument. So my question is, why does this hold?
As the generic filter is minimal over the ground model $V$, that is, for any set of ordinals $X\in V[G]$ we have that $X\in V$ or $G\in V[X]$, it suffices to show that $f\notin V$. I have tried two approaches to prove this:
- Showing that $f:\omega\rightarrow\{0,1\}$ is a Cohen real.
- Proving that for any filter $G'$ of perfect trees such that $f\upharpoonright n\in p$ for all $p\in G'$ we have that $G'$ is generic over $V$.
However, I think the first approach is wrong, and I have no idea on how to prove the second one.
Thanks.
I claim that $G$ is definable from $f$; indeed, $G$ consists precisely of the ground model trees containing the generic branch $f$. Of course, every tree in $G$ contains the branch $f$ by definition. Now assume that there is a tree $T\notin G$ containing the branch $f$. Let $S\in G$ be a condition forcing that $T$ contains $f$. Since $T$ is not in $G$, there must be a node $x\in S\setminus T$. Let's denote by $S_x$ the induced subtree of $S$, i.e. the set of nodes in $S$ compatible with $x$. Then $S_x$ is a perfect tree, it strengthens $S$ and it forces that the generic branch goes through $x$. But this means that $S_x$ cannot force that $T$ contains the generic branch. Contradiction.
Miha's answer is the answer to your main question, but let me just answer the question in the title: no Sacks real is ever Cohen.
For example, consider the tree of all sequences never containing "00." This is clearly a perfect tree, so corresponds to a condition in Sacks forcing; but any real satisfying this condition will not be Cohen, because the set of reals containing "00" is dense open for Cohen forcing.
In general, it is open dense in the Cohen sense to fall off of any perfect tree whose set of branches has empty interior in Cantor space; and the set of such trees is dense open in the Sacks sense. So no Sacks generic real will ever be Cohen generic.