Canonical $\mathbb{P}$-name If $G$ is a subset of some forcing poset $P$ and for $x \in V$ (where I think $V$ is some model of ZFC but I'm not clear what it means) the canonical $\mathbb{P}$-name is defined as
$$ \underset{\dot{\hphantom{x}}}{x}:=\{\langle\underset{\dot{\hphantom{y}}}{y},0\rangle\mid y\in x\} $$  
then how do I see the second equality:
$$ \underset{\dot{\hphantom{x}}}{x}[G] = \{ \underset{\widetilde{\hphantom{y}}}{y}[G] \mid \exists p \in G: \langle \underset{\widetilde{\hphantom{y}}}{y}, p \rangle \in \underset{\dot{\hphantom{x}}}{x} \} = \{ \underset{\dot{\hphantom{y}}}{y}[G] : y \in x \}$$
assuming $0 \in G$ where $0$ is the smallest element in $P$? Thanks for your help!
 A: In forcing we start with a model of ZFC, of course we cannot prove (from ZFC) that such model exists, but it would be quite strange to assume the theory we want to work with is inconsistent.
So we have a class, $V$ and a relation $E$ defined on $V$ that we understand as $xEy$ to mean $x\in y$. Now we can use all the machinery of forcing.
First we define $\mathbb P$-names, these are defined by induction as follows:


*

*$V^\mathbb P_0 = \varnothing$,

*$V^\mathbb P_{\alpha+1} = \{\langle x,p\rangle\mid x\in V^\mathbb P_\alpha, p\in\mathbb P\}$

*If $\beta$ is a limit ordinal then $V^\mathbb P_\beta=\bigcup_{\alpha<\beta} V^\mathbb P_\alpha$


Later when we have fixed a generic filter $G$, by identifying the $p\in G$ as "true" and $q\notin G$ as false, we can interpret the names into actual sets, and the truth values of the resulting model will be given by the set which are interpreted nicely.
We would like it if the ground model $V$ will be a subclass of $V[G]$, and if it will be canonically defined. Luckily, this is just what the canonical $\mathbb P$-names are for. We define those, again, by induction


*

*$\check\varnothing=\varnothing$ (I have taken the notation of Jech here),

*$\check x = \{\langle\check y,0\rangle\mid y\in x\}$.


This tells us that $0$ will force that $y\in x$, where as $0$ is the least element of the forcing poset, so if $0$ will force $y\in x$ every condition will have to force that as well.
Lastly, if $\sigma$ is a $\mathbb P$-name, we define the interpretation of $\sigma$ by $G$ as:
$$\sigma[G] = \{y[G] \mid \exists p\in G:\langle y,p\rangle\in\sigma\}$$
This exactly means that some $p\in G$ was forcing that $\dot y\in\dot\sigma$, or using the $\Vdash$ relation: $p\Vdash\dot y\in\dot\sigma$. If the generic filter $G$ was chosen, the result will be that indeed $y\in\sigma$.
We now want to check that the canonical names are interpreted exactly as the original elements of $V$. For this we need only to verify that indeed $G$ interprets $\check x$ as $x$ again. 
$$\check x[G] = \{\check y[G]\mid \langle \check y,0\rangle\in\check x\}$$
Inductively assume that every rank below the rank of $\check x$ was interpreted correctly, then $\check x[G] = \{y[G]\mid y\in x\} = \{y\mid y\in x\}$ as wanted. 
Note: Since $G$ is a generic filter, every two elements are compatible. Namely, if $p\Vdash\varphi$ and $q\in G$ then $q$ cannot force $\lnot\varphi$ (it may not decide, but it cannot force the negation). Since $0\in G$ for every $G$, we have that if $0\Vdash\varphi$ then for every $p\in G: p\Vdash\varphi$.
