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.