Axiom of Choice and fullness of the class of terms of the forcing language It is well-known that when doing forcing over some ground model $M$, if we assume the Axiom of Choice in $M$, then the class of terms of the language of forcing has the property that for any $p \in \mathbb{P}$, if $$p \Vdash_{\mathbb{P}} \exists x \varphi(x),$$
then there exists a term $\tau \in M^\mathbb{P}$ such that 
$$p \Vdash_{\mathbb{P}} \varphi(\tau).$$
It is often underlined that this maximality property (that the class of names is full in the sense above) is actually crucial for many arguments. 
My questions are as follows: 
(1) can you please give examples of theorems in the theory of forcing that would not hold if the class of names was not full (so I do not mean the ones in the proofs of which this property just appears, but the ones in which it is indeed essentially used)?
(2) if we drop the assumption of AC in the ground model, how much of the properties from the reply to (1) can we keep/recover (and what kind of forms of weak AC would be necessary then)?
(3) how do you prove that if $M \not\models AC$, then fullness does not hold?  
 A: The thing about fullness is that it is very convenient. It allows you to reason about "future objects" from "the present". In other words, it lets you talk about a [name for an] element of a set $\dot A$, if you know that it is not empty.
But the machinery of forcing is set up such that you can avoid doing that. $p\Vdash\dot A\neq\varnothing$, then there is some $q<p$ and some $\dot a$ such that $q\Vdash\dot a\in\dot A$. So by extending $p$, we can seemingly overcome this problem.
When does fullness really play a significant role then? When we need to make infinitely many choices, of course. Because if we can continue choosing without having to worry about extending the condition $p$, then we don't run into closure properties or chain conditions, which are combinatorially more complicated. 
As for actual examples? None come to mind. In the absence of choice forcing is more complicated because closure properties and chain conditions no longer have the same influence as they did in $\sf ZFC$. Of course, we normally use these properties to prove fullness to begin with, so that makes sense.
Iterated forcing becomes more of a nuisance, because anything which is not a finite-support iteration is using fullness in a very fundamental way. We can still overcome this quite easily, and then the problem become choosing the sequences for the names at limit steps, which is where choice really plays a role.

Finally, to see why fullness implies choice, go back to the very first paragraph. If $A=\{A_i\mid i\in I\}$ is a family of pairwise disjoint non-empty sets, define $\Bbb P=\{A\}\cup A$, and $q<p\leftrightarrow q\in p$.
Now consider $\dot X$ to be the name $\{(A_i,\check a)\mid a\in A_i, i\in I\}$, in other words each $A_i$ forces that $\dot X$ is $A_i$ itself. We have that $A$, which is the maximum condition of $\Bbb P$, forces $\dot X\neq\varnothing$, that is to say, $\exists x(x\in\dot X)$. By fullness there is a name $\dot x$ such that $A\Vdash\dot x\in\dot X$. But now each $A_i$ must interpret $\dot x$ as one of its own elements, which is a choice function.
