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.