FOM: Applications of real mathematics to proof theory

[Andreas Weiermann]

Dear members of FOM,

I would like to take the opportunity to
announce some results which follow
from an application of real mathematics to 
proof theory. Perhaps there is some interest in
these since usual classical proof theory does rarely
use methods of standard mathematics.

The results are refined versions of
Harvey Friedman's results on slowly well 
(quasi) ordered sequences. 
Let A(f) be the statement:
For all K there is an N such that for every
sequence a_0>...>a_n of ordinals below epsilon_0
which satisfies |a_i|<= f(K,i) for all i<=n
we have that n<N.
Here |a| denotes the lengths of a
which by def. is the number of occurences of omega in the
normal form of a.
According to Friedman we have
PA does not prove A(f) for f(K,i)=K+i.
One can show that PA does not prove A(f) for 
F(K,i)=K+|i|.|i|_h
for any natural number h>0.
Here |i|_h denotes the h-times iterated binary length of i
and |i|=|i|_1.
For Friedman's result on Kruskal's theorem
and its refinement by Matousek and Loebl
one obtains the following.
Let B(f) be the statement:
For all K there is an N such that for every
bad sequence t_0...t_n of finite trees
which satisfies |t_i|<= f(K,i) for all i<=n
we have that n<N.
According to Friedman we have that
PA (and even ATR_0...) does not prove B(f) for f(K,i)=K+i.
One can
show that PA does not prove B(f) for F(K,i)=K+|i|.r
for any rational number r>1/log_2(alpha) where
alpha=2.95576... is Otter's tree constant.
Similar results hold for the fragments
of PA, Higman's Lemma
and Kruskal's theorem for binary trees.
My proofs utilize an asymptotic
analysis of Polya style enumerations. 
Perhaps different proofs are possible
using purely logical methods.
 
With best regards,
Andreas Weiermann.