Valuation of names and M[G]

In ZF, for any $G\subseteq P$ and P-name tau define

${\mathrm{val}}_G(\tau )=\{{\mathrm{val}}_G(\sigma ):\mathrm{\exists }p\in G(⟨\sigma ,p⟩\in \tau )\}\mathrm{.}$

The subname relation is well-founded and setlike, as in Absoluteness of names and their ranks and its name definition. For a supplied set function on the predecessors, Separation selects those with a coefficient in G and Replacement takes their values. This is a uniquely valued set rule, so Recursion on well-founded setlike relations gives a unique definable valuation and all its set restrictions. The empty name evaluates to empty. Even G empty is permitted here; then every name evaluates to empty.

For a transitive set ground model M containing P, write

$M[G]=\{{\mathrm{val}}_G(\tau ):\tau \in M\text{ is a P-name}\}\mathrm{.}$

Separation on M and Replacement make this an external set. If M satisfies ZF, namehood in this display agrees with its internal namehood by Absoluteness of names and their ranks. The notation asserts neither genericity of G nor that M[G] is a model of ZF. For a definable class ground model the same display is interpreted as a definable class.