Why does the Solovay-Tennenbaum theorem work? I have decided to learn iterations at long last, and I am reading through Jech's Set Theory for now. The standard example after explaining what is an iteration with finite support is the following theorem (quoted from Jech, Theorem 16.13):

Theorem (Solovay-Tennenbaum). Assume GCH and let $\kappa$ be a regular cardinal greater than $\aleph_1$. There is a c.c.c. notion of forcing $P$ such that the generic extension $V[G]$ by $P$ satisfies Martin's Axiom and $2^{\aleph_0}=\kappa$.

I believe that I understood the proof mechanically, but even though I feel that I understand it in a more profound way - I have this feeling that I really didn't get the point. It feels like magic. 
What I managed to understand is that we have enumerations of all isomorphism classes of small posets in each stage, and generically we reach them all. Alas, like any new forcing argument, this too feels like some sort of witchcraft.
I also understand completely why $2^{\aleph_0}=\kappa$, and I have to admit that this is one clever argument, but I can't really see the full intuition behind it. I just see that it works, and I can reason why it works, by MA there is a generic for any $<\kappa$ dense sets, but this means that we have to have at least $\kappa$ dense subsets in the universe so $2^{\aleph_0}\geq\kappa$, where the other side of the inequality follows from the fact that $|P|\leq\kappa$ and $P$ is c.c.c.

Can anyone shed some intuition behind the proof? Some insights about why it works?
 A: There are $\kappa$ many stages in which you add Cohen reals. so you will have at least $\kappa$ reals at the end. This is really a very simple principle: "if you want to add something, add it."
THe other direction is slightly more involved:  Do not add anything you don't want to add, and keep your fingers crossed that unwanted objects (such as:  more than $\kappa$ reals) don't find their way into the construction anyway.
The "nice names" argument is very basic and practically always used whenever you want to get an upper bound on the number of new reals. Every new real $x$ is described by a family of countably many maximal antichains, plus a coloring functions mapping each antichain into 
$\{0,1\}$ --- assigning to condition $p$ in antichain $A_n$ the value that $p$ forces to $x(n)$. Count how many such families of colored antichains there are, this will be an upper bound on the continuum in the extension. 
If you want to count subsets of $\lambda$, you will of course have $\lambda$ many antichains. 
A: Let me add a couple of comments to Joel's and Martin's answers.  They both pointed out that you get $\kappa$ reals for a much simpler reason than having forced MA, namely that at $\kappa$ stages you chose to add a Cohen real. You might ask what happens if you never choose to add a real.  Indeed, that's the original Solovay-Tennenbaum situation, where each step was forcing with a Suslin tree, which doesn't add reals.  Nevertheless, you get new reals anyway.  Cohen reals appear at the limit stages of cofinality $\omega$ in any finite-support iteration.  
I think of MA as a compatibility result.  There are lots of things that would naturally be done by ccc forcing --- killing a Suslin tree, adding a single measure-zero set that covers all the ground model's (coded) measure-zero sets (amoeba forcing), adding Cohen reals, etc.  The main point of MA is that you can do all these things together, and mixing them together won't produce disasters.  Notice that, in other circumstances, mixing innocuous-looking forcings can produce disasters, expecially collapsing cardinals. For example, if you specialize an Aronszajn tree and I add a path through it, then between us we've collapsed $\aleph_1$.  Similarly if you shoot a club through a stationary co-stationary set and I shoot a club through its complement.  The key technical fact underlying MA is that a finite-support iteration of arbitrary ccc forcings is still ccc.  So you can mix these forcings at will, without any risk of collapsing cardinals.
A: The key to the proof is to think of Martin's axiom as the assertion that "a lot of c.c.c. forcing has already taken place". Thus, to force MA, what you need to do is to force over as many different kinds of c.c.c. forcing as you can imagine, and to do so again and again as long as they remain c.c.c. Of course, we won't literally force over all c.c.c. forcing, since this would continually push the continuum higher and higher, as $\text{Add}(\omega,\theta)$ is c.c.c. for any $\theta$. But luckily, there is a lemma that MA is equivalent to the assertion involving only c.c.c. forcing of size less than the continuum. 
So we only really need to consider forcing notions of size less than continuum. So the strategy, aiming just for the case $\kappa=\omega_2$, which illustrates all the important ideas, is to start with GCH and force with as many different c.c.c. forcing notions of size at most $\omega_1$ as we can imagine, in an iteration of length $\omega_2$. This will necessarily have the effect of pushing up the continuum to $\omega_2$, because we will very often have to be adding a Cohen real.
So, we perform a finite-support iteration $\mathbb{P}$ of length $\omega_2$. At stage $\alpha$, think of $\alpha$ as coding a pair of ordinals $\langle\beta,\gamma\rangle$, where $\beta\leq\alpha$. Let $\mathbb{Q}_\alpha$ be the $\gamma$ th poset (with respect to some well-ordering fixed in advance) in the stage $\beta$ extension $V[G_\beta]$, regarded as a partial order in $V[G_\alpha]$, provided that this partial order is still c.c.c. there. Let $G\subset\mathbb{P}$ be $V$-generic for the iteration. This is a c.c.c. iteration, and so preserves all cardinals. The continuum becomes $\omega_2$, since we very often chose to add a Cohen real. Meanwhile, if $\mathbb{Q}$ is any c.c.c. partial order in $V[G]$ and $D$ is a family of at most $\omega_1$ many dense sets in $\mathbb{Q}$, then since $\mathbb{Q}$ and $D$ have size $\omega_1$, they are already known at some stage of the forcing $V[G_\beta]$ for $\beta\lt\omega_2$, and so $\mathbb{Q}$ arises at some later stage $\alpha$. At that stage, we add a $V[G_\alpha]$-generic filter $F\subset\mathbb{Q}$, which is therefore also $V[G_\beta]$-generic and consequently $D$-generic. And so this instance of MA is fulfilled by the iteration. 
The general case of making the continuum equal to $\kappa$ is essentially the same idea. The iteration simply proceeds longer, and handles more and larger forcing notions. 
The idea of this proof extends to many other iterations, which are trying to force over as many different partial orders of a certain type as possible. For example, this same idea arises in the Laver preparation and in the Baumgartner forcing of PFA, and in the lottery preparation. 
One curiosity: although MA asserts essentially that "a lot of c.c.c. forcing has been done", and Tony Martin confirmed to me (while riding together on a river tour boat in Poland) that this idea was present from the start in the treatment of this axiom, Jonas Reitz proved in his dissertation that MA is consistent with the Ground Axiom, which asserts that the universe was not obtained by (set) forcing at all. 
