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.