Editing Forcing (mathematics) (section)

== Forcing ==

Given a generic filter <math> G \subseteq \mathbb{P}</math>, one proceeds as follows. The subclass of <math> \mathbb{P} </math>-names in <math> M </math> is denoted <math> M^{(\mathbb{P})} </math>. Let

:<math> M[G] = \left\{ \operatorname{val}(u,G) ~ \Big| ~ u \in M^{(\mathbb{P})} \right\}.</math>

To reduce the study of the set theory of <math> M[G] </math> to that of <math> M </math>, one works with the "forcing language", which is built up like ordinary [[first-order logic]], with membership as the binary relation and all the <math> \mathbb{P} </math>-names as constants.

Define <math> p \Vdash_{M,\mathbb{P}} \varphi(u_1,\ldots,u_n) </math> (to be read as "<math>p</math> forces <math> \varphi </math> in the model <math> M </math> with poset <math> \mathbb{P} </math>"), where <math> p </math> is a condition, <math> \varphi </math> is a formula in the forcing language, and the <math> u_{i} </math>'s are <math> \mathbb{P} </math>-names, to mean that if <math> G </math> is a generic filter containing <math> p </math>, then <math> M[G] \models \varphi(\operatorname{val}(u_1,G),\ldots,\operatorname{val}(u_{n},G)) </math>. The special case <math> \mathbf{1} \Vdash_{M,\mathbb{P}} \varphi </math> is often written as "<math> \mathbb{P} \Vdash_{M,\mathbb{P}} \varphi </math>" or simply "<math> \Vdash_{M,\mathbb{P}} \varphi </math>". Such statements are true in <math> M[G] </math>, no matter what <math> G </math> is.

What is important is that this '''external''' definition of the forcing relation <math> p \Vdash_{M,\mathbb{P}} \varphi </math> is equivalent to an '''internal''' definition within <math> M </math>, defined by [[transfinite induction]] (specifically [[Epsilon-induction|<math>\in</math>-induction]]) over the <math> \mathbb{P} </math>-names on instances of <math> u \in v </math> and <math> u = v </math>, and then by ordinary induction over the complexity of formulae. This has the effect that all the properties of <math> M[G] </math> are really properties of <math> M </math>, and the verification of <math> \mathsf{ZFC} </math> in <math> M[G] </math> becomes straightforward. This is usually summarized as the following three key properties:

*'''Truth''': <math> M[G] \models \varphi(\operatorname{val}(u_1,G),\ldots,\operatorname{val}(u_n,G)) </math> [[if and only if]] it is forced by <math> G </math>, that is, for some condition <math> p \in G </math>, we have <math> p \Vdash_{M,\mathbb{P}} \varphi(u_1,\ldots,u_n) </math>.
*'''Definability''': The statement "<math> p \Vdash_{M,\mathbb{P}} \varphi(u_1,\ldots,u_n) </math>" is definable in <math> M </math>.
*'''Coherence''': <math> 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) </math>.

=== Internal definition ===
There are many different but equivalent ways to define the forcing relation <math>\Vdash_{M,\mathbb{P}}</math> in <math>M</math>.{{sfn|Kunen|1980}} One way to simplify the definition is to first define a modified forcing relation <math>\Vdash_{M,\mathbb{P}}^*</math> that is strictly stronger than <math>\Vdash_{M,\mathbb{P}}</math>. The modified relation <math>\Vdash_{M,\mathbb{P}}^*</math> still satisfies the three key properties of forcing, but <math>p \Vdash_{M,\mathbb{P}}^* \varphi</math> and <math>p \Vdash_{M,\mathbb{P}}^* \varphi'</math> are not necessarily equivalent even if the first-order formulae <math>\varphi</math> and <math>\varphi'</math> are equivalent. The unmodified forcing relation can then be defined as
<math display="block">p\Vdash_{M,\mathbb P} \varphi \iff p\Vdash_{M,\mathbb P}^* \neg \neg \varphi.</math>
In fact, Cohen's original concept of forcing is essentially <math>\Vdash_{M,\mathbb{P}}^*</math> rather than <math>\Vdash_{M,\mathbb{P}}</math>.{{sfn|Shoenfield|1971}}

The modified forcing relation <math>\Vdash_{M,\mathbb{P}}^*</math> can be defined recursively as follows:
# <math>p \Vdash_{M,\mathbb{P}}^* u \in v</math> means <math>(\exists (w, q) \in v) (q \ge p \wedge p \Vdash_{M,\mathbb{P}}^* w = u).</math>
# <math>p \Vdash_{M,\mathbb{P}}^* u \ne v</math> means <math>(\exists (w, q) \in v) (q \ge p \wedge p \Vdash_{M,\mathbb{P}}^* w \notin u) \vee (\exists (w, q) \in u) (q \ge p \wedge p \Vdash_{M,\mathbb{P}}^* w \notin v).</math>
# <math>p \Vdash_{M,\mathbb{P}}^* \neg \varphi</math> means <math>\neg (\exists q \le p) (q \Vdash_{M,\mathbb{P}}^* \varphi).</math>
# <math>p \Vdash_{M,\mathbb{P}}^* (\varphi \vee \psi)</math> means <math>(p \Vdash_{M,\mathbb{P}}^* \varphi) \vee (p \Vdash_{M,\mathbb{P}}^* \psi).</math>
# <math>p \Vdash_{M,\mathbb{P}}^* \exists x\, \varphi(x)</math> means <math>(\exists u \in M^{(\mathbb{P})}) (p \Vdash_{M,\mathbb{P}}^* \varphi(u)).</math>
Other symbols of the forcing language can be defined in terms of these symbols: For example, <math>u = v</math> means <math>\neg (u \ne v)</math>, <math>\forall x\, \varphi(x)</math> means <math>\neg \exists x\, \neg \varphi(x)</math>, etc. Cases 1 and 2 depend on each other and on case 3, but the recursion always refer to <math>\mathbb{P}</math>-names with lesser [[Rank (set theory)|ranks]], so transfinite induction allows the definition to go through.

By construction, <math>\Vdash_{M,\mathbb{P}}^*</math> (and thus <math>\Vdash_{M,\mathbb{P}}</math>) automatically satisfies '''Definability'''. The proof that <math>\Vdash_{M,\mathbb{P}}^*</math> 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 <math>\vee</math> and <math>\exists</math> as the elementary symbols<ref>Notably, if defining <math>\Vdash_{M,\mathbb{P}}</math> directly instead of <math>\Vdash_{M,\mathbb{P}}^*</math>, one would need to replace the <math>\vee</math> with <math>\wedge</math> in case 4 and <math>\exists</math> with <math>\forall</math> in case 5 (in addition to making cases 1 and 2 more complicated) to make this internal definition agree with the external definition. However, then when trying to prove '''Truth''' inductively, case 4 will require the fact that <math>G</math>, as a [[Filter (mathematics)|filter]], is downward [[Directed set|directed]], and case 5 will outright break down.</ref>), cases 1 and 2 relies only on the assumption that <math>G</math> is a filter, and only case 3 requires <math>G</math> to be a ''generic'' filter.{{sfn|Shoenfield|1971}}

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

: For any formula <math>\varphi(x_1,\dots,x_n)</math> there is a theorem <math>T</math> of the theory <math>\mathsf{ZFC}</math> (for example conjunction of finite number of axioms) such that for any countable transitive model <math>M</math> such that <math>M\models T</math> and any atomless partial order <math>\mathbb{P}\in M</math> and any <math>\mathbb{P}</math>-generic filter <math>G</math> over <math>M</math> <math display="block">(\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)).</math>

This the sense under which the forcing relation is indeed "definable in <math>M</math>".