The following is a rather silly statement which I can neither prove nor refute.
Let $M\in V\models\mathrm{ZFC}$ such that $M$ is countable and transitive in $V$ and $M\models\mathrm{ZFC}$. Suppose $\mathbb P$ is a poset in $M$ that we use for forcing. If $p\in\mathbb P$ and $\varphi(\sigma,v)$ is a formula in the forcing language such that $p\Vdash\exists v\ \varphi(\sigma,v)$, then there is a $\mathbb P$-name $\tau\in M^{\mathbb P}$ such that $p\Vdash\varphi(\sigma,\tau)$.
I can (dis)prove the analogous statements for $\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\forall$, but for some reason, this one seems to be much harder than the others.
I expect this statement to be false, but I managed to find names that witness whatever existential formulas I came up with.
If the statement quoted above turns out to be true, then how would one prove it? If the statement is false, then is there a simple counterexample in which the poset $\mathbb P$ is Cohen's?
No. This is called the mixing lemma, or the maximum principle.
The way to prove it is to see that the definition of $p\vDash\exists\tau\varphi$ is that there exists a set which is dense below $p$ such that for every $q$ in that set there exists a name $\tau_q$ for which $q\vDash\varphi(\sigma,\tau_q)$. We may assume that if $(q',\tau')\in\tau_q$ then $q'\leq q$.
Now conclude that there exists $C$ which is a maximal (below $p$) antichain of such conditions, and take the name $\tau=\bigcup_{q\in C}\tau_q$. Show that $\tau$ is the name you seek.
Interesting to point out, this principle is equivalent to the axiom of choice in $\sf ZF$.