Another independence result for PA

[Andreas Weiermann]

Dear colleagues,


maybe the following is of interest to some of you.


Discussions with Harvey Friedman led to the following

independence result where this time no set of terms is involved.

With 2_K(l) let us denote a tower of k 2's with an l on top (iterated 
exponential).

For k>=2 let us denote by a[k:=l] the result of replacing in the 
complete base k representation

every occurrence of k by l.


Let G be the following principle:

For all positive integers K there exists a positive integer M which is 
so big that

for any choice of numbers a_0,...a_M satisfying a[2+i:=2]<=2_K(i) for 
all i<=M

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


The principle G is natural in the sense that it does not refer to 
external concepts like ordinals, trees or term complexities.

What is needed is basically the Euclidean algorithm for developing base 
k normal forms, a substitution process for bases and

iterated exponential terms.


The theorem is that G is true but unprovable from the Peano axioms.


If one looks at more general notions of k normal form one can arrive at 
statements like G which are independent of ATR_0 or ID_1 etc.



Harvey Friedman arrived also at some very nice new principles which do 
not rely on external concepts.


All the best,

Andreas