This continues the previous post on A lower bound for .

Only recently I was made aware of a note dated November 22, 2001, posted on Harvey Friedman‘s page, “Lecture notes on enormous integers”. In section 8, Friedman recalls the definition of the function , the length of the longest possible sequence from with the property that for no , the sequence is a subsequence of .

Friedman says that “A good upper bound for is work in progress”, and states (without proof):

Theorem., where .

Here, are the functions of the Ackermann hierarchy (as defined in the previous post).

He also indicates a much larger *lower bound* for . We need some notation first: Let . Use exponential notation to denote composition, so .

Theorem.Let . Then .

He also states a result relating the rate of growth of the function to what logicians call subsystems of first-order arithmetic. A good reference for this topic is the book Metamathematics of First-order Arithmetic, by Hájek and Pudlák, available through Project Euclid.

There is a recent question on MathOverflow on this general topic.