[FOM] 271:Clarification of Smith Article

[Timothy Y. Chow]

Andreas Weiermann <weiermann at math.uu.nl> wrote:
> 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.
> > 
> > Here 2^[1000] is an exponential stack of 2's of height 1000.

Not even close.  In Knuth's arrow notation, this isn't even enough arrows 
for the 2nd of 64 layers needed to state Graham's number.

It isn't even close to some of the numbers used in Harvey Friedman's other 
work on combinatorial problems involving enormous integers.

Tim