For the product forcing order, let and be the coordinate projections of :These are nonempty upward-closed, directed filters in an ordered set. Clearly . If and , choose and . Directedness supplies below both, so . Upward closure of gives . Therefore the projection of a product-generic filter satisfiesNo greatest conditions in the factors are required for this argument.
Let be a dense subset of a forcing order . Then is dense in the product forcing order: below , choose in and retain . The generic filter meets it, so its first projection meets . Together with the filter properties proved above, this givesThe same argument proves that is -generic over , but genericity over the larger generic extension needs the next argument.
We prove mutual genericity for product forcing. Let be a dense subset of , and take a forcing name evaluating to . By the forcing theorem, some forces that is a dense subset of the canonical forcing name for .
In defineThis set is dense in the product forcing order. Given , the incompatible case is immediate. Otherwise first strengthen below . The forced density assertion and the existential clause of syntactic forcing supply a further and a ground-model with . To justify choosing a ground-model , a name forced to lie in can densely be made equal to some by the atomic membership clause; strengthen to that equality and use the forced order comparison. Thus lies below .
The generic filter meets . It cannot meet the first part, because its first projection contains and is directed. Hence there is with and . Soundness of the forcing theorem gives , and the projection gives . Since every such is met,This establishes the stronger property, rather than merely meeting dense ground-model subsets.
Articles by others on the same topic
There are currently no matching articles.