The following is from Halbeisen, page 289, on generic extensions:
This leads to one of the key features of forcing: By knowing whether a certain condition $p$ belongs to $G \subseteq P$, people living in $\mathbf V$ can figure out whether a given sentence of the forcing language is true or false in $\mathbf V [G]$. Moreover, it will turn out that people living in $\mathbf V$ are able to verify that in certain models $\mathbf V [G]$ all axioms of $ZFC$ are true.
I have three questions related to this passage.
One is: Why is it desirable to verify the truth or falsity of statements in $\mathbf V[G]$ from within $\mathbf V$? Why would it not be good enough to verify them in $\mathbf V [G]$?
Two: Do I understand correctly that people in $\mathbf V$ use $P$ names to verify that $ZFC$ holds in $\mathbf V [G]$? (the passage does not talk about this)
Three: I thought that if $\mathbf V$ satisfied $ZFC$ then so would $\mathbf V [G]$ but the passage says only "certain models $\mathbf V [G]$" satisfy all axioms of $ZFC$. Which do and which don't?
Many thanks for your help.
This is the question I am most shaky on, so forgive me if this makes no sense. The desirability of people in $\newcommand{\V}{\mathbf V}\V$ being able to verify the truth of statements holding in $\V [ G ]$ is that otherwise it may not be verifiable that $\V [G]$ satisfies ZFC for $G$ $P$-generic over $\V$. Consider Separation:
The definability of $\Vdash$ in $\V$ also allows for the likelihood of using combinatorial properties of the forcing notion $P$ (which can be verified in $\V$) to determine truth of certain statements in $\V [G]$. For example, if $P$ is ccc (meaning that people in $\V$ think $P$ is ccc), then every cardinal in $\V$ remains a cardinal in $\V [ G ]$. If there was no way to determine truth in $\V [ G ]$ from $\V$ then it would be doubtful that there would be a strong connection between the combinatorics of $P$, and truth in $\V [ G ]$. It turns out that using these combinatorial properties is central to many forcing proofs.
As people in $\V$ only have access to $\V [ G ]$ via the $P$-names, they use $P$-names to verify $\V [ G ] \models \phi$. In particular, the Pairing Axiom is verified in $\V$ to hold in $\V [ G ]$ as follows:
As above, combinatorial properties of $P$ may also be used. But at some point someone must have verified the connection between the combinatorics of $P$ and truth in $\V [G]$ (often by using these combinatorial properties to manipulate $P$-names in an appropriate manner).
Note that $\V [ G ]$ need not satisfy all axioms of ZFC for arbitrary $G \subseteq P$, even arbitrary filters $G \subseteq P$. Kunen's text states that Extensionality, Foundation, Pairing and Union all hold under the assumption that $G$ is just a filter in $P$. Using the countable transitive model approach to forcing, by coding a well-ordering of $\omega$ of order-type $> o(V)$ you can construct a filter $G \subseteq P$ such that $V[G]$ does not satisfy Replacement (as noted in this previous answer).
It is true that for every $P$-generic filter $G$ over $\V$ that $\V [ G ]$ will satisfy ZFC, but this notion appears to be introduced in the next section of Halbeisen's text (even though I have mentioned it copiously above).