Forcing and generic extensions 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.
 A: *

*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:

Let $X , a \in \V [G]$, and suppose $\phi ( x , y )$ is some formula.  We wish to construct $Y \in \V [G]$ such that $$\V [ G ] \models ( \forall x ) ( x \in Y \leftrightarrow ( x \in X \wedge \phi ( x,a ) ).$$  We know that $X$ has a name $\dot{X}$ in $\V$, and similarly $a$ has a name $\dot a$ in $\V$.  We may then consider $$\sigma = \{ \langle \tau , p \rangle \in \mathrm{dom} ( \dot{X} ) \times P : p \Vdash ( \tau \in \dot{X} \wedge \phi ( \tau , \dot a ) ) \}.$$  It should be clear $\sigma$ is a $P$-name, and that under the assumptions stated above $Y = \sigma [G]$ would have the desired property.  However if $\Vdash$ were not definable in $\V$ (meaning that there is no formula $\psi$ such that $(\psi ( p , \tau , \dot a ) )^{\V} \Leftrightarrow p \Vdash ( \phi (\tau , \dot a)$), then $\sigma$ need not be in $\V$ (and hence $Y$ itself need not be in $\V [G]$).  Without appealing to some property in $\V$ I honestly don't know how to in general construct the desired $P$-name in $\V$ (i.e., the desired set in $\V [G]$).

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:

Let $\sigma , \tau$ be any two $P$-names (in $\V)$.  Construct the following $P$-name: $\theta = \{ \langle \sigma , \mathbf 0 \rangle , \langle \tau , \mathbf 0 \rangle \}$.  By applications of the Pairing Axiom in $\V$ we know that $\theta \in \V$, and it is easy to see that $\theta$ is a $P$-name.  Furthermore, given any filter $G \subseteq P$, since $\mathbf 0 \in G$ it follows that $$\theta [ G ] = \{ \sigma [ G ] , \tau [ G ] \}.$$  As all objects in $\V [ G ]$ have $P$-names in $\V$, it follows that $\V [ G ] \models \text{Pairing}$.

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).
