In mathematics, forcing is a method of constructing new models M[G] of set theory by adding a generic subset G of a poset P to a model M. The poset P used will determine what statements hold in the new universe (the 'extension'); to force a statement of interest thus requires construction of a suitable P. This article lists some of the posets P that have been used in this construction.
Notation P is a poset with order < V is the universe of all sets M is a countable transitive model of set theory G is a generic subset of P over M.
Definitions P satisfies the countable chain condition if every antichain in P is at most countable. This implies that V and V[G] have the same cardinals (and the same cofinalities). A subset D of P is called dense if for every p ∈ P there is some q ∈ D with q ≤ p. A filter on P is a nonempty subset F of P such that if p < q and p ∈ F then q ∈ F, and if p ∈ F and q ∈ F then there is some r ∈ F with r ≤ p and r ≤ q. A subset G of P is called generic over M if it is a filter that meets every dense subset of P in M.
Amoeba forcing Amoeba forcing is forcing with the amoeba order, and adds a measure 1 set of random reals.
Cohen forcing
In Cohen forcing (named after Paul Cohen) P is the set of functions from a finite subset of ω2 × ω to {0,1} and p < q if p ⊇ q. This poset satisfies the countable chain condition. Forcing with this poset adds ω2 distinct reals to the model; this was the poset used by Cohen in his original proof of the independence of the continuum hypothesis. More generally, one can replace ω2 by any cardinal κ so construct a model where the continuum has size at least κ. Here, there is no restriction. If κ has cofinality ω, the cardinality of the reals ends up bigger than κ.
Grigorieff forcing Grigorieff forcing (after Serge Grigorieff) destroys a free ultrafilter on ω.
Hechler forcing Hechler forcing (after Stephen Herman Hechler) is used to show that Martin's axiom implies that every family of less than c functions from ω to ω is eventually dominated by some such function. P is the set of pairs (s, E) where s is a finite sequence of natural numbers (considered as functions from a finite ordinal to ω) and E is a finite subset of some fixed set G of functions from ω to ω. The element (s, E) is stronger than (t, F) if t is contained in s, F is contained in E, and if k is in the domain of s but not of t then s(k) > h(k) for all h in F.
Iterated forcing
Iterated forcing with finite supports was introduced by Solovay and Tennenbaum to show the consistency of Suslin's hypothesis. Easton introduced another type of iterated forcing to determine the possible values of the continuum function at regular cardinals. Iterated forcing with countable support was investigated by Laver in his proof of the consistency of Borel's conjecture, Baumgartner, who introduced Axiom A forcing, and Shelah, who introduced proper forcing. Revised countable support iteration was introduced by Shelah to handle semi-proper forcings, such as Prikry forcing, and generalizations, notably including Namba forcing.
Jockusch–Soare forcing Forcing with Π 1 0 {\displaystyle \Pi _{1}^{0}} classes was invented by Robert Soare and Carl Jockusch to prove, among other results, the low basis theorem. Here P is the set of nonempty Π 1 0 {\displaystyle \Pi _{1}^{0}} subsets of 2 ω {\displaystyle 2^{\omega }} (meaning the sets of paths through infinite, computable subtrees of 2 < ω {\displaystyle 2^{<\omega }} ), ordered by inclusion. While most forcing notions on this page relate to set theory, this one relates to recursion theory.
Laver forcing Laver forcing was used by Laver to show that Borel's conjecture, which says that all strong measure zero sets are countable, is consistent with ZFC. (Borel's conjecture is not consistent with the continuum hypothesis.)
P is the set of Laver trees, ordered by inclusion. A Laver tree p is a subset of the finite sequences of natural numbers such that
p is a tree: p contains any initial sequence of any element of p, equivalently stated as p is closed under initial segments p has a stem: a maximal node s(p) = s ∈ p such that s ≤ t or t ≤ s for all t in p, If t ∈ p and s ≤ t then t has an infinite number of immediate successors tn in p for n ∈ ω. If G is generic for (P, ≤), then the real {s(p) : p ∈ G}, called a Laver-real, uniquely determines G. Laver forcing satisfies the Laver property.
Laver preparation The Laver preparation was introduced by Laver in the context of forcing while preserving large cardinal axioms. Specifically, if κ is a supercompact cardinal, then after forcing with the Laver preparation at κ, κ remains a supercompact cardinal, and moreover will still remain so after any further κ-directed-closed forcing. The Laver preparation Pκ on κ is an Easton support iteration of length κ, guided by a Laver function f. This is a function such that for any x in V, there is a λ-supercompactness embedding j with critical point κ (for suitable λ) such that j(f)(κ)=x; Laver shows that such a function exists for every supercompact cardinal κ. The iteration Pκ only has non-trivial forcing at certain stages α for which f(α) is a suitable name for an α-directed-closed forcing, in which case f(α) is used as the stage α forcing.
Levy collapsing
These posets will collapse various cardinals, in other words force them to be equal in size to smaller cardinals.
… excerpt ends here. Continue reading the full article.
