van der Waerden's theorem in Reverse Mathematics

Question

What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem?

van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is this proof ever not pointless — i.e. is there an axiom system where such a technique would shorten a proof or proof schema?

If there were finitely many primes, then we could associate to each natural number $n$ the tuple of $v_p(n) {\rm mod} 2$ for each prime p, where $v_p(n)$ is the largest $i$ such that $p^i$ is a factor of $n$.

By van der Waerden's theorem, there arbitrarily long arithmetic progression on which the sequence is constant.

If $a, a+d, a+2d, a+3d$ is an arithmetic progression of length $4$, and $R = \prod_p {p_i}^{e_i}$ where $e_i$ is $v_p(a) {\rm mod} 2$, then we can divide by $R$ to get a sequence of squares. But there is no four term arithmetical progression of perfect squares. QEA

If we also colour each natural number by the list of primes dividing it, we could get a contradiction more easily by looking at an arithmetic progression of length larger than the square of the largest prime; if the progression is $a, a+d, a+2d, \dots$ then:

If for some prime $p$ $v_p(a) < v_p(d)$ then $v_p(a+pd) = v_p(a + d) + 1$ QEA

If for some prime $p$ $v_p(a) = v_p(d)$ then $v(a+kd) = v_p(a) + 1$ if $k$ is chosen so that $k \leq p^2$ and $A + kD \equiv p \pmod {p^2}$, where $a = p^i A$, $d = p^j D$ with $A$ and $D$ prime to $p$. QEA

But if $v_p(a) < v_p(d)$ for every prime $p$ then $v_p(a) = v_p(a+d)$ for all $p$ QEA.

To see that there is no arithmetic progression of four squares: suppose without loss of generality that all four squares are odd and pairwise relatively prime, and call the elements: $x - 6n,$ $x - 2n,$ $ x + 2n,$ $ x + 6n$. Then: $y^2 = (x^2 - 4n^2)(x^2 - 36n^2) = (x^2 - 20n^2)^2 - 256 n^4$

Then we have a Pythagorean triple : $(16n^2, y, x^2 - 20n^2)$. So there exist $u$, $v$ such that $2u$ and $v$ are relatively prime and $4uv = 16n^2$, $4u^2 + v^2 = x^2 - 20n^2$. So $u$ is even, and we can write $u = 4A^2$, $v = 4D^2$ with $D$ odd.

So $4A^2 + D^2$ and $16 A^2 + D^2$ are squares.

So we can write $2A = 2UV$, $U^2 - V^2 = \pm D$ and $4U'V' = 4A$ $4U'^2 V'^2 = \pm D$.

This implies $UV = U'V' = A$, so $\pm D$ is a difference of two squares in two different ways, so we can write $\pm D = 4a^2b^2 - c^2d^2 = 16a^2 c^2 -b^2 d^2$ with $2a,b,c,d$ pairwise relatively prime. enabling us to create an arithmetic progression of relatively prime squares with smaller difference $4ad$.

Answer 1

There is a powerful combinatorial theorem, known as the Hales–Jewett theorem, which readily implies van der Waerden's theorem. On the other hand, the paper below by Matet exhibits primitive recursive upper bounds for the Hales–Jewett function $HJ(m,n)$, and therefore for the van der Waerden function $W(m,n)$. This was originally shown in a paper of Shelah: Primitive recursive bounds for van der Waerden numbers, J. Amer. Math. Soc. 1 no. 3 (1988), 683–697, doi:10.1090/S0894-0347-1988-0929498-X.

The last paragraph of Matet's paper makes it clear that the Hales–Jewett theorem (in the form $\forall m \forall n\, HJ(m,n) \text{ exists}$), and (therefore also van der Waerden's theorem in the form $\forall m \forall n\, W(m,n) \text{ exists}$) is provable in the fragment of Peano arithmetic known as superexponential function arithmetic (often denoted $\textrm{I}\Delta_0 + \text{Supexp}$).

For $HJ(m,n)$ to exist for concrete $m$ and $n$, one only needs the weaker system known as exponential (or elementary) function arithmetic (often denoted $\textrm{I}\Delta_0 + \text{Exp}$).

• Pierre Matet, Shelah's proof of the Hales–Jewett theorem revisited, European J. Combin. 28 (2007), no. 6, 1742–1745, doi:10.1016/j.ejc.2006.06.021.