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

Pierre Matet, Shelah's proof of the Hales-Jewett theorem revisited, European J. Combin. 28 (2007), no. 6, 1742–1745.

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.