A forcing atom determines a ground-model generic filter

ID: a-forcing-atom-determines-a-ground-model-generic-filter

For a forcing atom in a ground-model forcing order, is a ground-model generic filter. It contains and is upward closed. For , choose and . The atom property gives , so is a common strengthening of . Thus is a filter in an ordered set. Every dense subset of a forcing order has some , and . The defining compatibility predicate is bounded to the ground-model set of conditions, so axiom schema of separation forms inside the ground model. For a nonminimal atom, this filter can strictly contain the principal filter above .

New to topics? Read the docs here!