In set-theoretic forcing arguments, why do we need to prove facts about M[G] from the “perspective” of M? I’m trying to work through the forcing relation in set theory and the independence proof of GCH in particular. Although I feel like each step locally makes sense, I’m a bit confused about the necessity of some of the last steps which makes me think I’ve misunderstood something fundamental about the strategy. My understanding of the high-level argument is:

*

*Take a countable transitive model of ZFC M and take a generic ultrafilter G over some suitable Poset in M

*Show that the extended model M[G] is also a model of ZFC and that M can prove this

*Even though M cannot “see” G, by use of Names and the forcing relation we can prove that there is some element p in G such that M proves that, for any generic ultrafilter G’ containing p, the sentence we want to force is true in M[G’].

*So M proves that the sentence we want to force is in fact consistent with ZFC

Maybe this is a misunderstanding on my part, if so happy to be corrected here!
If that’s largely accurate though, I guess I’m confused why we need to prove so much about what M can prove about M[G] from its own “perspective”. Intuitively it seems enough that we can see “from the outside” that if M is a model of ZFC then so is M[G], and so the Names/forcing relation steps seem confusing to me - I’m not seeing the necessity of proving that all of this is provable from within our original model.
 A: Belatedly turning my comments into an answer, the point is not that we care about definability-in-$M$ for its own sake (although it is super cool); rather, the definability lemma is pretty much the only way we can figure out how $M[G]$ behaves, and this includes even very basic questions like "Does $M[G]\models\mathsf{CH}$?" and so forth.
Consider for example the following pair of extremely useful slogans:

*

*"Forcing with a c.c.c. poset doesn't collapse cardinals."


*"Forcing with a countably closed poset doesn't add reals."
Each of these is absolutely crucial for the forcing-only proof of the independence of $\mathsf{CH}$, and can be intuitively justified without much effort. However, they're also critically under-nuanced as written. For simplicity let's look at the case where we're forcing over a c.t.m. $M$ - so generic filters actually exist unproblematically in reality, and the construction of the corresponding generic extensions is straightforward. Then every poset in $M$ is c.c.c. "in reality" and no (nontrivial) poset in $M$ is countably closed "in reality," simply because $M$ itself is countable. So the slogans above only make sense when interpreted internally: the right claims are "If $M$ thinks $\mathbb{P}$ is [c.c.c./countably closed] then every $\mathbb{P}$-generic extension of $M$ has the same [cardinals/reals] as $M$" respectively.
To drive this point home, let's think about how we would prove that if $M\models$ "$\mathbb{P}$ is countably closed" and $G$ is $\mathbb{P}$-generic over $M$ then $\mathbb{R}^{M[G]}=\mathbb{R}^G$. Letting $\nu\in M^\mathbb{P}$ be a name for a real, we have that for every $p\in\mathbb{P}$ there is a sequence of strengthenings $p\ge q_0\ge q_1\ge...$ such that $q_i$ decides the $i$th bit of $\nu$. We want to apply countable closure to this sequence to get a common strengthening $r$ which will then decide all of $\nu$. However, both parts of this idea rely on $M$-definability of forcing! Firstly, since $\mathbb{P}$ can't possibly be truly countably closed (unless it's trivial), we can only find such an $r$ if $M$ can see the sequence $\overline{q}$, which in turn is only plausible if $M$ can define the forcing relation. Secondly, in order to go from "the condition $r$ decides all bits of $\nu$" to "Any generic $G\ni r$ has $\nu[G]\in M$" we need $M$ to be able to see how $r$ decides the bits of $\nu$.
