Forcing names and the forcing theorem

Continue the external conditional setting of a countable transitive M satisfying ZFC, and let P∈M be a set forcing order with a weakest condition 1. A P-name is a set of pairs whose first coordinates are earlier names and second coordinates are conditions. The well-founded name hierarchy makes valuation possible: retain a pair exactly when its condition belongs to G, evaluate its first coordinate, and collect the resulting values. Different pairs can yield the same value, since the output is a set rather than a multiset.

The canonical name check-x for a ground set x pairs each canonical name check-y for y∈x with 1. Induction on membership gives check-x evaluated by G equal to x. The extension M[G] consists of valuations of all P-names belonging to M. It contains M and G, is transitive, and has the same ordinals as M. Saying that it satisfies all of ZFC requires the forcing theorem and axiom verification; transitivity alone would not establish Power Set or Replacement.

For each fixed first-order formula φ, the set-forcing theorem provides a ground-model definable relation p forces φ of the indicated names. Definability is a formula-by-formula scheme; it is not an internal truth predicate for every statement of the whole universe. The truth lemma says that φ holds of the evaluated names in M[G] exactly when some p in G forces φ of the names. A condition forcing a statement therefore ensures it in every relevant generic extension containing that condition, not merely in one arbitrarily chosen branch.

Forcing is persistent under strengthening: once p forces a statement, a stronger q also forces it. A condition need not decide a sentence, but the conditions that decide it form a dense set. Negation is governed by the absence of stronger conditions forcing the opposite statement, not by failure of the original condition to force it. The recursive atomic definitions, quantifier clauses, and their inductive verification are substantial parts of the theorem, cited here rather than replaced by an informal appeal to eventual truth.

Consider a three-condition order with weakest condition 1 and two incompatible atoms p₀ and p₁ below it. The two generic filters are {1,p₀} and {1,p₁}. Each is already an element of M in this finite example, so neither extension adds new sets. This does not contradict the earlier Cohen-real argument: its newness proof used dense disagreement requirements and the possibility of splitting further, while an atom has no two incompatible stronger extensions.

A name can nevertheless take different ground-set values in these two filters. The weakest condition can force a statement true for both values while deciding neither of two incompatible alternatives separately. This is useful for separating the logical meaning of forcing from the vague idea of choosing a single future. The truth lemma uses some condition in the actual filter as a witness, and strengthening reaches a deciding atom here. An undecided top condition does not make the entire forcing relation undefined or undermine definability.