Philip Welch

An iteration to define L[Reg]

We define, informally, an iteration of Jensen's O^sword in which L[Reg] is definable as an inner model.
(This is the first part of a series of lectures to prove that L[Reg] is a class hyper-generic extension of W. This part requires a knowledge of iteration theory of mice; the next part(s) of iterated Magidor forcing.)