巴黎-哈林顿原理实例的证明长度

正如Paris和Harrington著名地证明，皮亚诺算术不能证明对所有数 $k,m,n$ 存在满足陈述 $\operatorname{PH}(k,m,n,N)$ 的 $N$：对其 $n$ 元子集的任意 $k$ 着色，集合 \{0,\dots,N-1\} 有一个大小 $\geq m$ 的大齐次子集。同时，极弱的理论能确立对任意固定参数 $k,m,n$ 的 $\Sigma_1$-陈述 $\exists_N\operatorname{PH}(\overline k,\overline m,\overline n,N)$。那么，形式化这些实例的自然证明需要何种理论？已知 $\forall_m\exists_N\operatorname{PH}(\overline k,m,\overline n,N)$ 通过 $\Sigma_{n-1}$-归纳有一个自然且简短的证明（相对于 $n$ 和 $k$）。相反，我们展示存在一个初等函数 $e$ 使得任何通过 $\Sigma_{n-2}$-归纳对 $\exists_N\operatorname{PH}(\overline{e(n)},\overline{n+1},\overline n,N)$ 的证明都长得离谱。为确立这一关于证明长度的结果，我们给出对慢可证性（slow provability）的计算分析，这是由Sy-David Friedman, Rathjen和Weiermann引入的概念。我们将看到慢一致 $\Sigma_1$-反射关联于一个增长速率远低于 $F_{\varepsilon_0}$ 但在快增长层级中主导所有 $\alpha<\varepsilon_0$ 的函数 $F_\alpha$ 的函数。