Forcing name (source code)

= Forcing name
{title2=$\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>.