[FOM] 271:Clarification of Smith Article

[Andreas Weiermann]

I raised the following issue and recognized that the question
was not very well posed. 

> It might be of some general interest to see whether the lower bound in
> H. Friedman's Theorem 2 (cited below) is larger
> than the Graham number holding the world record for
> a natural number appearing in a mathematical proof.

>> THEOREM 2. Theorem 1 can be proved in strictly finite mathematics. 
>> However,
>> any such proof in ACA_0 + Pi12-BI must use at least 2^[1000] symbols.

I am well aware that 2^[1000] is tiny
when compared to the Graham number.
I meant by my question whether the number of symbols
needed for the proof of Theorem 1 in finite mathematics
is larger than the Graham number.

Anyway the answer to my question has been given
promptly by Harvey Friedman in:

http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html

The values of lower bounds for TREE[3] are really impressing and should have
some general interest. (I intend to use them in my next lecture
on proof theory.)

Thanks

Andreas Weiermann