Editing Forcing (mathematics) (section)

=== 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>".