Forcing (mathematics)

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

The basic idea

The basic idea of ​​forcing method is a given model of set theory ( the basic model ) add a certain amount such that again a model of ZFC arises ( the generic extension ). The construction proceeds so that it can be approximated in the basic model; This enables properties such as the invalidity of the continuum hypothesis to express by a definable in the basic model language and to prove so.

Model M [G]

Below is a countable, transitive model of ZFC. See the justification for this assumption below under " Forcing and relative consistency proofs".

Condition amounts and generic filters

On one condition meant a lot in custom triple, with a quasi-ordering on who owns the largest element. The elements of hot conditions. A condition is stronger than a condition necessary. In the application, most condition quantities are antisymmetric, ie posets. For the theory, however, this need not be required.

A set is dense if

So if for any condition a stronger condition exists in or is cofinal in. A filter is called generic if it is true of every dense subset, if so tight for everyone.

It follows from the lemma Rasiowa - Sikorski that exists for each a generic filter containing. For all the interesting condition amounts not in.

Name

Recursive is now the class of all names defined in:

Thus, one of the empty set, because the right condition is met for a trivial way. Next, all are among the names, is because ( transitive M! ) Because and and the second part of the condition is true, because we already know ( Rekursion! ) that, etc. The totality of the name makes for a real class.

The generic extension

In defining the binary relation by:

As this definition uses the filter, it is generally not feasible. Let now recursively defined by:

The generic extension is defined as the image below. The model is thus the Mostowski collapse of.

The forcing relation

For a formula and then defining

Appropriate, applies to all - generic:

The definition of the used filters, which does not lie generally in the. However, it appears ( Definierbarkeitslemma ) that can perform an equivalent definition of in:

Other features of are:

• Valid and is thus also ( Erweiterungslemma )
• ( Wahrheitslemma )

By means of this relation thus can be understood as properties of all the properties of. Now one can show that for each condition and each quantity - generic filter is a model of ZFC. While fundamental axioms like the pair axiom, the union axiom or the existence of the empty set should be verified directly, one needs the forcing relation for the stronger axioms as the replacement scheme, the separation scheme or the power set axiom.

If you want to weed out a lot by example, so is

A name for the desired amount. In addition, for the model:

• Is transitive
• Contains No New ordinals:
• Is the smallest transitive model with and

Antichain condition

One difficulty in the consideration of cardinal numbers in: Any cardinal number in that is in, there is also a cardinal. However, the converse is not true in general. This has the consequence that may be in countable in uncountable sets. However, we choose the conditional set so that each antichain of is in countable ( " countable antichains condition", often called ccc after the English name countable chain condition) then for every - generic filter every cardinal number Cardinal numbers within the meaning of.

More generally: Is in regular cardinal, and has antichain in smaller cardinality than ("P satisfies the anti - chain condition" ), each cardinal number is also cardinal number in.

Forcing and relative consistency proofs

To show the consistency of a mathematical theory, it is sufficient after Gödel's completeness theorem, a model indicate that meets all of the statements from ( this corresponds to the model). Since after the second Gödel's incompleteness theorem can not be proved the existence of such a model for " strong" theories (ie in particular ), you have to be limited to relative consistency proofs, ie, the existence of a model of ZFC in addition assume ( this corresponds to the model). Because the sets of Löwenheim - Skolem and Mostowski it is not to accept any limitation of this model as a countable and transitive.

However, this method provides only a relative consistency proof within ZFC itself ( that is, the formula is provable in ZFC ). For a strictly finitistic proof, which is to provide a method that converts from concrete proof of a contradiction in such of, you have to continue to delve: Be given a proof by contradiction of. After the compactness theorem, there is already a finite part contradictory theory. As for the evidence that per axiom only a finite number of axioms are used, can now find a theory, so that:

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

After the reflection principle, there is a (again, without limitation countable, transitive ) model M with. So it is in the generic extension. There is contradictory, but ZFC proves that a model has, ZFC is itself contradictory.

Since it does not depend on the subsystems or specifically used, it has established itself in practice to speak of as a model of ZFC quite how we did it here.

Application: unprovability the continuum hypothesis

The continuum hypothesis is the statement, which by definition: The cardinality of the power set of the natural numbers is equal to the first uncountable cardinal number. This statement is neither refuted nor proven. The former Kurt Gödel had already shown in 1939, see Konstruierbarkeitsaxiom, the latter Paul Cohen has shown in 1963 with the help of the forcing method developed for this purpose by him:

Be a countable, transitive model of ZFC. Define in a conditional set

Sorted by. It holds if and only if it is continued by. For a - generic filter now consider. Because is and we have:

• Is total function:
• The component functions are different in pairs.

For both properties, the genericity of responsibility. Now applies to the assessment:

With the help of the delta lemma, one can show that the countable antichain condition is met. Therefore remains in uncountable cardinal number as the second.

So is true in the model, so that the continuum hypothesis is violated in this model. Therefore, the continuum hypothesis in ZFC can not be provable.

Further methods

• Produktforcing
• Iterated Forcing