iterated forcing

We can define an iterated forcing of length α by inductionMathworldPlanetmath as follows:

Let P0=.

Let Q^0 be a forcingMathworldPlanetmath notion.

For βα, Pβ is the set of all functions f such that dom(f)β and for any idom(f), f(i) is a Pi-name for a member of Q^i. Order Pβ by the rule fg iff dom(g)dom(f) and for any idom(f), gif(i)Q^ig(i). (Translated, this means that any generic subset including g restricted to i forces that f(i), an element of Q^i, be less than g(i).)

For β<α, Q^β is a forcing notion in Pβ (so PβQ^β is a forcing notion).

Then the sequence Q^ββ<α is an iterated forcing.

If Pβ is restricted to finite functions that it is called a finite support iterated forcing (FS), if Pβ is restricted to countableMathworldPlanetmath functions, it is called a countable support iterated function (CS), and in general if each function in each Pβ has size less than κ then it is a <κ-support iterated forcing.

Typically we construct the sequence of Q^β’s by induction, using a function F such that F(Q^ββ<γ)=Q^γ.

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