|
We can define an iterated forcing of length $\alpha$ by induction as follows:
Let $P_0=\emptyset$
Let $\hat{Q}_0$ be a forcing notion.
For $\beta\leq\alpha$ $P_\beta$ is the set of all functions $f$ such that $\operatorname{dom}(f)\subseteq\beta$ and for any $i\in\operatorname{dom}(f)$ $f(i)$ is a $P_i$ name for a member of $\hat{Q}_i$ Order $P_\beta$ by the rule $f\leq g$ iff $\operatorname{dom}(g)\subseteq\operatorname{dom}(f)$ and for any $i\in\operatorname{dom}(f)$ $g\upharpoonright i\Vdash
f(i)\leq_{\hat{Q}_i}g(i)$ (Translated, this means that any generic subset including $g$ restricted to $i$ forces that $f(i)$ an element of $\hat{Q}_i$ be less than $g(i)$ )
For $\beta<\alpha$ $\hat{Q}_\beta$ is a forcing notion in $P_\beta$ (so $\Vdash_{P_\beta} \hat{Q}_\beta$ texttt is a forcing notion).
Then the sequence $\langle \hat{Q}_\beta\rangle_{\beta<\alpha}$ is an iterated forcing.
If $P_\beta$ is restricted to finite functions that it is called a finite support iterated forcing (FS), if $P_\beta$ is restricted to countable functions, it is called a countable support iterated function (CS), and in general if each function in each $P_\beta$ has size less than $\kappa$ then it is a $<\kappa$ support iterated forcing.
Typically we construct the sequence of $\hat{Q}_\beta$ s by induction, using a function $F$ such that $F(\langle \hat{Q}_\beta\rangle_{\beta<\gamma})=\hat{Q}_\gamma$
|