iterated forcing

We can define an iterated forcing of length $\alpha$ by induction as follows:

Let $P_0=\mathrm{\varnothing }$.

Let ${\widehat{Q}}_0$ be a forcing notion.

For $\beta \le \alpha$, $P_{\beta }$ is the set of all functions $f$ such that $\mathrm{dom}(f)\subseteq \beta$ and for any $i\in \mathrm{dom}(f)$, $f(i)$ is a $P_i$-name for a member of ${\widehat{Q}}_i$. Order $P_{\beta }$ by the rule $f\le g$ iff $\mathrm{dom}(g)\subseteq \mathrm{dom}(f)$ and for any $i\in \mathrm{dom}(f)$, $g\upharpoonright i⊩f(i){\le }_{{\widehat{Q}}_i}g(i)$. (Translated, this means that any generic subset including $g$ restricted to $i$ forces that $f(i)$, an element of ${\widehat{Q}}_i$, be less than $g(i)$.)

For , ${\widehat{Q}}_{\beta }$ is a forcing notion in $P_{\beta }$ (so ${⊩}_{P_{\beta }}{\widehat{Q}}_{\beta }$ is a forcing notion).

Then the sequence 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 -support iterated forcing.

Typically we construct the sequence of ${\widehat{Q}}_{\beta }$’s by induction, using a function $F$ such that .

Title	iterated forcing
Canonical name	IteratedForcing
Date of creation	2013-03-22 12:54:47
Last modified on	2013-03-22 12:54:47
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	5
Author	Henry (455)
Entry type	Definition
Classification	msc 03E35
Classification	msc 03E40
Defines	FS
Defines	CS
Defines	finite support
Defines	finite support iterated forcing
Defines	countable support
Defines	countable support iterated forcing
Defines	support iterated forcing