iterated forcing
We can define an iterated forcing of length α by induction as follows:
Let P0=∅.
Let ˆQ0 be a forcing notion.
For β≤α, Pβ is the set of all functions f such that dom(f)⊆β and for any i∈dom(f), f(i) is a Pi-name for a member of ˆQi. Order Pβ by the rule f≤g iff dom(g)⊆dom(f) and for any i∈dom(f), g↾. (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 |