Proof lengths for instances of the Paris-Harrington principle (Q526964)

It is well known that Peano arthmetic cannot prove the Paris-Harrington principle \(\forall k\), \(m\), \(n\exists N\mathrm{PH}(k,m,n,N)\), where \(\mathrm{PH}(k,m,n,N)\) means that any \(k\)-colouring of \([N]^m\) has a large homogeneous set of size at least \(m\). However, the instances \(\exists N\,\mathrm{PH}(\overline k,\overline m,\overline n,N)\) of the principle are provable already in Robinson's arithmetic \(Q\), being true \(\Sigma_1\) sentences. The principal problem investigated in this paper is how long the proofs of these instances need to be in PA and its fragments, in terms of the parameters \(k\), \(m\), \(n\). Notice that on the one hand, the instances have proofs of length \(O(\log(k+m+n))\) in theories that prove the full Paris-Harrington principle; on the other hand, there is no obvious way how to prove them in \(Q\) other than by exhibiting the witness \(N\), which is astronomically large (its growth is related to the \(F_{\varepsilon_0}\) function in the fast-growing hierarchy). In fact, as stated by the author, the intent is rather to study what fragments of PA have natural proofs of the instances \(\exists N\,\mathrm{PH}(\overline k,\overline m,\overline n,N)\). While this is a vague informal question, one can argue that for lower bounds astronomically large proofs are not natural. (For upper bounds, we may hope just to recognize a natural proof when we see it.) As shown in [\textit{P. Hájek} and \textit{P. Pudlák}, Metamathematics of first-order arithmetic. Berlin: Springer-Verlag (1993; Zbl 0781.03047)], even the partly universally quantified instances \(\forall m\,\exists N\,\mathrm{PH}(\overline k,m,\overline n,N)\) have (fairly natural) primitive recursive \(I\Sigma_{n-1}\)-proofs. The present paper complements this by showing that \(I\Sigma_{n-2}\)-proofs of \(\exists N\,\mathrm{PH}(\overline{e(n)},\overline{n+1},\overline n,N)\), where \(e(n)=10^{35(n-2)^2}\), are absurdly large (of size at least \(F_{\varepsilon_0}(n-3)\) for \(n\gg 0\)), and similarly for \(I\Sigma_{n-3}\)-proofs of \(\exists N\,\mathrm{PH}(\overline8,\overline{n+1},\overline n,N)\) where the number of colours is constant. The basic tool used in the paper is the observation that if a theory \(T\) proves the uniform \(\Sigma_1\)-reflection principle for a proof predicate \(P\), then \(P\)-proofs of instances of a \(\Sigma_1\) formula cannot be much shorter than witnesses of the formula, up to speed-up given by a \(T\)-provably total recursive function. Notice that this applies to a proof predicate of a fixed theory, whereas in the main result of the paper, the theory (\(I\Sigma_{n-2}\)) varies with \(n\). In order to achieve this dependency, the author takes for \(P\) a slow provability predicate for PA, as in [\textit{S.-D.Friedman} et al., Ann. Pure Appl. Logic 164, No. 3, 382--393 (2013; Zbl 1263.03055)]. The technical part of the paper is an analysis of provably total recursive functions of the theory PA + the \(\Sigma_1\)-reflection principle for slow provability in PA.