I am studying (unramified) forcing, and am trying to prove the axiom schema of replacement for $M[G]$. To me, the idea seems to be vaguely similar to the proof that forcing with a c.c.c. poset doesn't collapse cardinals. So I go as follows:
- For any formula $\phi(x, y)$, I can use separation in $M$ to find the set of forcing conditions $p$ such that $p \Vdash \forall x\in A\ \exists !y\ \phi(x, y)$. (In hindsight this step seems to be unnecessary, since if this condition isn't satisfied then the instance of replacement is vacuously true.)
- Now I can find a formula in $M$ that means "$p$ forces $\underline{y}$ to be a name for the (unique) $y$ such that $\phi(x, y)$". However, for fixed $p$ and $\underline{x}$, the class of $\underline{y}$ satisfying this formula is still a proper class, since any member of $M[G]$ has a lot of names.
- In order to apply Replacement in $M$, I want a formula that maps each pair $(\underline{x}, p)$ to a single set in $M$. Scott's trick comes to mind, so from each of the aforementioned proper class, I take the set of its members with the least rank.
- Now I can apply Replacement and Union in $M$ to construct a name for the set required by Replacement in $M[G]$.
However, I am not sure whether Scott's trick, or in general some reference to the cumulative hierarchy, is "needed" here, or if there is a simpler proof. When I searched on the internet, I didn't find any source that links forcing with Scott's trick, which adds to my uncertainty.
Is my proof correct, and if so is the use of Scott's trick "necessary" in some sense?
Essentially, yes, Scott's trick is somehow needed. But this isn't surprising. There is a proper class of names which evaluate to the empty set. And it's not always obvious how to circumvent this by assigning some kind of a canonical name. Although sometimes, of course, it is easy.
Your proof is fine, you can really skip the first step. We can start with the assumption that $p\Vdash\forall x\in\dot A\exists!y\varphi(x,y)$, and simply show that there is a name $\dot B$ so that $p$ forces to be the image of $\dot A$ under that $\varphi$.
If you're working with $\sf ZFC$, this is fairly easy and we can sweep a bunch of things under the table. We can use Collection instead of Replacement, as suggested in the comments, and then apply $\sf AC$ to select and use mixing (or fullness as it is sometimes called) to pull everything so that $p$ forces everything directly.
If you want to minimise the amount of $\sf AC$ that you're using here, we can reach all the way down to "none of it", of course. This requires a slightly more careful unpacking of what exactly it means for $p$ to force a statement involving quantifiers (namely, things happen on a dense set below $p$). But essentially, yeah, we need to utilise Scott's trick in one way or another.