A special method for constructing models of axiomatic set theory. It was proposed by P.J. Cohen in 1963 to prove the compatibility of the negation of the continuum hypothesis, , and other set-theoretic assumptions with the axioms of the Zermelo–Fraenkel system ZF . The forcing method was subsequently simplified and modernized –. In particular, it was found that the method was related to the theory of Boolean-valued models (cf. Boolean-valued model) ,  and Kripke models .
The central concept of the forcing method is the forcing relation
( "the condition p forces the formula f" ).
The definition of the forcing relation is preceded by the specification of a language and a partially ordered set of forcing conditions with order relation . The language may contain variables and constants of different sorts (or types).
The construction of the model of ZF proposed by Cohen, in which the continuum hypothesis is violated, proceeds as follows. A set is called transitive if
Let be a denumerable transitive set which is a model of ZF, and let be an ordinal number (in the sense of von Neumann), i.e. . Let be an arbitrary set (possibly ), where is the first infinite ordinal number. If is a transitive set, let denote the set of all -definable subsets (cf. Gödel constructive set), i.e. . A process similar to that of constructing Gödel constructive sets is used to inductively define a set for any ordinal number ,
Let , where . The model of ZF in which the continuum hypothesis is violated is to be found among the models of type . Let be an ordinal number such that the statement "l is the second uncountable ordinal" is true in .
The set of forcing conditions and the relation is defined by the following equivalences: a) is a function defined on some finite subset of the set with values in the set ; b) is an extension of . The language which is taken is a so-called ramified language, with many types of variables (each having its own type of variables running through the set ) and containing names (i.e. individual constants) for each set from . If , the name of is written as . Let be the name of the set . The forcing relation is introduced by an inductive definition which has, in particular, the following characteristics
if is the type of the variable , then
5) : , where is the set of all constants of type .
A sequence of forcing conditions
is called complete if for any closed formula of one has
The countability of the set of all closed formulas of and 2) above make it possible to demonstrate the existence of a complete sequence, beginning from an arbitrary .
A set contained in is called generic with respect to the model if there exists a complete sequence such that is the characteristic function of . The following two facts about generic sets and the forcing relation are of fundamental importance.
I) If is a generic set, then
where means that formula is true in .
II) The relation
where are constants in , regarded as a relation between , can be expressed in the model .
In view of the above facts, it is sufficient to show that the statement
is true in the model , i.e. to prove that . The verification of the validity of the axioms of ZF and in the model is based on this proposition. The verification of in also involves the use of the special properties of the set of forcing conditions, which makes it possible to show that:
(1)) If the ordinal numbers are unequal, one has
There is the following relation between forcing and Boolean-valued models.
If one introduces the notation
then is a complete Boolean algebra, and is the Boolean value of the formula . Thus, to specify a partially ordered set and to define the relation is equivalent to construct some Boolean-valued model . The analysis of the proof of theorems of the type:
where is an axiom of ZF or , leads to the conclusion that the formulas of ZF expressing the theorem
i.e. , are deducible from the axioms of ZF. Thus, is a Boolean-valued model for , constructed with the tools of ZF. The assumption of the existence of a denumerable transitive set which is a model of ZF, and the concept of a generic set, are both unessential in the proof of the relative consistency.
It has been shown that the construction of the Boolean-valued model may be simplified , , . In particular, the introduction of the ramified language is not necessary. A generic model may also be constructed as follows .
A subset of a partially ordered set is called dense if
Let and the relation be elements of some denumerable transitive set which is a model of ZF. A subset is called an -generic filter if
Let be an -generic filter in . Since is denumerable, exists. In general, . The relation is defined by the equivalence
where and are arbitrary elements of the model .
Let a function be defined on by the equations
If is a closed formula of the language ZF supplemented by constants to denote each set from , one defines
It can be shown that
(II)) The relation can be defined in the model for each formula .
By using solely (I) and (II) and basing oneself on the fact that is a model of ZF, it is possible to establish that is a model of ZF. If is defined by the equivalences a) and b), one has and is the characteristic function of some set and . The relation , which is definable in , does not satisfy points 3) and 5) of Cohen's definition of the forcing relation. One has
If one assumes that
a Boolean-valued model for is obtained which is definable in and has a Boolean algebra which is identical with that of Cohen.
Thus, the forcing method consists in fact of constructing a -model and a homomorphism which preserves certain infinite unions and intersections of the algebra into the two-element algebra . For applications of the forcing method in set theory see, for example, .
|||P.J. Cohen, "Set theory and the continuum hypothesis" , Benjamin (1966)|
|||T.J. Jech, "Lectures in set theory: with particular emphasis on the method of forcing" , Lect. notes in math. , 217 , Springer (1971)|
|||G. Takeuti, W.M. Zaring, "Axiomatic set theory" , Springer (1973)|
|||J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)|
|||Yu.I. Manin, "The problem of the continuum" J. Soviet Math. , 5 : 4 (1976) pp. 451–502 Itogi Nauk. i Tekhn. Sovrem. Problemy , 5 (1975) pp. 5–73|
|||M.C. Fitting, "Intuitionistic logic, model theory and forcing" , North-Holland (1969)|
|[a1]||K. Kunen, "Set theory, an introduction to independence proofs" , North-Holland (1980)|
|[a2]||J.L. Bell, "Boolean-valued models and independence proofs in set theory" , Oxford Univ. Press (1977)|
|[a3]||J.P. Burgess, "Forcing" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 403–452|
|[a4]||T.J. Jech, "Set theory" , Acad. Press (1978) pp. 523ff (Translated from German)|
Forcing method. V.N. Grishin (originator), Encyclopedia of Mathematics. URL: http://www.encyclopediaofmath.org/index.php?title=Forcing_method&oldid=15569