Projective Determinacy and Zero Sharp over Third-Order Arithmetic

Definitions and mathematical statement

The supplied question concerns a provability implication over a theory denoted by $Z_3$, called third-order arithmetic. Its intended axiom system is not specified. Third-order arithmetic ordinarily has objects representing natural numbers, sets of natural numbers, and collections of sets of natural numbers; this description alone does not fix its comprehension or other axioms.

For the usual interpretation of determinacy, write ${\mathbb{N}}^{{\mathbb{N}}}$ for Baire space and ${\mathbb{N}}^{<{\mathbb{N}}}$ for the finite sequences of natural numbers. Given a payoff set $A\subseteq{\mathbb{N}}^{{\mathbb{N}}}$, players I and II alternately choose natural numbers, with I moving first, producing $x\in{\mathbb{N}}^{{\mathbb{N}}}$. Player I wins exactly when $x\in A$; otherwise player II wins. A strategy assigns a natural-number move to each finite position at which the relevant player moves. It is winning if every play consistent with it is won by that player. The set $A$ is determined if one of the players has a winning strategy.

In the usual descriptive-set-theoretic interpretation, a $\Pi^1_1$ payoff set has a definition of the form \[ x\in A\quad\Longleftrightarrow\quad \forall y\in{\mathbb{N}}^{{\mathbb{N}}}\;\theta(x,y,p), \] where $\theta$ is arithmetical and $p$ denotes any permitted real parameters. The assertion $\Pi^1_1\text{-}\mathrm{Det}$ says that every payoff set in the specified $\Pi^1_1$ class is determined. The source does not specify whether real parameters are permitted, nor whether this is formalized by a formula scheme or by quantification over third-order payoff sets.

The notation $0^{\#}$ conventionally denotes zero sharp, a real associated with the theory of the constructible universe $L$ with indiscernibles. The source does not give a formula in third-order arithmetic expressing its existence, or specify how the necessary constructibility and indiscernibility notions are represented there.

With these unresolved choices explicitly retained, the intended question is whether \[ Z_3\ \vdash\ \left(\Pi^1_1\text{-}\mathrm{Det}\ \Longrightarrow\ \exists r\subseteq{\mathbb{N}}\;(r\text{ codes }0^{\#})\right). \] This display is a template for the intended implication, not a fully specified sentence of a fixed formal theory. A precise provability question requires the axioms of $Z_3$, the determinacy formulation and parameter convention, and the internal predicate for coding $0^{\#}$ to be supplied.

Short English statement

The question asks whether third-order arithmetic can prove that determinacy of all $\Pi^1_1$ games implies the existence of zero sharp. The supplied record leaves the base theory and the internal formulations insufficiently specified, so the displayed implication remains a statement template requiring human mathematical review.

Sources

• Local UnsolvedMath registry, data/unsolvedmath/problems.json, permanent ID $30002481$, source problem code catalogue entry. The supplied record belongs to the Oberwolfach Reports Open Problems collection and lists proposed year 2014; no individual proposer is identified.
• Supplied report citation: Set Theory (2014), Oberwolfach Reports, pp. 91--144, DOI 10.4171/owr/2014/02. https://doi.org/10.4171/owr/2014/02. The supplied citation gives a report-wide page range, without an exact location for this question.
• Supplied literature source: Oberwolfach set theory report. https://ems.press/content/serial-article-files/46488.
• Supplied literature source: Cheng--Schindler, higher-order arithmetic. https://arxiv.org/abs/1503.04000.
• Literature assessment dated exactly 2026-08-21: the supplied curation labels the problem open, states that the classical implication from $\Pi^1_1$ determinacy to the existence of $0^{\#}$ is a theorem over $\mathrm{ZF}$, and describes the higher-order-arithmetic formulation as imprecise and the corresponding $Z_3$ question as unresolved. This is supplied dated curation derived from the OWR record, not an independently verified literature assessment. Its time-sensitive status and cited claims require independent verification.
• The supplied registry assigns the statement the label corrected_verified and reports a manual semantic, typographic, and LaTeX review of its cleanup. These supplied editorial labels do not resolve the formalization choices identified above or establish mathematical correctness.