iterated forcing
We can define an iterated forcing of length by induction as follows:
Let .
Let be a forcing notion.
For , is the set of all functions such that and for any , is a -name for a member of . Order by the rule iff and for any , . (Translated, this means that any generic subset including restricted to forces that , an element of , be less than .)
For , is a forcing notion in (so is a forcing notion).
Then the sequence is an iterated forcing.
If is restricted to finite functions that it is called a finite support iterated forcing (FS), if is restricted to countable functions, it is called a countable support iterated function (CS), and in general if each function in each has size less than then it is a -support iterated forcing.
Typically we construct the sequence of ’s by induction, using a function 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 |