Forcing

from Wikipedia, the free encyclopedia

Forcing (German also enforcement or enforcement method ) is in the set theory , a technique for constructing models , which is mainly used for relative consistency evidence to lead. It was first developed and used by Paul Cohen in 1963 to prove the independence of the axiom of choice and the continuum hypothesis . This achievement was honored in 1966 with the award of the Fields Medal . The forcing method has been further developed by various mathematicians.

Basic idea

The basic idea of ​​the forcing method is to add a certain set to a given model of set theory (the basic model ) in such a way that a ZFC model is created again (the generic extension ). The construction is so that it can be approximated in the basic model; this enables properties of , such as B. the invalidity of the continuum hypothesis, to be expressed by a language that can be defined in the basic model and thus to be proven.

description

The following is a countable , transitive model of ZFC . For the justification of this assumption see below under Forcing and Relative Consistency Proofs .

Condition sets and generic filters

A set of conditions is understood to be a triple defined in , with a quasi-order on which has the largest element. The elements of hot conditions. A condition is stronger than a condition if . In the application, most of the sets of conditions are antisymmetric, i.e. half orders . However, this need not be required for theory.

A lot is called dense, if

if there is a stronger condition in for every condition or if it is confinal in . A filter is called generic if it matches every dense subset , i.e. if it applies to all dense ones.

From the Rasiowa-Sikorski lemma it follows that for each there is a generic filter that contains. For all interesting sets of conditions is not in .

Names

With transfinite recursion the class of all names is now defined in:

Accordingly, the empty set belongs to , because the right condition is trivially fulfilled for. Next all belong with the name, because due and (M is transitive!) Is and the second part of the condition is true, because we already know (recursion!) That etc.

The totality of the names forms for a real class.

The generic extension

On one defines the two-digit relation by:

Since this definition uses the filter , it is generally not feasible in. Now be defined recursively by

The generic extension is defined as the image of under . So the model is the Mostowski collapse of .

The forcing relation

For a formula and one now defines

(read: " enforces for "),

if for all -generic with applies:

The definition of uses the filter that is generally not in . However, it turns out (definability lemma) that an equivalent definition of in can be carried out:

is a definable class in

Further properties of are:

  • Applies and is , so also (extension lemma).
  • (Truth lemma).

Using this relation, all properties of can be understood as properties of . Now we can show that for every set of conditions and every generic filter there is a model of ZFC. While basic axioms like the pair set axiom , the union set axiom or the existence of the empty set have to be checked directly, one needs the forcing relation for the stronger axioms like the substitution scheme , the discarding scheme or the power set axiom .

For example, if you want to sort out a lot , this is

a name for the amount you are looking for. In addition, the following applies to the model :

  • is transitive;
  • ;
  • ;
  • Contains No New ordinals: ;
  • is the smallest transitive model with and .

Anti-chain condition

There is one difficulty in considering cardinal numbers in : Every cardinal number in that is in is also a cardinal number there. However, the reverse is generally not true. As a result, uncountable quantities can become countable in. However one chooses the conditional set so that each antichain of in is countable ( "countable antichains condition", often ccc named after the English name countable chain condition ) then for each -generischen filter every cardinal and cardinal in the sense of .

More generally, if in is a regular cardinal number and if every anti-chain is smaller than (“P fulfills the -Antiketten-condition”), then every cardinal in is also cardinal in .

Forcing and relative proofs of consistency

In order to show the consistency of a mathematical theory , it is sufficient, according to Gödel's theorem of completeness , to specify a model that fulfills all statements from (this corresponds to the model ). Since, according to Gödel's second incompleteness theorem, the existence of such a model cannot be proven for “strong” theories (i.e. in particular for ), one has to restrict oneself to relative consistency proofs, i.e. additionally presuppose the existence of a model for ZFC (this corresponds to the model ) . On the basis of the Löwenheim-Skolem and Mostowski theorems , there is no restriction to accept this model as countable and transitive.

However, this procedure only provides a relative proof of consistency within ZFC itself (that is, the formula can be proven in ZFC). For a strictly finitistic proof, which consists in the specification of a procedure that converts the proof of a contradiction from concrete to such from, one has to go further: Let a contradiction proof of given. According to the compactness theorem, there is already a finite, contradicting partial theory . Since for the proof that only finitely many axioms are used per axiom, a theory can now be found such that:

  • If is a countable, transitive model of , then for a -generic one holds :
  • , But is still finite.

According to the principle of reflection there is a (again, countable, transitive) model with . So it applies in the generic extension . Since ZFC proves that a model owns but is contradicting, ZFC itself is contradicting itself.

Since it depends on the specific subsystems used or not, it has become established in practice to speak of a model for the whole of ZFC, as we have done here.

Application: Unprovability of the continuum hypothesis

The continuum hypothesis says that the power of the set of natural numbers is equal to that of the first uncountable cardinal number. This statement can neither be refuted nor proven in ZFC. Kurt Gödel had already proven the former in 1939 (see constructability axiom ), while Paul Cohen demonstrated the latter in 1963 with the help of the forcing method he developed. Here is a sketch of the proof:

The power set of the set of natural numbers corresponds reversibly and uniquely to the set of 0-1 sequences, i.e. the set of functions from in to the set that is called in set theory . Their thickness is also denoted by. The smallest uncountable cardinal number is denoted by, the next largest by . The continuum hypothesis then says its negation .

For the proof, let the basic model be a countable, transitive model of ZFC in which the continuum hypothesis holds. The aim is to construct a generic extension in which applies. The idea is to add many pairs of different 0-1 sequences to the basic model , so that the power of in the generic extension is at least . Or to put it another way: You need an injective function from to that "numbers" these many 0-1 sequences. Due to, this corresponds to a function from to .

We therefore define the set of "finite approximations" to such a function as the set of conditions , that is, the set of all partial functions from to with a finite domain:

This amount is ordered by the supersets relationship , so it holds if and when by continues.

If then a -generic filter is considered, one considers . Wegen is also and from the genericity of follows:

  • is a total function
  • The component functions are different functions from to in pairs

In this way, the estimate applies

With the help of the delta lemma one finally shows that the countable antichain condition is fulfilled and therefore remains in as the second uncountable cardinal number. The continuum hypothesis is thus violated in the model .

This has shown that if ZFC is consistent, then the continuum hypothesis cannot be proven in ZFC.

Advanced methods

literature