fbpx
Wikipedia

Forcing (mathematics)

In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. Intuitively, forcing can be thought of as a technique to expand the set theoretical universe to a larger universe by introducing a new "generic" object .

Forcing was first used by Paul Cohen in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo–Fraenkel set theory. It has been considerably reworked and simplified in the following years, and has since served as a powerful technique, both in set theory and in areas of mathematical logic such as recursion theory. Descriptive set theory uses the notions of forcing from both recursion theory and set theory. Forcing has also been used in model theory, but it is common in model theory to define genericity directly without mention of forcing.

Intuition edit

Forcing is usually used to construct an expanded universe that satisfies some desired property. For example, the expanded universe might contain many new real numbers (at least   of them), identified with subsets of the set   of natural numbers, that were not there in the old universe, and thereby violate the continuum hypothesis.

In order to intuitively justify such an expansion, it is best to think of the "old universe" as a model   of the set theory, which is itself a set in the "real universe"  . By the Löwenheim–Skolem theorem,   can be chosen to be a "bare bones" model that is externally countable, which guarantees that there will be many subsets (in  ) of   that are not in  . Specifically, there is an ordinal   that "plays the role of the cardinal  " in  , but is actually countable in  . Working in  , it should be easy to find one distinct subset of   per each element of  . (For simplicity, this family of subsets can be characterized with a single subset  .)

However, in some sense, it may be desirable to "construct the expanded model   within  ". This would help ensure that   "resembles"   in certain aspects, such as   being the same as   (more generally, that cardinal collapse does not occur), and allow fine control over the properties of  . More precisely, every member of   should be given a (non-unique) name in  . The name can be thought as an expression in terms of  , just like in a simple field extension   every element of   can be expressed in terms of  . A major component of forcing is manipulating those names within  , so sometimes it may help to directly think of   as "the universe", knowing that the theory of forcing guarantees that   will correspond to an actual model.

A subtle point of forcing is that, if   is taken to be an arbitrary "missing subset" of some set in  , then the   constructed "within  " may not even be a model. This is because   may encode "special" information about   that is invisible within   (e.g. the countability of  ), and thus prove the existence of sets that are "too complex for   to describe".[1][2]

Forcing avoids such problems by requiring the newly introduced set   to be a generic set relative to  .[1] Some statements are "forced" to hold for any generic  : For example, a generic   is "forced" to be infinite. Furthermore, any property (describable in  ) of a generic set is "forced" to hold under some forcing condition. The concept of "forcing" can be defined within  , and it gives   enough reasoning power to prove that   is indeed a model that satisfies the desired properties.

Cohen's original technique, now called ramified forcing, is slightly different from the unramified forcing expounded here. Forcing is also equivalent to the method of Boolean-valued models, which some feel is conceptually more natural and intuitive, but usually much more difficult to apply.[3]

The role of the model edit

In order for the above approach to work smoothly,   must in fact be a standard transitive model in  , so that membership and other elementary notions can be handled intuitively in both   and  . A standard transitive model can be obtained from any standard model through the Mostowski collapse lemma, but the existence of any standard model of   (or any variant thereof) is in itself a stronger assumption than the consistency of  .

To get around this issue, a standard technique is to let   be a standard transitive model of an arbitrary finite subset of   (any axiomatization of   has at least one axiom schema, and thus an infinite number of axioms), the existence of which is guaranteed by the reflection principle. As the goal of a forcing argument is to prove consistency results, this is enough since any inconsistency in a theory must manifest with a derivation of a finite length, and thus involve only a finite number of axioms.

Forcing conditions and forcing posets edit

Each forcing condition can be regarded as a finite piece of information regarding the object   adjoined to the model. There are many different ways of providing information about an object, which give rise to different forcing notions. A general approach to formalizing forcing notions is to regard forcing conditions as abstract objects with a poset structure.

A forcing poset is an ordered triple,  , where   is a preorder on  , and   is the largest element. Members of   are the forcing conditions (or just conditions). The order relation   means "  is stronger than  ". (Intuitively, the "smaller" condition provides "more" information, just as the smaller interval   provides more information about the number π than the interval   does.) Furthermore, the preorder   must be atomless, meaning that it must satisfy the splitting condition:

  • For each  , there are   such that  , with no   such that  .

In other words, it must be possible to strengthen any forcing condition   in at least two incompatible directions. Intuitively, this is because   is only a finite piece of information, whereas an infinite piece of information is needed to determine  .

There are various conventions in use. Some authors require   to also be antisymmetric, so that the relation is a partial order. Some use the term partial order anyway, conflicting with standard terminology, while some use the term preorder. The largest element can be dispensed with. The reverse ordering is also used, most notably by Saharon Shelah and his co-authors.

Examples edit

Let   be any infinite set (such as  ), and let the generic object in question be a new subset  . In Cohen's original formulation of forcing, each forcing condition is a finite set of sentences, either of the form   or  , that are self-consistent (i.e.   and   for the same value of   do not appear in the same condition). This forcing notion is usually called Cohen forcing.

The forcing poset for Cohen forcing can be formally written as  , the finite partial functions from   to   under reverse inclusion. Cohen forcing satisfies the splitting condition because given any condition  , one can always find an element   not mentioned in  , and add either the sentence   or   to   to get two new forcing conditions, incompatible with each other.

Another instructive example of a forcing poset is  , where   and   is the collection of Borel subsets of   having non-zero Lebesgue measure. The generic object associated with this forcing poset is a random real number  . It can be shown that   falls in every Borel subset of   with measure 1, provided that the Borel subset is "described" in the original unexpanded universe (this can be formalized with the concept of Borel codes). Each forcing condition can be regarded as a random event with probability equal to its measure. Due to the ready intuition this example can provide, probabilistic language is sometimes used with other divergent forcing posets.

Generic filters edit

Even though each individual forcing condition   cannot fully determine the generic object  , the set   of all true forcing conditions does determine  . In fact, without loss of generality,   is commonly considered to be the generic object adjoined to  , so the expanded model is called  . It is usually easy enough to show that the originally desired object   is indeed in the model  .

Under this convention, the concept of "generic object" can be described in a general way. Specifically, the set   should be a generic filter on   relative to  . The "filter" condition means that it makes sense that   is a set of all true forcing conditions:

  •  
  •  
  • if  , then  
  • if  , then there exists an   such that  

For   to be "generic relative to  " means:

  • If   is a "dense" subset of   (that is, for each  , there exists a   such that  ), then  .

Given that   is a countable model, the existence of a generic filter   follows from the Rasiowa–Sikorski lemma. In fact, slightly more is true: Given a condition  , one can find a generic filter   such that  . Due to the splitting condition on  , if   is a filter, then   is dense. If  , then   because   is a model of  . For this reason, a generic filter is never in  .

P-names and interpretations edit

Associated with a forcing poset   is the class   of  -names. A  -name is a set   of the form

 

Given any filter   on  , the interpretation or valuation map from  -names is given by

 

The  -names are, in fact, an expansion of the universe. Given  , one defines   to be the  -name

 

Since  , it follows that  . In a sense,   is a "name for  " that does not depend on the specific choice of  .

This also allows defining a "name for  " without explicitly referring to  :

 

so that  .

Rigorous definitions edit

The concepts of  -names, interpretations, and   are actually defined by transfinite recursion. With   the empty set,   the successor ordinal to ordinal  ,   the power-set operator, and   a limit ordinal, define the following hierarchy:

 

Then the class of  -names is defined as

 

The interpretation map and the map   can similarly be defined with a hierarchical construction.

Forcing edit

Given a generic filter  , one proceeds as follows. The subclass of  -names in   is denoted  . Let

 

To reduce the study of the set theory of   to that of  , one works with the "forcing language", which is built up like ordinary first-order logic, with membership as the binary relation and all the  -names as constants.

Define   (to be read as "  forces   in the model   with poset  "), where   is a condition,   is a formula in the forcing language, and the  's are  -names, to mean that if   is a generic filter containing  , then  . The special case   is often written as " " or simply " ". Such statements are true in  , no matter what   is.

What is important is that this external definition of the forcing relation   is equivalent to an internal definition within  , defined by transfinite induction (specifically  -induction) over the  -names on instances of   and  , and then by ordinary induction over the complexity of formulae. This has the effect that all the properties of   are really properties of  , and the verification of   in   becomes straightforward. This is usually summarized as the following three key properties:

  • Truth:   if and only if it is forced by  , that is, for some condition  , we have  .
  • Definability: The statement " " is definable in  .
  • Coherence:  .

Internal definition edit

There are many different but equivalent ways to define the forcing relation   in  .[4] One way to simplify the definition is to first define a modified forcing relation   that is strictly stronger than  . The modified relation   still satisfies the three key properties of forcing, but   and   are not necessarily equivalent even if the first-order formulae   and   are equivalent. The unmodified forcing relation can then be defined as

 
In fact, Cohen's original concept of forcing is essentially   rather than  .[3]

The modified forcing relation   can be defined recursively as follows:

  1.   means  
  2.   means  
  3.   means  
  4.   means  
  5.   means  

Other symbols of the forcing language can be defined in terms of these symbols: For example,   means  ,   means  , etc. Cases 1 and 2 depend on each other and on case 3, but the recursion always refer to  -names with lesser ranks, so transfinite induction allows the definition to go through.

By construction,   (and thus  ) automatically satisfies Definability. The proof that   also satisfies Truth and Coherence is by inductively inspecting each of the five cases above. Cases 4 and 5 are trivial (thanks to the choice of   and   as the elementary symbols[5]), cases 1 and 2 relies only on the assumption that   is a filter, and only case 3 requires   to be a generic filter.[3]

Formally, an internal definition of the forcing relation (such as the one presented above) is actually a transformation of an arbitrary formula   to another formula   where   and   are additional variables. The model   does not explicitly appear in the transformation (note that within  ,   just means "  is a  -name"), and indeed one may take this transformation as a "syntactic" definition of the forcing relation in the universe   of all sets regardless of any countable transitive model. However, if one wants to force over some countable transitive model  , then the latter formula should be interpreted under   (i.e. with all quantifiers ranging only over  ), in which case it is equivalent to the external "semantic" definition of   described at the top of this section:

For any formula   there is a theorem   of the theory   (for example conjunction of finite number of axioms) such that for any countable transitive model   such that   and any atomless partial order   and any  -generic filter   over  
 

This the sense under which the forcing relation is indeed "definable in  ".

Consistency edit

The discussion above can be summarized by the fundamental consistency result that, given a forcing poset  , we may assume the existence of a generic filter  , not belonging to the universe  , such that   is again a set-theoretic universe that models  . Furthermore, all truths in   may be reduced to truths in   involving the forcing relation.

Both styles, adjoining   to either a countable transitive model   or the whole universe  , are commonly used. Less commonly seen is the approach using the "internal" definition of forcing, in which no mention of set or class models is made. This was Cohen's original method, and in one elaboration, it becomes the method of Boolean-valued analysis.

Cohen forcing edit

The simplest nontrivial forcing poset is  , the finite partial functions from   to   under reverse inclusion. That is, a condition   is essentially two disjoint finite subsets   and   of  , to be thought of as the "yes" and "no" parts of  , with no information provided on values outside the domain of  . "  is stronger than  " means that  , in other words, the "yes" and "no" parts of   are supersets of the "yes" and "no" parts of  , and in that sense, provide more information.

Let   be a generic filter for this poset. If   and   are both in  , then   is a condition because   is a filter. This means that   is a well-defined partial function from   to   because any two conditions in   agree on their common domain.

In fact,   is a total function. Given  , let  . Then   is dense. (Given any  , if   is not in  's domain, adjoin a value for  —the result is in  .) A condition   has   in its domain, and since  , we find that   is defined.

Let  , the set of all "yes" members of the generic conditions. It is possible to give a name for   directly. Let

 

Then   Now suppose that   in  . We claim that  . Let

 

Then   is dense. (Given any  , find   that is not in its domain, and adjoin a value for   contrary to the status of " ".) Then any   witnesses  . To summarize,   is a "new" subset of  , necessarily infinite.

Replacing   with  , that is, consider instead finite partial functions whose inputs are of the form  , with   and  , and whose outputs are   or  , one gets   new subsets of  . They are all distinct, by a density argument: Given  , let

 

then each   is dense, and a generic condition in it proves that the αth new set disagrees somewhere with the  th new set.

This is not yet the falsification of the continuum hypothesis. One must prove that no new maps have been introduced which map   onto  , or   onto  . For example, if one considers instead  , finite partial functions from   to  , the first uncountable ordinal, one gets in   a bijection from   to  . In other words,   has collapsed, and in the forcing extension, is a countable ordinal.

The last step in showing the independence of the continuum hypothesis, then, is to show that Cohen forcing does not collapse cardinals. For this, a sufficient combinatorial property is that all of the antichains of the forcing poset are countable.

The countable chain condition edit

An (strong) antichain   of   is a subset such that if   and  , then   and   are incompatible (written  ), meaning there is no   in   such that   and  . In the example on Borel sets, incompatibility means that   has zero measure. In the example on finite partial functions, incompatibility means that   is not a function, in other words,   and   assign different values to some domain input.

  satisfies the countable chain condition (c.c.c.) if and only if every antichain in   is countable. (The name, which is obviously inappropriate, is a holdover from older terminology. Some mathematicians write "c.a.c." for "countable antichain condition".)

It is easy to see that   satisfies the c.c.c. because the measures add up to at most  . Also,   satisfies the c.c.c., but the proof is more difficult.

Given an uncountable subfamily  , shrink   to an uncountable subfamily   of sets of size  , for some  . If   for uncountably many  , shrink this to an uncountable subfamily   and repeat, getting a finite set   and an uncountable family   of incompatible conditions of size   such that every   is in   for at most countable many  . Now, pick an arbitrary  , and pick from   any   that is not one of the countably many members that have a domain member in common with  . Then   and   are compatible, so   is not an antichain. In other words,  -antichains are countable.[citation needed]

The importance of antichains in forcing is that for most purposes, dense sets and maximal antichains are equivalent. A maximal antichain   is one that cannot be extended to a larger antichain. This means that every element   is compatible with some member of  . The existence of a maximal antichain follows from Zorn's Lemma. Given a maximal antichain  , let

 

Then   is dense, and   if and only if  . Conversely, given a dense set  , Zorn's Lemma shows that there exists a maximal antichain  , and then   if and only if  .

Assume that   satisfies the c.c.c. Given

forcing, mathematics, forcing, recursion, theory, forcing, computability, contents, intuition, role, model, forcing, conditions, forcing, posets, examples, generic, filters, names, interpretations, rigorous, definitions, forcing, internal, definition, consiste. For the use of forcing in recursion theory see Forcing computability Contents 1 Intuition 1 1 The role of the model 2 Forcing conditions and forcing posets 2 1 Examples 3 Generic filters 4 P names and interpretations 4 1 Rigorous definitions 5 Forcing 5 1 Internal definition 6 Consistency 7 Cohen forcing 8 The countable chain condition 9 Easton forcing 10 Random reals 11 Boolean valued models 12 Meta mathematical explanation 13 Logical explanation 14 See also 15 Notes 16 References 17 Bibliography In the mathematical discipline of set theory forcing is a technique for proving consistency and independence results Intuitively forcing can be thought of as a technique to expand the set theoretical universe V displaystyle V to a larger universe V G displaystyle V G by introducing a new generic object G displaystyle G Forcing was first used by Paul Cohen in 1963 to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo Fraenkel set theory It has been considerably reworked and simplified in the following years and has since served as a powerful technique both in set theory and in areas of mathematical logic such as recursion theory Descriptive set theory uses the notions of forcing from both recursion theory and set theory Forcing has also been used in model theory but it is common in model theory to define genericity directly without mention of forcing Intuition editForcing is usually used to construct an expanded universe that satisfies some desired property For example the expanded universe might contain many new real numbers at least ℵ 2 displaystyle aleph 2 nbsp of them identified with subsets of the set N displaystyle mathbb N nbsp of natural numbers that were not there in the old universe and thereby violate the continuum hypothesis In order to intuitively justify such an expansion it is best to think of the old universe as a model M displaystyle M nbsp of the set theory which is itself a set in the real universe V displaystyle V nbsp By the Lowenheim Skolem theorem M displaystyle M nbsp can be chosen to be a bare bones model that is externally countable which guarantees that there will be many subsets in V displaystyle V nbsp of N displaystyle mathbb N nbsp that are not in M displaystyle M nbsp Specifically there is an ordinal ℵ 2 M displaystyle aleph 2 M nbsp that plays the role of the cardinal ℵ 2 displaystyle aleph 2 nbsp in M displaystyle M nbsp but is actually countable in V displaystyle V nbsp Working in V displaystyle V nbsp it should be easy to find one distinct subset of N displaystyle mathbb N nbsp per each element of ℵ 2 M displaystyle aleph 2 M nbsp For simplicity this family of subsets can be characterized with a single subset X ℵ 2 M N displaystyle X subseteq aleph 2 M times mathbb N nbsp However in some sense it may be desirable to construct the expanded model M X displaystyle M X nbsp within M displaystyle M nbsp This would help ensure that M X displaystyle M X nbsp resembles M displaystyle M nbsp in certain aspects such as ℵ 2 M X displaystyle aleph 2 M X nbsp being the same as ℵ 2 M displaystyle aleph 2 M nbsp more generally that cardinal collapse does not occur and allow fine control over the properties of M X displaystyle M X nbsp More precisely every member of M X displaystyle M X nbsp should be given a non unique name in M displaystyle M nbsp The name can be thought as an expression in terms of X displaystyle X nbsp just like in a simple field extension L K 8 displaystyle L K theta nbsp every element of L displaystyle L nbsp can be expressed in terms of 8 displaystyle theta nbsp A major component of forcing is manipulating those names within M displaystyle M nbsp so sometimes it may help to directly think of M displaystyle M nbsp as the universe knowing that the theory of forcing guarantees that M X displaystyle M X nbsp will correspond to an actual model A subtle point of forcing is that if X displaystyle X nbsp is taken to be an arbitrary missing subset of some set in M displaystyle M nbsp then the M X displaystyle M X nbsp constructed within M displaystyle M nbsp may not even be a model This is because X displaystyle X nbsp may encode special information about M displaystyle M nbsp that is invisible within M displaystyle M nbsp e g the countability of M displaystyle M nbsp and thus prove the existence of sets that are too complex for M displaystyle M nbsp to describe 1 2 Forcing avoids such problems by requiring the newly introduced set X displaystyle X nbsp to be a generic set relative to M displaystyle M nbsp 1 Some statements are forced to hold for any generic X displaystyle X nbsp For example a generic X displaystyle X nbsp is forced to be infinite Furthermore any property describable in M displaystyle M nbsp of a generic set is forced to hold under some forcing condition The concept of forcing can be defined within M displaystyle M nbsp and it gives M displaystyle M nbsp enough reasoning power to prove that M X displaystyle M X nbsp is indeed a model that satisfies the desired properties Cohen s original technique now called ramified forcing is slightly different from the unramified forcing expounded here Forcing is also equivalent to the method of Boolean valued models which some feel is conceptually more natural and intuitive but usually much more difficult to apply 3 The role of the model edit In order for the above approach to work smoothly M displaystyle M nbsp must in fact be a standard transitive model in V displaystyle V nbsp so that membership and other elementary notions can be handled intuitively in both M displaystyle M nbsp and V displaystyle V nbsp A standard transitive model can be obtained from any standard model through the Mostowski collapse lemma but the existence of any standard model of Z F C displaystyle mathsf ZFC nbsp or any variant thereof is in itself a stronger assumption than the consistency of Z F C displaystyle mathsf ZFC nbsp To get around this issue a standard technique is to let M displaystyle M nbsp be a standard transitive model of an arbitrary finite subset of Z F C displaystyle mathsf ZFC nbsp any axiomatization of Z F C displaystyle mathsf ZFC nbsp has at least one axiom schema and thus an infinite number of axioms the existence of which is guaranteed by the reflection principle As the goal of a forcing argument is to prove consistency results this is enough since any inconsistency in a theory must manifest with a derivation of a finite length and thus involve only a finite number of axioms Forcing conditions and forcing posets editEach forcing condition can be regarded as a finite piece of information regarding the object X displaystyle X nbsp adjoined to the model There are many different ways of providing information about an object which give rise to different forcing notions A general approach to formalizing forcing notions is to regard forcing conditions as abstract objects with a poset structure A forcing poset is an ordered triple P 1 displaystyle mathbb P leq mathbf 1 nbsp where displaystyle leq nbsp is a preorder on P displaystyle mathbb P nbsp and 1 displaystyle mathbf 1 nbsp is the largest element Members of P displaystyle mathbb P nbsp are the forcing conditions or just conditions The order relation p q displaystyle p leq q nbsp means p displaystyle p nbsp is stronger than q displaystyle q nbsp Intuitively the smaller condition provides more information just as the smaller interval 3 1415926 3 1415927 displaystyle 3 1415926 3 1415927 nbsp provides more information about the number p than the interval 3 1 3 2 displaystyle 3 1 3 2 nbsp does Furthermore the preorder displaystyle leq nbsp must be atomless meaning that it must satisfy the splitting condition For each p P displaystyle p in mathbb P nbsp there are q r P displaystyle q r in mathbb P nbsp such that q r p displaystyle q r leq p nbsp with no s P displaystyle s in mathbb P nbsp such that s q r displaystyle s leq q r nbsp In other words it must be possible to strengthen any forcing condition p displaystyle p nbsp in at least two incompatible directions Intuitively this is because p displaystyle p nbsp is only a finite piece of information whereas an infinite piece of information is needed to determine X displaystyle X nbsp There are various conventions in use Some authors require displaystyle leq nbsp to also be antisymmetric so that the relation is a partial order Some use the term partial order anyway conflicting with standard terminology while some use the term preorder The largest element can be dispensed with The reverse ordering is also used most notably by Saharon Shelah and his co authors Examples edit Let S displaystyle S nbsp be any infinite set such as N displaystyle mathbb N nbsp and let the generic object in question be a new subset X S displaystyle X subseteq S nbsp In Cohen s original formulation of forcing each forcing condition is a finite set of sentences either of the form a X displaystyle a in X nbsp or a X displaystyle a notin X nbsp that are self consistent i e a X displaystyle a in X nbsp and a X displaystyle a notin X nbsp for the same value of a displaystyle a nbsp do not appear in the same condition This forcing notion is usually called Cohen forcing The forcing poset for Cohen forcing can be formally written as Fin S 2 0 displaystyle operatorname Fin S 2 supseteq 0 nbsp the finite partial functions from S displaystyle S nbsp to 2 df 0 1 displaystyle 2 stackrel text df 0 1 nbsp under reverse inclusion Cohen forcing satisfies the splitting condition because given any condition p displaystyle p nbsp one can always find an element a S displaystyle a in S nbsp not mentioned in p displaystyle p nbsp and add either the sentence a X displaystyle a in X nbsp or a X displaystyle a notin X nbsp to p displaystyle p nbsp to get two new forcing conditions incompatible with each other Another instructive example of a forcing poset is Bor I I displaystyle operatorname Bor I subseteq I nbsp where I 0 1 displaystyle I 0 1 nbsp and Bor I displaystyle operatorname Bor I nbsp is the collection of Borel subsets of I displaystyle I nbsp having non zero Lebesgue measure The generic object associated with this forcing poset is a random real number r 0 1 displaystyle r in 0 1 nbsp It can be shown that r displaystyle r nbsp falls in every Borel subset of 0 1 displaystyle 0 1 nbsp with measure 1 provided that the Borel subset is described in the original unexpanded universe this can be formalized with the concept of Borel codes Each forcing condition can be regarded as a random event with probability equal to its measure Due to the ready intuition this example can provide probabilistic language is sometimes used with other divergent forcing posets Generic filters editEven though each individual forcing condition p displaystyle p nbsp cannot fully determine the generic object X displaystyle X nbsp the set G P displaystyle G subseteq mathbb P nbsp of all true forcing conditions does determine X displaystyle X nbsp In fact without loss of generality G displaystyle G nbsp is commonly considered to be the generic object adjoined to M displaystyle M nbsp so the expanded model is called M G displaystyle M G nbsp It is usually easy enough to show that the originally desired object X displaystyle X nbsp is indeed in the model M G displaystyle M G nbsp Under this convention the concept of generic object can be described in a general way Specifically the set G displaystyle G nbsp should be a generic filter on P displaystyle mathbb P nbsp relative to M displaystyle M nbsp The filter condition means that it makes sense that G displaystyle G nbsp is a set of all true forcing conditions G P displaystyle G subseteq mathbb P nbsp 1 G displaystyle mathbf 1 in G nbsp if p q G displaystyle p geq q in G nbsp then p G displaystyle p in G nbsp if p q G displaystyle p q in G nbsp then there exists an r G displaystyle r in G nbsp such that r p q displaystyle r leq p q nbsp For G displaystyle G nbsp to be generic relative to M displaystyle M nbsp means If D M displaystyle D in M nbsp is a dense subset of P displaystyle mathbb P nbsp that is for each p P displaystyle p in mathbb P nbsp there exists a q D displaystyle q in D nbsp such that q p displaystyle q leq p nbsp then G D displaystyle G cap D neq varnothing nbsp Given that M displaystyle M nbsp is a countable model the existence of a generic filter G displaystyle G nbsp follows from the Rasiowa Sikorski lemma In fact slightly more is true Given a condition p P displaystyle p in mathbb P nbsp one can find a generic filter G displaystyle G nbsp such that p G displaystyle p in G nbsp Due to the splitting condition on P displaystyle mathbb P nbsp if G displaystyle G nbsp is a filter then P G displaystyle mathbb P setminus G nbsp is dense If G M displaystyle G in M nbsp then P G M displaystyle mathbb P setminus G in M nbsp because M displaystyle M nbsp is a model of Z F C displaystyle mathsf ZFC nbsp For this reason a generic filter is never in M displaystyle M nbsp P names and interpretations editAssociated with a forcing poset P displaystyle mathbb P nbsp is the class V P displaystyle V mathbb P nbsp of P displaystyle mathbb P nbsp names A P displaystyle mathbb P nbsp name is a set A displaystyle A nbsp of the form A u p u is a P name and p P displaystyle A subseteq u p mid u text is a mathbb P text name and p in mathbb P nbsp Given any filter G displaystyle G nbsp on P displaystyle mathbb P nbsp the interpretation or valuation map from P displaystyle mathbb P nbsp names is given by val u G val v G p G v p u displaystyle operatorname val u G operatorname val v G mid exists p in G v p in u nbsp The P displaystyle mathbb P nbsp names are in fact an expansion of the universe Given x V displaystyle x in V nbsp one defines x ˇ displaystyle check x nbsp to be the P displaystyle mathbb P nbsp name x ˇ y ˇ 1 y x displaystyle check x check y mathbf 1 mid y in x nbsp Since 1 G displaystyle mathbf 1 in G nbsp it follows that val x ˇ G x displaystyle operatorname val check x G x nbsp In a sense x ˇ displaystyle check x nbsp is a name for x displaystyle x nbsp that does not depend on the specific choice of G displaystyle G nbsp This also allows defining a name for G displaystyle G nbsp without explicitly referring to G displaystyle G nbsp G p ˇ p p P displaystyle underline G check p p mid p in mathbb P nbsp so that val G G val p ˇ G p G G displaystyle operatorname val underline G G operatorname val check p G mid p in G G nbsp Rigorous definitions edit The concepts of P displaystyle mathbb P nbsp names interpretations and x ˇ displaystyle check x nbsp are actually defined by transfinite recursion With displaystyle varnothing nbsp the empty set a 1 displaystyle alpha 1 nbsp the successor ordinal to ordinal a displaystyle alpha nbsp P displaystyle mathcal P nbsp the power set operator and l displaystyle lambda nbsp a limit ordinal define the following hierarchy Name Name a 1 P Name a P Name l Name a a lt l displaystyle begin aligned operatorname Name varnothing amp varnothing operatorname Name alpha 1 amp mathcal P operatorname Name alpha times mathbb P operatorname Name lambda amp bigcup operatorname Name alpha mid alpha lt lambda end aligned nbsp Then the class of P displaystyle mathbb P nbsp names is defined as V P Name a a is an ordinal displaystyle V mathbb P bigcup operatorname Name alpha alpha text is an ordinal nbsp The interpretation map and the map x x ˇ displaystyle x mapsto check x nbsp can similarly be defined with a hierarchical construction Forcing editGiven a generic filter G P displaystyle G subseteq mathbb P nbsp one proceeds as follows The subclass of P displaystyle mathbb P nbsp names in M displaystyle M nbsp is denoted M P displaystyle M mathbb P nbsp Let M G val u G u M P displaystyle M G left operatorname val u G Big u in M mathbb P right nbsp To reduce the study of the set theory of M G displaystyle M G nbsp to that of M displaystyle M nbsp one works with the forcing language which is built up like ordinary first order logic with membership as the binary relation and all the P displaystyle mathbb P nbsp names as constants Define p M P f u 1 u n displaystyle p Vdash M mathbb P varphi u 1 ldots u n nbsp to be read as p displaystyle p nbsp forces f displaystyle varphi nbsp in the model M displaystyle M nbsp with poset P displaystyle mathbb P nbsp where p displaystyle p nbsp is a condition f displaystyle varphi nbsp is a formula in the forcing language and the u i displaystyle u i nbsp s are P displaystyle mathbb P nbsp names to mean that if G displaystyle G nbsp is a generic filter containing p displaystyle p nbsp then M G f val u 1 G val u n G displaystyle M G models varphi operatorname val u 1 G ldots operatorname val u n G nbsp The special case 1 M P f displaystyle mathbf 1 Vdash M mathbb P varphi nbsp is often written as P M P f displaystyle mathbb P Vdash M mathbb P varphi nbsp or simply M P f displaystyle Vdash M mathbb P varphi nbsp Such statements are true in M G displaystyle M G nbsp no matter what G displaystyle G nbsp is What is important is that this external definition of the forcing relation p M P f displaystyle p Vdash M mathbb P varphi nbsp is equivalent to an internal definition within M displaystyle M nbsp defined by transfinite induction specifically displaystyle in nbsp induction over the P displaystyle mathbb P nbsp names on instances of u v displaystyle u in v nbsp and u v displaystyle u v nbsp and then by ordinary induction over the complexity of formulae This has the effect that all the properties of M G displaystyle M G nbsp are really properties of M displaystyle M nbsp and the verification of Z F C displaystyle mathsf ZFC nbsp in M G displaystyle M G nbsp becomes straightforward This is usually summarized as the following three key properties Truth M G f val u 1 G val u n G displaystyle M G models varphi operatorname val u 1 G ldots operatorname val u n G nbsp if and only if it is forced by G displaystyle G nbsp that is for some condition p G displaystyle p in G nbsp we have p M P f u 1 u n displaystyle p Vdash M mathbb P varphi u 1 ldots u n nbsp Definability The statement p M P f u 1 u n displaystyle p Vdash M mathbb P varphi u 1 ldots u n nbsp is definable in M displaystyle M nbsp Coherence p M P f u 1 u n q p q M P f u 1 u n displaystyle p Vdash M mathbb P varphi u 1 ldots u n land q leq p implies q Vdash M mathbb P varphi u 1 ldots u n nbsp Internal definition edit There are many different but equivalent ways to define the forcing relation M P displaystyle Vdash M mathbb P nbsp in M displaystyle M nbsp 4 One way to simplify the definition is to first define a modified forcing relation M P displaystyle Vdash M mathbb P nbsp that is strictly stronger than M P displaystyle Vdash M mathbb P nbsp The modified relation M P displaystyle Vdash M mathbb P nbsp still satisfies the three key properties of forcing but p M P f displaystyle p Vdash M mathbb P varphi nbsp and p M P f displaystyle p Vdash M mathbb P varphi nbsp are not necessarily equivalent even if the first order formulae f displaystyle varphi nbsp and f displaystyle varphi nbsp are equivalent The unmodified forcing relation can then be defined asp M P f p M P f displaystyle p Vdash M mathbb P varphi iff p Vdash M mathbb P neg neg varphi nbsp In fact Cohen s original concept of forcing is essentially M P displaystyle Vdash M mathbb P nbsp rather than M P displaystyle Vdash M mathbb P nbsp 3 The modified forcing relation M P displaystyle Vdash M mathbb P nbsp can be defined recursively as follows p M P u v displaystyle p Vdash M mathbb P u in v nbsp means w q v q p p M P w u displaystyle exists w q in v q geq p wedge p Vdash M mathbb P w u nbsp p M P u v displaystyle p Vdash M mathbb P u neq v nbsp means w q v q p p M P w u w q u q p p M P w v displaystyle exists w q in v q geq p wedge p Vdash M mathbb P w notin u vee exists w q in u q geq p wedge p Vdash M mathbb P w notin v nbsp p M P f displaystyle p Vdash M mathbb P neg varphi nbsp means q p q M P f displaystyle neg exists q leq p q Vdash M mathbb P varphi nbsp p M P f ps displaystyle p Vdash M mathbb P varphi vee psi nbsp means p M P f p M P ps displaystyle p Vdash M mathbb P varphi vee p Vdash M mathbb P psi nbsp p M P x f x displaystyle p Vdash M mathbb P exists x varphi x nbsp means u M P p M P f u displaystyle exists u in M mathbb P p Vdash M mathbb P varphi u nbsp Other symbols of the forcing language can be defined in terms of these symbols For example u v displaystyle u v nbsp means u v displaystyle neg u neq v nbsp x f x displaystyle forall x varphi x nbsp means x f x displaystyle neg exists x neg varphi x nbsp etc Cases 1 and 2 depend on each other and on case 3 but the recursion always refer to P displaystyle mathbb P nbsp names with lesser ranks so transfinite induction allows the definition to go through By construction M P displaystyle Vdash M mathbb P nbsp and thus M P displaystyle Vdash M mathbb P nbsp automatically satisfies Definability The proof that M P displaystyle Vdash M mathbb P nbsp also satisfies Truth and Coherence is by inductively inspecting each of the five cases above Cases 4 and 5 are trivial thanks to the choice of displaystyle vee nbsp and displaystyle exists nbsp as the elementary symbols 5 cases 1 and 2 relies only on the assumption that G displaystyle G nbsp is a filter and only case 3 requires G displaystyle G nbsp to be a generic filter 3 Formally an internal definition of the forcing relation such as the one presented above is actually a transformation of an arbitrary formula f x 1 x n displaystyle varphi x 1 dots x n nbsp to another formula p P f u 1 u n displaystyle p Vdash mathbb P varphi u 1 dots u n nbsp where p displaystyle p nbsp and P displaystyle mathbb P nbsp are additional variables The model M displaystyle M nbsp does not explicitly appear in the transformation note that within M displaystyle M nbsp u M P displaystyle u in M mathbb P nbsp just means u displaystyle u nbsp is a P displaystyle mathbb P nbsp name and indeed one may take this transformation as a syntactic definition of the forcing relation in the universe V displaystyle V nbsp of all sets regardless of any countable transitive model However if one wants to force over some countable transitive model M displaystyle M nbsp then the latter formula should be interpreted under M displaystyle M nbsp i e with all quantifiers ranging only over M displaystyle M nbsp in which case it is equivalent to the external semantic definition of M P displaystyle Vdash M mathbb P nbsp described at the top of this section For any formula f x 1 x n displaystyle varphi x 1 dots x n nbsp there is a theorem T displaystyle T nbsp of the theory Z F C displaystyle mathsf ZFC nbsp for example conjunction of finite number of axioms such that for any countable transitive model M displaystyle M nbsp such that M T displaystyle M models T nbsp and any atomless partial order P M displaystyle mathbb P in M nbsp and any P displaystyle mathbb P nbsp generic filter G displaystyle G nbsp over M displaystyle M nbsp a 1 a n M P p P p M P f a 1 a n M p P f a 1 a n displaystyle forall a 1 ldots a n in M mathbb P forall p in mathbb P p Vdash M mathbb P varphi a 1 dots a n Leftrightarrow M models p Vdash mathbb P varphi a 1 dots a n nbsp This the sense under which the forcing relation is indeed definable in M displaystyle M nbsp Consistency editThe discussion above can be summarized by the fundamental consistency result that given a forcing poset P displaystyle mathbb P nbsp we may assume the existence of a generic filter G displaystyle G nbsp not belonging to the universe V displaystyle V nbsp such that V G displaystyle V G nbsp is again a set theoretic universe that models Z F C displaystyle mathsf ZFC nbsp Furthermore all truths in V G displaystyle V G nbsp may be reduced to truths in V displaystyle V nbsp involving the forcing relation Both styles adjoining G displaystyle G nbsp to either a countable transitive model M displaystyle M nbsp or the whole universe V displaystyle V nbsp are commonly used Less commonly seen is the approach using the internal definition of forcing in which no mention of set or class models is made This was Cohen s original method and in one elaboration it becomes the method of Boolean valued analysis Cohen forcing editThe simplest nontrivial forcing poset is Fin w 2 0 displaystyle operatorname Fin omega 2 supseteq 0 nbsp the finite partial functions from w displaystyle omega nbsp to 2 df 0 1 displaystyle 2 stackrel text df 0 1 nbsp under reverse inclusion That is a condition p displaystyle p nbsp is essentially two disjoint finite subsets p 1 1 displaystyle p 1 1 nbsp and p 1 0 displaystyle p 1 0 nbsp of w displaystyle omega nbsp to be thought of as the yes and no parts of p displaystyle p nbsp with no information provided on values outside the domain of p displaystyle p nbsp q displaystyle q nbsp is stronger than p displaystyle p nbsp means that q p displaystyle q supseteq p nbsp in other words the yes and no parts of q displaystyle q nbsp are supersets of the yes and no parts of p displaystyle p nbsp and in that sense provide more information Let G displaystyle G nbsp be a generic filter for this poset If p displaystyle p nbsp and q displaystyle q nbsp are both in G displaystyle G nbsp then p q displaystyle p cup q nbsp is a condition because G displaystyle G nbsp is a filter This means that g G displaystyle g bigcup G nbsp is a well defined partial function from w displaystyle omega nbsp to 2 displaystyle 2 nbsp because any two conditions in G displaystyle G nbsp agree on their common domain In fact g displaystyle g nbsp is a total function Given n w displaystyle n in omega nbsp let D n p p n is defined displaystyle D n p mid p n text is defined nbsp Then D n displaystyle D n nbsp is dense Given any p displaystyle p nbsp if n displaystyle n nbsp is not in p displaystyle p nbsp s domain adjoin a value for n displaystyle n nbsp the result is in D n displaystyle D n nbsp A condition p G D n displaystyle p in G cap D n nbsp has n displaystyle n nbsp in its domain and since p g displaystyle p subseteq g nbsp we find that g n displaystyle g n nbsp is defined Let X g 1 1 displaystyle X g 1 1 nbsp the set of all yes members of the generic conditions It is possible to give a name for X displaystyle X nbsp directly Let X n ˇ p p n 1 displaystyle underline X left left check n p right mid p n 1 right nbsp Then val X G X displaystyle operatorname val underline X G X nbsp Now suppose that A w displaystyle A subseteq omega nbsp in V displaystyle V nbsp We claim that X A displaystyle X neq A nbsp Let D A p n n Dom p p n 1 n A displaystyle D A p mid exists n n in operatorname Dom p land p n 1 iff n notin A nbsp Then D A displaystyle D A nbsp is dense Given any p displaystyle p nbsp find n displaystyle n nbsp that is not in its domain and adjoin a value for n displaystyle n nbsp contrary to the status of n A displaystyle n in A nbsp Then any p G D A displaystyle p in G cap D A nbsp witnesses X A displaystyle X neq A nbsp To summarize X displaystyle X nbsp is a new subset of w displaystyle omega nbsp necessarily infinite Replacing w displaystyle omega nbsp with w w 2 displaystyle omega times omega 2 nbsp that is consider instead finite partial functions whose inputs are of the form n a displaystyle n alpha nbsp with n lt w displaystyle n lt omega nbsp and a lt w 2 displaystyle alpha lt omega 2 nbsp and whose outputs are 0 displaystyle 0 nbsp or 1 displaystyle 1 nbsp one gets w 2 displaystyle omega 2 nbsp new subsets of w displaystyle omega nbsp They are all distinct by a density argument Given a lt b lt w 2 displaystyle alpha lt beta lt omega 2 nbsp let D a b p n p n a p n b displaystyle D alpha beta p mid exists n p n alpha neq p n beta nbsp then each D a b displaystyle D alpha beta nbsp is dense and a generic condition in it proves that the ath new set disagrees somewhere with the b displaystyle beta nbsp th new set This is not yet the falsification of the continuum hypothesis One must prove that no new maps have been introduced which map w displaystyle omega nbsp onto w 1 displaystyle omega 1 nbsp or w 1 displaystyle omega 1 nbsp onto w 2 displaystyle omega 2 nbsp For example if one considers instead Fin w w 1 displaystyle operatorname Fin omega omega 1 nbsp finite partial functions from w displaystyle omega nbsp to w 1 displaystyle omega 1 nbsp the first uncountable ordinal one gets in V G displaystyle V G nbsp a bijection from w displaystyle omega nbsp to w 1 displaystyle omega 1 nbsp In other words w 1 displaystyle omega 1 nbsp has collapsed and in the forcing extension is a countable ordinal The last step in showing the independence of the continuum hypothesis then is to show that Cohen forcing does not collapse cardinals For this a sufficient combinatorial property is that all of the antichains of the forcing poset are countable The countable chain condition editMain article Countable chain condition An strong antichain A displaystyle A nbsp of P displaystyle mathbb P nbsp is a subset such that if p q A displaystyle p q in A nbsp and p q displaystyle p neq q nbsp then p displaystyle p nbsp and q displaystyle q nbsp are incompatible written p q displaystyle p perp q nbsp meaning there is no r displaystyle r nbsp in P displaystyle mathbb P nbsp such that r p displaystyle r leq p nbsp and r q displaystyle r leq q nbsp In the example on Borel sets incompatibility means that p q displaystyle p cap q nbsp has zero measure In the example on finite partial functions incompatibility means that p q displaystyle p cup q nbsp is not a function in other words p displaystyle p nbsp and q displaystyle q nbsp assign different values to some domain input P displaystyle mathbb P nbsp satisfies the countable chain condition c c c if and only if every antichain in P displaystyle mathbb P nbsp is countable The name which is obviously inappropriate is a holdover from older terminology Some mathematicians write c a c for countable antichain condition It is easy to see that Bor I displaystyle operatorname Bor I nbsp satisfies the c c c because the measures add up to at most 1 displaystyle 1 nbsp Also Fin E 2 displaystyle operatorname Fin E 2 nbsp satisfies the c c c but the proof is more difficult Given an uncountable subfamily W Fin E 2 displaystyle W subseteq operatorname Fin E 2 nbsp shrink W displaystyle W nbsp to an uncountable subfamily W 0 displaystyle W 0 nbsp of sets of size n displaystyle n nbsp for some n lt w displaystyle n lt omega nbsp If p e 1 b 1 displaystyle p e 1 b 1 nbsp for uncountably many p W 0 displaystyle p in W 0 nbsp shrink this to an uncountable subfamily W 1 displaystyle W 1 nbsp and repeat getting a finite set e 1 b 1 e k b k displaystyle e 1 b 1 ldots e k b k nbsp and an uncountable family W k displaystyle W k nbsp of incompatible conditions of size n k displaystyle n k nbsp such that every e displaystyle e nbsp is in Dom p displaystyle operatorname Dom p nbsp for at most countable many p W k displaystyle p in W k nbsp Now pick an arbitrary p W k displaystyle p in W k nbsp and pick from W k displaystyle W k nbsp any q displaystyle q nbsp that is not one of the countably many members that have a domain member in common with p displaystyle p nbsp Then p e 1 b 1 e k b k displaystyle p cup e 1 b 1 ldots e k b k nbsp and q e 1 b 1 e k b k displaystyle q cup e 1 b 1 ldots e k b k nbsp are compatible so W displaystyle W nbsp is not an antichain In other words Fin E 2 displaystyle operatorname Fin E 2 nbsp antichains are countable citation needed The importance of antichains in forcing is that for most purposes dense sets and maximal antichains are equivalent A maximal antichain A displaystyle A nbsp is one that cannot be extended to a larger antichain This means that every element p P displaystyle p in mathbb P nbsp is compatible with some member of A displaystyle A nbsp The existence of a maximal antichain follows from Zorn s Lemma Given a maximal antichain A displaystyle A nbsp let D p P q A p q displaystyle D left p in mathbb P mid exists q in A p leq q right nbsp Then D displaystyle D nbsp is dense and G D displaystyle G cap D neq varnothing nbsp if and only if G A displaystyle G cap A neq varnothing nbsp Conversely given a dense set D displaystyle D nbsp Zorn s Lemma shows that there exists a maximal antichain A D displaystyle A subseteq D nbsp and then G D displaystyle G cap D neq varnothing nbsp if and only if G A displaystyle G cap A neq varnothing nbsp Assume that P displaystyle mathbb P nbsp satisfies the c c c Given x y V displaystyle x y in V span, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.