HOD is the proper class of all sets such that both and all the elements of the transitive closure of are definable using ordinal parameters. HOD is a model of ZFC, but in general its structure is not really known. In the late 90’s it was shown by Steel and Woodin that exhibits mouse-like behaviour, and since then there’s been a great interest in finding the HODs of other models than . I’ll here give a (non-exhaustive) overview of both which HODs have been shown to have this mouse-like structure and also explain the general strategy used so far in finding these mice.

Let’s start off with some history. Interest in studying the structure of HOD started in the beginning of the 80’s, where three out of the fourteen famous Delfino problems involved HOD. Assuming ,

- is every regular cardinal measurable? (yes, shown by Moschovakis and Kechris)
- is there a which is -supercompact in HOD? (no, shown by Woodin and Shelah)
- does HOD satisfy GCH? (yes, shown by Steel and Woodin)

The positive solution to the last question sparked a lot of interest, since Steel showed even more than just GCH – he showed the remarkable fact that, assuming , is a mouse below , the least ordinal to which there is no surjection . This was the kickoff to a great deal of HOD research, and Woodin showed that the full HOD of is a new kind of mouse, having both an extender sequence and a fragment of its own iteration strategy as predicates – this breed of mice is now called *hod mice*.

A natural question is then if this is something peculiar to or if it also holds in other HODs. Investigating the HOD of turned out to be incredibly hard, but the model turned out to be more amenable to an approach analogous to Steel’s approach to , where is -generic for collapsing the least inaccessible of to be . This has very recently been generalised by Sargsyan and Uhlenbrock to the HOD of .

Abstracting away, we can also view as simply a special case of a model satisfying , where is an ostensibly stronger version of . Taking this approach, we can then beef up this theory and ask about the HOD of the least model satisfying that theory. This has resulted in a HOD analysis of the least model of the various -theories floating around.

That was a bit of an overview. Let’s now dig down into *how* these HODs are being investigated. As a representative example, let’s take a look at the simplest instance: the HOD of . Let’s assume (boldface) -determinacy, which is equivalent to the existence of and for all reals . Strictly speaking we could do with the weaker assumption that

,

but having makes the argument a bit more clean. Fix some such that . Firstly, our hypothesis implies that has a unique iteration strategy , so we can construct the direct limit of all -iterates of such that , where is the Woodin cardinal of . Call this direct limit and its Woodin cardinal .

The problem with working with is that it doesn’t exist within , so we want to build an *internal* directed system of mice. I’ll leave out the technical details, but roughly speaking the system consists of all countable mice inside of which looks like (remember we’re in , so countable here means of size less than the first inaccessible of ). This then yields the direct limit .

To show that is a well-founded model, we define an elementary map , which suffices as is well-founded as it’s a -iterate of . This map is defined as taking , pulling it back to a mouse which is in both directed systems (the existence of such a mouse has to be shown here) and then going up to via the direct limit map. We also get that , so that in particular the two direct limits have the same Woodin cardinal.

To recap, we’ve now got an internal limit and an external limit which agree below their common Woodin cardinal . Since our internal directed system was definable in , we get that

.

The next step is to show the opposite inclusion, for which we need a so-called *derived model resemblance*. First, let define for any ordinal to be the image of inside , yielding a function . The *derived model* of is , where is -generic for collapsing the least inaccessible of strictly above to be . The derived model resemblance then implies that

for any formula and ordinals . The next step is then to show that

. (1)

We get the right-to-left inclusion simply because both and are -definable. For the other direction the first thing to show (which I’ll skip here) is that for an -definable . Given this fact we can then use the above resemblance to transfer the fact over to , so that lies in , yielding (1).

Now let be the restriction of to trees on such that . The last step is then showing that

,

which is done by showing that is definable using and , and then using (1). Summarising, HOD was found by

- Cooking up a directed system of mice
- Showing that we can transfer truths between and the derived model of the direct limit
- Establishing that HOD is of the form for some -definable
- Using (2) and (3) to show that HOD is of the form for some
- Defining a partial strategy of from .

This strategy is basically what’s going on in the cases as well, and I suspect this is also what’s happening with minimal models of -theories.