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