I've been doing some basic reading in inner model theory, and I'm at the point where I've seen the definition of things like MartinSteel and MitchellSteel inner models. I am wondering about the motivation for these constructions since they are much more complicated than the constructible universe $L$, or models like $L[X]$ built by adding a predicate to the construction of $L$. I am wondering, what makes a naive approach like taking $L[X]$ for the right sets fail for larger cardinals? Are there some results that pinpoint at what large cardinal strength more complicated constructions than $L[X]$ are needed? Thank you.

1$\begingroup$ The predicate we want to add is either a measure, a sequence of measures, an extender, or a certain sequence of extenders. Short extender sequences work up to a Woodin limit of Woodin (maybe a bit past ?, I am not sure here) after that I think one needs the long extenders. If you take a normal measure $U$ on $\kappa$ a measurable cardinal then $\mathcal{P}(\kappa) \in Ult(V,U)$, but we don't necessarily have $\mathcal{P}(\kappa^+) \in Ult(V,U)$. Extenders can be used to accomplish this and lot more actually. So extenders can be used to get all large cardinal properties basically... $\endgroup$– Rachid AtmaiOct 5 '13 at 19:33

1$\begingroup$ ...However more work is needed when dealing with $L[E]$: If you add an extender $E$ to $L$ to get $L[E]$, you don't get more than a measurable (I don't know the proof of this fact, but the extender to be added has to come from a certain background construction for the model to witness the large cardinal property). The main problem related to your question is the "moving spaces" problem. Steel showed that fine structural models of the type $L[\vec{E}]$ can't contain large cardinals past a supercompact. I apologize in advance if my comments are a bit vague. $\endgroup$– Rachid AtmaiOct 5 '13 at 19:39

$\begingroup$ I see, that helps a bit. Does anyone have an idea or proof reference why adding an extender to $L$ to get $L(E)$ does not get past a measurable cardinal? $\endgroup$– user40919Oct 5 '13 at 19:49

1$\begingroup$ I found that question on MO, this was asked a while back, hopefully this helps: mathoverflow.net/questions/79472/… $\endgroup$– Rachid AtmaiOct 5 '13 at 19:57

$\begingroup$ Thanks Carlo, I followed that past post. The Kunen paper seems very useful. His Theorem 7.1 shows that $L[V] = L[U]$, where V is any nonprincipal ultrafilter on $\kappa$, and $U$ is a normal ultrafilter on $\kappa$. He proves in the section before that $L[U]$ is canonical if may ways. Then Philip Welch's answer suggests to think of an extender $E$ witnessing that $\kappa$ is locally strong as an ultrafilter $Q'$ on $\mathcal{P}(\kappa)$. $\endgroup$– user40919Oct 5 '13 at 20:21
If $X$ is a set, then $L[X]$ does not have strong cardinals. In fact, $X^\sharp$ does not belong to $L[X]$, so any assumption that implies that $V$ is closed under sharps fails in these models.
Now, this is perhaps not the right example, as strong cardinals or supercompact cardinals essentially require a proper class of "witnesses". If you just want "local" versions, for example, having your model satisfy that there is an inaccessible $\kappa$ with $V_\kappa$ a model of "there is a proper class of strong cardinals" or more (say, having Woodin cardinals in your model), then models $L[X]$ are fine. In fact, contrary to your claim, the MitchellSteel models for Woodin cardinals are models of the form $L[X]$ for an appropriate set $X$.
So perhaps we need to refine your question to something much more specific, such as why we need complicated sequences of extenders (or measures) rather than just having $X$ be, say, an ultrafilter. This is easy to see when we try to model a degree of supercompactness, because nontrivial ultrafilters on $\mathcal P_\kappa(\lambda)$ concentrate on nontrivial sets (rather than sets of ordinals), so adding such an ultrafilter as a predicate $X$ ends up not doing much, since $L[X]$ cannot see any interesting measure $1$ sets, so $L[X]$ reduces to $L$ in this case. This has been known forever, it was noticed quickly after the $L[\mu]$ models for measurability began to be investigated.
Again, the above may not be the best example, since there are additional obstacles to developing finestructure theory even at the level of $\kappa^+$strong compactness, so we do not have "MitchellSteel" models for this assumption anyway.
Now, the complicated $L[\mathcal E]$ models are complicated because they are trying to do more than just modeling the large cardinal assumptions we are after. For example, to model that $\delta$ is Woodin, we need many "local" strong cardinals below $\delta$, so we need to add many ultrafilters to the model; this already indicates our constructions will have $\mathcal E$ be not a single measure, but rather a sequence of measures.
But the $L[\mathcal E]$ models do more: We want to add these ultrafilters in increasing order of "strength", which is measured by several parameters, such as their Mitchell order. This requires that we be able to organize the ultrafilters in some ordered fashion, avoiding clashes, so that if at some stage $\alpha$ we are to add a measure, there is exactly one candidate measure to add. This is useful to establish basic results such as condensation, the higher order versions of the result that elementary substructures of initial segments of $L$ are again initial segments of $L$.
We also want our models to be as canonical as possible, so in particular we must avoid coding sets by accident, which could happen if we are not careful on what measures we put in $\mathcal E$. There are additional requirements, all meant to ensure that the models we obtain can be compared with one another, carry no unwanted information, and add strength "from the ground up". To formalize this carefully ends up requiring some nontrivial amount of fine structure, and the verification that these fine structural assumptions indeed allow these constructions to succeed ends up being a careful inductive argument. This is the real source of the difficulties and technicalities associated with the theory of these models.
I suggest that you read the initial sections of the paper by Steel for the Handbook of set theory. They do a good job of spelling out some of these concerns and of describing how precisely the predicate $X$ that are used end up coding the ultrafilters witnessing the large cardinal assumptions one is after.
It may actually be useful to read first the appropriate sections in Zeman's book. The points above are illustrated there carefully, and one avoids the additional mathematical complications that come from iteration trees, which are inherent to the theory of Woodin cardinals. Truth is, when one first encounters iteration trees, they may appear rather complicated. It is natural that something complicated is needed, since we want to produce models that can code complicated sets of reals, and the complexity of the possible sets of reals of these $L[\mathcal E]$ models is closely tied up to the complexity of the comparison process. (This is nicely explained at the beginning of the MartinSteel paper on Iteration trees.)
What may not seem so natural is the solution of using iteration trees rather than other coding devices when indexing the ultrafilters in the sequences. In fact, other approaches were suggested, by Baldwin and others, more or less generalizing directly the theory we get at the level of models for $o(\kappa)=\kappa^{++}$. But these suggestions were the ones that ended up being rather complicated and led to the theory being stuck until Steel had the idea of iteration trees. In fact, the theory was stuck well before the level of Woodin cardinals. Thanks to the development of the MitchellSteel machinery, these prior levels could then be developed as well.

$\begingroup$ Thank you Andres, that is very helpful. I am trying to digest it all. I will definitely take a look at the Steel article and Zeman book. $\endgroup$ Oct 5 '13 at 20:26

$\begingroup$ Probably very basic, but might you know where I can read about how $\mathcal(P)_\kappa(\lambda)$ ultrafilters added to $L$ as predicates give us back $L$? $\endgroup$ Oct 5 '13 at 20:31

$\begingroup$ And also probably basic: for extenders $E$ on $\kappa$, any general results what $L[E]$ could be, whether it is $L$, $L[\mu]$, or something more complicated? Thank you $\endgroup$ Oct 5 '13 at 20:34

$\begingroup$ The first topic is covered in Kanamori's The higher infinite. Section 25 is on $\mathcal P_\kappa(\lambda)$, and the specific result on constructibility is exercise 25.8 (which has a generous hint). Extenders are discussed in section 26, but their relation with constructibility is not explored. This is discussed to some extent in Steel's handbook article, for example. Two key points are that you can code significant embeddings with extenders (which Kanamori discusses), and that extenders can be applied to models other than the one the embedding came from. Steel explains this carefully. $\endgroup$ Oct 5 '13 at 21:41

$\begingroup$ The thing is, what an extender codes depends among other things on what we call its length. Very short extenders are essentially ultrafilters, and we do not get more than an $L[\mu]$ model out of them (but this is as it should be). Longer extenders code more. And (to be safe, let's say) for a while at least, they relativize nicely so we can look at constructibility over them. Many of the complications of the sequences $\mathcal E$ are simply not relevant if we do not care about fine structural issues. That said, I cannot think of a reference explicitly addressing this. $\endgroup$ Oct 5 '13 at 21:42