This may be a basic question. I am studying forcing at Kunen's book. However, in several other papers that I am reading, they use that something is true in $V^P$ instead of $V[G]$. I know that if $V[G]\models \varphi((\tau_1)_G,\ldots, (\tau_n)_G)$, by the Truth Lemma, there is $p\in G$ such that $p\Vdash(\tau_1,\ldots, t_n)$. However, I think that what they mean with $\varphi$ is true in $V^P$, is that $\mathbb 1_P\Vdash\varphi(\tau_1,\ldots,\tau_n)$.
So let
(1) There is $p\in G$ such that $p\Vdash \varphi$.
(2) $\mathbb 1_P\Vdash\varphi$.
Obviously, (2) implies (1), since $\mathbb 1_P$ always belong to $G$. However, I cannot see that they are equivalent. My first question is: are they really equivalent?
And my second question, which is the motivation of all this, given a partial order $P$, what does it really mean $P$ forces $\varphi$? Does it mean (1) or (2) in the case they are not equivalent? Above all, I would like that a forcing P that I am building really forces a formula $\varphi$. However, I would like to say this as a formula of just $V$ (i.e., something like $"V\models P$ forces $\varphi"$, so I cannot mention $G$). However, if the "real" definition of $P$ forces $\varphi$ is (1), I do not know how to do it.
It is often the case that one works with lots of notions of forcing at once (lots = more than one, but usually more than two and sometimes there are several models to work with as well), in which case it becomes much easier to use $V^P$ rather than $V[G]$, as it saves us the need to track which generic filter comes from where.
So when we write $V^P\models\ldots$ we really mean that $V[G]\models\ldots$ where $G$ is a $P$-generic filter over $V$.
For example, suppose that you have an elementary embedding $j\colon V\to M$ and $P\in V$ is a forcing, then $j(P)\in M$ is a forcing. Now you want to talk about $V[G]$ and $M[H]$ where $H$ is $j(P)$-generic over $M$. Instead it's much easier to talk about $V^P$ and $M^{j(P)}$.
(I was generally against this sort of abuse of the notation, but recently I sat in a course about forcing, large cardinals and combinatorial properties of small cardinals. After just two weeks it became apparent how superior this is to $V[G]$ notation in most cases.)
Addition with respect to the comments.
We can define forcing internally and externally. The external definition is simple, $p\Vdash\varphi$ if for every generic filter $G$ such that $p\in G$ it is true that $V[G]\models\varphi$.
Now it is also true that if $V[G]\models\varphi$ then there is $p\in G$ such that $p\Vdash\varphi$. Otherwise every element in $G$ does not force $\varphi$, but since $\{q\in P\mid q\Vdash\varphi\lor q\Vdash\lnot\varphi\}$ is dense, there is some $p\in G$ deciding the truth value of $\varphi$, so there must be one forcing $\lnot\varphi$. So $V[G]$ cannot satisfy $\varphi$.
The above is easily shown from the internal definition of the forcing relation.
Therefore it is true that $V[G]\models\varphi$ if and only if there exists $p\in G$ such that $p\Vdash\varphi$.
Now if we require that for every generic $G$, then $1_P$ forces $\varphi$, because it appears in every generic filter $G$.