Proof Lengths for Instances of the Paris-Harrington Principle

As Paris and Harrington have famously shown, Peano Arithmetic does not prove that for all numbers $k,m,n$ there is an $N$ which satisfies the statement $\mathrm{PH}(k,m,n,N)$: For any $k$-colouring of its $n$-element subsets the set $\{0,\dots ,N-1\}$ has a large homogeneous subset of size $\ge m$. At the same time very weak theories can establish the ${\mathrm{\Sigma }}_1$-statement ${\mathrm{\exists }}_N\mathrm{PH}(\bar{k},\bar{m},\bar{n},N)$ for any fixed parameters $k,m,n$. Which theory, then, does it take to formalize natural proofs of these instances? It is known that ${\mathrm{\forall }}_m{\mathrm{\exists }}_N\mathrm{PH}(\bar{k},m,\bar{n},N)$ has a natural and short proof (relative to $n$ and $k$) by ${\mathrm{\Sigma }}_{n-1}$-induction. In contrast, we show that there is an elementary function $e$ such that any proof of $\exists_N\operatorname{PH}(\overline{e(n)},\overline{n+1},\overline n,N)$by$\Sigma_{n-2}$-induction is ridiculously long. In order to establish this result on proof lengths we give a computational analysis of slow provability, a notion introduced by Sy-David Friedman, Rathjen and Weiermann. We will see that slow uniform ${\mathrm{\Sigma }}_1$-reflection is related to a function that has a considerably lower growth rate than $F_{{\epsilon }_0}$ but dominates all functions $F_{\alpha }$ with $\alpha <{\epsilon }_0$ in the fast-growing hierarchy.