I’m learning set theory and forcing in the (french) book from Jean-Louis Krivine “Théorie des ensembles”.

Given a countable transitive model $\mathscr{M}$ of ZFC together with a poset $P$, he constructs the model $\mathscr{M}[G]$ where $G$ is a $P$-generic in the ambient universe $\mathscr{U}$. The countability of $\mathscr{M}$ is essential in order for such a generic $G$ to exist.

But I saw several times in answers on MO that forcing could be defined over any model of ZFC and that, for example, CH and ~CH can both be forced over any model of ZFC.

My questions are:

• How does this kind of forcing work? I guess that we cannot anymore suppose that there exists a generic $G$, so how is the new universe constructed? And what does the truth lemma becomes?

• When do we need to use this kind of forcing? For example if I want to prove that some proposition $P$ is independant of ZFC, I can always assume that my initial model of ZFC is countable and “usual” forcing will probably be sufficient.

Any reference about this will be more than welcome.

Thanks.