Example of a filter $G$ on $\mathbb{P}$ for which $\mathbb{P}\setminus G\notin M[G]$. This is exercise IV.2.47 from Kunen's Set Theory. 

Assume that M is a ctm for ZFC Give an example of a $\mathbb{P}\in M$ and a (non-generic) filter G on P for which $(\mathbb{P}\setminus G)\notin M[G].$

It includes this hint:

Hint: One could let $\mathbb{P}$ be HF ,and let $\leq$ be an appropriate forcing order such that $p\leq q \leq p$ whenever rank($p$)=rank($q$). Then $G$ can be built by a diagonal argument. Observe that for filters, $G \subseteq H \implies rank(\tau_G)\leq rank(\tau_H)$.

I am very confused about what Kunen is suggesting I diagonalize or how I'm supposed to take advantage of the last observation. I studied the fact that $\mathring{G} = \{(\check{p},q):p,q\in\mathbb{P}\land p\perp q\}$ names $\mathbb{P}\setminus G$ whenever $G$ is generic and how this name can sometimes fail (for example when $G=\{\mathbb{1}\}$) but it hasn't helped. 
I've also been trying to construct $G$ by induction on some well order of HF in such a way that I never add a name that names $\mathbb{P}\setminus G$, but haven't been succesful.
Can anybody guide me in some way towards the solution? Thank you.
 A: A bit late, but I think this does the job.
First of all, let's recall the definition of $M[G]$ which Kunen uses (and which, to address Mitchell's comments, is different from the $L$-style definition): $$M[G]=\{\nu[G]: \nu\in M^\mathbb{P}\},$$ that is, $M[G]$ is the set of all $\mathbb{P}$-names in $M$ evaluated at $G$. Note that the evaluation of a name $\nu$ at $G$ makes sense for $G$ an arbitrary subset of $\mathbb{P}$ (not even a filter!): it's defined inductively as $\{(p_i, \nu_i): i\in I\}[G]=\{\nu_i[G]: p_i\in G\}$. Of course, this is much less natural if $G$ isn't a filter.
The key point is that $\nu[G]$ is a positive object: we determine positive facts about membership in $\nu[G]$ based on positive facts about membership in $G$. Now, if $G$ is a generic filter, then each negative fact is determined by a positive fact: if $p\not\in G$, then there's some $q\in G$ which prevented $p$ from being in $G$. However, if $G$ isn't generic, this breaks down, and now - if we want to show that $\mathbb{P}\setminus G\in M[G]$ - we're faced with the task of giving a positive description of a negatively-defined object.
And the point is that there's no reason in general to believe this can be done.
A tangent: there are often interesting analogies to be drawn between forcing and ideas from computability theory; here, the one that leaps out to me is the distinction between Turing reducibility and enumeration reducibility, in the context of pinning down this positive/negative distinction.

Alright, so that's the intuition; how are we going to build the desired $\mathbb{P}$ and $G$? I'm going to depart from Kunen's hint here, since frankly I don't find it very helpful. I'm also going to try to do something a bit more interesting than just solving the problem as stated:

Claim: there is some $\mathbb{P}\in M$, some $\mathbb{Q}\in M$, some $H$ which is $\mathbb{Q}$-generic over $M$, and some name $\mu\in M^\mathbb{Q}$ such that $G=\mu[H]$ is a (non-generic) filter through $\mathbb{P}$ and $\mathbb{P}\setminus G\not\in M[G]$.

That is, a desired counterexample can be built by actual forcing! This is actually already implicit in Kunen's hint: "by diagonalization" is slang for "using forcing" :P.
Alright, how are we going to do it? Well, we want our $\mathbb{P}$ to have lots of compatibilities, so that "positive" information doesn't give us "negative" information (e.g. the poset $2^{<\omega}$ would be a bad idea, since e.g. knowing $01001\in G$ would tell us $01000\not\in G$). Let's take something really simple - say, $\mathbb{P}=\mathcal{P}_{fin}(\omega)$, ordered by inclusion. From the perspective of forcing, this is a very silly poset since it has no incompatibilities at all! But it still has lots of incomparabilities, and so many (non-generic) filters.
Now we want our $\mathbb{Q}$ to build a "bad" filter through $\mathbb{P}$. How will we do this? Well, we have a bunch of requirements to meet: for each $\nu\in M^\mathbb{P}$, we need to satisfy $$\nu[G]\not=\mathbb{P}\setminus G$$ (where $G=\mu[H]$ - we haven't specified what $\mu$ is, or even what $\mathbb{Q}$ is, so this is all vague; the only point is to build a bit of intuition). To satisfy this, we want our $G$ to have lots of negative information which can't be detected; put another way, $H$ needs to build $G$ by making both positive and negative declarations about $G$ (so that $G$ has lots of negative information folded into it). So one natural guess for $\mathbb{Q}$ is the set of pairs $(A, B)$ of disjoint finite sets of natural numbers, ordered by $$(A, B)\le(C, D)\iff A\supseteq C, B\supseteq D.$$ (Note that this is just Cohen forcing in disguise.) The generic $H$ is essentially a partition of $\omega$, and we'll let $G$ be the left side of the partition; formally, we let $$G=\{n: \exists (A, B)\in H(n\in A)\}.$$ If you prefer to be super-formal, the specific name $\mu$ we're looking at is $$\mu=\{((A, B), \check{n}): n\in A\}.$$
I claim this does the job. So let $H$ be $\mathbb{Q}$-generic over $M$, and $G=\mu[H]$; I claim that $\mathbb{P}\setminus G\not\in M[G]$. To show this, it will be enough to argue that for each $\nu\in M^\mathbb{P}$, we have $\nu[G]\not=\mathbb{P}\setminus G$. We'll argue via genericity, as usual. So fix a $\nu\in M^\mathbb{P}$ and a condition $q\in\mathbb{Q}$; we'll find a $q'\le q$ which forces $\nu[G]\not=\mathbb{P}\setminus[G]$.
There are a few ways to do this; I like the following. Let $q=(A, B)$, fix some $n\not\in A\cup B$, and let $q_0=(A, B\cup\{n\})$. Then WLOG we can find some $q_1=(A', B')\le q_0$ such that $A'\vdash n\in \nu$; otherwise, take $q'=q_0$ (since $\nu[G]$ will now be guaranteed to not see that $n\in\mathbb{P}\setminus G$).
OK, now let $q'=(A'\cup\{n\}, B)$, and think about what $q'$ forces about what $\nu$ thinks about $\mathbb{P}\setminus G$ . . . $\Box$
