# A game with boldface strength

This is a problem which has been bothering me for a while now; it doesn't seem inherently too hard, but I haven't been able to make any real headway, so I'm putting it out in the open since at this point I just want to know the answer. I don't think it has any deep value, but it's a natural question (at least to me) which I haven't seen addressed in the literature.

In brief: is there a single game $G$, defined by a formula in the language of second-order arithmetic, such that the statement "$G$ is determined" isn't true in any Turing ideal with a maximal element (viewed as an $\omega$-model of RCA$_0$)? Say in this case that $G$ has boldface strength (as opposed to the merely lightface strength that we're used to individual instances of principles having, in reverse mathematics).

(Note,of course,that because a model $M$ thinks $G$ is determined doesn't mean $M$ contains an actual winning strategy, or even that $M$ is correct about who wins.)

Let me say a bit about my thoughts so far:

Why the answer might be yes: the statement "$G$ is determined" is $\Sigma^1_2$ on top of $G$; so it easily has enough quantifier complexity to have boldface strength, even if $G$ is low in the projective hierarchy. Now of course $G$ can't be too low in the projective hierarchy - after all, we need the Turing ideal generated by a winning strategy for $G$ to not satisfy "$G$ is determined," so membership in $G$ has to be sufficiently non-absolute. But once $G$ gets complicated enough, all bets seem off. That is: if $G$ is sufficiently complicated, then merely having a winning strategy doesn't matter, the model needs enough structure to be able to verify that the strategy always wins, and there's no obvious upper bound to how complicated this extra structure could be.

An obstacle: A natural guess for a game with boldface strength is the following: Player $1$ plays a second-order sentence $\varphi$ of some bounded complexity (say, $\Pi^1_7$), and player $2$ plays "true" or "false" then player $2$ wins iff $\varphi$'s truth value is player $2$'s play. (The bound on the complexity of $\varphi$ is needed for this game to be definable.) However, this doesn't work, since by Martin's cone theorem the models corresponding to all sufficiently large degrees will yield the same theory, so once our topped models get big enough they'll see how to win this game.

A response: More generally, the obstacle above suggests that the game needs to involve playing a specific element of the top degree of the model (if there is one). This suggests a game like the following: player $2$ builds a real of maximal Turing degree, and also responds to player $1$'s queries about that real. To give player $2$ a chance, we should demand that player $1$ only gets to ask finitely many questions. Meanwhile, we have a real synergy between this game and the existence of a maximally complicated real: on the one hand, in a model with a maximally complicated real player $2$'s strategy must build something as complicated as itself, while in a model with no maximally complicated real player $1$ wins vacuously (e.g. the classical analysis has no relevance to the case we're interested in).

In particular, a game of the following form seems promising: Player $2$ builds a real $r$, while player $1$ plays finitely many second-order sentences of some fixed complexity (say, $\Pi^1_7$), and player $2$ responds to player $1$'s queries with "True" or "False" as above; player $2$ then wins iff $r$ has maximal Turing degree and they never guessed incorrectly about the theory of $(\omega\cup\mathcal{P}(\omega); +,\times, r)$. (Note that all of this is defined internally.)

Another obstacle: This suggests some recursion theorem trickery, where player $1$ manages to ask player $2$ about their own strategy in such a way that player $2$ is trapped. In particular, the real that player $2$ builds is guaranteed to compute all of their strategy, if player $2$ is playing according to a winning strategy. However, I haven't managed to get this line of attack to pan out, the main problem being that player $2$'s real (and hence the way player $2$'s real computes player $2$'s strategy) depends on player $1$'s queries.

Is there a single game with boldface strength?

The proof of the Kechris-Solovay theorem produces a real $x_0$ such that whenever $x_0 \leq_T x$, every game lightface definable in $M_x = (\omega, \{y : y\leq_T x\},\in)$ is determined in $M_x$. This shows there are many principal Turing ideals in which lightface PD holds. We basically copy the argument given in Woodin-Koellner Theorem 6.6.
If there does not exist such an $x_0$, by $\Delta^1_1$ Turing Determinacy, there must be a real $x_0$ such that whenever $x_0\leq_T x$, there is some game lightface definable in $M_x$ that is not determined in $M_x$. For any $x$, let $\varphi_x$ be the least formula defining in $M_x$ a nondetermined set of reals, if there is one, and let $\varphi_x$ be undefined otherwise. If $\varphi_x$ is defined, let $A^x$ be the set of reals defined in $M_x$ by $\varphi_x$.
Consider the game $G$ (defined in $V$) where I plays $a,b$ and II plays $c,d$ (alternating in the usual way), and I wins if $\varphi_{\langle a,b,c,d\rangle}$ is defined and $a*d\in A^{\langle a,b,c,d\rangle}$. By $\Delta^1_1$-Determinacy, one player has a winning strategy. We aim to get a contradiction, no matter who wins.
Suppose I wins by the strategy $\sigma_0$. Take $x\geq_T\sigma_0,x_0$. We claim there is a strategy $\sigma \leq_T x$ such that for any $d\leq_T x$, $\sigma * d\in A^x$, which contradicts that $A^x$ is not determined in $M_x$. Against $d\in \omega^\omega$, $\sigma$ will respond (well, $\sigma$ goes first but you know what I mean) with the real $a$ such that $\sigma_0$ plays $a,b$ against $x,d$. Then $\sigma$ is recursive in $x$. We must show $\sigma*d\in A^x$ when $d\leq_T x$. But note that with $a,b$ defined as above from $d$, $x\equiv_T \langle a,b,x,d\rangle$, so the fact that $\sigma_0$ is winning for I in $G$ implies $a*d\in A^{\langle a,b,x,d\rangle} = A^x$, and hence $\sigma*d\in A^x$.
The contradiction in the case that II wins $G$ by $\tau_0$ is reached by a symmetric argument, with the minor modification that we use the fact that $x\geq_T x_0$ to show that II wins the relevant plays by $\tau_0$ because $a*d\notin A^{\langle a,x,c,d\rangle}$, and not because $\varphi_{\langle a,x,c,d\rangle}$ was undefined.