[FOM] real number for predicative analysis
Andreas Weiermann
weiermann at math.uu.nl
Thu May 18 15:49:44 EDT 2006
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
More information about the FOM
mailing list