Strength of the Auslander–Ellis Theorem

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work in second-order arithmetic over $\mathsf{RCA}_0$, the base theory with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The strength of a principle means which subsystems prove it and which subsystems it implies over that base; equivalence requires both implications. Here $\mathsf{ACA}_0$ adds comprehension for all arithmetical formulas. For a set $X$, its Turing jump $X'$ codes which oracle computations with oracle $X$ halt; $X^{(\omega)}=\bigoplus_{n\geq0}X^{(n)}$ joins all finite jumps. The theory $\mathsf{ACA}_0^+$ is $\mathsf{RCA}_0+\forall X\,\exists X^{(\omega)}$. The Auslander--Ellis theorem says that for every compact metric space $(X,d)$, continuous $T:X\to X$ and $x\in X$, there is $y\in X$ which is uniformly recurrent and proximal to $x$. Uniform recurrence means $\forall\varepsilon>0\,\exists m\geq1\,\forall n\geq0\,\exists k<m:\ d(T^{n+k}y,y)<\varepsilon$. Proximality means that, for every $\varepsilon>0$, infinitely many $n$ satisfy $d(T^nx,T^ny)<\varepsilon$.

Statement recorded in the supplied source.

Is the Auslander--Ellis theorem equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$? [S2]

Short English statement

Does the existence of a uniformly recurrent point proximal to each starting point have exactly the strength of arithmetic comprehension?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500118 (AMR-074-0118). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint dated 17 August 2010, Question 18, printed p. 7--8. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.