Previously I’ve only been talking about large cardinals and determinacy theories as if they were the only consistency hierarchies around. There is another important class of axioms, which has the added benefit of being, dare I say it, more useful to mathematicians not working in set theory. The reason for this is probably that these forcing axioms have a handful of consequences of a non-set theoretic nature, making them easier to apply in (mathematical) practice. When it comes to the consistency strength of these axioms though, things get a lot more hazy: we know very little about the strength of (almost all of) these axioms. I’ll introduce these axioms here and state what is known to date.
I was recently playing a (set-theoretic) game and the question of whether it was determined slowly emerged. As I was working in a ZFC context, most of the determinacy results were of no use to me, so I tried to investigate how much we really know about ZFC determinacy. Of course we can’t have full determinacy (AD), but how about definable variants, where we alter both the objects played and the length of the game?
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.
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.
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.