*Wissenschaftliches Programm*   *Liste der Vortragenden*

Sektion 16
Donnerstag, 21.09.2000, 17.00–17.20 Uhr, WIL C 307

An independence result for first order Peano arithmetic via Polya style enumeration

Andreas Weiermann, Universität Münster, Institut für Mathematische Logik

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 e0 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.