|
|
(One intermediate revision by one other user not shown) |
Line 1: |
Line 1: |
− | A special method for constructing models of [[Axiomatic set theory|axiomatic set theory]]. It was proposed by P.J. Cohen in 1963 to prove the compatibility of the negation of the [[Continuum hypothesis|continuum hypothesis]], <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407701.png" />, and other set-theoretic assumptions with the axioms of the Zermelo–Fraenkel system ZF [[#References|[1]]]. The forcing method was subsequently simplified and modernized [[#References|[2]]]–[[#References|[6]]]. In particular, it was found that the method was related to the theory of Boolean-valued models (cf. [[Boolean-valued model|Boolean-valued model]]) [[#References|[2]]], [[#References|[3]]] and [[Kripke models|Kripke models]] [[#References|[6]]]. | + | A special method for constructing models of [[Axiomatic set theory|axiomatic set theory]]. It was proposed by P.J. Cohen in 1963 to prove the compatibility of the negation of the [[Continuum hypothesis|continuum hypothesis]], $ \neg \mathsf{CH} $, and other set-theoretic assumptions with the axioms of the Zermelo–Fraenkel system $ \mathsf{ZF} $ ([[#References|[1]]]). The forcing method was subsequently simplified and modernized ([[#References|[2]]]–[[#References|[6]]]). In particular, it was found that the method was related to the theory of [[Boolean-valued model|Boolean-valued models]] ([[#References|[2]]], [[#References|[3]]]) and [[Kripke models|Kripke models]] ([[#References|[6]]]). |
| | | |
| The central concept of the forcing method is the forcing relation | | The central concept of the forcing method is the forcing relation |
| + | $$ |
| + | p \Vdash \phi. |
| + | $$ |
| + | (This is to be read as “the condition $ p $ forces the formula $ \phi $”.) |
| | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407702.png" /></td> </tr></table>
| + | The definition of the forcing relation is preceded by the specification of a language $ \mathcal{L} $ and a partially ordered set $ \mathbb{P} $ of forcing conditions $ p $ with an order relation $ \leq $. The language $ \mathcal{L} $ may contain variables and constants of different sorts (or types). |
| | | |
− | ( "the condition p forces the formula f" ).
| + | The construction of the model of $ \mathsf{ZF} $ proposed by Cohen in which $ \mathsf{CH} $ is violated proceeds as follows. A set $ M $ is called '''[[Transitive set|transitive]]''' if |
| + | $$ |
| + | x \in M \Rightarrow x \subseteq M. |
| + | $$ |
| | | |
− | The definition of the forcing relation is preceded by the specification of a language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407703.png" /> and a partially ordered set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407704.png" /> of forcing conditions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407705.png" /> with order relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407706.png" />. The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407707.png" /> may contain variables and constants of different sorts (or types).
| + | Let $ M $ be a denumerable transitive set that is a model of $ \mathsf{ZF} $, and let $ \lambda \in M $ be an ordinal number in the sense of von Neumann, i.e., $ \lambda = \{ \alpha \mid \alpha < \lambda \} $. Let $ A \subseteq \lambda \times \omega_{0} $ be an arbitrary set (possibly $ A \notin M $), where $ \omega_{0} $ denotes the first infinite ordinal number. If $ X $ is a transitive set, then let $ \operatorname{Def}(X) $ denote the set of all $ X $-definable subsets, i.e., $ \operatorname{Def}(X) = \operatorname{Def}(X,\in \!\! |_{X \times X}) $. A process similar to that of defining [[Gödel constructive set|Gödel constructive sets]] is used to define, via transfinite induction, a set $ {M_{\alpha}}[A] $ for any ordinal number $ \alpha $: |
| + | $$ |
| + | {M_{\alpha}}[A] \stackrel{\text{df}}{=} \bigcup_{\beta < \alpha} \operatorname{Def}({M_{\beta}}[A]) \cup \{ x \in M \cup \{ A\} \mid x \subseteq {M_{\beta}}[A] \}. |
| + | $$ |
| | | |
− | The construction of the model of ZF proposed by Cohen, in which the continuum hypothesis is violated, proceeds as follows. A set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407708.png" /> is called transitive if | + | Let $ M[A] \stackrel{\text{df}}{=} {M_{\alpha_{0}}}[A] $, where $ a_{0} \stackrel{\text{df}}{=} \{ \alpha \in M \mid \alpha \text{ is an ordinal number} \} $. The model of $ \mathsf{ZF} $ in which $ \mathsf{CH} $ is violated is to be found among models of the type $ M[A] $. Let $ \lambda $ be an ordinal number such that the statement “$ \lambda $ is the second uncountable ordinal” is true in $ M $. |
| | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f0407709.png" /></td> </tr></table>
| + | The set of forcing conditions $ \mathbb{P} $ and the relation $ \leq $ are defined by the following equivalences: (a) $ p \in \mathbb{P} \iff p $ is a function defined on some finite subset of $ \lambda \times \omega_{0} $, with values in $ \{ 0,1 \} $; (b) $ p \leq q \iff q $ is an extension of $ p $. The language $ \mathcal{L} $ considered is a so-called '''ramified language''', with many types of variables (each $ \alpha \leq \alpha_{0} $ having its own type of variables running through the set $ {M_{\alpha}}[A] $) and with names (i.e., individual constants) for each set from $ M[A] $. If $ x \in M $, then the name of $ x $ is denoted by $ x^{\vee} $. Let $ a $ be the name of the set $ A $. The forcing relation $ p \Vdash \phi $ is introduced by a definition involving transfinite induction, which has, in particular, the following characteristics: |
| | | |
− | Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077010.png" /> be a denumerable transitive set which is a model of ZF, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077011.png" /> be an ordinal number (in the sense of von Neumann), i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077012.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077013.png" /> be an arbitrary set (possibly <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077014.png" />), where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077015.png" /> is the first infinite ordinal number. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077016.png" /> is a transitive set, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077017.png" /> denote the set of all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077018.png" />-definable subsets (cf. [[Gödel constructive set|Gödel constructive set]]), i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077019.png" />. A process similar to that of constructing Gödel constructive sets is used to inductively define a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077020.png" /> for any ordinal number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077021.png" />,
| + | # $ (p \Vdash \langle \delta,n \rangle^{\vee} \in a) \iff (p(\langle \delta,n \rangle) = \mathbf{1}) $; |
| + | # $ (p \Vdash \neg \phi) \iff \neg (\exists q \geq p)(q \Vdash \phi) $; |
| + | # $ (p \Vdash (\phi \lor \psi)) \iff ((p \Vdash \phi) \lor (p \Vdash \psi)) $; |
| + | # $ (p \Vdash (\phi \land \psi)) \iff ((p \Vdash \phi) \land (p \Vdash \psi)) $; |
| + | # If $ \alpha $ is the type of the variable $ x $, then $ (p \Vdash (\exists x) \phi(x)) \iff (\exists c \in C_{\alpha})(p \Vdash \phi(c)) $, where $ C_{\alpha} $ is the set of all constants of type $ \alpha $. |
| | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077022.png" /></td> </tr></table>
| + | A sequence of forcing conditions in $ \mathbb{P} $, |
| + | $$ |
| + | p_{0} \leq \ldots \leq p_{n} \leq \ldots, |
| + | $$ |
| + | is called '''complete''' if for any closed formula $ \phi $ of $ \mathcal{L} $, one has |
| + | $$ |
| + | \exists n \in \omega_{0}: \qquad (p_{n} \Vdash \phi) \lor (p_{n} \Vdash \neg \phi). |
| + | $$ |
| + | The countability of the set of all closed formulas of $ \mathcal{L} $, together with (2), makes it possible to demonstrate the existence of a complete sequence that begins with an arbitrary forcing condition $ p_{0} \in \mathbb{P} $. |
| | | |
− | Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077023.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077024.png" />. The model of ZF in which the continuum hypothesis is violated is to be found among the models of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077025.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077026.png" /> be an ordinal number such that the statement "l is the second uncountable ordinal" is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077027.png" />.
| + | A set $ A $ contained in $ \lambda \times \omega_{0} $ is called '''generic''' with respect to the model $ M $ if there exists a complete sequence $ (p_{n})_{n \in \omega_{0}} $ such that $ \displaystyle \bigcup_{n < \omega_{0}} p_{n} $ is the characteristic function $ \chi_{A} $ of $ A $. The following two facts about generic sets and the forcing relation are of fundamental importance: |
| | | |
− | The set of forcing conditions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077028.png" /> and the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077029.png" /> is defined by the following equivalences: a) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077030.png" /> is a function defined on some finite subset of the set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077031.png" /> with values in the set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077032.png" />; b) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077033.png" /> is an extension of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077034.png" />. The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077035.png" /> which is taken is a so-called ramified language, with many types of variables (each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077036.png" /> having its own type of variables running through the set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077037.png" />) and containing names (i.e. individual constants) for each set from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077038.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077039.png" />, the name of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077040.png" /> is written as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077041.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077042.png" /> be the name of the set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077043.png" />. The forcing relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077044.png" /> is introduced by an inductive definition which has, in particular, the following characteristics
| + | * If $ A $ is a generic set, then $$ M[A] \models \phi \iff (\exists p \subseteq \chi_{A})(p \Vdash \phi), $$ where $ M[A] \models \phi $ means that formula $ \phi $ is true in $ M[A] $. |
| + | * The relation $$ p \Vdash \phi(c_{1},\ldots,c_{n}), \qquad (\text{where } c_{1},\ldots,c_{n} \text{ are constants in } \mathcal{L}) $$ regarded as a relation among $ p,c_{1},\ldots,c_{n} $, can be expressed in the model $ M $. |
| | | |
− | 1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077045.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077046.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077047.png" />;
| + | In view of the aforementioned facts, it is sufficient to show that the statement |
| + | $$ |
| + | (\forall p)(p \Vdash \neg \neg \phi), \qquad \text{i.e.}, \qquad (\forall p)(\exists q \geq p)(q \Vdash \phi), |
| + | $$ |
| + | is true in the model $ M $, i.e., to prove that $ M[A] \models \phi $. The verification of the validity of the axioms of $ \mathsf{ZF} $ and $ \neg \mathsf{CH} $ in the model $ M[A] $ is based upon this proposition. The verification of $ \neg \mathsf{CH} $ in $ M[A] $ also involves the use of special properties of the set of forcing conditions, which makes it possible to show that: |
| | | |
− | 2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077048.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077049.png" />; | + | # If the ordinal numbers $ \delta_{1},\delta_{2} < \lambda $ are unequal, then one has $$ (\forall p)(\exists q \geq p)(\exists n < \omega_{0})(q(\langle \delta_{1},n \rangle) \neq q(\langle \delta_{2},n \rangle)), $$ that is, $$ A_{\delta_{1}} \neq A_{\delta_{2}}, \qquad \text{where } A_{\delta} \stackrel{\text{df}}{=} \{ n < \omega_{0} \mid \langle \delta,n \rangle \in A \}. $$ |
| + | # $ M[A] \models (\lambda \text{ is the second uncountable ordinal}) $. |
| | | |
− | 3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077050.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077051.png" />;
| + | There is the following relation between forcing and Boolean-valued models: If one introduces the notation |
| + | \begin{gather} |
| + | \| \phi \| \stackrel{\text{df}}{=} \{ p \in \mathbb{P} \mid p \Vdash \neg \neg \phi \}, \\ |
| + | \mathbb{B} \stackrel{\text{df}}{=} \{ X \subseteq \mathbb{P} \mid (\forall p)((p \in X) \iff (\forall q \geq p)(\exists r \geq q)(r \in X)) \}, |
| + | \end{gather} |
| + | then $ (\mathbb{B},\subseteq) $ is a complete [[Boolean algebra|Boolean algebra]], and $ \| \phi \| \in \mathbb{B} $ is the Boolean value of the formula $ \phi $. Hence, to specify a partially ordered set $ (\mathbb{P},\leq) $ and to define the relation $ p \Vdash \neg \neg \phi $ is equivalent to constructing some Boolean-valued model $ \mathfrak{M} $. The analysis of the proof of theorems of the type |
| + | $$ |
| + | M[A] \models \phi_{0}, |
| + | $$ |
| + | where $ \phi_{0} $ is an axiom of $ \mathsf{ZF} $ or $ \neg \mathsf{CH} $, leads to the conclusion that the formulas of $ \mathsf{ZF} $ expressing the theorem |
| + | $$ |
| + | (\forall p)(p \Vdash \neg \neg \phi_{0}), |
| + | $$ |
| + | i.e., $ \| \phi_{0} \| = 1_{\mathbb{B}} $, are deducible from the axioms of $ \mathsf{ZF} $. Therefore, $ \mathfrak{M} $ is a Boolean-valued model for $ \mathsf{ZF} + \neg \mathsf{CH} $, constructed solely with the tools of $ \mathsf{ZF} $. The assumption of countability of a transitive set that is a model of $ \mathsf{ZF} $ and the concept of a generic set are both inessential in the relative consistency proof. |
| | | |
− | 4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077052.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077053.png" />;
| + | It has been shown that the construction of the Boolean-valued model may be simplified ([[#References|[2]]], [[#References|[3]]], [[#References|[5]]]). In particular, the introduction of the ramified language $ \mathcal{L} $ is not necessary. A generic model $ M[A] $ may also be constructed as follows ([[#References|[4]]]): |
| | | |
− | if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077054.png" /> is the type of the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077055.png" />, then | + | A subset $ X $ of a partially ordered set $ (\mathbb{P},\leq) $ is called '''dense''' if |
| + | $$ |
| + | (\forall p)(\exists q \geq p)(q \in X). |
| + | $$ |
| + | Let $ \mathbb{P} $ and the relation $ \leq $ be elements of some denumerable transitive set $ M $ that is a model of $ \mathsf{ZF} $. A subset $ G \subseteq \mathbb{P} $ is called an '''$ M $-generic filter''' if |
| | | |
− | 5) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077056.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077057.png" />: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077058.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077059.png" /> is the set of all constants of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077060.png" />.
| + | # $ ((p \in G) \land (q \leq p)) \Rightarrow (q \in G) $; |
| + | # $ ((p \in G) \land (q \in G)) \Rightarrow (\exists r \in G)((p \leq r) \land (q \leq r)) $; |
| + | # $ ((X \in M) \land (X \text{ is dense in } \mathbb{P})) \Rightarrow X \cap G \neq \varnothing $. |
| | | |
− | A sequence of forcing conditions
| + | Let $ G $ be an $ M $-generic filter in $ \mathbb{P} $. As $ M $ is denumerable, $ G $ exists. In general, $ G \notin M $. A relation $ \in_{G} $ is then defined by the equivalence |
− | | + | $$ |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077061.png" /></td> </tr></table>
| + | x \in_{G} y \iff (\exists p \in G)(\langle x,p \rangle \in y), |
− | | + | $$ |
− | is called complete if for any closed formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077062.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077063.png" /> one has
| + | where $ x $ and $ y $ are arbitrary elements of the model $ M $. |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077064.png" /></td> </tr></table>
| |
− | | |
− | The countability of the set of all closed formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077065.png" /> and 2) above make it possible to demonstrate the existence of a complete sequence, beginning from an arbitrary <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077066.png" />.
| |
− | | |
− | A set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077067.png" /> contained in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077068.png" /> is called generic with respect to the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077069.png" /> if there exists a complete sequence such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077070.png" /> is the characteristic function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077071.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077072.png" />. The following two facts about generic sets and the forcing relation are of fundamental importance.
| |
− | | |
− | I) If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077073.png" /> is a generic set, then
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077074.png" /></td> </tr></table>
| |
− | | |
− | where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077075.png" /> means that formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077076.png" /> is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077077.png" />.
| |
− | | |
− | II) The relation
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077078.png" /></td> </tr></table>
| |
− | | |
− | where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077079.png" /> are constants in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077080.png" />, regarded as a relation between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077081.png" />, can be expressed in the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077082.png" />.
| |
− | | |
− | In view of the above facts, it is sufficient to show that the statement
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077083.png" /></td> </tr></table>
| |
− | | |
− | is true in the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077084.png" />, i.e. to prove that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077085.png" />. The verification of the validity of the axioms of ZF and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077086.png" /> in the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077087.png" /> is based on this proposition. The verification of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077088.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077089.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077090.png" /> are unequal, one has
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077091.png" /></td> </tr></table>
| |
− | | |
− | that is,
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077092.png" /></td> </tr></table>
| |
− | | |
− | (2)) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077093.png" />.
| |
− | | |
− | There is the following relation between forcing and Boolean-valued models.
| |
− | | |
− | If one introduces the notation
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077094.png" /></td> </tr></table>
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077095.png" /></td> </tr></table>
| |
− | | |
− | then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077096.png" /> is a complete [[Boolean algebra|Boolean algebra]], and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077097.png" /> is the Boolean value of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077098.png" />. Thus, to specify a partially ordered set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f04077099.png" /> and to define the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770100.png" /> is equivalent to construct some Boolean-valued model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770101.png" />. The analysis of the proof of theorems of the type:
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770102.png" /></td> </tr></table>
| |
− | | |
− | where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770103.png" /> is an axiom of ZF or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770104.png" />, leads to the conclusion that the formulas of ZF expressing the theorem
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770105.png" /></td> </tr></table>
| |
− | | |
− | i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770106.png" />, are deducible from the axioms of ZF. Thus, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770107.png" /> is a Boolean-valued model for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770108.png" />, 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 [[#References|[2]]], [[#References|[3]]], [[#References|[5]]]. In particular, the introduction of the ramified language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770109.png" /> is not necessary. A generic model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770110.png" /> may also be constructed as follows [[#References|[4]]].
| |
− | | |
− | A subset <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770111.png" /> of a partially ordered set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770112.png" /> is called dense if
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770113.png" /></td> </tr></table>
| |
− | | |
− | Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770114.png" /> and the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770115.png" /> be elements of some denumerable transitive set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770116.png" /> which is a model of ZF. A subset <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770117.png" /> is called an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770119.png" />-generic filter if | |
− | | |
− | (1)) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770120.png" />;
| |
− | | |
− | (2)) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770121.png" />;
| |
− | | |
− | (3)) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770122.png" />.
| |
− | | |
− | Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770123.png" /> be an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770124.png" />-generic filter in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770125.png" />. Since <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770126.png" /> is denumerable, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770127.png" /> exists. In general, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770128.png" />. The relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770129.png" /> is defined by the equivalence
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770130.png" /></td> </tr></table>
| |
− | | |
− | where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770131.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770132.png" /> are arbitrary elements of the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770133.png" />. | |
− | | |
− | Let a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770134.png" /> be defined on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770135.png" /> by the equations
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770136.png" /></td> </tr></table>
| |
| | | |
| + | Let a function $ F_{G} $ be defined on $ M $ by the equations |
| + | $$ |
| + | {F_{G}}(y) \stackrel{\text{df}}{=} \{ {F_{G}}(x) \mid x \in_{G} y \}, |
| + | $$ |
| and let | | and let |
| + | $$ |
| + | N_{G} \stackrel{\text{df}}{=} \{ {F_{G}}(x) \mid x \in M \}. |
| + | $$ |
| + | If $ \phi $ is a closed formula of the language $ \mathsf{ZF} $, supplemented by constants to denote each set from $ M $, then one defines |
| + | $$ |
| + | p \Vdash \phi \iff (\forall G \ni p)(G \text{ is an } M\text{-generic filter} \Rightarrow N_{G} \models \phi). |
| + | $$ |
| + | It can be now shown that: |
| | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770137.png" /></td> </tr></table>
| + | (I) $ N_{G} \models \phi \iff (\exists p \in G)(p \Vdash \phi) $. |
| | | |
− | If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770138.png" /> is a closed formula of the language ZF supplemented by constants to denote each set from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770139.png" />, one defines
| + | (II) The relation $ p \Vdash \phi(c_{1},\ldots,c_{n}) $ can be defined in the model $ M $ for each formula $ \phi $. |
| | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770140.png" /></td> </tr></table>
| + | By using solely (I) and (II), and basing oneself on the fact that $ M $ is a model of $ \mathsf{ZF} $, it is possible to establish that $ N_{G} $ is a model of $ \mathsf{ZF} $. If $ \mathbb{P} $ is defined by the equivalences (a) and (b) given much earlier on, then one has $ N_{G} \models \neg \mathsf{CH} $, that $ \displaystyle \bigcup G $ is the characteristic function of some set $ A \subseteq \lambda \times \omega_{0} $, and $ M[A] = N_{G} $. The relation $ p \Vdash \phi $, which is definable in $ M $, does not satisfy points (3) and (5) of Cohen’s definition of the forcing relation. One has instead |
| + | $$ |
| + | (p \Vdash (\exists x) \phi(x)) \iff (\forall p' \geq p)(\exists p'' \geq p')(\exists a \in M)(p'' \Vdash \phi(a)). |
| + | $$ |
| + | If it is assumed that |
| + | $$ |
| + | \| \phi \| \stackrel{\text{df}}{=} \{ p \in \mathbb{P} \mid p \Vdash \phi \}, |
| + | $$ |
| + | then a Boolean-valued model for $ \mathsf{ZF} + \neg \mathsf{CH} $ is obtained that is definable in $ M $ and has a Boolean algebra $ \mathbb{B} $ that is identical with that of Cohen. |
| | | |
− | It can be shown that
| + | Therefore, the forcing method consists, in fact, of constructing a $ \mathbb{B} $-valued model and a homomorphism, which preserves certain infinite unions and intersections of the algebra $ \mathbb{B} $, into the two-element algebra $ \{ 0,1 \} $. For applications of the forcing method in set theory see, for example, [[#References|[2]]]. |
| | | |
− | (I)) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770141.png" />.
| + | ====References==== |
| | | |
− | (II)) The relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770142.png" /> can be defined in the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770143.png" /> for each formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770144.png" />.
| + | <table> |
| + | <TR><TD valign="top">[1]</TD> <TD valign="top"> P.J. Cohen, “Set theory and the continuum hypothesis”, Benjamin (1966).</TD></TR> |
| + | <TR><TD valign="top">[2]</TD> <TD valign="top"> T.J. Jech, “Lectures in set theory: with particular emphasis on the method of forcing”, ''Lect. notes in math.'', '''217''', Springer (1971).</TD></TR> |
| + | <TR><TD valign="top">[3]</TD> <TD valign="top"> G. Takeuti, W.M. Zaring, “Axiomatic set theory”, Springer (1973).</TD></TR> |
| + | <TR><TD valign="top">[4]</TD> <TD valign="top"> J.R. Shoenfield, “Mathematical logic”, Addison-Wesley (1967).</TD></TR> |
| + | <TR><TD valign="top">[5]</TD> <TD valign="top"> 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.</TD></TR> |
| + | <TR><TD valign="top">[6]</TD> <TD valign="top"> M.C. Fitting, “Intuitionistic logic, model theory and forcing”, North-Holland (1969).</TD></TR> |
| + | </table> |
| | | |
− | By using solely (I) and (II) and basing oneself on the fact that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770145.png" /> is a model of ZF, it is possible to establish that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770146.png" /> is a model of ZF. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770147.png" /> is defined by the equivalences a) and b), one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770148.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770149.png" /> is the characteristic function of some set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770150.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770151.png" />. The relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770152.png" />, which is definable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770153.png" />, does not satisfy points 3) and 5) of Cohen's definition of the forcing relation. One has
| + | ====Comments==== |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770154.png" /></td> </tr></table>
| |
− | | |
− | If one assumes that
| |
− | | |
− | <table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770155.png" /></td> </tr></table>
| |
− | | |
− | a Boolean-valued model for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770156.png" /> is obtained which is definable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770157.png" /> and has a Boolean algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770158.png" /> which is identical with that of Cohen.
| |
| | | |
− | Thus, the forcing method consists in fact of constructing a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770159.png" />-model and a homomorphism which preserves certain infinite unions and intersections of the algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770160.png" /> into the two-element algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040770/f040770161.png" />. For applications of the forcing method in set theory see, for example, [[#References|[2]]].
| + | For a modern elementary introduction with applications, see [[#References|[a1]]]. A quicker, though incomplete, account is [[#References|[a3]]]. [[#References|[a2]]] presents the Boolean-valued approach mentioned above. |
| | | |
| ====References==== | | ====References==== |
− | <table><TR><TD valign="top">[1]</TD> <TD valign="top"> P.J. Cohen, "Set theory and the continuum hypothesis" , Benjamin (1966)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top"> T.J. Jech, "Lectures in set theory: with particular emphasis on the method of forcing" , ''Lect. notes in math.'' , '''217''' , Springer (1971)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top"> G. Takeuti, W.M. Zaring, "Axiomatic set theory" , Springer (1973)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top"> J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top"> 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</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top"> M.C. Fitting, "Intuitionistic logic, model theory and forcing" , North-Holland (1969)</TD></TR></table>
| |
− |
| |
− |
| |
− |
| |
− | ====Comments====
| |
− | For a modern elementary introduction with applications see [[#References|[a1]]]. A quicker, though incomplete, account is [[#References|[a3]]]. [[#References|[a2]]] presents the Boolean-valued approach mentioned above.
| |
| | | |
− | ====References====
| + | <table> |
− | <table><TR><TD valign="top">[a1]</TD> <TD valign="top"> K. Kunen, "Set theory, an introduction to independence proofs" , North-Holland (1980)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top"> J.L. Bell, "Boolean-valued models and independence proofs in set theory" , Oxford Univ. Press (1977)</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top"> J.P. Burgess, "Forcing" J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland (1977) pp. 403–452</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top"> T.J. Jech, "Set theory" , Acad. Press (1978) pp. 523ff (Translated from German)</TD></TR></table> | + | <TR><TD valign="top">[a1]</TD> <TD valign="top"> K. Kunen, “Set theory, an introduction to independence proofs”, North-Holland (1980).</TD></TR> |
| + | <TR><TD valign="top">[a2]</TD> <TD valign="top"> J.L. Bell, “Boolean-valued models and independence proofs in set theory”, Oxford Univ. Press (1977).</TD></TR> |
| + | <TR><TD valign="top">[a3]</TD> <TD valign="top"> J.P. Burgess, “Forcing”, J. Barwise (ed.), ''Handbook of mathematical logic'', North-Holland (1977), pp. 403–452.</TD></TR> |
| + | <TR><TD valign="top">[a4]</TD> <TD valign="top"> T.J. Jech, “Set theory”, Acad. Press (1978), pp. 523ff. (Translated from German)</TD></TR> |
| + | </table> |
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, $ \neg \mathsf{CH} $, and other set-theoretic assumptions with the axioms of the Zermelo–Fraenkel system $ \mathsf{ZF} $ ([1]). The forcing method was subsequently simplified and modernized ([2]–[6]). In particular, it was found that the method was related to the theory of Boolean-valued models ([2], [3]) and Kripke models ([6]).
The central concept of the forcing method is the forcing relation
$$
p \Vdash \phi.
$$
(This is to be read as “the condition $ p $ forces the formula $ \phi $”.)
The definition of the forcing relation is preceded by the specification of a language $ \mathcal{L} $ and a partially ordered set $ \mathbb{P} $ of forcing conditions $ p $ with an order relation $ \leq $. The language $ \mathcal{L} $ may contain variables and constants of different sorts (or types).
The construction of the model of $ \mathsf{ZF} $ proposed by Cohen in which $ \mathsf{CH} $ is violated proceeds as follows. A set $ M $ is called transitive if
$$
x \in M \Rightarrow x \subseteq M.
$$
Let $ M $ be a denumerable transitive set that is a model of $ \mathsf{ZF} $, and let $ \lambda \in M $ be an ordinal number in the sense of von Neumann, i.e., $ \lambda = \{ \alpha \mid \alpha < \lambda \} $. Let $ A \subseteq \lambda \times \omega_{0} $ be an arbitrary set (possibly $ A \notin M $), where $ \omega_{0} $ denotes the first infinite ordinal number. If $ X $ is a transitive set, then let $ \operatorname{Def}(X) $ denote the set of all $ X $-definable subsets, i.e., $ \operatorname{Def}(X) = \operatorname{Def}(X,\in \!\! |_{X \times X}) $. A process similar to that of defining Gödel constructive sets is used to define, via transfinite induction, a set $ {M_{\alpha}}[A] $ for any ordinal number $ \alpha $:
$$
{M_{\alpha}}[A] \stackrel{\text{df}}{=} \bigcup_{\beta < \alpha} \operatorname{Def}({M_{\beta}}[A]) \cup \{ x \in M \cup \{ A\} \mid x \subseteq {M_{\beta}}[A] \}.
$$
Let $ M[A] \stackrel{\text{df}}{=} {M_{\alpha_{0}}}[A] $, where $ a_{0} \stackrel{\text{df}}{=} \{ \alpha \in M \mid \alpha \text{ is an ordinal number} \} $. The model of $ \mathsf{ZF} $ in which $ \mathsf{CH} $ is violated is to be found among models of the type $ M[A] $. Let $ \lambda $ be an ordinal number such that the statement “$ \lambda $ is the second uncountable ordinal” is true in $ M $.
The set of forcing conditions $ \mathbb{P} $ and the relation $ \leq $ are defined by the following equivalences: (a) $ p \in \mathbb{P} \iff p $ is a function defined on some finite subset of $ \lambda \times \omega_{0} $, with values in $ \{ 0,1 \} $; (b) $ p \leq q \iff q $ is an extension of $ p $. The language $ \mathcal{L} $ considered is a so-called ramified language, with many types of variables (each $ \alpha \leq \alpha_{0} $ having its own type of variables running through the set $ {M_{\alpha}}[A] $) and with names (i.e., individual constants) for each set from $ M[A] $. If $ x \in M $, then the name of $ x $ is denoted by $ x^{\vee} $. Let $ a $ be the name of the set $ A $. The forcing relation $ p \Vdash \phi $ is introduced by a definition involving transfinite induction, which has, in particular, the following characteristics:
- $ (p \Vdash \langle \delta,n \rangle^{\vee} \in a) \iff (p(\langle \delta,n \rangle) = \mathbf{1}) $;
- $ (p \Vdash \neg \phi) \iff \neg (\exists q \geq p)(q \Vdash \phi) $;
- $ (p \Vdash (\phi \lor \psi)) \iff ((p \Vdash \phi) \lor (p \Vdash \psi)) $;
- $ (p \Vdash (\phi \land \psi)) \iff ((p \Vdash \phi) \land (p \Vdash \psi)) $;
- If $ \alpha $ is the type of the variable $ x $, then $ (p \Vdash (\exists x) \phi(x)) \iff (\exists c \in C_{\alpha})(p \Vdash \phi(c)) $, where $ C_{\alpha} $ is the set of all constants of type $ \alpha $.
A sequence of forcing conditions in $ \mathbb{P} $,
$$
p_{0} \leq \ldots \leq p_{n} \leq \ldots,
$$
is called complete if for any closed formula $ \phi $ of $ \mathcal{L} $, one has
$$
\exists n \in \omega_{0}: \qquad (p_{n} \Vdash \phi) \lor (p_{n} \Vdash \neg \phi).
$$
The countability of the set of all closed formulas of $ \mathcal{L} $, together with (2), makes it possible to demonstrate the existence of a complete sequence that begins with an arbitrary forcing condition $ p_{0} \in \mathbb{P} $.
A set $ A $ contained in $ \lambda \times \omega_{0} $ is called generic with respect to the model $ M $ if there exists a complete sequence $ (p_{n})_{n \in \omega_{0}} $ such that $ \displaystyle \bigcup_{n < \omega_{0}} p_{n} $ is the characteristic function $ \chi_{A} $ of $ A $. The following two facts about generic sets and the forcing relation are of fundamental importance:
- If $ A $ is a generic set, then $$ M[A] \models \phi \iff (\exists p \subseteq \chi_{A})(p \Vdash \phi), $$ where $ M[A] \models \phi $ means that formula $ \phi $ is true in $ M[A] $.
- The relation $$ p \Vdash \phi(c_{1},\ldots,c_{n}), \qquad (\text{where } c_{1},\ldots,c_{n} \text{ are constants in } \mathcal{L}) $$ regarded as a relation among $ p,c_{1},\ldots,c_{n} $, can be expressed in the model $ M $.
In view of the aforementioned facts, it is sufficient to show that the statement
$$
(\forall p)(p \Vdash \neg \neg \phi), \qquad \text{i.e.}, \qquad (\forall p)(\exists q \geq p)(q \Vdash \phi),
$$
is true in the model $ M $, i.e., to prove that $ M[A] \models \phi $. The verification of the validity of the axioms of $ \mathsf{ZF} $ and $ \neg \mathsf{CH} $ in the model $ M[A] $ is based upon this proposition. The verification of $ \neg \mathsf{CH} $ in $ M[A] $ also involves the use of special properties of the set of forcing conditions, which makes it possible to show that:
- If the ordinal numbers $ \delta_{1},\delta_{2} < \lambda $ are unequal, then one has $$ (\forall p)(\exists q \geq p)(\exists n < \omega_{0})(q(\langle \delta_{1},n \rangle) \neq q(\langle \delta_{2},n \rangle)), $$ that is, $$ A_{\delta_{1}} \neq A_{\delta_{2}}, \qquad \text{where } A_{\delta} \stackrel{\text{df}}{=} \{ n < \omega_{0} \mid \langle \delta,n \rangle \in A \}. $$
- $ M[A] \models (\lambda \text{ is the second uncountable ordinal}) $.
There is the following relation between forcing and Boolean-valued models: If one introduces the notation
\begin{gather}
\| \phi \| \stackrel{\text{df}}{=} \{ p \in \mathbb{P} \mid p \Vdash \neg \neg \phi \}, \\
\mathbb{B} \stackrel{\text{df}}{=} \{ X \subseteq \mathbb{P} \mid (\forall p)((p \in X) \iff (\forall q \geq p)(\exists r \geq q)(r \in X)) \},
\end{gather}
then $ (\mathbb{B},\subseteq) $ is a complete Boolean algebra, and $ \| \phi \| \in \mathbb{B} $ is the Boolean value of the formula $ \phi $. Hence, to specify a partially ordered set $ (\mathbb{P},\leq) $ and to define the relation $ p \Vdash \neg \neg \phi $ is equivalent to constructing some Boolean-valued model $ \mathfrak{M} $. The analysis of the proof of theorems of the type
$$
M[A] \models \phi_{0},
$$
where $ \phi_{0} $ is an axiom of $ \mathsf{ZF} $ or $ \neg \mathsf{CH} $, leads to the conclusion that the formulas of $ \mathsf{ZF} $ expressing the theorem
$$
(\forall p)(p \Vdash \neg \neg \phi_{0}),
$$
i.e., $ \| \phi_{0} \| = 1_{\mathbb{B}} $, are deducible from the axioms of $ \mathsf{ZF} $. Therefore, $ \mathfrak{M} $ is a Boolean-valued model for $ \mathsf{ZF} + \neg \mathsf{CH} $, constructed solely with the tools of $ \mathsf{ZF} $. The assumption of countability of a transitive set that is a model of $ \mathsf{ZF} $ and the concept of a generic set are both inessential in the relative consistency proof.
It has been shown that the construction of the Boolean-valued model may be simplified ([2], [3], [5]). In particular, the introduction of the ramified language $ \mathcal{L} $ is not necessary. A generic model $ M[A] $ may also be constructed as follows ([4]):
A subset $ X $ of a partially ordered set $ (\mathbb{P},\leq) $ is called dense if
$$
(\forall p)(\exists q \geq p)(q \in X).
$$
Let $ \mathbb{P} $ and the relation $ \leq $ be elements of some denumerable transitive set $ M $ that is a model of $ \mathsf{ZF} $. A subset $ G \subseteq \mathbb{P} $ is called an $ M $-generic filter if
- $ ((p \in G) \land (q \leq p)) \Rightarrow (q \in G) $;
- $ ((p \in G) \land (q \in G)) \Rightarrow (\exists r \in G)((p \leq r) \land (q \leq r)) $;
- $ ((X \in M) \land (X \text{ is dense in } \mathbb{P})) \Rightarrow X \cap G \neq \varnothing $.
Let $ G $ be an $ M $-generic filter in $ \mathbb{P} $. As $ M $ is denumerable, $ G $ exists. In general, $ G \notin M $. A relation $ \in_{G} $ is then defined by the equivalence
$$
x \in_{G} y \iff (\exists p \in G)(\langle x,p \rangle \in y),
$$
where $ x $ and $ y $ are arbitrary elements of the model $ M $.
Let a function $ F_{G} $ be defined on $ M $ by the equations
$$
{F_{G}}(y) \stackrel{\text{df}}{=} \{ {F_{G}}(x) \mid x \in_{G} y \},
$$
and let
$$
N_{G} \stackrel{\text{df}}{=} \{ {F_{G}}(x) \mid x \in M \}.
$$
If $ \phi $ is a closed formula of the language $ \mathsf{ZF} $, supplemented by constants to denote each set from $ M $, then one defines
$$
p \Vdash \phi \iff (\forall G \ni p)(G \text{ is an } M\text{-generic filter} \Rightarrow N_{G} \models \phi).
$$
It can be now shown that:
(I) $ N_{G} \models \phi \iff (\exists p \in G)(p \Vdash \phi) $.
(II) The relation $ p \Vdash \phi(c_{1},\ldots,c_{n}) $ can be defined in the model $ M $ for each formula $ \phi $.
By using solely (I) and (II), and basing oneself on the fact that $ M $ is a model of $ \mathsf{ZF} $, it is possible to establish that $ N_{G} $ is a model of $ \mathsf{ZF} $. If $ \mathbb{P} $ is defined by the equivalences (a) and (b) given much earlier on, then one has $ N_{G} \models \neg \mathsf{CH} $, that $ \displaystyle \bigcup G $ is the characteristic function of some set $ A \subseteq \lambda \times \omega_{0} $, and $ M[A] = N_{G} $. The relation $ p \Vdash \phi $, which is definable in $ M $, does not satisfy points (3) and (5) of Cohen’s definition of the forcing relation. One has instead
$$
(p \Vdash (\exists x) \phi(x)) \iff (\forall p' \geq p)(\exists p'' \geq p')(\exists a \in M)(p'' \Vdash \phi(a)).
$$
If it is assumed that
$$
\| \phi \| \stackrel{\text{df}}{=} \{ p \in \mathbb{P} \mid p \Vdash \phi \},
$$
then a Boolean-valued model for $ \mathsf{ZF} + \neg \mathsf{CH} $ is obtained that is definable in $ M $ and has a Boolean algebra $ \mathbb{B} $ that is identical with that of Cohen.
Therefore, the forcing method consists, in fact, of constructing a $ \mathbb{B} $-valued model and a homomorphism, which preserves certain infinite unions and intersections of the algebra $ \mathbb{B} $, into the two-element algebra $ \{ 0,1 \} $. For applications of the forcing method in set theory see, for example, [2].
References
[1] | P.J. Cohen, “Set theory and the continuum hypothesis”, Benjamin (1966). |
[2] | T.J. Jech, “Lectures in set theory: with particular emphasis on the method of forcing”, Lect. notes in math., 217, Springer (1971). |
[3] | G. Takeuti, W.M. Zaring, “Axiomatic set theory”, Springer (1973). |
[4] | J.R. Shoenfield, “Mathematical logic”, Addison-Wesley (1967). |
[5] | 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. |
[6] | M.C. Fitting, “Intuitionistic logic, model theory and forcing”, North-Holland (1969). |
For a modern elementary introduction with applications, see [a1]. A quicker, though incomplete, account is [a3]. [a2] presents the Boolean-valued approach mentioned above.
References
[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) |