Can anyone point out some good reference to understand how Paul Cohen proved that the continuum hypothesis is independent of ZFC? I know he used the so called forcing technique to construct two different models of ZFC, but I don't quite understand how.
Raymond Smullyan and Melvin Fitting wrote a long (but very readable) monograph, called "Set theory and the continuum problem" (Oxford Logic Guides, 34. Oxford Science Publications. The Clarendon Press, Oxford University Press, New York, 1996. xiv+288 pp. ISBN: 0-19-852395-5) which starts from the very beginning, introducing the von Neumann-Bernays-Godel "class-set" formalism, establishing all the basic properties, etc. culminating in a complete, self-contained exposition of Cohen's result and the basics of forcing.
There are three parts. The first part is foundational. The second is an exposition of Godel's relative consistency result, which says that the continuum hypothesis is consistent with NBG (or ZFC if you prefer). The third is about forcing, and Cohen's result.
In very, very broad outline, the point of Godel's argument is to exhibit a "model" of class-set theory with as few sets as possible: the only sets are those that are absolutely required to be there by some application of the axioms. Each set therefore carries with it a formula which requires it to exist. There are so few objects in this model that the continuum hypothesis is seen to be true because every element of the continuum that is required to exist is required by some explicit "reason", and the reasons can be enumerated.
The point of forcing is to show that one can build a new model in which there are many more objects, by adding new objects when there is no explicit reason why they can't exist (i.e. they are "forced" to exist) and keeping careful track of how many such objects you can add without reaching a contradiction. Certain tools (eg "compactness") are required to be able to add infinitely many new objects in this way.
It's not easy to describe in a non-technical way. One good first source is the article "Forcing for Dummies" by Chow, available here. For more details, Cohen's book "Set Theory and the Continuum Hypothesis" is pretty readable.
EDIT : I forgot - Chow has an enhanced version of Forcing for Dummies entitled "A beginner's guide to forcing", available here.
Before you settle down for anything have a look at J. L. Bell's "Boolean-valued models and independence proofs in set theory". I don't know this book, but several others of the same author, and he always writes in a very clear and very well motivated style - marvellous!
Three non-standard sources (just as a complement):
I liked Rosser's "Simplified Independence Proofs" - there you get a detailed proof of the independence, with an intuitive basic idea, but without (or a different variant of) forcing (although he includes some remarks on what Cohen's forcing has to do with his method). This method was invented in 1966 by Scott and Solovay.
You will probably have other things to do than start going through a whole different theory, but there is a topos theoretic point of view on forcing, explained here, which ultimately lets forcing lose some of its mystery.
A more set-theoretic and less categorical predecessor of the topos view can be found in Vopenka's articles (the first one from 1965!), see the list here. This is somehow intermediate between the topos view and Scott & Solovay's Boolean algebra view.
Cohen's original articles are available online:
If you want to look at the original. They are both rather short.
I like Kunen (Set Theory, an introduction to independence proofs) myself. I did read parts of Bell's book, using Boolean models, but the more modern way Kunen works is like you'd read it in more modern works. So if you are interested in doing research along those lines, and/or reading modern papers on forcing, check it out.