His thesis, -determinacy and sharps, is a survey of the Harrington-Martin theorem, showing the equivalence between a definable fragment of determinacy, and a large cardinal hypothesis.
After the fold, I review the basic notions, and give the tiniest of hints of what the theorem is and how its proof goes. Since the material is technical, the post is not really self-contained.
Baire space is the set of all (infinite) sequences of natural numbers, that is, the set of all functions (as customary, we identify with the ordinal ). We can consider Baire space as a topological space by giving the discrete topology, and the product topology. This is a completely metrizable topology, with metric given by and, if , then iff is least such that .
A subset of Baire space is coanalytic, or , iff its complement is the image of Baire space under a continuous function.
Given a set , the Gale-Stewart game associated to is the infinite game between two players I and II that alternate playing natural numbers in each turn, with I playing first. At the end of a run of the game, the two players have collaborated to produce an element of Baire space, and player I wins the game iff . We say that (or the associated game) is determined iff one of the players has a winning strategy.
(This can be readily generalized: Given , we can consider the similar game where the players now play elements of rather than natural numbers.)
Coanalytic determinacy is the statement that all sets are determined. Although one can prove in that all Borel games are determined, is not enough to prove the same result for all coanalytic games.
Tony Martin proved in 1970 that coanalytic determinacy holds as long as we assume the existence of mild large cardinals, see
- Donald A. Martin. Measurable cardinals and analytic games. Fund. Math., 66 (3), (1969/1970), 287–291. MR0258637 (41 #3283).
Specifically, Martin showed this from the assumption that there is a measurable cardinal. Recall that is measurable iff it is the critical point of a nontrivial elementary embedding from the universe into some transitive class . It is a classical result of Gale and Stewart that all closed games (on any , where again is discrete and carries the product topology) are determined.
What Martin did was to associate to each coanalytic set a closed set in a (much) larger space in such a way that the corresponding games are equivalent, in the sense that either player has a winning strategy in one iff the same player has a winning strategy in the other, and in fact there is a translation procedure that associates strategies in one game with strategies in the other.
Very roughly speaking, what Martin does is to take advantage of the fact that coanalytic sets admit a nice representation: A set is coanalytic iff it is -Suslin, that is, there is a tree on such that for all in Baire space, iff there is some such that for all (that is is in the first-coordinate projection of the closed set of infinite branches through the tree ).
Given such a tree , a point is not in iff the corresponding tree of attempts to find a “witness” is well-founded. This is the tree on whose elements are finite sequences of countable ordinals such that if is the length of , then . This means that the tree admits a rank function, that associates to each an ordinal in such a way that if properly extends , then .
What Martin does is to use the ultrafilter associated to the measurable cardinal to select “typical” ordinals that “anticipate” the values of the ranking function.
Actually, analysis of the proof shows that the measurable is an overkill, and the assumption that all elements of Baire space admit sharps suffices (in the published paper, Martin uses that there is a Ramsey cardinal). Given a point , the assertion that the sharp for exists is (equivalent to) the statement that there is a nontrivial elementary embedding . This provides us with an -ultrafilter that suffices to carry out the ranking argument hinted at above.
Leo Harrington showed in 1978 that the use of sharps is necessary, in the paper
- Leo Harrington. Analytic determinacy and . J. Symbolic Logic, 43 (4), (1978), 685–693. MR0518675 (80b:03065).
What Leo did was to identify an assumption that implies the existence of sharps, and then show that the determinacy of certain games implies this assumption. Specifically, to prove that exists it suffices to establish that there is a point in Baire space such that, for all (sufficiently large) countable ordinals , if is admissible, then is a cardinal of . Here, a structure is admissible iff it is a model of , a weak fragment of set theory that allows us to carry out basic recursive arguments.
Assuming coanalytic determinacy, Leo proceeds to find such a point using the winning strategy of the following game : As usual, I and II alternate playing natural numbers. The moves of I code a binary relation on , and the moves of II code another binary relation . Player I loses unless is a well-ordering of . If it is a well-ordering, let be its order type. In that case, Player II wins iff is a model of extensionality that end-extends . One needs to verify of course that the payoff set of is indeed and that player I does not have a winning strategy. The determinacy assumption then gives us that there is a winning strategy for player II. We can identify with a point in Baire space.
Given a countable ordinal with admissible, Harrington then uses Steel’s forcing over to argue that must be a cardinal in . Essentially, if this is not the case, then a collapsing map witnessing that is not a cardinal can be identified “too quickly” (using a generic for Steel’s forcing), contradicting the admissibility of .
Shehzad presentation of sharps is “classic”. For a presentation in terms of mice, I recommend Ralf Schindler‘s recent book.