The Paris-Harrington theorem says that a variant of the finite Ramsey theorem is not provable in Peano arithmetic, but it is provable in stronger systems.
The proof of the strengthened finite Ramsey theorem in ZFC is non-constructive, so given $n, k, m$ (see the wikipedia link) it doesn't tell us how to find $N\in\mathbb{N}$ for which the relevant statement $P(n, k, m, N)$ holds.
I am curious, are there any results that tell us the upperbound on $N$ given $n, k, m$? If not, is there a proof that this can't be done in Peano arithmetic or ZFC? If yes, what is the result and in what system is it proven?
See "Rapidly growing Ramsey functions" by Jussi Ketonen and Robert Solovay [Annals of Mathematics 113 (1981) pp/ 267--314]. If I remember correctly, the necessary size $N$ for the Paris-Harrington theorem is "just barely" beyond the order of growth attainable by provably recursive functions of PA.