Forcing names and their rank

In ZF let P be the nonempty forcing preorder of Forcing preorders, compatibility and filters. A P-name is a set of pairs $⟨\sigma ,p⟩$, with name first and condition second, where $p\in P$ and every sigma is again a P-name. The empty set is a name. Formally use Transfinite recursion to define

$N_0=\mathrm{\varnothing },N_{\alpha +1}=\mathcal{P}(N_{\alpha }\times P),N_{\lambda }={\bigcup }_{\beta <\lambda }{N}_{\beta }(\lambda \text{ a nonzero limit}),$

and call elements of the union of these levels names. The levels nest: $N_0\subseteq N_1$, successor inclusions follow by monotonicity of the product and power set, and at a limit each earlier member is already a set of pairs with first coordinate in the union, so belongs to its next power-set stage.

The first-coordinate predecessor relation on names is setlike: predecessors of tau are obtained from its pair entries by Replacement. It is well-founded because the actual membership rank of the first coordinate of a Kuratowski pair in tau is strictly less than the rank of tau. Hence Recursion on well-founded setlike relations defines the name rank

${\mathrm{rk}}_P(\tau )=\sup \{{\mathrm{rk}}_P(\sigma )+1:\mathrm{\exists }p\in P(⟨\sigma ,p⟩\in \tau )\}\mathrm{.}$

The empty supremum is zero. Conversely a set of pairs whose first coordinates are names belongs to a level: Replacement collects their least containing-stage indices, a common ordinal bounds them, and the set of pairs belongs to the next stage. This verifies the recursive description without an unbounded set of names. Every descendant of a name is a name. These are definable classes and set-valued recursions, not class objects; no Choice is used. Name rank is distinct from the membership rank of a condition.