[ouid]

My mistake. I, and I suspect the original commenter, was thinking about the strengthened finite Ramsey theorem. From wikipedia: https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...

For any positive integers n, k, m, such that m ≥ n, one can find N with the following property: if we color each of the n-element subsets of S = {1, 2, 3,..., N} with one of k colors, then we can find a subset Y of S with at least m elements, such that all n-element subsets of Y have the same color, and the number of elements of Y is at least the smallest element of Y.

This function is outside the reach of Peano arithmetic.