Does the Laver real determine the generic filter?

Question

Let us concern the Laver forcing $ \mathbb{L} $.

Let $ G $ be $ \mathbb{L} $-generic over a c.t.m. $ M $ for ZFC. Let $$ x_G := \bigcup \{ \operatorname{stem}(p) : p \in G \} $$ be the Laver real determined by $ G $.

Now, Jech ("Set Theory", 3rd edition, p.565) claims $$ G = \{ p \in \mathbb{L}^M : \forall n < \omega \ x_G \mathord{\upharpoonright} n \in p \} =: F. $$

The inclusion $ G \subseteq F $ clearly holds.

But how can one show $ F \subseteq G $?

---

Is $ F $ even a filter?

For example, imagine the following situation:

• $ x_G(n) = 0 $ for all $ n < \omega $,
• there are $ p, q \in \mathbb{L}^M $ such that
• $ \operatorname{stem}(p) = \operatorname{stem}(q) = \emptyset $,
• at each node of $ p $ the successors are exactly $ 0, 2, 4, 6, \ldots $,
• at each node of $ q $ the successors are exactly $ 0, 1, 3, 5, \ldots $.

Then $ p, q \in F $, but $ p \perp q $ because $ p \cap q = \{ x_G \mathord{\upharpoonright} n : n < \omega \} $ does not contain any Laver tree.

What am I missing?

Answer 1

Lemma.

Let $ p \in \mathbb{L} $ and suppose $ q \subseteq \omega^{< \omega} $ is a tree that does not contain any Laver tree.

Then there is a Laver tree $ r \in \mathbb{L} $ such that $ [r] \subseteq [p] \setminus [q] $.

Proof. Note $ [p] \setminus [q] \neq \emptyset $. Otherwise $ [p] \subseteq [q] $, so $$ p = \{ x \mathord{\upharpoonright} n : x \in [p] \land n < \omega \} \subseteq \{ x \mathord{\upharpoonright} n : x \in [q] \land n < \omega \} \subseteq q, $$ a contradiction.

Let $ x \in [p] \setminus [q] $. Then there is some $ n < \omega $ such that $ x \mathord{\upharpoonright} n \notin [q] $. Now, $$ r := \{ s \in p : s \subseteq x \mathord{\upharpoonright} n \lor s \supseteq x \mathord{\upharpoonright} n \} $$ is as wished.

QED.

---

Proof of $ F \subseteq G $. (Based on hot_queen's answer and comments.)

Assume $ G \subsetneq F $. Then we find $ q \in F \setminus G $ and $ p \in G $ such that $ p \perp q $, i.e. $ \forall r \in \mathbb{L}^M \ r \nsubseteq p \cap q $.

Now $$ D_q := \{ r \in \mathbb{L}^M : ([r] \cap [q] = \emptyset)^M \} \in M $$ is dense below $ p $. To see this, fix $ p' \leq p $. Then $ p' \perp q $, so $ q' := p' \cap q $ does not contain any Laver tree. We use the above Lemma (within $ M $) to find $ r \leq p' $ with $$ \Bigl( [r] \subseteq [p'] \setminus [q'] = [p'] \setminus ([p'] \cap [q]) = [p'] \setminus [q] \Bigr)^M, $$ so $ ([r] \cap [q] = \emptyset)^M $ and hence $ r \in D_q $.

Now, fix $ r \in G \cap D_q $. Then $ ([r \cap q] = [r] \cap [q] = \emptyset)^M $, i.e. $$ ({\supsetneq} \text{ is well-founded on the tree } r \cap q)^M. $$ But the notion of well-foundation is absolute, so $ (x_G \in [r \cap q] = \emptyset)^{M[G]} $ - a contradiction.

QED.

Answer 2

Can you show (or maybe disprove this): If $T$ is Laver tree and $T'$ is a tree which doesn't contain a Laver tree then $[T] \backslash [T']$ contains the set of branches through a Laver tree?

Ok. Now using a density argument show the following: If $p \in G$, then for every Laver tree $q$, if $p, q$ are incompatible then there is some $p_1 \leq p$, $p_1 \in G$ and $[p_1] \cap [q] = \phi$. It follows that if $x_G \in [q]$, then $q \in G$ - Otherwise, for some $p \in G$, $p, q$ are incompatible, hence for some $p_1 \leq p$, $p_1 \in G$ and $[p_1] \cap [q] = \phi$ which is impossible because $x_G \in [p_1] \cap [q]$.

Let me also add a few remarks about how the situation is analogous to random forcing (and many other forcings): In the random poset $P$, conditions are compact subsets of $\mathbb{R}$ of positive measure and for $p, q \in P$, we write $p \leq q$ iff $p \subseteq q$. If $G$ is $P$-generic over the ground model then there is a unique real $r_G$ which is a member of every set in $G$. You can then show that $G$ is the set of all positive measure compact sets coded in the ground model which contain $r_G$. Along the way, you'll also show that there is no measure zero Borel set coded in the ground model which contains $r_G$; this is also sufficient for $r_G$ to be random generic. The analogue of this for Laver forcing is that the Laver real cannot be a branch of any tree in the ground model which does not contain a Laver tree. Maybe you can now show that Laver reals are precisely the reals which do not form a branch of a small tree coded in the ground model where small means that it does not contain a Laver tree.