Coding a model of $0^\sharp$ from a $\Pi^1_1$ Gale-Stewart game

Question

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"?

Edit:

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.

Answer 1

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.

Here,

• 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 Ralf Schindler and Yong's joint work "Harrington's Principle in Higher Order Arithmetic" (published in J. Symb. Log. vol. 80, no. 2), 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.

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.