A filter is a nonempty upward-closed subset of a partial order such that every two members have a common lower bound in . With standard notation for forcing, lower means stronger, so these are exactly the directed filters used to define a generic filter. The projection of a product-generic filter uses these properties before genericity of its factor filters is proved.
The principal filter in an ordered set generated by contains exactly the elements above . It is upward closed, and is a common lower bound in the filter for any two of its members. With standard notation for forcing, these are the conditions weaker than . The principal filter need not be a generic filter: a dense set can require a strict strengthening. The compatible-condition filter in a forcing atom determines a ground-model generic filter includes strengthenings as well as weakenings and can therefore be strictly larger.
Articles by others on the same topic
There are currently no matching articles.