Determinacy and reflection principles in second-order arithmetic

Work inside a model of $\mathsf{ACA}_{0}$. First suppose that the reflection principle $\Pi^{1}_{n}\text{-}\mathsf{Ref}(T)$ holds. Fix a standard formula $\varphi(x)$. Let $a\in\mathbb{N}$ be such that $\mathrm{Pr}_{T}(\ulcorner\varphi(a)\urcorner)$. $\varphi(a)$ is a sentence inside the model, so we can use the reflection principle, so $\varphi(a)$ is true.

Now, suppose the reflection scheme $\Pi^{1}_{n}\text{-}\mathsf{RFN}(T)$ holds. Let $\varphi$ be a sentence inside the model such that $\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)$ holds. For a contradiction, suppose that $\varphi$ is false. Fix a standard universal lightface $\Pi^{1}_{n}$-formula $\pi^{1}_{n}(x)$. For some $e\in\mathbb{N}$, $\mathrm{Pr}_{\mathsf{RCA}_{0}}(\ulcorner\varphi\leftrightarrow\pi^{1}_{n}(e)\urcorner)$ holds. Therefore $\mathrm{Pr}_{T}(\ulcorner\pi^{1}_{n}(e)\urcorner)$. The reflection instance for $\pi^{1}_{n}$ implies that $\pi^{1}_{n}(e)$ is true.

Note that we may take the arithmetical parts of $\varphi$ and $\pi^{1}_{n}$ to be $\Sigma^{0}_{2}$. That is, $\neg\varphi$ is $\exists X\forall m_{0}\exists m_{1}.\psi(X,m_{0},m_{1})$. Fix $X_{0}$ such that $\forall m_{0}\exists m_{1}.\psi(X_{0},m_{0},m_{1})$ holds. We can use $\mathsf{ACA}_{0}$ to construct an $\omega$-model $\mathcal{M}$ which satisfies $\mathsf{RCA}_{0}$ and includes $X_{0}$. Since $X_{0}\in\mathcal{M}$, we have $\mathcal{M}\models\mathsf{RCA}_{0}+\neg\varphi$, and so $\mathcal{M}\models\neg\pi^{1}_{n}(e)$. Since the arithmetical part of $\pi^{1}_{n}$ is $\Sigma^{0}_{2}$, we can show that $\mathcal{M}\models\pi^{1}_{n}(e)$ also holds. We conclude that $\varphi$ is true. ∎

Fix $n\in\mathbb{N}$ and $X\subseteq\mathbb{N}$. We prove the existence of a sequence ${\langle X_{0},\dots,X_{n}\rangle}$ of sets such that $X_{0}=X$ and $X_{i+1}=\mathrm{TJ}(X_{i})$, for $i<n$. Let $\pi^{0}_{1}$ be a fixed universal lightface $\Pi^{0}_{1}$-formula. The Turing Jump $\mathrm{TJ}(X)$ of $X$ is the set of $m$ such that $\neg\pi^{0}_{1}(m,X)$ holds.

We claim that there is a set $\tilde{\tau}$ computing universal winning strategies for all $(\Sigma^{0}_{1})_{k}$ games on Cantor space with only $X$ as a parameter, for all $k\in\mathbb{N}$. Consider the following game: $\mathsf{I}$ chooses an index $e$ for the payoff of a $(\Sigma^{0}_{1})_{k}$ game, coded as a sequence of $e$-many $0$s followed by a $1$; $\mathsf{II}$ answers with their choice of role in the game with index $e$; then $\mathsf{I}$ and $\mathsf{II}$ play the game with index $e$; whoever wins the subgame wins the whole game. The payoff of this game has complexity $(\Sigma^{0}_{1})_{2k+2}$. As we have $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$, the game above is determined. Since $\mathsf{I}$ cannot win, $\mathsf{II}$ has a winning strategy $\tilde{\tau}$; this $\tilde{\tau}$ computes winning strategies for all $(\Sigma^{0}_{1})_{k}$ games.

Since we have $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$, we also have $(\Sigma^{0}_{1})_{2}\text{-}\mathsf{Det}^{*}$, and so $\mathsf{ACA}_{0}$ is true. Let $\mathcal{M}$ be a strict $\beta$-model including $X$ and a universal winning strategy $\tilde{\tau}$ for $(\Sigma^{0}_{1})_{2^{n+2}}$. The strict $\beta$-model $\mathcal{M}$ satisfies $\mathsf{WKL}_{0}$ and induction. Since $\tilde{\tau}\in\mathcal{M}$, every $(\Sigma^{0}_{1})_{2^{n+2}}$ game on Cantor space with only $X$ as a parameter is determined in $\mathcal{M}$.

We consider the following two player game inside $\mathcal{M}$. $\mathsf{I}$ starts the game by playing ${\langle m,i\rangle}$, with $i\leq n$, to ask $\mathsf{II}$ whether $m\in X_{i}$. $\mathsf{II}$ then plays $1$ to answer ‘yes’, or $0$ to answer ‘no’. If $\mathsf{II}$ answers $1$, they must show that $m\in X_{i}$; if $\mathsf{II}$ answers $0$, $\mathsf{I}$ must show that $m\in X_{i}$. Denote by $\mathsf{V}$ (verifier) the player who is trying to show $m\in X_{i}$ and by $\mathsf{R}$ (refuter) the other player.

Suppose $i>0$. $\mathsf{V}$ wants to show $m\in X_{i}$. So they play a finite sequence $X^{f}_{i-1}$ witnessing so. $X^{f}_{i-1}$ is intended to be an initial segment of $X_{i-1}$. Then, $\mathsf{R}$ plays $m^{\prime}\leq\mathrm{lh}(X^{f}_{i-1})$, to state that $X_{i-1}(m^{\prime})\neq X^{f}_{i-1}(m^{\prime})$. If $X^{f}_{i-1}(m^{\prime})=0$, $\mathsf{R}$ is stating that $m\in X_{i-1}$, so $\mathsf{V}$ and $\mathsf{R}$ exchange roles. Otherwise, $\mathsf{R}$ is asking $\mathsf{V}$ to show that $m\in X_{i-1}$, and the roles stay the same. Either way, $\mathsf{V}$ and $\mathsf{R}$ proceed to argue whether $m^{\prime}\in X_{i-1}$.

Now suppose $\mathsf{V}$ and $\mathsf{R}$ are arguing whether $m^{\prime}\in X_{0}$. $\mathsf{V}$ wins (automatically) iff $m^{\prime}\in X_{0}$.

Before we consider the descriptive complexity of the payoffs of these games, consider the following example:

Note that in this game $\mathsf{I}$ and $\mathsf{II}$ play both roles $\mathsf{V}$ and $\mathsf{R}$.

Since we want a game with payoff in Cantor space, the players cannot directly play natural numbers. Code a play of a natural number $m$ by a sequence of plays consisting of $m$ many zeroes and ending with a one. We identify finite sequences of natural numbers with their codes. As the players must alternate playing, when it is a player’s turn to play a natural number (i.e, a sequence of zeroes ending with a one), the other player is on stand-by, and must plays only zeroes. In particular, the example play above becomes:

We can describe the restrictions on each move using a $\Sigma^{0}_{1}$ set or a $\Pi^{0}_{1}$ set, depending on which player must follow the rule. Also, we can check if the witnesses given by $\mathsf{V}$ are right with a $\Pi^{0}_{1}$ condition. Therefore we can write the game above as a finite difference of $2^{n+2}$ open sets on Cantor space, and it is determined. (The complexity bound of the game need not be strict, as we assume $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$.)

We claim that $\mathsf{I}$ cannot have a winning strategy inside $\mathcal{M}$. Suppose $\sigma\in\mathcal{M}$ is a winning strategy for $\mathsf{I}$. Now, after $\mathsf{I}$ plays $\sigma({\langle\rangle})={\langle m,i\rangle}$, $\mathsf{II}$ must try to show that $m\in X_{i}$ or ask $\mathsf{I}$ to do so; for either choice the subsequent game is symmetric, only changing who is going to play $\mathsf{V}$ and $\mathsf{R}$. Therefore if $\mathsf{I}$ wins as $\mathsf{V}$, then $\mathsf{II}$ can also win as $\mathsf{V}$, using essentially the same strategy. Therefore $\mathsf{II}$ can use a (slightly modified variant of) $\sigma$ to defeat $\sigma$. And so $\sigma$ cannot be winning.

Let $\tau$ be a winning strategy for $\mathsf{II}$ inside $\mathcal{M}$ and define $Z=\{{\langle m,i\rangle}\mid\tau({\langle m,i\rangle})=1\}$. We can show that $(Z)_{0}=X$ and $(Z)_{i+1}=\mathrm{TJ}((Z)_{i})$ for $i<n$ by induction inside $\mathcal{M}$. As $\mathcal{M}$ is a strict $\beta$-model and $(Z)_{i+1}=\mathrm{TJ}((Z)_{i})$ is a $\Pi^{0}_{1}$ statement, we also have that $(Z)_{0}=X$ and $(Z)_{i+1}=\mathrm{TJ}((Z)_{i})$ hold outside of $\mathcal{M}$. We conclude that $\mathsf{ACA}_{0}^{\prime}$ holds. ∎

We proved that $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$ implies $\mathsf{ACA}_{0}^{\prime}$ in Proposition 3. We show that the converse holds by a generalization of Theorem 3.7 of [nemoto2007infinite]. As $\mathsf{ACA}_{0}^{\prime}$ is a $\Pi^{1}_{2}$-sentence, we will have the proposition.

Fix a difference $\varphi(f)$ of $2k$ many $\Sigma^{0}_{1}$ formulas with set parameter $X$. $\varphi(F)$ can be thought as a formula

where the $R_{l}$ are $\Pi^{0}_{0}$-formulas and the $\psi_{l}$ are $\Pi^{0}_{1}$-formulas, for all $l\leq k$. Define the sets:

• •

  $W_{0}:=\{u\in 2^{<\mathbb{N}}\mid\exists v\subseteq u.R_{0}(v)\text{ and $\mathsf{I}$ wins $\psi_{0}(f)$ starting at $u$}\}$; and

• •

  $W_{l+1}:=\{u\in W_{l}\mid\exists v\subseteq u.R_{l+1}(v)\text{ and $\mathsf{I}$ wins $\psi_{l+1}(f)$ starting at $u$ and playing inside $W_{l}$}\}$.

Define the game $\psi^{*}(f)\leftrightarrow\exists n.W_{k-1}(f[n])$. By Theorem 3.6 of [nemoto2007infinite], $W_{0}$ is $\Pi^{0}_{1}$ and each $W_{l+1}$ is $\Pi^{0}_{1}$ in $W_{l}$ as a parameter. By bounded induction on $n$, we can compute $W_{k-1}$ from the $k$th jump of $X$. Analogously to Claim 3.7.1, from a strategy for $\mathsf{I}$ in $\psi^{*}$ we can compute a strategy for $\mathsf{I}$ in the game with payoff $\varphi(f)$, and the same holds with $\mathsf{II}$ in place of $\mathsf{I}$. As $\psi^{*}$ is a $\Sigma^{0}_{1}$ game on Cantor space, it is determined. Therefore the game with payoff $\varphi$ is also determined. As this argument holds for any $k\in\mathbb{N}$, $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$ is true. ∎

Every game on Cantor space can be seen as a game on Baire space by adding a $\Pi^{0}_{1}$ condition: $\mathsf{I}$ and $\mathsf{II}$ play only zeroes and ones. Therefore a game in Cantor space which payoff is in $(\Sigma^{0}_{2})_{n}$ is still a $(\Sigma^{0}_{2})_{n}$ game in Baire space. So $\forall n.(\Sigma^{0}_{2})_{n}$-$\mathsf{Det}$ implies $\forall n.(\Sigma^{0}_{2})_{n}$-$\mathsf{Det}^{*}$.

By Lemma 4.2 of [nemoto2007infinite], if a game on Baire space has payoff $A\in(\Sigma^{0}_{2})_{n}$, then there is a game on Cantor space with payoff $A^{*}\in(\Sigma^{0}_{2})_{n+2}$ such that $\mathsf{I}$($\mathsf{II}$) has a winning strategy in $A$ iff $\mathsf{I}$($\mathsf{II}$) has a winning strategy in $A^{*}$. Therefore $\forall n.(\Sigma^{0}_{2})_{n}$-$\mathsf{Det}^{*}$ implies $\forall n.(\Sigma^{0}_{2})_{n}$-$\mathsf{Det}$. ∎

We first prove that $\Pi^{1}_{1}\text{-}\mathsf{CA}_{0}^{\prime}$ is equivalent to “for all $X\subseteq\mathbb{N}$ and $n\in\mathbb{N}$, the $n^{\mathrm{th}}$ iterated hyperjump $\mathrm{HJ}^{n}(X)$ of $X$ exists”. The proof of this equivalence is essentially the proof of Theorem VII.2.9 of [simpson2009sosoa]. Fix a sequence of coded $\beta$-models $X_{0}\in X_{1}\in\cdots\in X_{n}$ with $X\in X_{0}$. We can define $\mathrm{HJ}(X)$ arithmetically using $X_{0}$ as a parameter, so $\mathrm{HJ}(X)$ exists. Since $X_{0}\in X_{1}\models\mathsf{ACA}_{0}$. Again, we can define $\mathrm{HJ}^{2}(X)$ arithmetically using $X_{0}$ as a parameter. Repeating this process boundedly many times, we can define $\mathrm{HJ}^{n+1}(X)$. On the other hand, suppose the hyperjumps $\mathrm{HJ}(X),\dots,\mathrm{HJ}^{n}(X)$ exist. From $\mathrm{HJ}(X)$ we can define a $\beta$-model $X_{0}\ni X$. By bounded induction, given $X_{i}$ and $\mathrm{HJ}^{i+1}(X)$, we can define $X_{i+1}$ with $X_{i}\in X_{i+1}$ and $\mathrm{HJ}^{i}(X)\in X_{i+1}$. Therefore there is a sequence $X_{0}\in\cdots\in X_{n}$ with $X\in X_{0}$.

Suppose $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}$ holds and fix $n\in\mathbb{N}$ and $X\subseteq\mathbb{N}$. We prove the existence of the sequence ${\langle\mathrm{HJ}(X),\dots,\mathrm{HJ}^{n}(X)\rangle}$.

Similar to Proposition 3, we claim that there is a set $\tilde{\tau}$ computing winning strategies for all $(\Sigma^{0}_{1})_{k}$ games on Baire space with only $X$ as a parameter, for all $k\in\mathbb{N}$. Consider the following game: $\mathsf{I}$ chooses an index $e$ for the payoff of a $(\Sigma^{0}_{1})_{k}$ game; $\mathsf{II}$ answers with their choice of role in the game with index $e$; then $\mathsf{I}$ and $\mathsf{II}$ play the game with index $e$; whoever wins the subgame wins the whole game. The payoff of this game has complexity $(\Sigma^{0}_{1})_{2k}$. As we have $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}^{*}$, the game above is determined. Since $\mathsf{I}$ cannot win, $\mathsf{II}$ has a winning strategy $\tilde{\tau}$; this $\tilde{\tau}$ computes winning strategies for all $(\Sigma^{0}_{1})_{k}$ games.

Since we have $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}$, we also have $(\Sigma^{0}_{1})_{2}\text{-}\mathsf{Det}$, and so $\Pi^{1}_{1}\text{-}\mathsf{CA}_{0}$ holds. Let $\mathcal{M}$ be a $\beta$-model including $X$ and a universal winning strategy $\tilde{\tau}$ for $(\Sigma^{0}_{1})_{2^{n+2}}$ games with $X$ as the only parameter. The $\beta$-model $\mathcal{M}$ satisfies $\mathsf{ATR}_{0}$ and induction.

We consider games similar to the ones in the proof of Proposition 3. Player $\mathsf{I}$ starts by playing ${\langle m,i\rangle}$ with $i\leq n$, asking whether $m\in\mathrm{HJ}^{i}(X)$. Then $\mathsf{II}$ plays 1 to answer ‘yes’ and 0 to answer ‘no’. If $\mathrm{II}$ play 1, then they play the role of $\mathsf{V}$ (Verifier), otherwise they play the role of $\mathsf{R}$ (Refuter).

If $i>0$, $\mathsf{V}$ must now play the characteristic function $\chi_{\mathrm{HJ}^{i-1}(X)}(m^{\prime})$ of $\mathrm{HJ}^{i-1}(X)$ and a function $f$ witnessing that $m\in\mathrm{HJ}^{i}(X)$. While $\mathsf{V}$ is playing, $\mathsf{R}$ may contest $\mathsf{V}$’s choice of some $\chi_{\mathrm{HJ}^{i-1}(X)}(m^{\prime})$. If $\mathsf{V}$ stated that $m^{\prime}\not\in\mathrm{HJ}^{i-1}(X)$, then the players exchange roles; otherwise the roles stay the same. The players then proceed to discuss whether $m^{\prime}\in\mathrm{HJ}^{i-1}(X)$. In case $\mathsf{R}$ never contests, $\mathsf{V}$ wins iff $\pi^{0}_{1}(m,f,\mathrm{HJ}^{i-1}(X))$ holds. If $i=0$, $\mathsf{V}$ wins iff $m\in X$. This game can be described by a boolean combination of $2^{n+2}$-many $\Sigma^{0}_{1}$-formulas, and so it is determined. (The complexity bound of the game need not be strict, as we assume $\forall n.(\Sigma^{0}_{1})_{n}\text{-}\mathsf{Det}$.)

We claim that $\mathsf{I}$ cannot have a winning strategy inside $\mathcal{M}$. As in Proposition 3, $\mathsf{I}$ cannot have a winning strategy. Let $\tau$ be a winning strategy for $\mathsf{II}$. Define $Z=\{{\langle m,i\rangle}\mid\tau({\langle m,i\rangle})=1\}$. We can show that $(Z)_{0}=X$ and $(Z)_{i+1}=\mathrm{HJ}(\mathrm{HJ}^{i}(X))$ for $i<n$ by induction inside $\mathcal{M}$. As $\mathcal{M}$ is a $\beta$-model, the same holds outside of $\mathcal{M}$. We conclude that $\Pi^{1}_{1}\text{-}\mathsf{CA}_{0}^{\prime}$ holds. ∎

Fix $k\in\mathbb{N}$ and $X\subseteq\mathbb{N}$. Suppose $\forall n.(\Sigma^{0}_{2})_{n}\text{-}\mathsf{Det}$ is true. Let ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$ be a sequence of (indices of) $\Sigma^{1}_{1}$-inductive operators. We show that the set $V_{n}$ inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$ exists.

As in Propositions 3 and 6, we claim that there is a set $\tilde{\tau}$ computing universal winning strategies for all $(\Sigma^{0}_{2})_{k}$ games with only $X$ as a parameter, for all $k\in\mathbb{N}$. Consider the following game: $\mathsf{I}$ chooses an index $e$ for the payoff of a $(\Sigma^{0}_{2})_{k}$ game; $\mathsf{II}$ answers with their choice of role in the game with index $e$; then $\mathsf{I}$ and $\mathsf{II}$ play the game with index $e$; whoever wins the subgame wins the whole game. The payoff of this game has complexity $(\Sigma^{0}_{2})_{2k}$. As we have $\forall n.(\Sigma^{0}_{2})_{n}\text{-}\mathsf{Det}$, the game above is determined. Since $\mathsf{I}$ cannot win, $\mathsf{II}$ has a winning strategy $\tilde{\tau}$; this $\tilde{\tau}$ computes winning strategies for all $(\Sigma^{0}_{2})_{k}$ games.

Since we have $\forall n.(\Sigma^{0}_{2})_{n}\text{-}\mathsf{Det}$, we also have $(\Sigma^{0}_{1})_{2}\text{-}\mathsf{Det}$, and so $\Pi^{1}_{1}\text{-}\mathsf{CA}_{0}$ is true. Let $\mathcal{M}$ be a $\beta$-model including $X$ and a universal winning strategy $\tilde{\tau}$ for $(\Sigma^{0}_{2})_{{n}^{3}}$ games. The $\beta$-model $\mathcal{M}$ satisfies $\mathsf{ATR}_{0}$ and induction.

We use an unfolded version of a proof by MedSalem and Tanaka [medsalem2008weak]*Theorem 3.3 to show that the set $V_{n}$ inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$ exists inside $\mathcal{M}$. They prove that, for all $n\in\omega$, $[\Sigma^{1}_{1}]^{n}\text{-}\mathsf{ID}$ follows from $(\Sigma^{0}_{2})_{n}\text{-}\mathsf{Det}$ using $\mathsf{ATR}_{0}$ and induction on $n$. We sketch how to unfold their proof to show that $[\Sigma^{1,X}_{1}]^{n}\text{-}\mathsf{ID}$ follows from $(\Sigma^{0,X}_{2})_{{n}^{3}}\text{-}\mathsf{Det}$. Here, $\Sigma^{i,X}_{j}$ denotes the set of $\Sigma^{i}_{j}$ formulas whose only set parameter is $X$. Let $V_{i}$ be the set inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{i-1}\rangle}$, for $i=1,\dots n$. To show the existence of the set $V_{n}$ , we use the set $V_{{n}-1}$ and a $(\Sigma^{0}_{2})_{n}$ game. Unfolding the definitions of $V_{{n}-1}$, we can show the existence of $V_{n}$ using $V_{{n}-2}$ and a $(\Sigma^{0}_{2})_{{n}-1}\land(\Sigma^{0}_{2})_{n}$ game. Repeatedly unfolding the $V_{i}$, we an prove the existence of $V_{n}$ using a $\Sigma^{0}_{2}\land(\Sigma^{0}_{2})_{2}\land\cdots\land(\Sigma^{0}_{2})_{n}$ game. Furthermore, we can show that the payoff of this game is $(\Sigma^{0}_{2})_{{n}^{3}}$. (The complexity bound of the game need not be strict, as we assume $\forall n.(\Sigma^{0}_{2})_{n}\text{-}\mathsf{Det}$.)

Furthermore, the statement “$V_{n}$ is the set inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$” is a boolean combination of $\Pi^{1}_{1}$-sentences with $X,V_{n}$ as the only parameters. As $\mathcal{M}$ is a $\beta$-models, if $V_{n}$ is the set inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$ inside $\mathcal{M}$, then $V_{n}$ is also the set inductively defined by ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$ outside $\mathcal{M}$, as we wanted to show. Since the argument above holds for any $k\in\mathbb{N}$, $X\subseteq\mathbb{N}$ and ${\langle\Gamma_{0},\dots,\Gamma_{n-1}\rangle}$, we have that $\forall n.[\Sigma^{1}_{1}]^{n}\text{-}\mathsf{ID}$ holds. ∎