[FOM] 271:Clarification of Smith Article
weiermann at math.uu.nl
Wed Mar 29 16:20:45 EST 2006
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.
>> any such proof in ACA_0 + Pi12-BI must use at least 2^ symbols.
I am well aware that 2^ 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:
The values of lower bounds for TREE are really impressing and should have
some general interest. (I intend to use them in my next lecture
on proof theory.)
More information about the FOM