Proof Lengths for Instances of the Paris-Harrington Principle

TL;DR

This paper investigates the proof lengths of instances of the Paris-Harrington principle within formal theories, revealing that certain proofs require extremely long derivations, and analyzes the computational complexity of slow provability.

Contribution

It demonstrates that proofs of specific Paris-Harrington instances by low-level induction are extraordinarily long, and connects slow provability to a new growth rate in the fast-growing hierarchy.

Findings

Proof lengths for certain Paris-Harrington instances are extremely long.

Slow uniform $ ext{Σ}_1$-reflection relates to a growth rate below $F_{ε_0}$ but surpassing all $F_α$ for $ ext{α}<ε_0$.

The analysis links proof complexity with the growth rates in the fast-growing hierarchy.

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 $\operatorname{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 $\geq m$. At the same time very weak theories can establish the $\Sigma_1$-statement $\exists_N\operatorname{PH}(\overline k,\overline m,\overline 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 $\forall_m\exists_N\operatorname{PH}(\overline k,m,\overline n,N)$ has a natural and short proof (relative to $n$ and $k$) by $\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 $\Sigma_1$-reflection is related to a function that has a considerably lower growth rate than $F_{\varepsilon_0}$ but dominates all functions $F_\alpha$ with $\alpha<\varepsilon_0$ in the fast-growing hierarchy.