Solution (source code)

= Solution
{c}

Use <standard notation for forcing>, so $q\leq p$ means that $q$ is stronger. Let $\check p$ be the <canonical forcing name> for the ground-model condition $p$. Define
$$
\boxed{\tau=\{(\check p,q):p,q\in\mathbb P,\ q\perp p\}.}
$$
Here $q\perp p$ means that they are <incompatible forcing conditions>. The checks and their collection are formed by recursion and <Axiom schema of replacement> in $M$, and the displayed set is selected by <axiom schema of separation>, so this is a <forcing name> in $M$.

By <evaluation of a forcing name>,
$$
\operatorname{val}(\tau,G)=\{p\in\mathbb P:\exists q\in G\ (q\perp p)\}.
$$
If $p\in G$, directedness of the <generic filter> gives a common stronger condition for $p$ and each $q\in G$, so $p$ is absent from this value.

Conversely, for fixed $p\in\mathbb P$ the set
$$
D_p=\{q\in\mathbb P:q\leq p\text{ or }q\perp p\}
$$
is a <dense subset of a forcing order> belonging to $M$. A condition incompatible with $p$ is already in it, and one compatible with $p$ has a common extension below $p$. Genericity supplies $q\in G\cap D_p$. If $p\notin G$, upward closure of $G$ rules out $q\leq p$, hence $q\perp p$. Therefore
$$
\boxed{\operatorname{val}(\tau,G)=\mathbb P\setminus G.}
$$
This <forcing name for the complement of a generic filter> works without a separativity assumption on the order.