 Forcing name

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.