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 .
Articles by others on the same topic
There are currently no matching articles.