Strength of Szemerédi's 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 over $\mathsf{RCA}_0$, the subsystem of second-order arithmetic with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction; all structures and orders are countable and coded by sets of integers. $\mathsf{ACA}_0$ adds comprehension for every arithmetical formula (set parameters allowed), and $\mathsf{ATR}_0$ adds arithmetical transfinite recursion along every coded well-order. Reverse-mathematical equivalence means provability of both implications over this base. For $A\subseteq\mathbb N$ let $\overline d(A)=\limsup_{n\to\infty}|A\cap\{1,\ldots,n\}|/n$. Szemerédi's theorem asserts that if $\overline d(A)>0$, then for every $k\ge1$ there are positive integers $a,d$ with $a,a+d,\ldots,a+(k-1)d\in A$.

Statement recorded in the supplied source.

Determine the reverse-mathematical strength of this positive-upper-density form of Szemerédi's theorem over $\mathsf{RCA}_0$. In particular, is it provable in $\mathsf{ACA}_0$? [S2]

Short English statement

What axioms are needed to guarantee arbitrarily long arithmetic progressions in every positive-upper-density set, and does arithmetical comprehension suffice?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500208 (AMR-074-0208). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Stephen G. Simpson, Open Problems in Reverse Mathematics (15 December 1999), Szemerédi's Theorem. https://sgslogic.net/t20/talks/cta/problems/node6.html.