| Version current |
Version 1 |
| We can define an \emph{iterated forcing} of length $\alpha$ by induction as follows: |
We can define an \emph{iterated forcing} of length $\alpha$ by induction as follows: |
|
|
| Let $P_0=\emptyset$. |
Let $P_0=\emptyset$. |
|
|
| Let $\hat{Q}_0$ be a forcing notion. |
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\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}). |
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. |
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 \emph{finite support iterated forcing} (FS), if $P_\beta$ is restricted to countable functions, it is called a \emph{countale support iterated function} (CS), and in general if each function in each $P_\beta$ has size less than $\kappa$ then it is a \emph{$<\kappa$-support iterated forcing}. |
| If $P_\beta$ is restricted to finite functions that it is called a \emph{finite support iterated forcing} (FS), if $P_\beta$ is restricted to countable functions, it is called a \emph{countable support iterated function} (CS), and in general if each function in each $P_\beta$ has size less than $\kappa$ then it is a \emph{$<\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$. |
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$. |
