FS iterated forcing preserves chain condition

Let κ be a regular cardinal and let Q^ββ<α be a finite support iterated forcing where for every β<α, PβQ^β has the κ chain condition.

By inductionMathworldPlanetmath:

P0 is the empty setMathworldPlanetmath.

If Pα satisfies the κ chain condition then so does Pα+1, since Pα+1 is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to Pα*Qα and compositionMathworldPlanetmathPlanetmath preserves the κ chain condition for regularPlanetmathPlanetmathPlanetmathPlanetmath κ.

Suppose α is a limit ordinalMathworldPlanetmath and Pβ satisfies the κ chain condition for all β<α. Let S=pii<κ be a subset of Pα of size κ. The domains of the elements of pi form κ finite subsets of α, so if cf(α)>κ then these are boundedPlanetmathPlanetmathPlanetmathPlanetmath, and by the inductive hypothesis, two of them are compatible.

Otherwise, if cf(α)<κ, let αjj<cf(α) be an increasing sequence of ordinalsMathworldPlanetmathPlanetmath cofinal in α. Then for any i<κ there is some n(i)<cf(α) such that dom(pi)αn(i). Since κ is regular and this is a partitionMathworldPlanetmathPlanetmathPlanetmath of κ into fewer than κ pieces, one piece must have size κ, that is, there is some j such that j=n(i) for κ values of i, and so {pin(i)=j} is a set of conditions of size κ contained in Pαj, and therefore contains compatible members by the induction hypothesis.

Finally, if cf(α)=κ, let C=αjj<κ be a strictly increasing, continuousMathworldPlanetmathPlanetmath sequence cofinal in α. Then for every i<κ there is some n(i)<κ such that dom(pi)αn(i). When n(i) is a limit ordinal, since C is continuous, there is also (since dom(pi) is finite) some f(i)<i such that dom(pi)[αf(i),αi)=. Consider the set E of elements i such that i is a limit ordinal and for any j<i, n(j)<i. This is a club, so by Fodor’s lemma there is some j such that {if(i)=j} is stationary.

For each pi such that f(i)=j, consider pi=pij. There are κ of these, all members of Pj, so two of them must be compatible, and hence those two are also compatible in P.

Title FS iterated forcing preserves chain condition
Canonical name FSIteratedForcingPreservesChainCondition
Date of creation 2013-03-22 12:57:14
Last modified on 2013-03-22 12:57:14
Owner Henry (455)
Last modified by Henry (455)
Numerical id 4
Author Henry (455)
Entry type Result
Classification msc 03E35
Classification msc 03E40