I am a beginner of forcing, often I read from some articles something like "p forces \dot{G}"$p \Vdash \dot{G}$ is P$P$-generic over \check{M}$\check{M}$" (M bewhere $M$ is a CTMcountable transitive model, for instance).
Q1. I learnt from Jech'Jech's book a definition of "p forces \dot{x} in \check{M}"$p \Vdash \dot{x} \in \check{M}$", but I don't know how to translate "p forces \dot{G}"$p \Vdash \dot{G}$ is P$P$-generic over \check{M}$\check{M}$" into a formal version using this.
Q2. I also learnt from Kanamori'book HIGHER INFINITE LARGER CARDINALS...Kanamori's book that M is an DEFINABLEa definable proper class of M[G]$M[G]$ whenever G$G$ is generic over M$M$, why definable (i.e. a form of the form {x \in M[G]: \phi(x)}$\lbrace x \in M[G]: \phi(x) \rbrace$)?
