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

From MaRDI portal
Revision as of 19:17, 13 July 2024 by ReferenceBot (talk | contribs) (‎Changed an Item)
scientific article
Language Label Description Also known as
English
Proof lengths for instances of the Paris-Harrington principle
scientific article

    Statements

    Proof lengths for instances of the Paris-Harrington principle (English)
    0 references
    0 references
    15 May 2017
    0 references
    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.
    0 references
    Peano arithmetic
    0 references
    proof length
    0 references
    Paris-Harrington principle
    0 references
    finite Ramsey theorem
    0 references
    slow consistency
    0 references
    fast growing hierarchy
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references