# Omega-distributivity of the club shooting poset

I'm currently working through Lemma $$23.9$$ in Jech, which states (more or less) the following:

In some ground model $$M$$, let $$S\subseteq \omega_1$$ be stationary. Consider the notion of forcing $$P_S$$ that consists of all closed bounded subsets of $$\mathbb P$$, where $$q\leq p$$ if $$q$$ is an end extension of $$p$$ (i.e. $$p\subseteq q$$ and $$q\cap (\max(p)+1)=p$$). Then $$P_s$$ is $$\omega$$-distributive, or equivalently for all $$f:\omega\to Ord$$ in $$M[G]$$, in fact $$f\in M$$.

1. This is my paraphrase of the statement of the lemma by looking over the general structure of the proof. Is this a correct understanding of what $$\omega$$-distributivity means?

Now, on to the proof. I will interject from time to time with questions (or just to check my understanding).

Let $$p\Vdash \dot f:\omega\to \text{Ord}$$; we shall find a $$q\leq p$$ and some $$f$$ such that $$q\Vdash \dot f = f$$.

1. Just to confirm I have my "types" correct, we're looking for $$f\in M$$, and more precisely we're trying to show $$q\Vdash \dot f = \check f$$, right?

By induction we construct a chain $$\{A_\alpha: \alpha<\omega_1\}$$ of countable subsets of $$P_S$$. Let $$A_0=\{p\}$$, and $$A_\alpha = \bigcup_{\beta<\alpha} A_\beta$$ if $$\alpha$$ is a limit ordinal. Given $$A_\alpha$$, let $$\gamma_\alpha = \sup\{\max(q):q\in A_\alpha\}$$. For each $$q\in A_\alpha$$ and each $$n$$, we choose some $$r=r(q,n)\in P_S$$ such that $$r\leq q$$, $$r$$ decides $$\dot f(n)$$, and $$\max(r)>\gamma_\alpha$$. Then we let $$A_{\alpha+1} = A_\alpha \cup \{r(q,n):q\in A_\alpha, n<\omega\}$$.

The sequence $$\langle \gamma_\alpha : \alpha<\omega_1\rangle$$ is increasing and continuous. Let $$C=\{\lambda: \text{if \alpha<\lambda then \gamma_\alpha<\lambda}\}$$. As $$C$$ is club, there exists a limit ordinal $$\lambda$$ such that $$\lambda \in C \cap S$$. Let $$\langle \alpha_n:n<\omega\rangle$$ be an increasing sequence with limit $$\lambda$$; then $$\lim_n \gamma_{\alpha_n}=\lambda$$ as well.

1. Just to check undestanding, the reason $$C$$ is club is because it is the set of closure points of $$\alpha \mapsto \gamma_\alpha$$, right?

There is a sequence of conditions $$\langle p_n : n<\omega\rangle$$ such that $$p_0=p$$ and that for every $$n$$, $$p_{n+1}\in A_{\alpha_{n+1}}$$, $$p_{n+1}\leq p_n$$, and $$p_{n+1}$$ decides $$\dot f(n)$$.

1. To build this sequence, to determine $$p_{n+1}$$, we take $$r(p_n,n)$$ as defined above, right?

Since $$\gamma_{\alpha_n} < \max(p_{n+1})\leq \gamma_{\alpha_{n+1}}$$, we have $$\lim_n \max(p_n)=\lambda$$, and because $$\lambda\in S$$, the closed set $$\bigcup_{n<\omega} p_n \cup \{\lambda \}$$ is a condition in $$P_S$$. Since $$q\leq p_n$$ for all $$n$$, $$q$$ decides each $$\dot f(n)$$, and so there exists some $$f$$ such that $$q\Vdash\dot f=f. \quad \square$$

1. Is the reason this $$f$$ exists due to definability of forcing, so we can build the function directly in $$M$$?

1. Looks good. There are a few more equivalent ways to phrase $$\sigma$$-distributivity but the difference is merely cosmetic.
5. This is correct. For each $$n<\omega$$, there is a unique $$\xi_n\in \text{Ord}$$ definable in $$M$$ from $$P_S, q, \dot{f}$$ such that $$q\Vdash \dot{f}(n)=\check{\xi_n}$$, which is because $$q\le p_{n+1}\Vdash\dot{f}(n)=\check{\xi_n}$$. So in $$M$$ we define $$f:\omega\to\text{Ord}$$ via $$f(n)=\xi_n$$, and this $$f\in M$$ is as desired.