van der Waerden's theorem in Reverse Mathematics

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.

\vskip 1em

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$$.

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 (1988)].
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) \textrm{exists}$$), and (therefore also van der Waerden's theorem in the form $$\forall m \forall n W(m,n) \textrm{exists}$$) is provable in the fragment of Peano arithmetic known as superexponential function arithmetic (often denoted $$\textrm{I}\Delta_0 + \textrm{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 + \textrm{Exp}$$).
• +1. And to the OP, it's worth noting that I$\Delta_0$ + Supexp is much weaker than (the first-order part of) the usual base theory RCA$_0$ for reverse mathematics. (Recall that the provably total functions of RCA$_0$ are precisely the primitive recursive functions.) – Noah Schweber Nov 29 '18 at 17:19
• Following up on Noah Schweber's comment: there is a base theory for reverse mathematics that is much lesser known than $\mathrm{RCA_0}$ , it is usually referred to as $\mathrm{RCA^{*}_0}$; and its first order part is $\mathrm{I\Delta_0 + Exp + B\Sigma_1}$. It appears at the very end of Simpson's book, along with its $\Pi^1_1$-conservative counterpart $\mathrm{WKL^{*}_0}$. – Ali Enayat Nov 29 '18 at 21:27