An application of graphical enumeration to PA *
Andreas Weiermann · Journal of Symbolic Logic · 2003
For $\\al$ less than $ \\eo$ let $N\\al$ be the number of occurrences of $\\om$ in the Cantor normal form of $\\al$. Further let $\\lh n$ denote the binary length of a natural number $n$, let $\\lhh n$ denote the $h$-times iterated binary length of $n$ and let $\\inv n$ be the least $h$ such that $\\lhh n \\leq2$. We show that for any natural number $h$ first order Peano arithmetic, $\\PA$, does not prove the following sentence: For all $ K$ there exists an $ M$ which bounds the lengths $n$ of all strictly descending sequences $\\langle \\al0,... ,\\aln\\rangle$ of ordinals less than $\\eo$ which satisfy the condition that the Norm $N\\ali$ of the $i$-th term $\\ali$ is bounded by $K + \\lh i\\cdot \\lhh{i}$. ¶ As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, $\\PRA$, proves that for all $K$ there is an $M$ which bounds the length $n$ of any strictly descending sequence $\\langle \\al0,... ,\\aln\\rangle $ of ordinals less than $\\eo$ which satisfies the condition that the Norm $N\\ali$ of the $i$-th term $\\ali$ is bounded by $K + \\lh i \\cdot \\inv i$. The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations. ¶ Using results from Otter and from Matou{\\v{s}}ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856... .