A filter is generic over its ground model exactly when it meets each ground-model maximal forcing antichain in one point. Extensions of a maximal antichain form a dense set, while any ground dense set contains an antichain maximal in the whole forcing. Directedness permits at most one antichain member in a filter.
If is a countable transitive model, , and , enumerate the dense subsets of belonging to and recursively choose a decreasing sequence starting below that meets each one. Its upward closure is a generic filter over containing .
If is a generic filter over a countable transitive model , the generic extension consists of the interpretations by of all forcing names in .
Let for a fixed atomless forcing order , and . If a set were its internal power set of , choose with . The next generic filter belongs to , so ; transitivity of implies , contradicting generic filter for an atomless order is new. The chain is increasing but need not be an elementary chain.
For a forcing name , let consist of pairs where for some . Every ground-model subset of is a name whose value is contained in . Every subset has an equivalent such name: retain those with . The atomic membership truth lemma for forcing proves equality of values. Collect all these names from the ground-model power set into a single outer name, pairing each with every condition. Its value is the full internal power set, without presupposing that power set in the extension.
The forcing theorem identifies truth in a generic extension with the forcing relation: a formula is true in exactly when some condition in forces it.
For a name with finitely many possible values, record which value each condition forces, using an extra marker for undecided conditions. Equal patterns mean that any condition deciding one entry decides all entries with that pattern identically.
A generic extension of a transitive model has exactly the same ordinals as its ground model. Rank induction on names bounds every value; transitivity and agreement on membership make ordinalhood absolute.
A formula holds in a generic extension exactly when some condition in the generic filter forces it for names of its parameters.
For each formula, its forcing relation on names and conditions is uniformly first-order definable inside the ground model. This permits ground-model separation and replacement using forcing predicates.
For a countable transitive model , semantic forcing declares when every generic filter over containing gives .
The syntactic forcing relation is defined recursively inside the ground model from the ranks of forcing names and the logical complexity of . The forcing theorem proves that it agrees with the semantic forcing relation.
For forcing names and a generic filter , exactly when some syntactically forces . Assuming the equality truth lemma, interpreted membership supplies an active pair and a condition in forcing ; a common strengthening forces membership. Conversely the defining equality witnesses occur dense below a forcing condition forcing membership. The dense-below generic meeting lemma supplies one in , and the equality truth lemma recovers interpreted membership.
For the usual recursive syntactic forcing relation, means that conditions forcing for some forcing name are dense below a forcing condition . This density clause proves the existential step of the forcing theorem from the truth lemma for each named instance. A generic filter containing meets that dense set after it is augmented by conditions incompatible with .
Let be forcing names and let be a formula. The namebelongs to the ground model by axiom schema of separation. The forcing theorem shows that its value in a generic extension is exactlyConsequently every generic extension satisfies the separation schema.
Articles by others on the same topic
A generic filter is a conceptual tool or mechanism used in various fields, such as computer science, data processing, and image manipulation, to process or manipulate data in a flexible and reusable way. The term can apply in different contexts, so here are a few interpretations: 1. **In Programming**: A generic filter refers to a function or method that can take various types of input and apply a filtering operation based on specified criteria.