An unpublished result of Woodin says the following:
Theorem. Assuming the existence of large cardinals, it is consistent that $\forall \lambda, 2^{\lambda}=\lambda^{++}.$
In the paper "The generalized continuum hypothesis can fail everywhere, Ann. Math. 133 (1991), 1–35" it is stated that Woodin has proved this result assuming the existence of a $P^{2}(\kappa)-$hypermeasurable (or equivalently a $\kappa+2-$strong) cardinal $\kappa$.
But using core model theory we now that more than a $P^{2}(\kappa)-$hypermeasurable cardinal $\kappa$ is required for this result (though a $P^{3}(\kappa)-$hypermeasurable cardinal $\kappa$ is sufficient).
So my question is
Question. 1-What large cardinal assumption is used in the proof of the above Theorem.
2-Does anyone know the proof? Does it use the supercompact Radin forcing as in the paper stated above, or it uses the ordinary Radin forcing (like Cummings paper "A model in which GCH holds at successors but fails at limits").
Best Answer
As you say, Hugh's precise result is unpublished. I have not seen any written reports of it, so I do not know the precise hypotheses it uses. For purely historical reasons, I would be interested if someone has such a report.
I assume the Cummings-Woodin unpublished manuscript (mentioned here and here) was meant to present an account of the argument but, at least the version I have, stops before getting there (in a chapter titled "Modified Prikry forcing, Part I").
(By the way, send me an email if you'd like a copy and haven't been able to contact James for one.)
In any case, Hugh is arguing with hypermeasurables, and using the corresponding version of Radin forcing, instead of the original supercompact-based version. The argument in the Foreman-Woodin paper (that proves the consistency of the weaker statement "$\mathsf{GCH}$ fails everywhere", and uses a variant of the supercompact-based version) is actually much older. As they say in the paper,
On the other hand, there is at least one published proof of the result, see
(A preliminary version is available at the arXiv.)
Merimovich uses extender based Radin forcing. This is Merimovich's extension of a technique originally developed by Gitik and Magidor. The introduction to the paper gives a good account of the history of the problem, and of the techniques it uses, and appropriate references can be found there. For further (later) refinements of the technique, see
His argument can give a model of $\forall\lambda\,(2^\lambda=\lambda^{+n})$ for any fixed $n$, $1<n<\omega$, (call this statement $\mathsf{GCH}^{+n}$), though he presents the details for $n=3$. He assumes $\mathsf{GCH}$ and the existence of a cardinal $\kappa$ that is what is either called $(\kappa+n)$-strong, or $\kappa^{+n+1}$-strong, that is, there is an elementary embedding $j:V\to M$ with $\mathrm{cp}(j)=\kappa$ and $V_{\kappa+n}\subset M$. Using extender based Radin forcing at $\kappa$, he obtains an extension where $\kappa$ is still inaccessible, and $V_\kappa$ satisfies $\mathsf{GCH}^{+n}$. The final model is then $V_\kappa$.
(The Foreman-Woodin argument is similar in this respect, they begin with a supercompact $\kappa$ with infinitely many inaccessible cardinals above, and their final model is the $V_\kappa$ of the forcing extension. Again, $\kappa$ is inaccessible in this extension, and in fact significantly more. I do not know how to arrange such detailed global behavior of the continuum function, without cutting the universe at some point.)
Naturally, since the proof produces a set model of the desired statement, this means that Merimovich's assumptions are an overkill, but I do not know what the large cardinal companion of $\mathsf{GCH}^{+n}$ is, or even of better upper bounds. This seems a rather delicate and attractive problem (then again, this is an area I have always found very appealing.).