I am a beginner of forcing, often I read from some articles something like "p forces \dot{G} is P-generic over \check{M}" (M be a CTM, for instance). 

Q1. I learnt from Jech' book a definition of "p forces \dot{x} in \check{M}", but I don't know how to translate "p forces \dot{G} is P-generic over \check{M}" into a formal version using this.

Q2. I also learnt from Kanamori'book HIGHER INFINITE LARGER CARDINALS... that M is an DEFINABLE proper class of M[G] whenever G is generic over M, why definable(i.e. a form of {x \in M[G]: \phi(x)})?