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).
The other answers are excellent, but let me augment them by
offering an intuitive explanation of the kind you seem to
seek.
In most forcing arguments, the main idea is to construct a
partial order out of conditions that each consist of a tiny
part of the generic object that we would like to add; each
condition should make a tiny promise about what the new
generic object will be like. The generic filter in effect
provides a way to bundle these promises together into a
coherent whole having the desired properties.
For example, with the Cohen forcing
$\text{Add}(\omega,\theta)$, we want to add $\theta$ many
new subsets of $\omega$, in order to violate CH, say. So we
use conditions that specify finitely many bits in a
$\omega\times\theta$ matrix of zeros and ones. Each
condition makes a finite promise about how the entire
matrix will be completed. The union of all conditions in
the generic filter is a complete filling-in of the matrix.
Genericity guarantees that each column of this matrix is a
new real not present in the ground model and different from
all other columns, since any finite condition can be
extended so as to disagree on any particular column with
any particular real or from any particular other column.
With the collapse forcing $\text{Coll}(\omega,\kappa)$, we
want to add a new surjective function $f:\omega\to\kappa$.
So we use conditions consisting of the finite partial
functions $p:\omega\to\kappa$, ordered by extension. Each
such condition is a tiny piece of the generic function we
want to add, describing finitely much of it. The union of
the generic filter provides a total function $g:\omega\to
\kappa$, and the genericity of the filter will guarantee
that $g$ is surjective, since for any $\alpha<\kappa$, any
condition $p$ can be extended to a stronger condition
having $\alpha$ in the range.
And similarly with many other forcing arguments. We design
the partial order to consist of tiny pieces of the object
that we are trying to add, each of which makes a small
promise about the generic object. If $G$ is a generic
filter for this partial order, then the union of $G$ is the
joint collection of all these promises.
In many forcing arguments, it is not enough just to build a
partial order consisting of tiny pieces of the desired
object, since one also wants to know that the forcing
preserves other features. For example, we want to know that
the forcing does not inadvertently collapse cardinals or
that it can be iterated without collapsing cardinals. This
adds a wrinkle to the idea above, since one wants to use
tiny pieces of the generic object, but impose other
requirements on the conditions that will ensure that the
partial order has a nice chain-condition or is proper and
so on. So the design of a forcing notion is often a
trade-off between these requirements---one must find a
balance between simple-mindedly added pieces of the desired
generic object and ensuring that the partial order has
sufficient nice properties that it doesn't destroy too
much.
In this sense, I would say that the difficult part of most
forcing arguments is not the mastery of the forcing
technology, the construction of the generic filter and of
the model---although that aspect of forcing is indeed
nontrivial---but rather it is the detailed design of the
partial order to achieve the desired effect.
Best Answer
Forcing in set theory is usually performed to extend a model of set theory to another model $M[G]$ of set theory in which this or that statement of set theory (such as the continuum hypothesis) changes its truth-value. On the other hand, forcing over a model of arithmetic $M$ does not produce an extension of $M$, but a rather an expansion $(M,G)$.
A serious stumbling block for the application of forcing in $PA$ (Peano Arithmetic) to obtain independence results is a theorem of Gaifman that states that if $M$ and $N$ are models of $PA$ such that $M$ is cofinal in $N$, then $M$ is an elementary submodel of $N$, and in particular, $M$ and $N$ satisfy the same set of arithmetical sentences. Gaifman's proof, by the way, heavily relies on the so-called MRDP theorem (which states that every r.e. set is Diophantine).
Forcing has had an enormous success in clarifying definability questions in both arithmetic and set theory, but in comparsion, it has had rather limited efficacy so far in complexity theory, certainly not due to lack of effort or expertise: I know more than one expert in computational complexity whose résumé includes first rate papers on set-theoretical forcing.