Forcing theorem

Atomic relations are definable by F1. At conjunction and negation insert the already obtained subformula predicates into the clauses in F2; at an existential quantify over the definable class of M-names and over the set P. This gives a fixed first-order predicate for each fixed formula. Every parameter is P, its order, or one of the name arguments. F4 then supplies the truth lemma for this very internally defined predicate.

If $p{⊩}^M\phi$ and G is M-generic containing p, the right-to-left direction of F4 makes $\phi$ true in M[G]. This implication needs no assumption that any generic exists.

Suppose p does not force $\phi$. By density closure F3 the conditions forcing $\phi$ cannot be dense below p. Hence some $q\le p$ has no stronger condition forcing $\phi$, which says $q{⊩}^M\mathrm{\neg }\phi$ by F2. The extra generic-existence hypothesis supplies an M-generic G containing q; upward closure puts p in G. F4 makes $\mathrm{\neg }\phi$ true there. Thus the asserted truth in every generic through p fails.

Steps 2.1 and 2.2 give both directions of the display. The argument selected only one generic under the stated existence hypothesis; it did not select generics simultaneously or infer their existence from definability. Formula construction used an external finite induction, so no uniform truth predicate for the universe or AC was assumed.