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).