Forcing name ($\tau \in M^{\mathbb{P}}$)

A forcing name is a recursively built set of pairs $(\sigma ,p)$, where $\sigma$ is a lower-rank forcing name and $p$ is a forcing condition. Ground-model names are interpreted using a generic filter to form the generic extension.

The ordinal assigned recursively by $\mathrm{nrk}(\tau )=\sup \{\mathrm{nrk}(\sigma )+1:(\sigma ,p)\in \tau \}$. It measures dependency on subnames and justifies generic evaluation by recursion. The ordinary rank of a set also accounts for the coding of the ordered pairs and the forcing conditions; it need not equal this dependency rank of a set.

If the ground model has axiom of choice, well-order the set of subnames appearing in a forcing name for an arbitrary extension set. Evaluate those activated by the generic filter. Each element of the extension set has a least preimage index; ordering by these indices well-orders the set. Only ground choice and the ZF part of the forcing theorem are needed.

A name for a subset of a ground-model set, given coordinatewise by antichains in a forcing order. For countable-chain-condition forcing, each coordinate uses a countable antichain, which bounds the number of names for reals.

For the condition-first forcing name convention, pair every condition with each of two names $\tau ,{\tau }^{\prime }$. Under any nonempty generic filter, the evaluation of a forcing name is then $\{{\tau }_G,{\tau }_G^{\prime }\}$, the unordered pair of the two values. Equal values give a singleton. With the name-first convention, reverse the two components of each syntactic pair.

The forcing name $\{(\check{p},q):p,q\in \mathbb{P},q\perp p\}$ evaluates to $\mathbb{P}\setminus G$. If $p\notin G$, genericity applied to $\{q:q\le p\text{ or }q\perp p\}$ supplies an incompatible member of $G$. If $p\in G$, directedness prevents such a member.

Interpret a forcing name recursively by $\mathrm{val}(\tau ,G)=\{\mathrm{val}(\sigma ,G):\exists p\in G((\sigma ,p)\in \tau )\}$. The collection of interpreted ground-model names is the generic extension.

The canonical forcing name for a ground-model set $x$ is $\check{x}=\{(\check{y},1):y\in x\}$. Its evaluation of a forcing name under every generic filter is $x$.