Independence results inspired by Friedman style miniaturizations

[Andreas Weiermann]

Dear members of FOM,

Maybe the following is of interest for some of you.

Discussions with Harvey M. Friedman led to the following results.


Consider the set E exponential terms  in one variable x which is 
inductively defined by

a) 0 is in E

b) with a,b in E we have x^a+b in E.


For a term a in E and number k we let a(k) denote the value of a when x 
is put equal to k.

Let 2_0(l):=l and 2_{r+1}(l):=2^{2_r(l)} be the iterated exponential 
function.

All these concepts are natural and can be explained easily to a 
beginning student.


Let S be the statement (in the style of a Friedman miniaturization)

For all K there exists an M so big such that for all a_0,...,a_M in E

which satisfy the condition that a_i(2)\leq 2_K(i) for all i<=M

we will find at least one i<M such that a_i(2_K(M))<=a_{i+1}(2_K(M)).

Then S is true but unprovable in PA.


The statement S does not involve artificial concepts and not even a 
normal form

as it is used for Goodstein's assertion. S also does not speak about 
trees or ordinals.


The statement S is also quite versatile when it comes to extensions.

By adjoining Ackermannian terms to E in an appropriate way one

will obtain an independence result for ATR_0.

By adjoining terms for F_alpha (alpha<epsilon_0) in an appropriate way 
we obtain independence result

for ID_1 and this will extend to more general hierarchies.

I also can also offer Friedman style statements like S for natural well 
partial orders in terms of plus and times

which lead to independence results for PA and ATR_0.


Best, Andreas