Binary Choice Games and Arithmetical Comprehension

TL;DR

The paper investigates the logical strength of determinacy for constrained binary choice games and shows that, over $\mathsf{RCA}_0$, arithmetical comprehension ($\mathsf{ACA}_0$) is equivalent to determinacy for wellfounded binary choice game trees and to restricted forms of determinacy at levels of the difference hierarchy ($\Delta^0_1$ and $(\Sigma^0_1)_k$). It develops a precise framework for binary choice trees, regular/restricted strategies, and the payoff structure given by clopen sets in $\mathbb{N}^\mathbb{N}$, then proves both directions of the equivalence: (a) using an embedding into $2^\mathbb{N}$ and existing higher-level determinacy results to derive $(\Sigma^0_1)_k$-Det from $\mathsf{ACA}_0$, and (b) deriving ACA$_0$ from determinacy of wellfounded binary trees via a WKL$_0$-style contradiction argument that constructs a branch in an infinite tree using $\Sigma^0_1$-induction. The results illuminate the precise strength of game-theoretic determinacy in reverse mathematics and connect restricted game determinacy to classical comprehension axioms.

Abstract

We prove that Arithmetical Comprehension is equivalent to the determinacy of all clopen integer games in which each player has at most two moves per turn.

Figures (1)

• Figure 1: Proof that $f[1]$ has a successor in $T$.

Theorems & Definitions (11)

• Theorem 1.1
• Definition 2.1: Binary choice tree
• Definition 2.2
• Remark 2.3
• Definition 2.4
• Remark 2.5
• Definition 2.6
• Remark 2.7
• Definition 2.8
• Theorem 3.1