composition of forcing notions

Suppose P is a forcingMathworldPlanetmath notion in 𝔐 and Q^ is some P-name such that PQ^ is a forcing notion.

Then take a set of P-names Q such that given a P name Q~ of Q, PQ~=Q^ (that is, no matter which genericPlanetmathPlanetmathPlanetmath subset G of P we force with, the names in Q correspond precisely to the elements of Q^[G]). We can define


We can define a partial orderMathworldPlanetmath on P*Q such that p1,q^1p2,q^2 iff p1Pp2 and p1q^1Q^q^2. (A note on interpretationMathworldPlanetmathPlanetmath: q1 and q2 are P names; this requires only that q^1q^2 in generic subsets contain p1, so in other generic subsets that fact could fail.)

Then P*Q^ is itself a forcing notion, and it can be shown that forcing by P*Q^ is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to forcing first by P and then by Q^[G].

Title composition of forcing notions
Canonical name CompositionOfForcingNotions
Date of creation 2013-03-22 12:54:20
Last modified on 2013-03-22 12:54:20
Owner Henry (455)
Last modified by Henry (455)
Numerical id 4
Author Henry (455)
Entry type Definition
Classification msc 03E35
Classification msc 03E40
Related topic Forcing