Use standard notation for forcing: means that is stronger than . A closed forcing order is -closed when every decreasing sequence with has a common lower bound:The chain condition for forcing isAn antichain in a forcing order consists of pairwise incompatible forcing conditions; incompatibility means having no common stronger extension. In particular, the -chain condition is the countable chain condition for forcing. These properties and their sequences or antichains are computed inside the ground model .
False as printed: separativity alone does not guarantee a new generic filter. A separative forcing order means that if , some is incompatible with . The one-point order is separative vacuously. Its only generic filter is , and this belongs to . Thus no exists in this example.
The natural missing hypothesis is that the nonempty order is an atomless forcing order. Under that hypothesis the intended argument works. Since is a countable transitive model, enumerate externally its dense subsets as . Choose with . Thenis a directed upward-closed filter in an ordered set and meets every . This is the Rasiowa–Sikorski lemma, giving a generic filter over .
If , the set difference would belong to . It is dense: a condition outside is already in ; a condition in has two incompatible stronger conditions, at least one of which cannot be in the directed filter . Genericity would require , a contradiction. ThusThis uses generic filter for an atomless order is new. A forcing atom is precisely the obstruction illustrated by the counterexample; separativity does not remove it.
With the condition-first name convention used here, evaluation of a forcing name isSince a generic filter is nonempty, there is a condition in . In the given paired forcing name, every condition is paired with both and , and there are no other lower-rank names. ThereforeThis is the unordered pair of the two interpreted sets. If the interpretations coincide, it is a singleton. It is neither an ordered pair nor the set union of those interpretations. Reversing the two components in the name-pair convention changes only the syntax of the same recursive evaluation.
Closure preserves the ground-model cardinal . We use the stronger fact that closed forcing adds no short ordinal sequences. Fix an ordinal in and a forcing name that a condition forces to be an ordinal-valued function with domain .
Inside , recursively strengthen to decide each value , for . At a limit stage take a lower bound of the previously chosen descending sequence; its length is below , so -closure supplies one. After all values have been decided, closure supplies a common lower bound . The decided values form a function by the Axiom schema of replacement, andThe recursion is carried out within using the definable forcing theorem and a ground-model choice of deciding extensions, so every sequence to which closure is applied belongs to . Repeating the construction below any stronger condition shows that such full-decision conditions are dense below a forcing condition . The dense-below generic meeting lemma ensures that a generic filter containing meets them. Thus the interpreted function is in .
If ceased to be a cardinal number in , there would be a surjection for some ordinal . The forcing theorem gives a name and a condition in forcing this. The argument above makes its interpretation a ground-model function, but regards as a cardinal number and admits no such surjection. ThereforeNo regularity of is required; every recursion used has length strictly below . Finite cardinals are preserved automatically. This is cardinal preservation by closed forcing.
The Fn forcing here is ; larger partial functions are stronger conditions. This translates the inclusion description into standard notation for forcing as when . Compatible members of the generic filter agree wherever both are defined, sois a function. For every , the conditions whose domains contain that coordinate form a dense subset of a forcing order. This requirement belongs to , and the generic filter meets it. Consequently is total.
Define the generic coordinate reals for finite-function forcing byFor distinct , the conditions assigning opposite bits to those rows at some column form a dense subset of a forcing order. Given any finite condition, choose a column absent from both rows and extend by assigning zero to one coordinate and one to the other. Genericity supplies such a condition in , so .
The function is formed inside by separation and replacement from . HenceThis constructs an injective function on the ground-model ordinal ; preservation of its cardinal status is a separate issue.
Inside , the finite-function order has the countable chain condition for finite-function forcing. In an uncountable family of binary conditions there are uncountably many distinct finite domains, since each domain supports only finitely many conditions. These domains would have an uncountable Delta-system subfamily by the Delta-system lemma. There are only finitely many assignments to the common finite root, so thin further to an uncountable family agreeing there. Any two such conditions have a union that is again a function and is a common stronger extension. Thus no uncountable antichain in a forcing order exists.
Here is the relevant preservation argument, rather than an appeal to the condition alone. Fix forcing that a forcing name is a function . For each , choose inside a maximal antichain in a forcing order below deciding . By the countable chain condition for forcing, this antichain is countable in , so the possible values form a countable . The union is countable in , hence bounded below its regular . The interpreted has range contained in , by maximality and the dense-below generic meeting lemma. It therefore cannot be a surjection onto .
If were not a cardinal number in , it would be equinumerous with a smaller ordinal, which was countable already in ; composing with that ground-model enumeration would give a surjection . This is impossible. ThereforeThis is the possible-values lemma for chain-condition forcing specialized to . Countability and regularity in this proof are computed inside , not inferred from the external countability of .
Articles by others on the same topic
There are currently no matching articles.