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$.
- 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$.
- 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.
- 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)$.
- 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$
- Is the reason this $f$ exists due to definability of forcing, so we can build the function directly in $M$?
Best Answer
Looks good. There are a few more equivalent ways to phrase $\sigma$-distributivity but the difference is merely cosmetic.
This is correct.
This is correct.
This is correct.
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.