Proof lengths for instances of the Paris-Harrington principle

Recursive functions and relations, subrecursive hierarchies (03D20) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)

Abstract: 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

o p e r a t o r n a m e P H (k, m, n, N)

: For any

k

-colouring of its

n

-element subsets the set

0, d o t s, N - 1

has a large homogeneous subset of size

g e q m

. At the same time very weak theories can establish the

S i g m a_{1}

-statement

e x i s t s_{N} o p e r a t o r n a m e P H (o v e r l i n e k, o v e r l i n e m, o v e r l i n e 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

f o r a l l_{m} e x i s t s_{N} o p e r a t o r n a m e P H (o v e r l i n e k, m, o v e r l i n e n, N)

has a natural and short proof (relative to

n

and

k

) by

S i g m a_{n - 1}

-induction. In contrast, we show that there is an elementary function

e

such that any proof of

e x i s t s_{N} o p e r a t o r n a m e P H (o v e r l i n e e (n), o v e r l i n e n + 1, o v e r l i n e n, N)

by

S i g m a_{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

S i g m a_{1}

-reflection is related to a function that has a considerably lower growth rate than

F_{v a r e p s i l o n_{0}}

but dominates all functions

F_{a} l p h a

with

a l p h a < v a r e p s i l o n_{0}

in the fast-growing hierarchy.

Review text

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.

Recommendations

Cites work

Cited in

(10)

This page was built for publication: Proof lengths for instances of the Paris-Harrington principle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q526964)