Check names without a largest condition

For a nonempty forcing preorder P in ZF, define

$\check{x}=\{⟨\check{y},p⟩:y\in x,p\in P\},\dot{G}=\{⟨\check{p},p⟩:p\in P\}\mathrm{.}$

Membership recursion on sets is a well-founded setlike recursion, so Recursion on well-founded setlike relations supplies the unique class map $x\mapsto \check{x}$. The rule takes a product of the set of predecessor values with P, hence returns a set. Induction shows each output is a P-name; Replacement on P then shows that dot G is a name. The valuation convention is Valuation of names and M[G].

If M is a transitive ZF model containing P and x, perform the same recursion inside M. Induction on membership identifies its values with the external check names: all members of x and all conditions of P belong to M, and the set products and recursive values agree. Thus check x belongs to M, and internal Replacement on P puts dot G in M.

When P has a largest (weakest) condition 1, one may instead recurse using only pairs with coefficient 1. A nonempty forcing filter contains 1 by upward closure. Membership induction in the valuation equation then gives value x for that top-only check name, just as for the all-conditions version proved next. No largest condition is required for the displayed definition.