A definable failure of the singular cardinal hypothesis

We show first that it is consistent that κ is a measurable cardinal where the GCH fails, while there is a lightface definable wellorder of H(κ ⁺). Then with further forcing we show that it is consistent that GCH fails at ? _ω , ? _ω strong limit, while there is a lightface definable wellorder of H(? _ω+1) (“definable failure” of the singular cardinal hypothesis at ? _ω ). The large cardinal hypothesis used is the existence of a κ ⁺⁺-strong cardinal, where κ is κ ⁺⁺-strong if there is an embedding j: V → M with critical point κ such that H(κ ⁺⁺) ? M. By work of M. Gitik and W. J. Mitchell 12], 20], our large cardinal assumption is almost optimal. The techniques of proof include the “tuning-fork” method of 10] and 3], a generalisation to large cardinals of the stationary-coding of 4] and a new “definable-collapse” coding based on mutual stationarity. The fine structure of the canonical inner model LE] for a κ ⁺⁺-strong cardinal is used throughout.