The last two posts covered the ‘classical’ theory of scales, meaning the characterisation of the scaled pointclasses in the projective hierarchy. Noting that and , the natural generalisation of this characterisation is then to figure out which of the and classes are scaled, for . This is exactly what Steel (’83) did, and I’ll sketch the results leading up to this characterisation in a couple of blog posts. This characterisation is also precisely what’s used in organising the induction in core model inductions up to .
To be able to analyse in the depth that we need, we have to introduce some fine structure. This is mostly completely analogous to the fine structure of , so I’ll just mention a few results that we’ll need, without proof. The first one is that condensation still holds in our new setting.
Theorem (Condensation). If and then for some .
Next up, recall that there are uniformly surjections , as shown in Jensen (’72). Here’s the analogue.
Proposition. There are uniformly surjections .
The last fine structural fact that we’ll need is the existence of definable Skolem functions. As in the case of , also shown in Jensen (’72), this is a consequence of uniformisation.
Theorem. Whenever holds, satisfies uniformisation, so that has a Skolem function.
Here is the ‘th projectum as usual, and just means . The requirement on the projectum is necessary, as shown in the last part of Steel (’83). This is all the fine structure that we’ll need, so let’s return to the scales.
Moschovakis (’83) showed that to find scales on a given set, it suffices to construct a certain game representation of the set. We need a definition.
Definition. A closed game representation of a set is a pair such that
- is a closed game on of length
- There exists a binary relation such that player I has a winning quasi-strategy in iff , and is winning for player I iff holds, where .
We then have the following result due to Martin and Steel, building on the construction in Moschovakis (’83). To make the statement slightly more clear we introduce some notation. If is a closed game representation of then define the binary relation for as iff is a partial play in of length from which player I has a winning quasi-strategy.
Theorem (Moschovakis-Martin-Steel). Let be a closed game representation of and let be such that and for every . Then implies that there is a scale on in .
This is the primary, indeed only, method we’ll use to construct every scale we need. The first major theorem on the scale property is the following.
Theorem (Steel ’83). For and assuming holds, has the scale property (note that it’s lightface).
I’ve written up the full proof of this theorem here, but to just have an idea of what goes on I’ll give a (very rough) outline of the proof here. We pick some and want to produce a -scale on . To find this scale we use the above Moschovakis-Martin-Steel theorem, so the plan is to come up with a game representation. The case where is a limit is ever so slightly simpler, so that’s the case I’ll focus on in this sketch.
Let be a formula defining ; i.e. that iff . Further, for , define the sets
so that . The plan is then to construct closed game representations on each of the ‘s and then “glue” the corresponding scales together to get a scale on in such a way that the new “glued up” scale is a -scale on . Here’s a typical run of .
where , and for all . The idea behind the game is that player I tries to construct a -structure with . To do this we stitch together a theory such that whenever we have to have that and — the ‘s are the ones encoding this theory . The theory isn’t completely sufficient however, as it can’t encode the second-order property of being wellfounded and it doesn’t control which reals contains. The solution to the first issue is the ‘s, which encode an order-preserving map , and the second issue is solved by requiring that the ‘s are reals of and capture the truth of statements involving reals over .
There’s a part of the proof which I’d like to emphasize. To show that the resulting scale satisfies our definability requirement, a (simply definable) notion of an honest play is introduced, and the key lemma is then that, for player I, playing honestly is equivalent to winning the game (this is analogous to the fact that in closed games, player I playing non-losing plays is winning). That honest plays are winning is quite straight-forward, but I find the proof of the converse quite ingenious, a proof that’s due to Woodin.
What he does is consider the statement “if is a winning play then it’s honest”, call it , and the strategy is then to show that whenever is a countable transitive model of then , which suffices to show that . So, consider such an and, in , let be a winning strategy starting from . Then define to be the poset of all partial plays extending and following and force with .
The generic supplies us with a “generic play” of the game which is winning, circumventing the use of . It’s then relatively simple to show that is honest in the generic extension, and absoluteness of honesty then gives us honesty in . This way of using forcing as a choice principle also reminds me of the proof I sketched for the Hahn-Banach theorem, where an ultrafilter acted as the “glue” instead of a generic, producing a canonical element.
If you’re interested in the full proof, here you go. This was then the first step to finding scaled pointclasses, and next time we’ll use this result to find boldface scaled pointclasses as well, utilising the notion of a gap. More on that next time.