Forcing over an arbitrary model of ZFC 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 independent 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.
 A: $\def\zfc{\mathit{ZFC}}$No one seems to have mentioned another way to think about forcing, that can be sometimes helpful.
Let $\zfc_B$ denote $\zfc$ extended with an additional constant $B$ and an axiom that $B$ is a complete Boolean algebra. Let $\zfc_{B,G}$ be a theory in the language $\langle\in,B,G,U\rangle$ where $G$ is a constant, $U$ a unary predicate, with axioms stating that $U$ defines a transitive class, $\zfc_B$ holds in $U$, $\zfc$ (including replacement for all the new stuff) holds in the whole universe $V$, $G$ is a $U$-generic filter on $B$, and $V=U[G]$.
Any method of making sense of forcing (such as in the answers above) shows that $\zfc_{B,G}$ is a conservative extension of $\zfc_B$, in the sense that if $\phi$ is a $\langle\in,B\rangle$-sentence such that $\zfc_{B,G}\vdash\phi^U$, then $\zfc_B\vdash\phi$. Note that this can even be shown purely syntactically in a very weak metatheory.
In model-theoretic terms, this means that if $M\models\zfc$ and $M$ thinks that $B\in M$ is a complete Boolean algebra, then $M$ has an elementary extension $M'$ which has a generic extension $M'[G]$ with a generic for $B$.
However, the main point is that if you are now working inside $\zfc$ and you come upon a complete Boolean algebra $B$, you can safely pretend that your universe $V$ is included in a generic extension $V[G]$, even though you cannot actually define it from inside.
A: Guillaume : 
There are several ways of making sense of forcing. It is useful to be able to move between all these versions, as each may have its specific advantages in some cases.
The approach of consider countable transitive models $M$ and their extensions by explicit construction of generic objects is very useful, although somewhat restrictive, and we do not really need the restrictions it imposes. 
For example: One can use a purely syntactical approach, where we transform formulas into forcing statements, and never worry about models. In turn, there are several ways of doing this. We can, by simply manipulating formulas, check that the weakest condition forces the axioms of first order logic, and we can apply modus ponens and the rules about quantifiers to formulas forced by the empty condition. Then we can check that each axiom of ZFC is forced by the empty condition. Finally, we can check that if $p$ is a condition, the theory (without variables, but allowing appropriate names) that it forces is consistent.
(I actually wrote all of this down as a grad student. It is not entirely without pain. One can simplify this brutal approach at times, by using, say, the reflection theorem and a bit of the semantic approach you know of with countable models.)
Another approach is the Boolean-valued models construction. This is due to Dana Scott and Robert Solovay, and it is very flexible and useful. It makes sense over any model. This approach produces a proper class (from the point of view of the original model) and rather than being a model in the usual sense, truth-values are understood as varying over a complete Boolean algebra (the completion of the poset, from the point of view of the model). One can see that there is a natural way of interpreting the ground model as a (classical) substructure of its Boolean-valued extensions, so we can safely argue as if we had an ideal generic extension of the universe. If there are appropriate ultrafilters in the Boolean algebra (say, in the true universe of sets), then we can form a (Boolean) ultrapower and recover an honest model from a Boolean valued extension.
Sometimes, we can actually show that generics over certain ground models exist, and build transitive models even if the original model was uncountable. For example: Assuming appropriate large cardinals, the powet set of many posets in $L$ is actually countable in $V$, so we can find forcing extensions of $L$ as submodels of $V$. A cute example is that if $0^\sharp$ exists and $\kappa=\omega_1$ (of $V$, this is much larger than the $\omega_1$ of $L$), then in $V$ there is an inner model which is a forcing extension of $L$ by the poset ${\rm Col}(\omega,<\kappa)$, so this is a forcing extension of $L$ that computes $\omega_1$ correctly. However, we cannot have (in $V$) an inner model that is a forcing extension of $L$ and computes both $\omega_1$ and $\omega_2$ correctly (this would force $0^\sharp$ to belong to $L$).
As another example, under determinacy, given any (transitive) model of choice, a large initial segment of it is very small, so we can find generics over these models. This is useful to prove results about the models of determinacy, by arguing about its inner models of choice. A similar approach is used in Solovay's model to show Lebesgue measurability of all sets of reals. Essentially, by finding appropriate codes for the sets in small models of choice, and arguing that the sets the codes represent are measurable in these small models, and then using the codes to check that measurability is preserved. 
A good reference for this question, as Amit mentioned, is Kunen's book, chapter VII. I strongly recommend that you begin by looking at this book.
If you want to delve deeper: For the Boolean-valued approach, the best reference is John Bell, "Set Theory: Boolean-Valued Models and Independence Proofs" (Oxford Logic Guides), of which the third edition just appeared, in 2005. When Scott and Solovay developed forcing in terms of Boolean algebras, they promised a paper explaining their approach. The paper never quite materialized and somehow morphed into this book by Bell. 
I know some books try to avoid the "transitive models" approach since they are only interested in consistency results. I remember James Cummings criticized this avoidance a few years ago in a review (published in the JSL). For example, the countable models approach allows us to prove, using forcing, that $\Sigma^1_1$ sets are Lebesgue measurable (provably in ZFC), by adapting appropriately the argument I sort of hand-waved above about Solovay's model.
(The countable models version of forcing has other advantages. For example, to construct Suslin trees with special properties in $L$, one can proceed by induction on the levels of constructibility, and at appropriate limit stages choose the branches of the partially formed tree to be generic over the stage built so far.)
Once one realizes that forcing is essentially an internal construction, it is clear we do not really need the models we work with to be transitive, or countable, or any such thing. However, it is nice to see how to make explicit sense of the construction in other cases. The clearest presentation of this I have seen is by Woodin. You may want to look at the Woodin-Dales book, "An Introduction to Independence for Analysts", Cambridge UP (1987), and its sequel, "Super-Real Fields: Totally Ordered Fields with Additional Structure" London Mathematical Society Monographs New Series, Oxford UP (1996).
A: This is a great question that every set theorist first learning about the beautiful area of forcing should ask.  As Andres described, there are a number of ways to understand forcing, but I want to elaborate on the boolean-valued model method since I believe that this is the most intuitive way to understand what it means to "force over $V$."
First, let me briefly introduce the method for which you are familiar.  Cohen's forcing construction over an arbitrary partial order $\mathbb{P}$ involves the usage of what are called $\mathbb{P}$-names.  If we are working with a countable transitive model $M$, then we should have $\mathbb{P} \in M$, and we are restricting our attention to the class of $\mathbb{P}$-names in $M$, denoted $M^{\mathbb{P}}$.  Since $M$ is countable, we can use standard diagonalization techniques to construct an actual $M$-generic filter $G \subseteq \mathbb{P}$ in $V$.  Our choice of filter $G$ will determine the values of each of the $\mathbb{P}$-names that become the elements of $M[G]$.  But an amazing fact about forcing is that we actually have a definable "forcing relation" $\Vdash$ in $M$ such that $p \Vdash \varphi(\tau_1, \ldots, \tau_n)$ exactly when $M[G] \vDash \varphi(\tau_1^G, \ldots, \tau_n^G)$ for all $M$-generic filters $G$ with $p \in G$ where $\tau_1, \ldots, \tau_n \in M^{\mathbb{P}}$ is any collection of $\mathbb{P}$-names in $M$ and $\tau_i^G$ is the interpretation of the $\tau_i$ by $G$.  Another amazing fact about this forcing relation is that if $M[G] \vDash \varphi(\tau_1^G, \ldots, \tau_n^G)$, then there will be $p \in G$ such that $p \Vdash \varphi(\tau_1, \ldots, \tau_n)$.  Combining these facts, $M$ can assert "I may not know whether $\varphi$ will be true in extensions that are (possibly) fictitious to me, but I do know that $\varphi$ must be true exactly when the (imaginary) $M$-generic filter $G$ contains an element in $S_{\varphi}$ where $S_{\varphi}$ is the subcollection of conditions from $\mathbb{P}$ that force $\varphi$ to be true."  You can easily verify using these facts about forcing that statements $\varphi$ that are true in all forcing extensions have $S_{\varphi} = \mathbb{P}$ and those that are false have $S_{\varphi} = \emptyset$.
With this background, I can now talk about "forcing over" $V$ using the Boolean-valued model method.  In $V$, we can construct the proper class boolean-valued model $V^{\mathcal{B}}$ consisting of all $\mathcal{B}$-names from $V$ (same thing as $\mathbb{P}$-names but your poset is a complete boolean algebra $\mathcal{B}$).  This model will not have a $1-0$ (true-false) truth value predicate per-say but will instead have a truth value predicate that ranges among all values in the boolean algebra.  We denote the truth value of any statement $\varphi(\tau_1, \dots, \tau_n)$ by $\|\varphi(\tau_1,\ldots,\tau_n)\|$ for any collection of $\mathcal{B}$-names $\tau_1, \ldots, \tau_n \in V^{\mathbb{B}}$. Now let's compare this to the former construction.
First, the forcing relation that was said to be in $M$ was just a relativized version of the one in $V$.  Mainly, if we pretend our $V$ is this countable model $M$ and set $\mathbb{P} = \mathcal{B} \setminus \{0\}$, the same things will be true.  So $V$ can assert "I may not know whether $\varphi$ will be true in extensions that are (possibly) fictitious to me, but I do know that $\varphi$ must be true exactly when the (imaginary) $V$-generic filter $G$ contains an element in $S_{\varphi}$ where $S_{\varphi}$ is the subcollection of conditions from $\mathcal{B} \setminus \{0\}$ that force $\varphi$ to be true."  Note that as was the case with $M$, these generic filters are fictitious to $V$ (unless $\mathcal{B} \setminus \{0\}$ is trivial), but $V$ still can talk about the name for these hypothetical objects.  Also, the nice thing about complete boolean algebras is that all subcollections are closed under supremums.  Consequently these $S_{\varphi}$ will each have a supremum and the supremum will be the boolean value that will wind up being assigned to $\|\varphi\|$.  Note then that the statements that are always true in every forcing extension (such as the axioms of ZFC) will have $S_{\varphi} = \mathcal{B} \setminus \{0\}$ so that such $\varphi$ will be assigned boolean value $1$ while the statements that are always false in every forcing extension will have $S_{\varphi} = \emptyset$ so that these statements will all be assigned boolean value $0$.  More generally, you can use the properties of the forcing relation to verify that the conditions forcing $\varphi$ to be true in the extension are precisely those at or below $\|\varphi\|$ in the boolean algebra under the prescribed assignment.  This is why we commonly refer to these values from the boolean algebra as "probabilities" (though they aren't in general members of $[0, 1]$).  If the boolean value is 1, it's necessarily true in the extension; if it's $0$, it's necessarily false in the extension and if it's some other value, then it will be true in a wider range of extensions if it's closer to $1$ in the boolean algebra lattice.
Finally in regards to forcing over $V$, you may object that forcing over complete boolean algebras is not completely general, but in fact every partial order $\mathbb{P}$ can be associated with a complete boolean algebra $\mathcal{B}(\mathbb{P})$ such that any forcing extension that can arise over $\mathbb{P}$ is equivalent to one that can arise over $\mathcal{B}(\mathbb{P}) \setminus \{0\}$.
And to address your question about utility, we are often concerned not only about relative consistency results but where these results will be true.  For example, it is often more difficult to show that we can find a forcing extension of an inner model (transitive proper class model containing all of the ordinals) where $\varphi$ is true rather than a set where $\varphi$ is true.  Since inner models are ubiquitous in the study of large cardinals, this is why it is especially important that we distinguish between the two types of philosophical forcing methods.
