[FOM] real number for predicative analysis

[Andreas Weiermann]

There might be some interest in a real number
which is characteristic for predicative analysis
when Gamma_0 is taken as its proof-theoretic ordinal.
We consider Friedman's principle of slowly wellorderedness
for Gamma_0 with logarithmic growth rate condition.

Thus  SWO(r) stands for

For all K there is an M so large that for all
sequences of ordinals \alpha_0,...,\alpha_M<\Gamma_0:
If for all i\leq M: N(\alpha_i)\leq K+r\cdot log_2(i)
then we find j<M such that \alpha_j\leq \alpha_{j+1}.

Here N(\delta)=1+N(\alpha)+N(\beta)+N(\gamma)
if \delta is \varphi(\alpha,\beta)+\gamma in normal
form.

Then there is a real number c with decimal expansion 0.4004216002...
such that ATR_0 proves SWO(r) for r\leq c but
ATR_0 does not prove SWO(r) for r>c. (It is not
clear whether c is irrational or transcendental.)

Maple also computes similar real number constants for 
ordinals  \varphi(1,0,...,0) for n-ary and
variadic Veblen functions which are provable in
Weaver's system. 

I would like to
know what the limiting ordinal of Weaver's system is.
Is it below, above or equal to the Bachmann Howard
ordinal? Concerning extended predicative methods
I personally believe that there is a crucial jump in complexity
from the ordinal of ID_1 to the one of ID_2.


Best,
Andreas Weiermann