The talk is about applications of methods from discrete mathematics to proof theory. Let A(f) be the statement: For all K there is an N such that for all sequences a1 > ... > an of ordinals less than 0 the following holds: If for 1 < i < n the lengths of ai is bounded by f(K, i) then n < N. We show that for any natural number h first order Peano arithmetic does not prove A(f) for f(K, i) = K + |i| . |i|h, where |i| denotes the binary length of i and |i|h denotes the h-times iterated binary length.
Moreover we show that first order Peano arithmetic proves A(f) for f(K, i) = (K + 1) . |i|. The proof is based on an asymptotic analysis of a Polya style enumeration. Using Otter’s tree enumeration result we also obtain a refinement of Friedman’s miniaturization of Kruskal’s theorem. This result yields an application of Otter’s tree constant 2.955762856... to proof theory.