As a preface to this question, this is my first time asking on Math overflow, and this seemed like the sort of question that would be acceptable here. However, I apologize if it is not.

A method for coding models from a Gale-Stewart game proceeds as follows: Our aim is to obtain a model of the form $L_\gamma[a]$ such that $L_\gamma[a]\models$ "$a$ is a large cardinal property" where $a$ can be coded by a sequence of ordinals, $\mathcal{S}$. Since $a$ can be coded by a sequence of ordinals, we see that it can be coded by a real $x\in{}^\omega\omega$ by by coding each well-order in the sequence, of by coding a definition of the sequence. With that in mind, a rough set up of the game has a legal play $z\in{}^\omega\omega$ that codes both $\gamma$ and $\mathcal{S}$. One of the players wins when the model $L_\gamma[a]$ produced is the one we were looking for. This technique is due to Martin and Solovay.

One can show that $\Pi^1_1$-determinacy is equivalent to the existence of $0^\sharp$ (left to right is due to Harrington, and right to left is due to Martin), but every proof of "$\Pi^1_1$-determinacy implies that $0^\sharp$ exists" that I know of goes through the following lemma:

$\mathbf{Lemma}$: If there is a real $x$ such that every $x$-admissible ordinal is a cardinal in $L$, then $0^\sharp$ exists.

The question then arises as to whether or not it is possible to get $0^\sharp$ from $\Pi_1^1$-determinacy more directly. In particular, my question is as follows:

Is it possible to construct a $\Pi^1_1$ game that produces a model satisfying the statement "$0^\sharp$ exists"?


I've realized that this is actually a rather difficult question to answer as stated. I asked it because I could not have been the first person to think of this, and was curious if anyone else had made progress. However, the question was ill-formed in some sense, but here is related question that is perhaps more answerable:

As far as I know, there is no proof of "$0^\sharp$ exists from $\Pi^1_1$-determinacy that does not utilize the above lemma. Is this simply because no one has worked on this since, or because there is something about $\Pi^1_1$ sets that make this difficult?

From what I understand, $0^\sharp$ is a well-studied object insofar as much is known about it. There is also a fair bit of work that has been done on determinacy, but I have not seen as much in conjunction with $\Pi^1_1$ determinacy. Most of what I have seen is in regards to OD-Determinacy, Projective Determinacy, and Determinacy in $L(\mathbb{R})$. Now, if one were interested in trying to prove $0^\sharp$ exists from $\Pi^1_1$-determinacy, it seems that a good approach would be to try and produce a model that contains $0^\sharp$ from a $\Pi^1_1$ game. The next question is whether or not the above technique of Martin and Solovay would be the best approach. This technique was used with stronger determinacy hypotheses, so I wonder if the low complexity of $\Pi^1_1$ sets would make it the case that a different approach would be better.

A good starting place may be the known proofs of "$0^\sharp$ exists from $\Pi^1_1$-determinacy. We define a set $A\subset{}^\omega\omega$ as follows: $a\in A$ if, and only if there is a binary relation $R$ on $\omega$ which is recursive in $a$ such that $(\omega, R)$ is isomorphic to an end extension of $(L_{\omega_1(a)},\in)$ where $\omega_1(a)$ denotes the first $a$-admissible ordinal. We then prove that $A$ is $\Sigma^1_1$, closed under Turing equivalence, and non-empty. This is the game that Harrington used to prove that $0^\sharp$ exists. However in an exercise in Martin's notes on determinacy, he defines a different game in the hint.

We play a game $G$ on $^{<\omega}\omega$. For each play of $G$, $I$'s part codes a relation $R$ on $\omega$ and let $II$'s part of the play code a relation $E$ on $\omega$. If $R$ is not a well-ordering of $\omega$, $I$ loses. If $R$ is a wellordering of $\omega$, let $\beta$ be its order type. Then, $II$ wins if and only if $(\omega;E)$ is a model of extensionality, and there is a $g:L_\beta\rightarrow\omega$ that embeds $(L_\beta;\in)$ into $(\omega;E)$ as an initial segment. We then show that the set we are playing over is $\Pi^1_1$, and that $I$ has no winning strategy in $G$.

This seems a bit closer to the idea presented in the first real paragraph of this question. In particular, perhaps one could construct a $\Pi^1_1$ game that codes a nontrivial elementary embedding $j:L_\alpha\prec L_\beta$ for limit ordinals $\alpha$ and $\beta$ using a similar idea. This is not exactly what we are looking for, but it's getting closer.

  • 1
    $\begingroup$ I don't know any way to get $0^\#$ directly from a game, and I'm inclined to guess that no one else does either. The reasons for my guess are (1) this question has been here for a while (it's about to sink off the front page of MO) with no answer, and (2) the proof from $\Pi^1_1$ determinacy that $0^\#$ exists was, as you said, found by Harrington, not by Martin or Solovay. $\endgroup$ – Andreas Blass Jun 8 '13 at 14:37
  • $\begingroup$ That makes sense, thank you for the input. At the very worst, this suggests that the problem may be a fun one to play around with. $\endgroup$ – Shehzad Ahmed Jun 8 '13 at 17:22

This problem is very much open.

Cheng Yong calls Harrington's $\star$ the assumption that there is a real $x$ such that all $x$-admissible ordinals are $L$-cardinals. From the work of Yong we know that Second- and even Third-order arithmetic do not suffice to prove that Harrington's $\star$ implies the existence of $0^\sharp$. Whether this was possible was originally asked by Woodin, who proved that Second order arithmetic suffices to show that $\mathrm{Det}(\Sigma^1_1)$ implies Harrington's $\star$.

This appears in Yong's dissertation, Analysis of Martin-Harrington theorem "$\mathrm{Det}(\Sigma^1_1)\leftrightarrow 0^\sharp$ exists" in higher order arithmetic, National University of Singapore, 2012.


  • Second order arithmetic, $Z_2$, is formalized as: $(\mathsf{ZFC}-$ Power set axiom$)+$ All sets are countable.
  • Third order arithmetic, $Z_3$, is $(\mathsf{ZFC}-$ Power set axiom$)+\mathcal P(\omega)$ exists $+$ All sets have size at most continuum.
  • Fourth order arithmetic, which Yong shows proves that Harrington's $\star$ implies the existence of $0^\sharp$, is $(\mathsf{ZFC}-$ Power set axiom$)+\mathcal P^2(\omega)$ exists $+$ All sets have size at most $2^{2^{\aleph_0}}$.

In joint work by Ralf Schindler and Yong, the situation has been further clarified: $Z_2+$ Harrington's $\star$ is equiconsistent with $\mathsf{ZFC}$, and $Z_3+$ Harrington's $\star$ is equiconsistent with $\mathsf{ZFC}+$ There is a remarkable cardinal. See here.

As question 8.0.14 in his thesis, Yong asks whether $Z_2$ proves Harrington theorem. This is tricky, since $Z_2$ proves that $\mathrm{Det}(\mathbf\Sigma^1_1)$ is equivalent with "For all reals $x$, $x^\sharp$ exists." The reason why the lightface version is open, Yong admits, is that the only route we have from $\mathrm{Det}(\Sigma^1_1)$ to the existence of $0^\sharp$ is via Harrington's $\star$, so the question is effectively asking for a different argument. There are several sufficiently different proofs of Harrington's theorem. For example, there is the argument in Recursive Aspects of Descriptive Set Theory by Mansfield and Weitkamp, via non-$\omega$-models of $\mathsf{KP}$. There is Harrington's original proof, using Steel's forcing. There is Sami's proof, from Analytic determinacy and $0^\sharp$: A forcing-free proof of Harrington's theorem. All use Harrington's $\star$ in an essential fashion.

The question of whether a different route is possible has been studied, of course, but unsuccessfully.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.