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