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.

# Borel Determinacy

The proof of Borel determinacy doesn’t seem to have the best reputation, as it’s both rather long, quite technical and it’s really easy to lose track of what’s going on. I’ve noticed that the same proof can be presented in a more structural setting, making the core ideas of the proof be slightly clearer. I’ll try here to present what’s going on in the proof, using the structural framework of games I set up in my previous post. The full proof can be found in my determinacy project.

# The structure of games

Games in set theory are usually informally described by describing the rules of the two players and the winning condition. Sometimes we need to describe an interaction between games, which then becomes quite ad hoc, describing certain functions with properties that are desired in the specific proof in question. This is especially prominent in the proof of Borel determinacy, where *unraveling coverings* are used to transfer determinacy statements between games. I’ll here attempt to describe this framework in a more abstract setting, viewing games as *objects in their own right*, which at the very least might make the proof of Borel determinacy clearer.

# From Determinacy to a Woodin II

In the prequel I sketched a proof of how determinacy hypotheses could imply the measurability of both and inside . The latter is really the first step in showing the *much* stronger assertion that is Woodin. I’ll here sketch what main ideas are involved in the proof of this fact.

# What is K?

The *core model* K is, among other things, great for providing lower bounds for the consistency strength of some interesting theory. For instance, every Jónsson cardinal is Ramsey in K, showing that the two are equiconsistent. Usually there are a lot of *different* K’s with different properties, sometimes denoted by things like , or something along those lines. This is my attempt at (briefly) explaining what K is, and what the differences between the various versions are. Here’s an overview of the various core models I’ll cover:

# From Determinacy to a Woodin I

In my previous posts I provided a sketch of how a measurable above a limit of Woodins implies that holds in . The “converse”, saying that implies that there is a model with infinitely many Woodin cardinals, is a lot more complicated. I will try to simplify a lot of these complications here, to give an idea of what is going on. I will only focus on showing the existence of a single Woodin (for now), where the Woodin in question will be inside of . As always, I will be very sketchy in this blog post, but provide more details in my note.

# Hahn-Banach sans Zorn

The *Hahn-Banach* *Theorem* in functional analysis is the theorem saying more or less that normed vector spaces have many bounded linear functionals. The theorem is usually proven via Zorn’s lemma, giving the impression that Hahn-Banach uses the full power of choice. I’ll here give a proof based on the *ultrafilter lemma*, that every filter can be extended to an ultrafilter. One of the benefits of this approach, besides relying on a (strictly) weaker assumption, is that we get a little more information about how the functionals are constructed. The idea is that the ultrafilters allow us to “glue” functionals together. A latex’ed version can be found here.